%==============================================================================
% Project:	Microcontroller Programming in Datalog
% Version:	0.4
% Filename:	prover.pl
% Purpose:	Prover (Consistency Checker for Built-In Predicates)
% 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


%******************************************************************************
% Prover (Consistency Checker for Built-In Predicates):
%******************************************************************************


%==============================================================================
% Consistency Checker (Incomplete Detection of Inconsistencies):
%==============================================================================


%------------------------------------------------------------------------------
% is_inconsistent(+Formula):
%------------------------------------------------------------------------------

is_inconsistent(Formula) :-
	eval_obvious(Formula, Simplified),
	dbg_out_cc_start(Simplified),
	is_inconsistent1(Simplified),
	!,
	dbg_out_cc_success.

is_inconsistent(_Formula) :-
	dbg_out_cc_failure,
	fail.

%------------------------------------------------------------------------------
% is_inconsistent1(+Formula):
%------------------------------------------------------------------------------

% This is only to handle the trival case "false" (after simplification):

is_inconsistent1(false) :-
	!.

is_inconsistent1(Formula) :-
	eliminate_not(Formula,FormulaWithoutNot),
	%write('Not eliminated: '),
	%print_formula(FormulaWithoutNot),
	%nl,
	dnf(FormulaWithoutNot, DNF),
	%write('DNF: '),
	%print_dnf(DNF),
	%nl,
	is_inconsistent_dnf(DNF).

%------------------------------------------------------------------------------
% is_inconsistent_dnf(+DNF):
%------------------------------------------------------------------------------

is_inconsistent_dnf([]).

is_inconsistent_dnf([Conj|Rest]) :-
	is_inconsistent_conj(Conj),
	is_inconsistent_dnf(Rest).

%------------------------------------------------------------------------------
% dbg_out_cc_start(+Formula):
%------------------------------------------------------------------------------

dbg_out_cc_start(Formula) :-
	opt_dcc,
	!,
	write('\tInconsistency Check: '),
	print_formula(Formula),
	nl.

dbg_out_cc_start(_).

%------------------------------------------------------------------------------
% dbg_out_cc_success:
%------------------------------------------------------------------------------

dbg_out_cc_success :-
	opt_dcc,
	!,
	write('\tINCONSISTENT !'),
	nl,
	nl.

dbg_out_cc_success.

%------------------------------------------------------------------------------
% dbg_out_cc_failure:
%------------------------------------------------------------------------------

dbg_out_cc_failure :-
	opt_dcc,
	!,
	write('\tFailed to prove inconsistency.'),
	nl,
	nl.

dbg_out_cc_failure.

%==============================================================================
% Consistency Checker for Conjunctions:
%==============================================================================


%------------------------------------------------------------------------------
% is_inconsistent_conj(+AtomicFormulaList):
%------------------------------------------------------------------------------

is_inconsistent_conj(Conj) :-
	conj_contains_false(Conj),
	!.

is_inconsistent_conj(Conj) :-
	dbg_out_cc_conj(Conj),
	derive_all(Conj, AllConsequences),
	dbg_out_cc_derived(AllConsequences),
	conj_contains_false(AllConsequences).

%------------------------------------------------------------------------------
% dbg_out_cc_conj(+Conj):
%------------------------------------------------------------------------------

dbg_out_cc_conj(Conj) :-
	opt_dcc,
	!,
	write('\tCheck Conj.: '),
	print_conj(Conj),
	nl.

dbg_out_cc_conj(_).

%------------------------------------------------------------------------------
% dbg_out_cc_derived(+Conj):
%------------------------------------------------------------------------------

dbg_out_cc_derived(Conj) :-
	opt_dcc,
	!,
	conj_length(Conj, Length),
	write('\tDerived: '),
	write(Length),
	write(' Atomic Formulas.'),
	nl,
	print_conj_prover(Conj),
	nl.

dbg_out_cc_derived(_).

%------------------------------------------------------------------------------
% derive_all(+AtomicFormulaList, -ExtendedAtomicFormulaList):
%------------------------------------------------------------------------------

derive_all(Conj, AllConsequences) :-
	derive(Conj, AtomicFormula),
	\+ list_member(AtomicFormula, Conj),
	!,
	derive_all_break([AtomicFormula|Conj], AllConsequences).

derive_all(Conj, Conj).

% We can stop once false is derived:

derive_all_break([false|Conj], [false|Conj]) :-
	!.

derive_all_break(Conj, AllConsequences) :-
	derive_all(Conj, AllConsequences).

%------------------------------------------------------------------------------
% derive(+AtomicFormulaList, -AtomicFormula):
%------------------------------------------------------------------------------

derive(Conj, Consequence) :-
	list_member(AtomicFormula, Conj),
	consequence1(AtomicFormula, Consequence).

derive(Conj, Consequence) :-
	list_member(AtomicFormula1, Conj),
	list_member(AtomicFormula2, Conj),
	consequence2(AtomicFormula1, AtomicFormula2, Consequence).

derive(Conj, Consequence) :-
	list_member(AtomicFormula1, Conj),
	list_member(AtomicFormula2, Conj),
	list_member(AtomicFormula3, Conj),
	consequence3(AtomicFormula1, AtomicFormula2, AtomicFormula3,
			Consequence).

%derive(Conj, Consequence) :-
%	list_member(AtomicFormula1, Conj),
%	list_member(AtomicFormula2, Conj),
%	list_member(AtomicFormula3, Conj),
%	list_member(AtomicFormula4, Conj),
%	consequence4(AtomicFormula1, AtomicFormula2, AtomicFormula3,
%			AtomicFormula4, Consequence).

%------------------------------------------------------------------------------
% consequence1(+AtomicFormulaIn, -AtomicFormulaOut):
%------------------------------------------------------------------------------

% The consequence true is not interesting, but false is very interesting.
% Note that here, atomic formulas can also be built-in literals.

consequence1(eq(X,Y), eq(Y,X)) :-
	X \= Y.

consequence1(eq(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	Const1 \= Const2.

consequence1(ne(X,Y), ne(Y,X)).

consequence1(ne(Term,Term), false).

consequence1(succ(X,Y), ne(X,Y)).

consequence1(succ(0,Term), eq(Term,1)) :-
	Term \= 1.

consequence1(succ(Term,1), eq(Term,0)) :-
	Term \= 0.

consequence1(succ(_,0), false).

consequence1(ret_millis(0,_), false).

consequence1(lt(X,Y), ne(X,Y)).

consequence1(lt(X,Y), gt(Y,X)).

consequence1(lt(X,Y), le(X,Y)).

consequence1(le(X,Y), ge(Y,X)).

consequence1(ge(X,Y), le(Y,X)).

consequence1(gt(X,Y), ne(X,Y)).

consequence1(gt(X,Y), lt(Y,X)).

consequence1(gt(X,Y), ge(X,Y)).

% X + Y < Z. We know that the delay Y >= 0 and the start time X >= 0:
consequence1(plus_lt(X,_Y,Z), lt(X,Z)).

consequence1(plus_lt(_X,Y,Z), lt(Y,Z)).

% X + Y >= Z. We can only derive X>=0 and Y>=0.
% So far, all our numbers are non-negative, so this does not help much.

% This handles cases with two constants (TODO: There is some duplicate work):
consequence1(F, false) :-
	eval_obvious_atomic(F, Result),
	Result = false.

%------------------------------------------------------------------------------
% consequence2(+AtomicFormulaIn1, +AtomicFormulaIn2, -AtomicFormulaOut):
%------------------------------------------------------------------------------

% Equalities of the type X=X are not useful.

% Transitivity of eq:

consequence2(eq(X,Y), eq(Y,Z), eq(X,Z)) :-
	X \= Z.

% Can replace equals in ne:

consequence2(ne(X,Y), eq(Y,Y1), ne(X,Y1)).

consequence2(ne(X,Y), eq(X,X1), ne(X1,Y)).

% lt:

consequence2(lt(X,Y), eq(Y,Z), lt(X,Z)).

consequence2(lt(X,Y), le(Y,Z), lt(X,Z)).

consequence2(eq(X,Y), lt(Y,Z), lt(X,Z)).

consequence2(le(X,Y), lt(Y,Z), lt(X,Z)).

% le:

consequence2(le(X,Y), eq(Y,Z), le(X,Z)).

consequence2(le(X,Y), le(Y,Z), le(X,Z)).

consequence2(eq(X,Y), le(Y,Z), le(X,Z)).

% gt:

consequence2(gt(X,Y), eq(Y,Z), gt(X,Z)).

consequence2(gt(X,Y), ge(Y,Z), gt(X,Z)).

consequence2(eq(X,Y), gt(Y,Z), gt(X,Z)).

consequence2(ge(X,Y), gt(Y,Z), gt(X,Z)).

% ge:

consequence2(ge(X,Y), eq(Y,Z), ge(X,Z)).

consequence2(ge(X,Y), ge(Y,Z), ge(X,Z)).

consequence2(eq(X,Y), ge(Y,Z), ge(X,Z)).

% plus_lt (X+Y<Z):

consequence2(plus_lt(X,Y,Z), eq(X,X1), plus_lt(X1,Y,Z)).

consequence2(plus_lt(X,Y,Z), eq(Y,Y1), plus_lt(X,Y1,Z)).

consequence2(plus_lt(X,Y,Z), eq(Z,Z1), plus_lt(X,Y,Z1)).

consequence2(plus_lt(X,Y,Z), le(X1,X), plus_lt(X1,Y,Z)).

consequence2(plus_lt(X,Y,Z), le(Y1,Y), plus_lt(X,Y1,Z)).

consequence2(plus_lt(X,Y,Z), le(Z,Z1), plus_lt(X,Y,Z1)).

% plus_ge (X+Y>=Z):

consequence2(plus_ge(X,Y,Z), eq(X,X1), plus_ge(X1,Y,Z)).

consequence2(plus_ge(X,Y,Z), eq(Y,Y1), plus_ge(X,Y1,Z)).

consequence2(plus_ge(X,Y,Z), eq(Z,Z1), plus_ge(X,Y,Z1)).

consequence2(plus_ge(X,Y,Z), ge(X1,X), plus_ge(X1,Y,Z)).

consequence2(plus_ge(X,Y,Z), ge(Y1,Y), plus_ge(X,Y1,Z)).

consequence2(plus_ge(X,Y,Z), ge(Z,Z1), plus_ge(X,Y,Z1)).

% Conflict of plus_lt and plus_ge:

consequence2(plus_lt(X,Y,Z), plus_ge(X,Y,Z), false).

% succ:

consequence2(succ(X,Y), succ(X1,Y), eq(X,X1)) :-
	X \= X1.

consequence2(succ(X,Y), succ(X,Y1), eq(Y,Y1)) :-
	Y \= Y1.

consequence2(succ(X,Y), eq(X,X1), succ(X1,Y)).

consequence2(succ(X,Y), eq(Y,Y1), succ(X,Y1)).

% ret_millis:

consequence2(ret_millis(X,_), eq(X,0), false).

consequence2(ret_millis(X,Y), ret_millis(X,Y1), eq(Y,Y1)) :-
	Y \= Y1.

consequence2(ret_millis(X,Y), eq(X,X1), ret_millis(X1,Y)).

consequence2(ret_millis(X,Y), eq(Y,Y1), ret_millis(X,Y1)).

%------------------------------------------------------------------------------
% consequence3(+AtomicFIn1, +AtomicFIn2, +AtomicFIn3, -AtomicFormulaOut):
%------------------------------------------------------------------------------

consequence3(succ(X,Y), succ(X1,Y1), ne(X,X1),
		ne(Y,Y1)).

consequence3(succ(X,Y), succ(X1,Y1), ne(Y,Y1),
		ne(X,X1)).

consequence3(ret_millis(X,Y), ret_millis(X1,Y1), ne(Y,Y1),
		ne(X,X1)).

%------------------------------------------------------------------------------
% consequence4(+AtomicFIn1, +AtomicFIn2, +AtomicFIn3, +AtomicFIn4, -AtomicFOut):
%------------------------------------------------------------------------------

%consequence4(plus_lt(X1,Y1,Z), plus_ge(X2,Y2,Z), eq(X1,X2), eq(Y1,Y2), false).

%==============================================================================
% Tests of Consistency Checker:
%==============================================================================


%------------------------------------------------------------------------------
% Tests of the Inconsistency Checker:
%------------------------------------------------------------------------------

test_inconsistency :-
	test_inconsistency_pos,
	test_inconsistency_neg,
	nl,
	write('All tests successful!'),
	nl.

% test_inconsistency_pos:

test_inconsistency_pos :-
	write('Test1: X=Y, 1=2, X=Z'),
	nl,
	is_inconsistent_conj([eq(v('X'),v('Y')),eq(1,2),eq(v('X'),v('Z'))]),
	nl,
	write('Test2: 1=X, X=2'),
	nl,
	is_inconsistent_conj([eq(1,v('X')),eq(v('X'),2)]),
	nl,
	write('Test3: X=Y, A=B, Y=Z, X<>Z'),
	nl,
	Conj3=[eq(v('X'),v('Y')), eq(v('A'),v('B')), eq(v('Y'),v('Z')),
		ne(v('X'),v('Z'))],
	is_inconsistent_conj(Conj3),
	nl,
	!.

test_inconsistency_pos :-
	write('*** TEST FAILED ***'),
	nl.

% test_inconsistency_neg:

test_inconsistency_neg :-
	write('Test4: X=Y, 1=Z, X=Z, 1<>2 (consistent)'),
	nl,
	Conj=[eq(v('X'),v('Y')), eq(1,v('Z')), eq(v('X'),v('Z')), ne(1,2)],
	is_inconsistent_conj(Conj),
	write('*** TEST FAILED ***'),
	!,
	fail.

test_inconsistency_neg.

