%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Copyright (C) 2024 Christoph Wernhard
%%%%
%%%% This program is free software: you can redistribute it and/or modify it
%%%% under the terms of the GNU General Public License as published by the
%%%% Free Software Foundation, either version 3 of the License, or (at your
%%%% option) any later version.
%%%%
%%%% This program is distributed in the hope that it will be useful, but
%%%% WITHOUT ANY WARRANTY; without even the implied warranty of
%%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
%%%% Public License for more details.
%%%%
%%%% You should have received a copy of the GNU General Public License
%%%% along with this program.  If not, see <http://www.gnu.org/licenses/>.
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


:- module(synasp, [p_gamma/2,
                   p_seq/3,
                   f_encodes_p_form/2,
                   f_decode_p/3,
                   f_lp_ipol_form/4,
                   f_lp_ipol/4,
                   latest_ipol_form/1,
                   p_def/5
                   ]).

/** <module> Synthesizing Answer Set Programs

Prototypical implementation of the approach described in Jan Heuer and
Christoph Wernhard: "Synthesizing Strongly Equivalent Logic Programs: Beth
Definability for Answer Set Programs via Craig Interpolation in First-Order
Logic", 2024.

*Installation Notes.* Runs in the PIE environment http://cs.christophwernhard.com/pie/ . Tested with
SWI-Prolog 9.0.4 and PIE February 2024. Also Prover9/Mace4 is recommended.

*Version:* Tue Feb 13 10:54:39 2024

*Argument Types*

* Prog
  Logic program. List of rules, e.g.
  ==
  [(p(X) ; not q(X) <-- r(X), not s(X)), (p(X) <-- true), (false <-- q(X)]
  ==
* Form
  First-order formula in Prolog-readable PIE notation.
* Options
  List of options. Only options processed directly by the predicates in this
  module are described. The list is passed to underlying layers that do the
  proving and interpolation.

@author Christoph Wernhard

*/

:- use_module(folelim(logop_fol)).
:- use_module(folelim(prettysymbols_fol)).
:- use_module(folelim(utils_fol)).
:- use_module(folelim(simp_fol)).
:- use_module(folelim(innexing)).
:- use_module(nf(nf)).
:- use_module(swilib(err)).

%% For the syntax of logic programs:
:- op(900, fy, user:not).
:- op(1200, xfx, user:'<--').
%% true/false for empty body/head.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% The gamma Transformation
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/** p_gamma(+Prog, -Form) is det.

  Form is the gamma transformation of Prog.

*/
p_gamma(P, F) :-
        findall(C, ( member(R, P),
                     gamma_0(R, C1),
                     ( C = C1
                     ; f_rename_01(C1, C)
                     )
                   ),
                Cs),
        list_to_conjunction(Cs, F1),
        uclose(F1, F).

gamma_0((H <-- B), C) :-
        !,
        gamma_0_h(H, CH),
        gamma_0_b(B, CB),
        logform_disjoin(CB, CH, C).
gamma_0(X, _) :-
        err('Bad rule: ~q', [X]).

gamma_0_h(false, false) :-
        !.
gamma_0_h((L ; H), (L1 ; H1)) :-
        !,
        plit_to_01(L, L1),
        gamma_0_h(H, H1).
gamma_0_h(L, L1) :-
        plit_to_01(L, L1).

gamma_0_b(true, false) :-
        !.
gamma_0_b((L , H), (L1 ; H1)) :-
        !,
        plit_to_01(L, L2),
        local_lit_complement(L2, L1),
        gamma_0_b(H, H1).
gamma_0_b(L, L1) :-
        plit_to_01(L, L2),
        local_lit_complement(L2, L1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

plit_to_01(not A, ~A1) :-
        !,
        A =.. [P|T],
        atom_concat(P, '1', P1),
        A1 =.. [P1|T].
plit_to_01(A, A1) :-
        !,
        A =.. [P|T],
        atom_concat(P, '0', P1),
        A1 =.. [P1|T].

plit_predicate(not A, P/N) :-
        !,
        functor(A, P, N).
plit_predicate(A, P/N) :-
        functor(A, P, N).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

local_lit_atom(~A, A) :-
        !.
local_lit_atom(A, A).

local_lit_complement(~A, A) :-
                !.
local_lit_complement(A, ~A).

uclose(F, F1) :-
        term_variables(F, V),
        ( V = [] ->
          F1 = F
        ; logform_clean_vars_to_symbols(all(V, F), F2),
          logform_vars_to_pretty_symbols(F2, F1)
        ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/** p_seq(+Prog1, +Prog2, +Options) is semidet.

  Succeeds if it can be verified that Prog1 and Prog2 are strongly equivalent.

*/
p_seq(P, Q, Opts) :-
        %% two implications are for most provers easier to handle than an
        %% equivalence
        p_seq_forms(P, Q, F1, F2),
        ppl_valid(F1, [r=true, printing=false | Opts]),
        info(9, 'Verified ->'),
        ppl_valid(F2, [r=true, printing=false | Opts]),
        info(9, 'Verified <-').

p_seq_forms(P, Q, F1, F2) :-
        append(P, Q, PQ),
        p_sub(PQ, S),
        p_gamma(P, FP),
        p_gamma(Q, FQ),
        F1 = (S,FP -> FQ),
        F2 = (S,FQ -> FP).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Decoding
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


/** f_encodes_p_form(+Form1, -Form2) is det.

  Form2 is valid iff Form1 encodes a logic program.
*/
f_encodes_p_form(F, F1) :-
        f_sub(F, S),
        f_rename_01(F, R),
        F1 = (F, S -> R).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/** f_decode_p(+Form, -Prog, +Options) is det.

  Prog is obtained by decoding Form. Processed options include

* decode_cnf=CNF
  Specifies the variant of CNF transformation. See code for values of CNF.
* decode_partition=PM
  Specifies the partitioning method (Step 2 of the algorithm).
  See code for values of PM.
* decode_simp=Simp
  Specifies simplifications on the CNF before extraction.
  See code for values of Simp.

*/
f_decode_p(F, P, Opts) :-
        ( memberchk(decode_cnf=CNF, Opts) -> true ; CNF = 3 ),
        ( memberchk(decode_partition=PM, Opts) -> true ; PM = 1 ),
        ( memberchk(decode_simp=Simp, Opts) -> true ; Simp = 1 ),
        ( CNF = 0 ->
          cnf_fewsimp(F, M)
        ; CNF = 1 ->
          cnf(F, M)
        ; CNF = 3 ->
          cnf6(F, M)
        ),
        ( Simp = 0 ->
          MS = M
        ; Simp = 1 ->
          m_simp_msf_1(M, MS)
        ; Simp = 2 ->
          m_simp_msf_2(M, MS)
        ; Simp = 3 ->
          m_simp_msf_3(M, MS)
        ),
        m_split_01(MS, M0, M1),
        ( PM = 0 ->
          M1_1 = M1
        ; PM = 1 ->
          m_decode_partition(M1, M0, M1_1, _)
        ),
        append(M0, M1_1, MP),
        m_to_p(MP, P1),
        align_vars(P1, _, P).

m_to_p(MP, P) :-
        findall(R, ( member(C, MP), c_to_r(C, R) ), P).

c_to_r(C, (H <-- B)) :-
        cr1(C, PH, NH, PB, NB),
        append(PH, NH, H1),
        list_to_disjunction(H1, H),
        append(PB, NB, B1),
        list_to_conjunction(B1, B).

cr1([~A|C], PH, NH, PB, NB) :-
        !,
        A =.. [P|T],
        sub_atom(P, 0, _, 1, P1),
        A1 =.. [P1|T],
        ( sub_atom(P, _, 1, 0, '0') ->
          PB = [A1|PB1],
          PH = PH1,
          NH = NH1,
          NB = NB1
        ; NH = [not A1|NH1],
          PH = PH1,
          PB = PB1,
          NB = NB1
        ),
        cr1(C, PH1, NH1, PB1, NB1).
cr1([A|C], PH, NH, PB, NB) :-
        A =.. [P|T],
        sub_atom(P, 0, _, 1, P1),
        A1 =.. [P1|T],
        ( sub_atom(P, _, 1, 0, '0') ->
          PH = [A1|PH1],
          PB = PB1,
          NH = NH1,
          NB = NB1
        ; NB = [not A1|NB1],
          PH = PH1,
          NH = NH1,
          PB = PB1
        ),
        cr1(C, PH1, NH1, PB1, NB1).
cr1([], [], [], [], []).

align_vars([C|Cs], Vs, [C1|Cs1]) :-
        copy_term(C, C1),
        term_variables(C1, Vs1),
        set_vars(Vs1, Vs),
        align_vars(Cs, Vs, Cs1).
align_vars([], _, []).

set_vars([V|Vs], [V|Vs1]) :-
        set_vars(Vs, Vs1).
set_vars([], _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

m_decode_partition(M1, M0, M1_1, M1_2) :-
        m_rename_01(M0, M00),
        mdp(M1, M00, M1_1, M1_2).

mdp([C|M], M00, M1_1, M1_2) :-
        ( member(D, M00),
          clause_subsumes_chk(D, C) ->
          M1_2  = [C|M1_22],
          M1_1 = M1_11
        ; M1_2 = M1_22,
          M1_1 = [C|M1_11]
        ),
        mdp(M, M00, M1_11, M1_22).
mdp([], _, [], []).

m_split_01([C|M], M0, M1) :-
        ( c_contains_0(C) ->
          M0 = [C|M00],
          M1 = M11
        ; M0 = M00,
          M1 = [C|M11]
        ),
        m_split_01(M, M00, M11).
m_split_01([], [], []).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

c_contains_0(C) :-
        member(L, C),
        local_lit_atom(L, A),
        functor(A, P, _),
        sub_atom(P, _, 1, 0, '0').

c_is_taut(C) :-
        member(~A, C),
        member(B, C),
        A == B,
        !.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Renaming the "Superscript Decoration"
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

f_rename_01(F, F1) :-
        f_preds(F, Ps),
        findall(P-P1, ( member(P, Ps), pred0_to_pred1(P, P1) ), Map),
        logform_rename_free_predicates(F, Map, pn, F1).

m_rename_01(M, M1) :-
        findall(C, ( member(C1, M),
                     c_rename_01(C1, C) ),
                M1).

c_rename_01([L|Ls], [L1|Ls1]) :-
        lit_rename_01(L, L1),
        c_rename_01(Ls, Ls1).
c_rename_01([], []).

lit_rename_01(~A, ~A1) :-
        !,
        logatom_rename_01(A, A1).
lit_rename_01(A, A1) :-
        logatom_rename_01(A, A1).

logatom_rename_01(A, A1) :-
        A =.. [P|T],
        pred0_to_pred1(P, P1),
        !,
        A1 =.. [P1|T].
logatom_rename_01(A, A).

logatom_rename_pos_10(A, A1) :-
        A =.. [P|T],
        pred1_to_pred0(P, P1),
        !,
        A1 =.. [P1|T].
logatom_rename_pos_10(A, A).

logatom_rename_neg_01(A, A1) :-
        A =.. [P|T],
        pred0_to_pred1(P, P1),
        !,
        A1 =.. [P1|T].
logatom_rename_neg_01(A, A).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Some Formula Simplifications that are Modulo "S_F", Preserving
%%%% Strong Equivalence
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

m_simp_msf_1(M, M1) :-
        m_simp_msf_lit(M, M2),
        m_simp_msf_pos(M2, M1).

m_simp_msf_2(M, M1) :-
        m_simp_msf_pos(M, M1).

m_simp_msf_3(M, M1) :-
        m_simp_msf_lit(M, M2),
        m_simp_msf_pos(M2, M3),
        m_simp_msf_neg(M3, M1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%
%%%% Removal of a clause $C$ if, after setting in $C$ the superscript of all
%%%% positive literals to $0$, the clause is tautological or is subsumed by
%%%% some other clause~$D$.
%%%%
m_simp_msf_pos(M, M1) :-
        select(C, M, M2),
        c_rename_pos_10(C, C1),
        ( c_is_taut(C1) ->
          true
        ; member(D, M2),
          clause_subsumes_chk(D, C1)
        ),
        !,
        m_simp_msf_pos(M2, M1).
m_simp_msf_pos(M, M).

c_rename_pos_10([L|Ls], [L1|Ls1]) :-
        lit_rename_pos_10(L, L1),
        c_rename_pos_10(Ls, Ls1).
c_rename_pos_10([], []).

lit_rename_pos_10(~A, ~A) :-
        !.
lit_rename_pos_10(A, A1) :-
        logatom_rename_pos_10(A, A1).

%%%%
%%%% Analogous to m_simp_msf_pos. Not sure if m_simp_msf_neg is often
%%%% applicable.
%%%%
m_simp_msf_neg(M, M1) :-
        select(C, M, M2),
        c_rename_neg_01(C, C1),
        ( c_is_taut(C1) ->
          true
        ; member(D, M2),
          clause_subsumes_chk(D, C1)
        ),
        !,
        info(10, 'MSF NEG STEP PERFORMED'),
        m_simp_msf_neg(M2, M1).
m_simp_msf_neg(M, M).

c_rename_neg_01([L|Ls], [L1|Ls1]) :-
        lit_rename_neg_01(L, L1),
        c_rename_neg_01(Ls, Ls1).
c_rename_neg_01([], []).

lit_rename_neg_01(~A, ~A1) :-
        !,
        logatom_rename_neg_01(A, A1).
lit_rename_neg_01(A, A).

%%%%
%%%% Removal of a positive (negative) literal superscripted with $0$ ($1$)
%%%% from a clause if a literal with the same polarity, same arguments and the
%%%% corresponding predicate superscripted with $1$ ($0$) is also in the
%%%% clause.
%%%%
m_simp_msf_lit(M, M1) :-
        map_c_msm(M, M1).

map_c_msm([X|Xs], [X1|Xs1]) :-
        c_msm(X, X, X1),
        map_c_msm(Xs, Xs1).
map_c_msm([], []).

c_msm([~A|C], D, E) :-
        a_msm_1(A, A0),
        copy_term(A0, A0C),
        member(~A0C, D),
        A0C == A0,
        !,
        c_msm(C, D, E).
c_msm([~A|C], D, [~A|E]) :-
        !,
        c_msm(C, D, E).
c_msm([A|C], D, E) :-
        a_msm_0(A, A1),
        copy_term(A1, A1C),
        member(A1C, D),
        A1C == A1,
        !,
        c_msm(C, D, E).
c_msm([A|C], D, [A|E]) :-
        !,
        c_msm(C, D, E).
c_msm([], _, []).

a_msm_1(A, A0) :-
        A =.. [P|T],
        sub_atom(P, _, 1, 0, '1'),
        !,
        sub_atom(P, 0, _, 1, P1),
        atom_concat(P1, '0', P2),
        A0 =.. [P2|T].

a_msm_0(A, A0) :-
        A =.. [P|T],
        sub_atom(P, _, 1, 0, '0'),
        !,
        sub_atom(P, 0, _, 1, P1),
        atom_concat(P1, '1', P2),
        A0 =.. [P2|T].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred1_to_pred0(P0, P1) :-
        sub_atom(P0, _, 1, 0, '1'),
        !,
        sub_atom(P0, 0, _, 1, P),
        atom_concat(P, '0', P1).

pred0_to_pred1(P0, P1) :-
        sub_atom(P0, _, 1, 0, '0'),
        !,
        sub_atom(P0, 0, _, 1, P),
        atom_concat(P, '1', P1).

pred01_to_pred(P01, P) :-
        sub_atom(P01, _, 1, 0, X),
        ( X = '0' -> true ; X = '1' ),
        !,
        sub_atom(P01, 0, _, 1, P).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

p_predicates(Prog, PNs) :-
        findall(P/N, ( member(R, Prog),
                       rule_predicate(R, P/N)
                     ),
                PNs1),
        sort(PNs1, PNs).

rule_predicate((H <-- B), P/N) :-
        ( rule_predicate_h(H, P/N)
        ; rule_predicate_b(B, P/N)
        ).

rule_predicate_h((L ; H), P/N) :-
        !,
        ( plit_predicate(L, P/N)
        ; rule_predicate_h(H, P/N)
        ).
rule_predicate_h(false, _) :-
        !,
        fail.
rule_predicate_h(L, P/N) :-
        plit_predicate(L, P/N).

rule_predicate_b((L , B), P/N) :-
        !,
        ( plit_predicate(L, P/N)
        ; rule_predicate_b(B, P/N)
        ).
rule_predicate_b(true, _) :-
        !,
        fail.
rule_predicate_b(L, P/N) :-
        plit_predicate(L, P/N).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

p_sub(P, S) :-
        p_predicates(P, PNs),
        pns_sub(PNs, S).

f_sub(F, S) :-
        f_signature(F, PNs, _),
        findall(P/N, ( member(P1/N, PNs),
                       pred01_to_pred(P1, P) ),
                PNs1),
        sort(PNs1, PNs2),
        pns_sub(PNs2, S).

pns_sub(PNs, S) :-
        findall(F1, ( member(P/N, PNs),
                      pn_sub(P/N, F1) ),
                Fs),
        list_to_conjunction(Fs, S1),
        f_join_quants(S1, S).

pn_sub(P/N, F) :-
        atom_concat(P, '0', P0),
        atom_concat(P, '1', P1),
        functor(A0, P0, N),
        functor(A1, P1, N),
        A0 =.. [_|T],
        A1 =.. [_|T],
        ( T = [] ->
          F = (~A0 ; A1)
        ; uclose((~A0 ; A1), F)
        ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% LP-Interpolation
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


/** f_lp_ipol_form(+FormF, +FormG, +Options, -FormH) is det.

  FormH is the formula underlying the Craig-Lyndon interpolation
  for the LP-interplation of FormF and FormG.

*/
f_lp_ipol_form(F, G, Opts, F1) :-
        f_sub(F, SF),
        f_sub(G, SG),
        ( memberchk(lpip_simp_input = LSI, Opts) -> true ; LSI = 0 ),
        ( LSI = 1 ->
          F2 = F,
          f_join_quants(G, G2)
        ; LSI = 2 ->
          f_join_quants(F, F2),
          f_join_quants(G, G2)
        ; F2 = F,
          G2 = G
        ),
        logform_conjoin(F2, SF, Left),
        logform_negate(SG, SGN),
        logform_disjoin(SGN, G2, Right),
        F1 = (Left -> Right).

/** latest_ipol_form(?Form) is semidet.

   Form is the formula of the formula of the latest interpolation task. It is
   asserted before prover invocation. Useful, e.g., for debugging.

*/
:- dynamic latest_ipol_form/1.

/** f_lp_ipol(+FormF, +FormG, -FormH, +Options) is nondet.

  FormH is an LP-interpolant of FormF and FormG.

  Succeeds only if the underlying entailment can be proven. Enumerates
  alternate solutions in case options specify an interpolation method that
  enumerates different interpolants for different proofs.
*/
f_lp_ipol(F, G, H, Opts) :-
        f_lp_ipol_form(F, G, Opts, F1),
        retractall( latest_ipol_form(_) ),
        asserta( latest_ipol_form(F1) ),
        ( memberchk(lpip_dry=F1, Opts) ->
          true
        ; ppl_ipol(F1, [r=H0, printing=false|Opts]),
          f_rename_01(H0, H1),
          logform_conjoin(H0, H1, H),
          ( memberchk(lpip_h=H, Opts) -> true ; true )
        ).

%% Some possible options for interpolation:
%% [ip_mode=hyper] (for cmprover)
%% [prover=prover9]
%% [enum_ips=3,add_cm_options=[]-[r8(_)]]
%% [add_cm_options=[ordp]]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Synthesis
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/** p_def(+ProgP, +ProgQ, +Vocab, -ProgR, +Options) is nondet.

  ProgR is a definiens of ProgQ within ProgP in the vocabulary Vocab.

  Succeeds only if the underlying entailment can be proven. Enumerates
  alternate solutions in case options specify an interpolation method that
  enumerates different interpolants for different proofs.

@arg Vocab A list of predicates or a term v(VP,VP1,VN) where
  VP, VP1 and VN are lists of predicates, corresponding to the
  position constraining corollary. If the =forget= option is set, predicates
  disallowed in positives heads are VP cup VP1 and the predicates disallowed
  in negative bodies are VP1.

@arg Options See examples_synasp.pl for a compilation of useful options.
  Directly processed options include

* forget
  Interpret Vocab as specifying the predicates that are not allowed.
* lpip_simp_input=Simp
  Special formula simplification for interpolation arguments. Recognized values
  of Simp:
  * 0
    No special simplification.
  * 1
    Simplify the second interpolation argument such that it involves less
    distinct variables, typically resulting in less Skolem terms. Very useful
    with CMProver and Prover9.
  * 2
    Like 1 but the simplification is also
    applied to the first interolation argument.
* lpdef_dry=(FormF-FormG)
  Don't perform interpolation but instead return the input formulas
  to IP-interpolation.
* lpip_dry=Form
  Don't perform interpolation but instead return the input
  to Craig-Lyndon interpolation as implication.

*/
p_def(P, Q, V, R, Opts) :-
        ( memberchk(formpreds, Opts) ->
          V1 = V
        ; V = v(_,_,_) ->
          ( memberchk(forget, Opts) ->
            v3preds_for_forgetting(V, V1)
          ; v3preds(V, V1)
          )
        ; findall(P1, ( member(P2, V),
                        ( atom_concat(P2, '0', P1)
                        ; atom_concat(P2, '1', P1)
                        )
                      ),
                  V2),
          sort(V2, V1)
        ),
        p_gamma(P, FP),
        p_gamma(Q, FQ),
        logform_conjoin(FP, FQ, Left1),
        logform_negate(FP, FPN),
        logform_disjoin(FPN, FQ, Right0),
        ( memberchk(forget, Opts) ->
          f_prime(Right0, V1, Right1)
        ; f_prime_except(Right0, V1, Right1)
        ),
        ( memberchk(lpdef_dry=(Left1-Right1), Opts) ->
          true
        ; f_lp_ipol(Left1, Right1, H, Opts),
          ( memberchk(lpip_dry=_, Opts) ->
            true
          ; f_decode_p(H, R, Opts)
          )
        ).

v3preds(v(V1,V2,V3), V) :-
        %% Here we handle V1,V2 auch that:
        %%    allowed in pos head = V1
        %%    allowed in neg body = V1 cup V2
        findall(P-Pol, ( member(P1, V1), atom_concat(P1, '0', P), Pol = p
                       ; member(P1, V1), atom_concat(P1, '1', P), Pol = p
                       ; member(P1, V2), atom_concat(P1, '1', P), Pol = p
                       ; member(P1, V3), atom_concat(P1, '0', P), Pol = n
                       ; member(P1, V3), atom_concat(P1, '1', P), Pol = n
                       ),
                V0),
        sort(V0, V).

v3preds_for_forgetting(v(V1,V2,V3), V) :-
        %% Here we handle V1,V2 auch that:
        %%    not allowed in pos head = V1 cup V2
        %%    not allowed in neg body = V2
        findall(P-Pol, ( member(P1, V1), atom_concat(P1, '0', P), Pol = p
                       ; member(P1, V2), atom_concat(P1, '0', P), Pol = p
                       ; member(P1, V2), atom_concat(P1, '1', P), Pol = p
                       ; member(P1, V3), atom_concat(P1, '0', P), Pol = n
                       ; member(P1, V3), atom_concat(P1, '1', P), Pol = n
                       ),
                V0),
        sort(V0, V).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

f_preds(F, Ps) :-
        findall(P,
                (logform_enum_atoms(F, A), functor(A, P, _)),
                Ps1),
        sort(Ps1, Ps).

f_predpols(F, PPs) :-
        findall(P-Pol,
                (logform_enum_atoms(F, A, Pol), functor(A, P, _)),
                PPs1),
        sort(PPs1, PPs).

f_predpols_allpols(F, Ps) :-
        findall(P-Pol,
                (logform_enum_atoms(F, A), functor(A, P, _),
                 (Pol = p ; Pol = n)),
                Ps1),
        sort(Ps1, Ps).

f_predpols_n(F, PPs) :-
        findall((P/N)-Pol,
                (logform_enum_atoms(F, A, Pol), functor(A, P, N)), PPs1),
        sort(PPs1, PPs).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

canonicalize_predpols(PPs, PPs1) :-
        findall(P-Pol, ( member(X, PPs),
                         ( atom(X) ->
                           P = X,
                           ( Pol = p ; Pol = n)
                         ; X = P-Pol1,
                           ( Pol1 = pn ->
                             ( Pol = p ; Pol = n)
                           ; Pol = Pol1
                           )
                         )
                       ),
                PPs2),
        sort(PPs2, PPs1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%
%%%% The objective of this simplification is to keep the number of distinct
%%%% variables small. In particular to obtain a small number of distinct
%%%% Skolem terms with conventional Skolemization methods, which can have a
%%%% big effect on provers (CMProver) and the size of resulting proofs
%%%% (Prover9). Also to let formulas without Skolemized variables look nicer.
%%%% It is for now a bit ad-hoc and should be replaced by something more
%%%% systematic. Maybe there are related known Skolemization techniques. Maybe
%%%% it is required in two versions for positve and negative polarity of the
%%%% input formulas, to prevent moving existential over universal quantifiers,
%%%% or vice versa, which would result in Skolem functions with unnecessary
%%%% many arguments.
%%%%
f_join_quants(F, F1) :-
        quants_inward(F, F2),
        f_merge_quants(F2, F1).

f_merge_quants(F, F1) :-
        logform_clean_vars_to_prolog_vars(F, F2),
        logform_process_subforms(F2, fmq_aux, F3),
        logform_clean_vars_to_symbols(F3, F4),
        logform_vars_to_pretty_symbols(F4, F1).

fmq_aux((all(X, F), all(Y, G)), all(Z, FG)) :-
        !,
        fmq_merge_quants(X, Y, Z),
        logform_conjoin(F, G, FG).
fmq_aux((ex(X, F); ex(Y, G)), ex(Z, FG)) :-
        !,
        fmq_merge_quants(X, Y, Z),
        logform_disjoin(F, G, FG).
% fmq_aux((all(X, F), G), all(X, FG)) :-
%         !,
%         logform_conjoin(F, G, FG).
% fmq_aux((F, all(X, G)), all(X, FG)) :-
%         !,
%         logform_conjoin(F, G, FG).
% fmq_aux((all(X, F) ; G), all(X, FG)) :-
%         !,
%          logform_disjoin(F, G, FG).
% fmq_aux((F ; all(X, G)), all(X, FG)) :-
%         !,
%          logform_disjoin(F, G, FG).
% fmq_aux((ex(X, F); G), ex(X, FG)) :-
%         !,
%         logform_disjoin(F, G, FG).
% fmq_aux((F; ex(X, G)), ex(X, FG)) :-
%         !,
%         logform_disjoin(F, G, FG).
% fmq_aux((ex(X, F), G), ex(X, FG)) :-
%         !,
%         logform_conjoin(F, G, FG).
% fmq_aux((F, ex(X, G)), ex(X, FG)) :-
%         !,
%         logform_conjoin(F, G, FG).
fmq_aux(X, X).

fmq_merge_quants(X, Y, Z) :-
        var(X),
        !,
        fmq_merge_quants([X], Y, Z).
fmq_merge_quants(X, Y, Z) :-
        var(Y),
        !,
        fmq_merge_quants(X, [Y], Z).
fmq_merge_quants([X|Xs], [Y|Ys], [X|Zs]) :-
        !,
        X = Y,
        fmq_merge_quants(Xs, Ys, Zs).
fmq_merge_quants([], Y, Y) :-
        !.
fmq_merge_quants(X, [], X).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Priming
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

f_prime(F, PPs, F1) :-
        canonicalize_predpols(PPs, PPs1),
        f_predpols(F, PPF),
        ord_intersect(PPF, PPs1, PPE),
        findall(P, member(P-p, PPE), PEPos),
        findall(P, member(P-n, PPE), PENeg),
        ord_intersect(PEPos, PENeg, PEBoth),
        ord_subtract(PEPos, PENeg, PEOnlyPos),
        ord_subtract(PENeg, PEPos, PEOnlyNeg),
        findall(P, member(P-p, PPF), PFPos),
        findall(P, member(P-n, PPF), PFNeg),
        ord_intersect(PEOnlyPos, PFNeg, PEAuxPos),
        ord_intersect(PEOnlyNeg, PFPos, PEAuxNeg),
        ord_subtract(PEOnlyPos, PFNeg, PETVPos),
        ord_subtract(PEOnlyNeg, PFPos, PETVNeg),
        info(10, 'B: ~q P: ~q N: ~q PTV: ~q NTV: ~q',
             [PEBoth, PEAuxPos, PEAuxNeg, PETVPos, PETVNeg]),
        findall(P-Prime, ( ( member(P, PEBoth)
                           ; member(P, PEAuxPos)
                           ; member(P, PEAuxNeg)
                           ),
                           prime_predicate(P, Prime) ),
                 Map),
        logform_rename_free_predicates(F, Map, pn, F2),
        f_replace_predicates_by_tv(F2, PETVPos, false, F3),
        f_replace_predicates_by_tv(F3, PETVNeg, true, F4),
        f_signature(F, PNs, _),
        findall(P/N, (member(P, PEAuxPos), memberchk(P/N, PNs)), PNPos),
        findall(P/N, (member(P, PEAuxNeg), memberchk(P/N, PNs)), PNNeg),
        prime_aux_forms(PNNeg, FXP, p),
        prime_aux_forms(PNPos, FXN, n),
         logform_conjoin(FXP, FXN, FX),
        ( FX == true ->
          F5 = F4
        ; logform_disjoin(F4, ~FX, F5)
        ),
        simp_fol_fast(F5, F1).

f_prime_except(F, PPs, F1) :-
        canonicalize_predpols(PPs, PPs1),
        f_predpols(F, PPs2),
        ord_subtract(PPs2, PPs1, PPs3),
        f_prime(F, PPs3, F1).

f_replace_predicates_by_tv(F, Preds, TV, F1) :-
        logform_process_subforms(F, rptv_aux(Preds, TV), F1).

rptv_aux(Preds, TV, F, F1) :-
        logform_is_atom(F),
        functor(F, Pred, _),
        memberchk(Pred, Preds),
        !,
        F1 = TV.
rptv_aux(_, _, F, F).

prime_aux_forms(PNs, F, Mode) :-
        findall(F1, ( member(P/N, PNs),
                      prime_predicate(P, PPrime),
                      functor(A, P, N),
                      A =.. [_|T],
                      B =.. [PPrime|T],
                      ( Mode = p -> (F2 = (A->B))
                      ; Mode = n -> (F2 = (B->A))
                      ),
                      uclose(F2, F1) ),
                Fs),
        list_to_conjunction(Fs, F).

prime_predicate(P, PPrime) :-
        sub_atom(P, _, 1, 0, PDeco),
        ( PDeco = '0' -> true ; PDeco = '1' ),
        !,
        sub_atom(P, 0, _, 1, PPure),
        atomic_list_concat([PPure, '_prime_', PDeco], PPrime).
prime_predicate(P, PPrime) :-
        atom_concat(P, '_prime', PPrime).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%