%==============================================================================
% Project:	Microcontroller Programming in Datalog
% Version:	0.4
% Filename:	sld.pl
% Purpose:	SLD Resolution Steps, Computation of Violation Conditions
% Last Change:	29.03.2021
% Language:	Prolog (tested with SWI Prolog)
% Author:	Stefan Brass
% Email:	brass@informatik.uni-halle.de
% WWW:		http://www.informatik.uni-halle.de/~brass/
% Address:	Univ. Halle, Von-Seckendorff-Platz 1, D-06120 Halle, GERMANY
% Copyright:	(c) 2020-2021 by Stefan Brass
%==============================================================================

% For more information, see the main file: ctest.pl


%******************************************************************************
% SLD Resolution Steps, Unfolding, Computation of Violation Conditions:
%******************************************************************************


%==============================================================================
% Renaming of Variables:
%==============================================================================

% This translates v(Name) into v(Name,VerNo).

%------------------------------------------------------------------------------
% fresh_var_term(+TermIn, +VerNo, -TermOut):
%------------------------------------------------------------------------------

fresh_var_term(v(Name), VerNo, v(Name,VerNo)) :-
	!.

fresh_var_term(Const, _VerNo, Const) :-
	is_const(Const).

%------------------------------------------------------------------------------
% fresh_var_term_list(+TermListIn, +VerNo, -TermListOut):
%------------------------------------------------------------------------------

fresh_var_term_list([], _VerNo, []).

fresh_var_term_list([TermIn|RestIn], VerNo, [TermOut|RestOut]) :-
	fresh_var_term(TermIn, VerNo, TermOut),
	fresh_var_term_list(RestIn, VerNo, RestOut).

%------------------------------------------------------------------------------
% fresh_var_lit(+LitIn, +VerNo, -LitOut):
%------------------------------------------------------------------------------

fresh_var_lit(LitIn, VerNo, LitOut) :-
	LitIn =.. [Pred|ArgsIn],
	fresh_var_term_list(ArgsIn, VerNo, ArgsOut),
	LitOut =.. [Pred|ArgsOut].

%------------------------------------------------------------------------------
% fresh_var_lit_list(+LitListIn, +VerNo, -LitListOut):
%------------------------------------------------------------------------------

fresh_var_lit_list([], _VerNo, []).

fresh_var_lit_list([LitIn|RestIn], VerNo, [LitOut|RestOut]) :-
	fresh_var_lit(LitIn, VerNo, LitOut),
	fresh_var_lit_list(RestIn, VerNo, RestOut).

%------------------------------------------------------------------------------
% fresh_var_formula(+FormulaIn, +VerNo, -FormulaOut):
%------------------------------------------------------------------------------

fresh_var_formula(or(FormulaIn1,FormulaIn2), VerNo,
			or(FormulaOut1,FormulaOut2)) :-
	!,
	fresh_var_formula(FormulaIn1, VerNo, FormulaOut1),
	fresh_var_formula(FormulaIn2, VerNo, FormulaOut2).

fresh_var_formula(and(FormulaIn1,FormulaIn2), VerNo,
			and(FormulaOut1,FormulaOut2)) :-
	!,
	fresh_var_formula(FormulaIn1, VerNo, FormulaOut1),
	fresh_var_formula(FormulaIn2, VerNo, FormulaOut2).

fresh_var_formula(not(FormulaIn1), VerNo,
			not(FormulaOut1)) :-
	!,
	fresh_var_formula(FormulaIn1, VerNo, FormulaOut1).

fresh_var_formula(LitIn, VerNo, LitOut) :-
	fresh_var_lit(LitIn, VerNo, LitOut).

%------------------------------------------------------------------------------
% rule_with_fresh_var(+VerNo, -RuleNo, -Head, -Body):
%------------------------------------------------------------------------------

rule_with_fresh_var(VerNo, RuleNo, HeadOut, BodyOut) :-
	input_rule(rule(RuleNo, Head, Body)),
	fresh_var_lit(Head, VerNo, HeadOut),
	fresh_var_lit_list(Body, VerNo, BodyOut).

%------------------------------------------------------------------------------
% constraint_with_fresh_var(+VerNo, -ID, -Lit1, -Lit2, -Formula):
%------------------------------------------------------------------------------

constraint_with_fresh_var(VerNo, ID, LitOut1, LitOut2, FormulaOut) :-
	input_constraint(Constraint),
	constraint_data(Constraint, ID, Lit1, Lit2, Formula),
	fresh_var_lit(Lit1, VerNo, LitOut1),
	fresh_var_lit(Lit2, VerNo, LitOut2),
	fresh_var_formula(Formula, VerNo, FormulaOut).


%==============================================================================
% Generation of Unique Version Numbers:
%==============================================================================


%------------------------------------------------------------------------------
% unique_ver(-Ver):
%------------------------------------------------------------------------------

% Declaration of dynamic predicate:
:- dynamic(unique_ver/1).

%------------------------------------------------------------------------------
% init_unique_ver(+Ver):
%------------------------------------------------------------------------------

% Note: Versions 1 and 2 are fixed for the generation of violation conditions.
% Thus, this predicate should be called with version 3.
% The given version number for the variables is the first number returned.

init_unique_ver(Ver) :-
	delete_all(unique_ver, 1),
	assert(unique_ver(Ver)).

%------------------------------------------------------------------------------
% get_unique_ver(-Ver):
%------------------------------------------------------------------------------

get_unique_ver(Ver) :-
	unique_ver(Ver),
	!,
	retract(unique_ver(Ver)),
	NextVer is Ver + 1,
	assert(unique_ver(NextVer)).

get_unique_ver(error) :-
	nl,
	write('***** Error: unique_ver not initialized'),
	nl,
	fail.


%==============================================================================
% Unification:
%==============================================================================


%------------------------------------------------------------------------------
% unify_step(+Term1, +Term2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_step(v(Var), v(Var), Subst, Subst) :-
	!.

unify_step(v(Var,No), v(Var,No), Subst, Subst) :-
	!.

unify_step(v(Var), Term, SubstIn, SubstOut) :-
	!,
	subst_add(SubstIn, v(Var), Term, SubstOut).

unify_step(v(Var,No), Term, SubstIn, SubstOut) :-
	!,
	subst_add(SubstIn, v(Var,No), Term, SubstOut).

unify_step(Const, v(Var), SubstIn, SubstOut) :-
	is_const(Const),
	!,
	subst_add(SubstIn, v(Var), Const, SubstOut).

unify_step(Const, v(Var,No), SubstIn, SubstOut) :-
	is_const(Const),
	!,
	subst_add(SubstIn, v(Var,No), Const, SubstOut).

unify_step(Const, Const, Subst, Subst) :-
	is_const(Const).

%------------------------------------------------------------------------------
% unify_term(+Term1, +Term2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_term(Term1, Term2, SubstIn, SubstOut) :-
	do_subst_term(Term1, SubstIn, RealTerm1),
	do_subst_term(Term2, SubstIn, RealTerm2),
	unify_step(RealTerm1, RealTerm2, SubstIn, SubstOut).

%------------------------------------------------------------------------------
% unify_termlist(+TermList1, +TermList2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_termlist([], [], Subst, Subst).

unify_termlist([Term1|Rest1], [Term2|Rest2], SubstIn, SubstOut) :-
	unify_term(Term1, Term2, SubstIn, Subst),
	unify_termlist(Rest1, Rest2, Subst, SubstOut).

%------------------------------------------------------------------------------
% unify_lit(+Lit1, +Lit2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_lit(Lit1, Lit2, SubstIn, SubstOut) :-
	Lit1 =.. [Pred|Args1],
	Lit2 =.. [Pred|Args2],
	unify_termlist(Args1, Args2, SubstIn, SubstOut).

%------------------------------------------------------------------------------
% unify_lit(+Lit1, +Lit2, -Subst):
%------------------------------------------------------------------------------

unify_lit(Lit1, Lit2, Subst) :-
	empty_subst(EmptySubst),
	unify_lit(Lit1, Lit2, EmptySubst, Subst).

%------------------------------------------------------------------------------
% unify_pair(+Lits1, +Lits2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

% unused?
unify_pair([A1,A2], [B1,B2], SubstIn, SubstOut) :-
	unify_lit(A1, B1, SubstIn, Subst),
	unify_lit(A2, B2, Subst, SubstOut).

%------------------------------------------------------------------------------
% unify_pair(+Lits1, +Lits2, -Subst):
%------------------------------------------------------------------------------

% unused?
unify_pair(Lits1, Lits2, Subst) :-
	empty_subst(EmptySubst),
	unify_pair(Lits1, Lits2, EmptySubst, Subst).


%==============================================================================
% Computation of Violation Conditions:
%==============================================================================


%------------------------------------------------------------------------------
% violation_cond(-VioCond):
%------------------------------------------------------------------------------

violation_cond(VioCond) :-
	input_constraint(Constraint),
	constraint_data(Constraint, ID, Lit1, Lit2, ConstraintFormula),
	rule_with_fresh_var(1, No1, Head1, BodyList1),
	unify_lit(Head1, Lit1, Subst1),
	rule_with_fresh_var(2, No2, Head2, BodyList2),
	unify_lit(Head2, Lit2, Subst1, Subst),
	do_subst_litlist(BodyList1, Subst, LitList1),
	do_subst_litlist(BodyList2, Subst, LitList2),
	list_append(LitList1, LitList2, LitList),
	do_subst_formula(ConstraintFormula, Subst, Formula),
	eval_obvious(Formula, SimplifiedFormula),
	SimplifiedFormula \= false,
	make_viocond(ID, No1, No2, LitList, SimplifiedFormula, VioCond).


%==============================================================================
% Refutation of Violation Conditions:
%==============================================================================


%------------------------------------------------------------------------------
% refute_violation_cond(+VioCond, -RefuteReason):
%------------------------------------------------------------------------------

refute_violation_cond(VioCond, Refute) :-
	viocond_lits(VioCond, LitList),
	viocond_formula(VioCond, Formula),
	%write('\tStart Refute: '),
	%nl,
	%print_litlist(LitList),
	%nl,
	%
	extract_builtin(LitList, BuiltinList),
	conj_to_and(BuiltinList, BuiltinFormula),
	%
	%write('\tBuiltIn: '),
	%print_formula(BuiltinFormula),
	%nl,
	refute_violation_cond_cases(LitList, Formula, BuiltinFormula, Refute).

%------------------------------------------------------------------------------
% refute_violation_cond_cases(+LitList, +Formula, +BuiltinFormula, -Refute):
%------------------------------------------------------------------------------

refute_violation_cond_cases(LitList, Formula, BuiltinFormula, Refute) :-
	refute_violation_cond0(LitList, Formula, BuiltinFormula, Refute),
	!.

refute_violation_cond_cases(LitList, Formula, BuiltinFormula, Refute) :-
	refute_violation_cond1(LitList, Formula, BuiltinFormula, Refute),
	!.

%------------------------------------------------------------------------------
% refute_violation_cond0(+LitList, +Formula, +BuiltinFormula, -RefuteReason):
%------------------------------------------------------------------------------

% This checks whether the BuiltinFormula (derived from LitList)
% together with Formula (from the violation condition inherited from constraint)
% is already inconsistent.

refute_violation_cond0(_LitList, Formula, BuiltinFormula, Refute) :-
	VFormula0 = and(BuiltinFormula,Formula),
	eval_obvious(VFormula0, VFormula1),
	normalize_and(VFormula1, VFormula),
	is_inconsistent(VFormula),
	make_refute0(VFormula, Refute).

%------------------------------------------------------------------------------
% refute_violation_cond1(+LitList, +Formula, +BuiltinFormula, -RefuteReason):
%------------------------------------------------------------------------------

% This checks whether the violation condition "LitList and Formula"
% can be refuted with a single application of a constraint,
% namely constraint ID, matched with Literals Lit1 and Lit2 from LitList.
% Note that more than one application of a constraint might be needed,
% but this predicate checks only a single application.
% Therefore, the current prototype is incomplete.
% However, if the violation condition can be refuted,
% one can be sure that a constraint violation cannot occur in the situation
% described by the violation condition.

refute_violation_cond1(LitList, Formula, BuiltinFormula, Refute) :-
	init_unique_ver(3),
	unique_ver(Ver), % This will be 3.
	list_member(LitB1, LitList),
	constraint_with_fresh_var(Ver, ID, LitA1, LitA2, ConstraintFormula),
	unify_lit(LitA1, LitB1, Subst1),
	list_member(LitB2, LitList),
	LitB2 \= LitB1,
	unify_lit(LitA2, LitB2, Subst1, Subst),
	%
	dbg_out_rt_match(ID, LitB1, LitB2),
	%
	match_cond(LitB1, Subst, Cond1),
	%write('\tCond1: '),
	%print_formula(Cond1),
	%nl,
	%
	match_cond(LitB2, Subst, Cond2),
	%write('\tCond2: '),
	%print_formula(Cond2),
	%nl,
	%
	do_subst_formula(ConstraintFormula, Subst, Cond3),
	%write('\tCond3: '),
	%print_formula(Cond3),
	%nl,
	normalize_and(and(Cond1, and(Cond2, Cond3)), MatchCond),
	NotMatchCond = not(MatchCond),
	VFormula0 = and(and(BuiltinFormula,Formula),NotMatchCond),
	eval_obvious(VFormula0, VFormula1),
	normalize_and(VFormula1, VFormula),
	is_inconsistent(VFormula),
	make_refute1(LitB1, LitB2, ID, VFormula, Refute).

% It is important that the literals from the violation condition
% are the second literal in the call to the unification,
% because variable-to-variable bindings are done from first to second literal,
% and we do not want new variables in the extended violation condition.

%------------------------------------------------------------------------------
% dbg_out_rt_match(+ID, +Lit1, +Lit2):
%------------------------------------------------------------------------------

% Optional debug output for refutation try.

dbg_out_rt_match(ID, Lit1, Lit2) :-
	opt_drt,
	!,
	write('\tTrying refutation with Constraint: ('),
	write(ID),
	write(')'),
	nl,
	write('\t\tLit1:  '),
	print_lit(Lit1),
	nl,
	write('\t\tLit2:  '),
	print_lit(Lit2),
	nl,
	nl.

dbg_out_rt_match(_ID, _Lit1, _Lit2).

%------------------------------------------------------------------------------
% match_cond(+Lit, +Subst, -Cond):
%------------------------------------------------------------------------------

match_cond(Lit, Subst, Cond) :-
	Lit =..[_Pred|Args],
	match_cond_list(Args, Subst, Cond).

% match_cond_list(+TermList, +Subst, -Cond):

match_cond_list([], _Subst, true).

match_cond_list([Term], Subst, eq(Term,TermOut)) :-
	do_subst_term(Term, Subst, TermOut).

match_cond_list([Term1,Term2|Rest], Subst, and(eq(Term1,TermOut1),RestCond)) :-
	do_subst_term(Term1, Subst, TermOut1),
	match_cond_list([Term2|Rest], Subst, RestCond).

%------------------------------------------------------------------------------
% extract_builtin(+Body, -BuiltinList):
%------------------------------------------------------------------------------

extract_builtin([], []).

extract_builtin([succ(Term1,Term2)|Rest], [succ(Term1,Term2)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([plus_lt(T1,T2,T3)|Rest], [plus_lt(T1,T2,T3)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([plus_ge(T1,T2,T3)|Rest], [plus_ge(T1,T2,T3)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([ret_millis(T1,T2)|Rest], [ret_millis(T1,T2)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([_|Rest], BuiltinList) :-
	extract_builtin(Rest, BuiltinList).

