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(cbc_ba,[cbc_symbolic_invariant_violation/2,
6		tcltk_cbc_symbolic_invariant_violation/1]).
7
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,symbolic_model_checker).
10		:- module_info(description,'A constraint-based invariant checker using before-after predicates.').
11
12		:- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1,
13		b_get_properties_from_machine/1,
14		b_specialized_invariant_for_op/2]).
15		:- use_module(probsrc(before_after_predicates), [before_after_predicate_for_operation/2]).
16		:- use_module(symbolic_model_checker(predicate_handling), [prime_predicate/2]).
17		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,
18		create_negation/2]).
19		:- use_module(probsrc(preferences), [get_preference/2]).
20
21		:- use_module(probsrc(solver_interface), [solve_predicate/4]).
22		%:- use_module(symbolic_model_checker(solver_handling), [solve/2]).
23
24		cbc_symbolic_invariant_violation(OpName,Result) :-
25		b_get_properties_from_machine(PropertiesOnConstants),
26		b_get_invariant_from_machine(Inv), % TO DO?: split into conjuncts; use proof info
27		prime_predicate(Inv,PrimedInv),
28		create_negation(PrimedInv,NegInv),
29		before_after_predicate_for_operation(OpName,BA),
30		format('~nLooking for invariant violation for operation ~w~n',[OpName]),
31		(get_preference(use_po,false) -> NegInvForOp=NegInv
32		; b_specialized_invariant_for_op(OpName,UncheckedInvariant)
33		-> prime_predicate(UncheckedInvariant,PrimedUncheckedInv),
34		create_negation(PrimedUncheckedInv,NegInvForOp)
35		; NegInvForOp=NegInv, print(no_specialized_invariant_info_for_op(OpName)),nl
36		),
37		conjunct_predicates([PropertiesOnConstants,Inv,BA,NegInvForOp],Constraint),
38		(debug:debug_mode(on) -> translate:nested_print_bexpr(Constraint),nl ; true),
39		%solve(Constraint,Result).
40		solve_predicate(Constraint,_State,1,Result).
41
42		% TO DO:
43		% static_symmetry_reduction_for_global_sets(State)
44		% (get_proven_invariant(OpName,ProvenInvariant) -> true
45
46		% use_module(symbolic_model_checker(cbc_ba)), cbc_symbolic_invariant_violation(Op,R).
47		% use_module(symbolic_model_checker(cbc_ba)), cbc_symbolic_invariant_violation(Op,R), R\=contradiction_found.
48		% use_module(symbolic_model_checker(cbc_ba)), findall((Op,R),cbc_symbolic_invariant_violation(Op,R),L), print(L),nl.
49
50		tk_call_cbc(O,R) :-
51		cbc_symbolic_invariant_violation(O,Res), translate(Res,R).
52
53		translate(contradiction_found,R) :- !, R=ok.
54		translate(contradiction_found(_),R) :- !,R=ok.
55		translate(no_solution_found(_),R) :- !, R=ok_for_set_sizes.
56		translate(solution(_),R) :- !,R=invariant_violation.
57		translate(Res,F) :- functor(Res,F,_).
58
59
60		:- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer/1]).
61		tcltk_cbc_symbolic_invariant_violation(list([list(['Operation','Status'])|Res])) :-
62		start_ms_timer(Timer),
63		findall(list([OpName,Result]),tk_call_cbc(OpName,Result),Res),
64		stop_ms_timer(Timer).