b_simplifier

b_arithmetic_expression(BExpr,Res) :-
    get_texpr_expr(BExpr,Expr),
    get_texpr_type(BExpr,integer), % only an integer expression
    b_arithmetic_expression1(Expr,Res).

b_arithmetic_expression1(integer(X),X) :- !,
    number(X).

b_arithmetic_expression1(unary_minus(E),Res) :- !,
    b_arithmetic_expression(E,ERes),
    Res = '-'(ERes).

b_arithmetic_expression1(add(E1,E2),Res) :- !,
    b_arithmetic_expression(E1,E1Res),
    b_arithmetic_expression(E2,E2Res),
    Res = '+'(E1Res,E2Res).

b_arithmetic_expression1(minus(E1,E2),Res) :- !,
    b_arithmetic_expression(E1,E1Res),
    b_arithmetic_expression(E2,E2Res),
    Res = '-'(E1Res,E2Res).

b_arithmetic_expression1(multiplication(E1,E2),Res) :- !,
    b_arithmetic_expression(E1,E1Res),
    b_arithmetic_expression(E2,E2Res),
    Res = '*'(E1Res,E2Res).

b_integer_value(BExpr,IsIntValue,Res,NewBExpr) :-
    b_arithmetic_expression(BExpr,X),!,
    Res is X,IsIntValue=true,
    create_texpr(integer(Res),integer,[],NewBExpr).

b_integer_value(BExpr,IsIntValue,Res,NewBExpr) :-
    Res = BExpr,IsIntValue=false,
    NewBExpr=BExpr.

compare(Operator,LHS,RHS,Functor,Type,Res) :-
    b_integer_value(LHS,IsIntValueX,EX,NewLHS),
    b_integer_value(RHS,IsIntValueY,EY,NewRHS),
    ((IsIntValueX,IsIntValueY) ->
    (memberchk(Operator,['<','>','=<','>=','==','=\\=']) ->
    Call =.. [Operator,EX,EY],
    (Call -> create_texpr(truth,Type,[],Res); create_texpr(falsity,Type,[],Res))
    ;
    add_internal_error('Internal error: Unexpected arithmetic comparison Operator: ', Operator),
    BExpr =.. [Functor,NewLHS,NewRHS],
    create_texpr(BExpr,Type,[],Res)
    )
    ;
    BExpr =.. [Functor,NewLHS,NewRHS],
    create_texpr(BExpr,Type,[],Res)
).

is_absorption_rule_conjunct(LHS,RHS,Res) :-
    is_a_disjunct(RHS,P,Q),
    (same_texpr(LHS,P); same_texpr(LHS,Q)),!,
    Res = LHS.

is_absorption_rule_conjunct(LHS,RHS,Res) :-
    is_a_disjunct(LHS,P,Q),
    (same_texpr(RHS,P); same_texpr(RHS,Q)),!,
    Res = RHS.

is_absorption_rule_disjunct(LHS,RHS,Res) :-
    is_a_conjunct(RHS,P,Q),
    (same_texpr(LHS,P); same_texpr(LHS,Q)),!,
    Res = LHS.

is_absorption_rule_disjunct(LHS,RHS,Res) :-
    is_a_conjunct(LHS,P,Q),
    (same_texpr(RHS,P); same_texpr(RHS,Q)),!,
    Res = RHS.

is_false_constant(Expr) :-
    (is_falsity(Expr); Expr=boolean_false).

is_global_integer_set(Set,GlobalSet) :-
    get_texpr_expr(Set,SetExpr),
    SetExpr = integer_set(GlobalSet),
    memberchk(GlobalSet,['NATURAL','NAT','INTEGER','INT']).

is_interval_set(b(interval(b(Low,integer,_),b(Up,integer,_)),set(integer),_),Low,Up).

is_true_constant(Expr) :-
    (is_truth(Expr); Expr=boolean_true).

negate_and_swap(less_real,less_equal_real).

negate_and_swap(less_equal_real,less_real).

negated_binary_pred(member, not_member).

negated_binary_pred(not_member, member).

negated_binary_pred(less, greater_equal).

negated_binary_pred(less_equal, greater).

negated_binary_pred(greater, less_equal).

negated_binary_pred(greater_equal, less).

negated_binary_pred(equal, not_equal).

negated_binary_pred(not_equal, equal).

negated_binary_pred(subset, not_subset).

negated_binary_pred(not_subset, subset).

negated_binary_pred(subset_strict, not_subset_strict).

negated_binary_pred(not_subset_strict, subset_strict).

simplify_b_predicate(Pred,Res) :-
    get_texpr_expr(Pred,Expr),
    get_texpr_type(Pred,Type),
    simplify_b_predicate2(Expr,Type,Res).

simplify_b_predicate2(truth,Type,Res) :- !,
    create_texpr(truth,Type,[],Res).

simplify_b_predicate2(falsity,Type,Res) :- !,
    create_texpr(falsity,Type,[],Res).

simplify_b_predicate2(negation(BExpr),_Type,Res) :- !,
    simplify_negation(BExpr,Res).

simplify_b_predicate2(conjunct(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    ( is_false_constant(SimplifiedLHS) -> % FALSE & f == FALSE
    create_texpr(falsity,Type,[],Res)
    ; is_true_constant(SimplifiedLHS) -> % TRUE & f == f
    simplify_b_predicate(RHS,Res)
    ;
    simplify_b_predicate(RHS,SimplifiedRHS),
    ( is_false_constant(SimplifiedRHS) -> % f & FALSE == FALSE
    create_texpr(falsity,Type,[],Res)
    ; is_true_constant(SimplifiedRHS) -> % f & TRUE == f
    Res = SimplifiedLHS
    ; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f & f == f (idempotence)
    Res = SimplifiedLHS
    ; is_absorption_rule_conjunct(SimplifiedLHS,SimplifiedRHS,Res) -> % f & (f or g) == f (absorption)
    true
    ; test_transitivity(SimplifiedLHS,SimplifiedRHS,Res) -> % (f => g) & (g => h) == (f => h)
    true
    ;
    conjunct_predicates([SimplifiedLHS,SimplifiedRHS],Res)
)
).

simplify_b_predicate2(disjunct(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    ( is_true_constant(SimplifiedLHS) -> % TRUE or f == TRUE
    create_texpr(truth,Type,[],Res)
    ; is_false_constant(SimplifiedLHS) -> % FALSE or f == f
    simplify_b_predicate(RHS,Res)
    ;
    simplify_b_predicate(RHS,SimplifiedRHS),
    ( is_true_constant(SimplifiedRHS) -> % f or TRUE == TRUE
    create_texpr(truth,Type,[],Res)
    ; is_false_constant(SimplifiedRHS) -> % f or FALSE == f
    Res = SimplifiedLHS
    ; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f or f == f (idempotence)
    Res = SimplifiedLHS
    ; is_absorption_rule_disjunct(LHS,RHS,Res) -> % f or (f & g) == f (absorption)
    true
    ;
    disjunct_predicates([SimplifiedLHS,SimplifiedRHS],Res)
)
).

simplify_b_predicate2(implication(LHS,RHS),_Type,Res) :- !,
    simplify_b_predicate(RHS,SimplifiedRHS),
    simplify_implication(LHS,SimplifiedRHS,Res).

simplify_b_predicate2(equivalence(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    ( same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f <=> f == TRUE
    create_texpr(truth,Type,[],Res)
    ; is_negation_of(SimplifiedLHS,SimplifiedRHS) -> % f <=> not(f) == FALSE
    create_texpr(falsity,Type,[],Res)
    ;
    create_equivalence(SimplifiedLHS,SimplifiedRHS,Res)
).

simplify_b_predicate2(equal(LHS,RHS),Type,Res) :- !,
    print(equal(LHS,RHS)),nl,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    (same_texpr(SimplifiedLHS,SimplifiedRHS) ->
    create_texpr(truth,Type,[],Res)
    ; different_texpr_values(SimplifiedLHS,SimplifiedRHS) ->
    create_texpr(falsity,Type,[],Res)
    ;
    compare('==',SimplifiedLHS,SimplifiedRHS,equal,Type,Res)
%% extract_info(SimplifiedLHS,SimplifiedRHS,Info),
%% create_texpr(equal(SimplifiedLHS,SimplifiedRHS),Type,Info,Res)
).

simplify_b_predicate2(not_equal(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    (same_texpr(SimplifiedLHS,SimplifiedRHS) ->
    create_texpr(falsity,Type,[],Res)
    ; different_texpr_values(SimplifiedLHS,SimplifiedRHS) ->
    create_texpr(truth,Type,[],Res)
    ;
    compare('=\\=',SimplifiedLHS,SimplifiedRHS,not_equal,Type,Res)
%% extract_info(SimplifiedLHS,SimplifiedRHS,Info),
%% create_texpr(not_equal(SimplifiedLHS,SimplifiedRHS),Type,Info,Res)
).

simplify_b_predicate2(greater(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    compare('>',SimplifiedLHS,SimplifiedRHS,greater,Type,Res).

simplify_b_predicate2(greater_equal(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    compare('>=',SimplifiedLHS,SimplifiedRHS,greater_equal,Type,Res).

simplify_b_predicate2(less(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    compare('<',SimplifiedLHS,SimplifiedRHS,less,Type,Res).

simplify_b_predicate2(less_equal(LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(LHS,SimplifiedLHS),
    simplify_b_predicate(RHS,SimplifiedRHS),
    compare('=<',SimplifiedLHS,SimplifiedRHS,less_equal,Type,Res).

simplify_b_predicate2(forall(Ids,LHS,RHS),Type,Res) :- !,
    simplify_b_predicate(RHS,SimplifiedRHS),
    (is_true_constant(SimplifiedRHS) ->
    create_texpr(truth,Type,[],Res)
    ;
    simplify_b_predicate(LHS,SimplifiedLHS),
    create_implication(SimplifiedLHS,SimplifiedRHS,ImplicationRes),
    create_forall(Ids,ImplicationRes,Res)
).

simplify_b_predicate2(exists(Ids,Pred),Type,Res) :- !,
    simplify_b_predicate(Pred,SimplifiedPred),
    (is_true_constant(SimplifiedPred) ->
    create_texpr(truth,Type,[],Res)
    ; is_false_constant(SimplifiedPred) ->
    create_texpr(falsity,Type,[],Res)
    ;
    create_or_merge_exists(Ids,SimplifiedPred,Res)
).

simplify_b_predicate2(member(Element,Set),Type,Res) :- !,
    simplify_membership_predicate(Element,Set,Type,Res).

simplify_b_predicate2(not_member(Element,Set),Type,Res) :- !,
    simplify_non_membership_predicate(Element,Set,Type,Res).

simplify_b_predicate2(BExpr,Type,Res) :-
    create_texpr(BExpr,Type,[],Res).

simplify_implication(_LHS,SimplifiedRHS,Res) :-
    is_true_constant(SimplifiedRHS),!, % f => TRUE == TRUE
    create_texpr(truth,pred,[],Res).

simplify_implication(LHS,SimplifiedRHS,Res) :-
    is_false_constant(SimplifiedRHS),!, % f => FALSE == neg(f)
    simplify_b_predicate(LHS,SimplifiedLHS),
    create_negation(SimplifiedLHS,Res).

simplify_implication(LHS,SimplifiedRHS,Res) :-
    simplify_b_predicate(LHS,SimplifiedLHS),
    (is_false_constant(SimplifiedLHS) -> % FALSE => f == TRUE
    create_texpr(truth,pred,[],Res)
    ; is_true_constant(SimplifiedLHS) -> % TRUE => f == f
    Res = SimplifiedRHS
    ; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f => f == TRUE
    create_texpr(truth,pred,[],Res)
    ;
    create_implication(SimplifiedLHS,SimplifiedRHS,Res)
).

simplify_membership_predicate(Element,Set,Type,Res) :-
    b_integer_value(Element,IsIntValue,EX,_NewElement),
    IsIntValue,
    test_integer_membership(Set,EX,Type,Res),!.

simplify_membership_predicate(Element,Set,Type,Res) :-
    b_integer_value(Element,_IsIntValue,_EX,NewElement),
    create_texpr(member(NewElement,Set),Type,[],Res).

simplify_negation(b(negation(BExpr),pred,_), Res) :- !, % double negation "not not f == f"
    simplify_b_predicate(BExpr, Res).

simplify_negation(Impl, Res) :-
    Impl = b(implication(Lhs,Rhs),pred,Info),
    !,
    simplify_b_predicate(Impl, SImpl),
    ( SImpl \= b(implication(_,_),pred,_)
    -> % implication could be simplified to TRUTH, FALSITY or a single negation
    simplify_b_predicate(b(negation(SImpl),pred,Info), Res)
    ; % "not (a => b) == a and not b"
    NRhs = b(negation(Rhs),pred,[]),
    simplify_b_predicate(b(conjunct(Lhs,NRhs),pred,Info), Res)
).

simplify_negation(b(conjunct(Lhs,Rhs),pred,Info), Res) :- !,
    NLhs = b(negation(Lhs),pred,[]),
    NRhs = b(negation(Rhs),pred,[]),
    simplify_b_predicate(b(disjunct(NLhs,NRhs),pred,Info), Res).

simplify_negation(b(disjunct(Lhs,Rhs),pred,Info),Res) :- !,
    NLhs = b(negation(Lhs),pred,[]),
    NRhs = b(negation(Rhs),pred,[]),
    simplify_b_predicate(b(conjunct(NLhs,NRhs),pred,Info), Res).

simplify_negation(b(forall(Ids,Lhs,Rhs),pred,Info),Res) :- !,
    simplify_b_predicate(b(negation(b(implication(Lhs,Rhs),pred,Info)),pred,[]), Body),
    Res = b(exists(Ids,Body),pred,Info).

simplify_negation(b(exists(Ids,Body),pred,Info),Res) :- !,
    simplify_b_predicate(b(negation(Body),pred,[]), NBody),
    generate_typing_predicates(Ids, TypingList),
    conjunct_predicates(TypingList, Typing),
    Res = b(forall(Ids,Typing,NBody),pred,Info).

simplify_negation(b(Node,pred,Info),Res) :-
    Node =.. [Functor,Lhs,Rhs],
    negated_binary_pred(Functor, NegFunctor),
    !,
    NegNode =.. [NegFunctor,Lhs,Rhs],
    simplify_b_predicate(b(NegNode,pred,Info), Res).

simplify_negation(b(Node,pred,Info),Res) :-
    Node =.. [Functor,Lhs,Rhs],
    negate_and_swap(Functor, NegFunctor),
    !,
    NegNode =.. [NegFunctor,Rhs,Lhs],
    simplify_b_predicate(b(NegNode,pred,Info), Res).

simplify_negation(BExpr, Res) :-
    simplify_b_predicate(BExpr, SimplifiedBExpr),
    % Simplifications like "not(FALSE) == TRUE" and "not(TRUE) == FALSE" will be applied by create_negation/2
    create_negation(SimplifiedBExpr, Res).

simplify_non_membership_predicate(Element,Set,Type,Res) :-
    b_integer_value(Element,IsIntValue,EX,_NewElement),
    IsIntValue,
    test_integer_membership(Set,EX,Type,Res1),!,
    (is_true_constant(Res1) ->
    create_texpr(falsity,Type,[],Res)
    ; is_false_constant(Res1) ->
    create_texpr(truth,Type,[],Res)
    ;
    add_internal_error('Internal error: Unexpected result from test_integer_membership/4 predicate in simplify_membership_predicate/4: ',Res1)
).

simplify_non_membership_predicate(Element,Set,Type,Res) :-
    b_integer_value(Element,_IsIntValue,_EX,NewElement),
    create_texpr(not_member(NewElement,Set),Type,[],Res).

tcltk_simplify_b_predicate(String,StringResult) :-
    b_parse_machine_predicate(String,Tree),
    simplify_b_predicate(Tree,Res),
    translate_bexpression(Res,StringResult).

tcltk_simplify_b_predicate_error(String,StringResult) :-
    if(tcltk_simplify_b_predicate(String,StringResult),true,
    (StringResult = 'Error or User-Interrupt')).

test(simplify_neg_conj, [all(Simplified = [b(less_equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])])]) :-
    IntOne = b(integer(1),integer,[]),
    Id = b(identifier(x),integer,[]),
    Greater = b(greater(Id,IntOne),pred,[]),
    Pred = b(negation(b(conjunct(Greater,Greater),pred,[])),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_neg_disj, [all(Simplified = [b(less_equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])])]) :-
    IntOne = b(integer(1),integer,[]),
    Id = b(identifier(x),integer,[]),
    Greater = b(greater(Id,IntOne),pred,[]),
    Pred = b(negation(b(disjunct(Greater,Greater),pred,[])),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_neg_equal, [all(Simplified = [b(not_equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Id = b(identifier(x),integer,[]),
    Pred = b(negation(b(equal(Id,IntOne),pred,[])),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_neg_not_equal, [all(Simplified = [b(equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Id = b(identifier(x),integer,[]),
    Pred = b(negation(b(not_equal(Id,IntOne),pred,[])),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_impl_to_truth, [all(Simplified = [b(truth,pred,[])])]) :-
    IntOne = b(integer(1),integer,[]),
    Id = b(identifier(x),integer,[]),
    Greater = b(greater(Id,IntOne),pred,[]),
    Pred = b(implication(Greater,Greater),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_impl_to_falsity, [all(Simplified = [b(falsity,pred,[])])]) :-
    IntOne = b(integer(1),integer,[]),
    Id = b(identifier(x),integer,[]),
    Greater = b(greater(Id,IntOne),pred,[]),
    Pred = b(negation(b(implication(Greater,Greater),pred,[])),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_impl_same, [all(Simplified = [b(implication(b(greater(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[]),b(less(b(identifier(y),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])])]) :-
    IntOne = b(integer(1),integer,[]),
    Id1 = b(identifier(x),integer,[]),
    Id2 = b(identifier(y),integer,[]),
    Greater = b(greater(Id1,IntOne),pred,[]),
    Less = b(less(Id2,IntOne),pred,[]),
    Pred = b(implication(Greater,Less),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test(simplify_neg_impl, [all(Simplified = [b(conjunct(b(greater(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[]),b(greater_equal(b(identifier(y),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])])]) :-
    IntOne = b(integer(1),integer,[]),
    Id1 = b(identifier(x),integer,[]),
    Id2 = b(identifier(y),integer,[]),
    Greater = b(greater(Id1,IntOne),pred,[]),
    Less = b(less(Id2,IntOne),pred,[]),
    Pred = b(negation(b(implication(Greater,Less),pred,[])),pred,[]),
    simplify_b_predicate(Pred, Simplified),
    ground(Simplified).

test_integer_membership(b(empty_set,set(integer),_),_X,Type,Res) :- !,
    create_texpr(falsity,Type,[],Res).

test_integer_membership(b(value(avl_set(AVLSet)),set(integer),_),X,Type,Res) :- !,
    (avl_fetch(int(X),AVLSet) ->
    create_texpr(truth,Type,[],Res)
    ;
    create_texpr(falsity,Type,[],Res)
).

test_integer_membership(Set,X,Type,Res) :-
    is_interval_set(Set,Low,Up),!,
    ((Low=<X,X=<Up) ->
    create_texpr(truth,Type,[],Res)
    ;
    create_texpr(falsity,Type,[],Res)
).

test_integer_membership(Set,X,Type,Res) :-
    is_global_integer_set(Set,GlobalSet),!,
    (element_of_global_set(int(X),GlobalSet) ->
    create_texpr(truth,Type,[],Res)
    ;
    create_texpr(falsity,Type,[],Res)
).

test_transitivity(LHS,RHS,Res) :-
    is_an_implication(LHS,P,Q),
    is_an_implication(RHS,Q1,R),
    same_texpr(Q,Q1),!,
    create_implication(P,R,Res).

test_transitivity(LHS,RHS,Res) :-
    is_an_implication(LHS,Q,R),
    is_an_implication(RHS,P,Q1),
    same_texpr(Q,Q1),!,
    create_implication(P,R,Res).