1		% (c) 2015 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(predicate_abstraction, [get_abstract_domain/1,
6		concrete_state_to_abstract_state/3]).
7
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,symbolic_model_checker).
10		:- module_info(description,'An abstract domain using predicate abstraction.').
11
12		:- use_module(library(lists), [append/2]).
13		:- use_module(library(ordsets), [list_to_ord_set/2]).
14
15		:- use_module(probsrc(bsyntaxtree), [create_implication/3,
16		create_negation/2,
17		get_texpr_type/2,
18		safe_create_texpr/3,
19		conjunct_predicates/2,
20		conjunction_to_list/2]).
21		:- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1,
22		b_get_machine_variables/1]).
23
24		:- use_module(symbolic_model_checker(solver_handling)).
25		:- use_module(symbolic_model_checker(predicate_handling)).
26
27		% the abstract domain consists of:
28		% 1. the conjuncts of the invariant
29		% 2. the conjuncts of the predicate describing the initial state
30		% 3. pairwise inequalities x < y for all variables
31		get_abstract_domain(Set) :-
32		get_conjuncts_of_invariant(Invariant),
33		get_conjuncts_of_initial_state(Init),
34		pairwise_inequalities_of_variables(PW),
35		append([Invariant,Init,PW],L),
36		list_to_ord_set(L, Set).
37
38		get_conjuncts_of_invariant(C) :-
39		b_get_invariant_from_machine(I),
40		conjunction_to_list(I,C).
41
42		get_conjuncts_of_initial_state(C) :-
43		get_initial_state_predicate(I),
44		conjunction_to_list(I,C).
45
46		pairwise_inequalities_of_variables(PW) :-
47		b_get_machine_variables(Vars),
48		pairwise_inequalities_of_variables(Vars,PW).
49
50		pairwise_inequalities_of_variables([],[]).
51		pairwise_inequalities_of_variables([V1|T],PW) :- !,
52		pairwise_inequalities_of_variables(T,V1,PWTemp),
53		pairwise_inequalities_of_variables(T,PWTemp2),
54		append(PWTemp,PWTemp2,PW).
55
56		pairwise_inequalities_of_variables([],_,[]).
57		pairwise_inequalities_of_variables([V1|Vs],V2,[PW|PWs]) :-
58		get_texpr_type(V1,integer),
59		get_texpr_type(V2,integer), !,
60		safe_create_texpr(less(V1,V2),pred,PW),
61		pairwise_inequalities_of_variables(Vs,V2,PWs).
62		pairwise_inequalities_of_variables([V1|Vs],V2,[PW|PWs]) :-
63		get_texpr_type(V1,Type),
64		get_texpr_type(V2,Type), !,
65		safe_create_texpr(not_equal(V1,V2),pred,PW),
66		pairwise_inequalities_of_variables(Vs,V2,PWs).
67		pairwise_inequalities_of_variables([_|Vs],V2,PWs) :-
68		pairwise_inequalities_of_variables(Vs,V2,PWs).
69
70		concrete_state_to_abstract_state(Dom,CState,AbsState) :-
71		concrete_state_to_abstract_state_aux(Dom,CState,AbsStateConjuncts),
72		conjunct_predicates(AbsStateConjuncts,AbsState).
73		concrete_state_to_abstract_state_aux([],_ConcreteState,[]).
74		concrete_state_to_abstract_state_aux([ADomElement|Elements],ConcreteState,[ADomElement|T]) :-
75		create_implication(ConcreteState,ADomElement,Implies),
76		solve_negated(Implies,contradiction_found(_)), !,
77		concrete_state_to_abstract_state_aux(Elements,ConcreteState,T).
78		concrete_state_to_abstract_state_aux([ADomElement|Elements],ConcreteState,[NegDomElement|T]) :-
79		create_negation(ADomElement,NegDomElement),
80		create_implication(ConcreteState,NegDomElement,Implies),
81		solve_negated(Implies,contradiction_found(_)), !,
82		concrete_state_to_abstract_state_aux(Elements,ConcreteState,T).
83		concrete_state_to_abstract_state_aux([_|Elements],ConcreteState,T) :-
84		concrete_state_to_abstract_state_aux(Elements,ConcreteState,T).