use newer quip format, with bool-c taking terms

src/base-term/Proof.ml

@@ -6,29 +6,25 @@ type term = T.t
 type ty = Ty.t
 
 type lit =
-  | L_eq of term * term
+  | L_eq of bool * term * term
-  | L_neq of term * term
+  | L_a of bool * term
-  | L_a of term
-  | L_na of term
 
 let lit_not = function
-  | L_eq (a,b) -> L_neq(a,b)
+  | L_eq (sign,a,b) -> L_eq(not sign,a,b)
-  | L_neq (a,b) -> L_eq(a,b)
+  | L_a (sign,t) -> L_a (not sign,t)
-  | L_a t -> L_na t
-  | L_na t -> L_a t
 
-let pp_lit_with ~pp_t out = function
+let pp_lit_with ~pp_t out =
-  | L_eq (t,u) -> Fmt.fprintf out "(@[+@ (@[=@ %a@ %a@])@])" pp_t t pp_t u
+  let strsign = function true -> "+" | false -> "-" in
-  | L_neq (t,u) -> Fmt.fprintf out "(@[-@ (@[=@ %a@ %a@])@])" pp_t t pp_t u
+  function
-  | L_a t -> Fmt.fprintf out "(@[+@ %a@])" pp_t t
+  | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u
-  | L_na t -> Fmt.fprintf out "(@[-@ %a@])" pp_t t
+  | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t
 let pp_lit = pp_lit_with ~pp_t:Term.pp
 
-let lit_a t = L_a t
+let lit_a t = L_a (true,t)
-let lit_na t = L_na t
+let lit_na t = L_a (false,t)
-let lit_eq t u = L_eq (t,u)
+let lit_eq t u = L_eq (true,t,u)
-let lit_neq t u = L_neq (t,u)
+let lit_neq t u = L_eq (false,t,u)
-let lit_st (t,b) = if b then lit_a t else lit_na t
+let lit_mk b t = L_a (b,t)
 
 type clause = lit list
 
@@ -49,7 +45,7 @@ type t =
   | Bool_true_is_true
   | Bool_true_neq_false
   | Bool_eq of term * term (* equal by pure boolean reasoning *)
-  | Bool_c of bool_c_name * clause (* boolean tautology *)
+  | Bool_c of bool_c_name * term list (* boolean tautology *)
   | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
   | Ite_false of term
   | LRA of clause
@@ -135,15 +131,17 @@ let true_neq_false : t = Bool_true_neq_false
 let bool_eq a b : t = Bool_eq (a,b)
 let bool_c name c : t = Bool_c (name, c)
 
-let hres_l c l : t = Hres (c,l)
+let hres_l p l : t =
-let hres_iter c i : t = Hres (c, Iter.to_list i)
+  let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
+  if l=[] then p else Hres (p,l)
+let hres_iter c i : t = hres_l c (Iter.to_list i)
 
 let lra_l c : t = LRA c
 let lra c = LRA (Iter.to_rev_list c)
 
 let iter_lit ~f_t = function
-  | L_eq (a,b) | L_neq (a,b) -> f_t a; f_t b
+  | L_eq (_,a,b) -> f_t a; f_t b
-  | L_a t | L_na t -> f_t t
+  | L_a (_,t) -> f_t t
 
 let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
   match p with
@@ -168,7 +166,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
   | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us
   | Bool_true_is_true | Bool_true_neq_false -> ()
   | Bool_eq (t, u) -> f_t t; f_t u
-  | Bool_c (_,c) -> f_clause c
+  | Bool_c (_, ts) -> List.iter f_t ts
   | Ite_true t | Ite_false t -> f_t t
   | LRA c -> f_clause c
   | Composite { assumptions; steps } ->
@@ -295,6 +293,9 @@ module Quip = struct
   TODO: make sure we print terms properly
   *)
 
+  (* TODO: print into a buffer, without Format (should be faster) *)
+  (* TODO: print as C-sexp *)
+
   let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l
   let pp_a ppx out l = Fmt.(array ~sep:(return "@ ") ppx) out l
   let pp_cl ~pp_t out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l (pp_lit_with ~pp_t)) c
@@ -319,7 +320,8 @@ module Quip = struct
     | Bool_eq (a,b) ->
       Fmt.fprintf out "(@[bool-eq@ %a@ %a@])"
         pp_t a pp_t b
-    | Bool_c (name,c) -> Fmt.fprintf out "(@[bool-c %s@ %a@])" name pp_cl c
+    | Bool_c (name,ts) ->
+      Fmt.fprintf out "(@[bool-c %s@ %a@])" name (pp_l pp_t) ts
     | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t t
     | Assertion_c c ->
       Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c

src/base-term/Proof.mli

@@ -9,7 +9,7 @@ val isa_disj : ty -> term -> term -> t
 val cstor_inj : Cstor.t -> int -> term list -> term list -> t
 
 val bool_eq : term -> term -> t
-val bool_c : string -> lit list -> t
+val bool_c : string -> term list -> t
 val ite_true : term -> t
 val ite_false : term -> t
 

src/cc/Sidekick_cc.ml

@@ -661,7 +661,9 @@ module Make (A: CC_ARG)
         let proof =
           let lits =
             Iter.of_list lits
-            |> Iter.map (fun lit -> P.lit_not @@ P.lit_st (Lit.signed_term lit))
+            |> Iter.map (fun lit ->
+                let t, sign = Lit.signed_term lit in
+                P.lit_mk (not sign) t)
           in
           P.cc_lemma lits
         in
@@ -783,7 +785,9 @@ module Make (A: CC_ARG)
                let p =
                  A.P.cc_lemma
                    (Iter.of_list lits
-                    |> Iter.map (fun l -> A.P.(lit_st (Lit.signed_term l))))
+                    |> Iter.map (fun lit ->
+                        let t, sign = Lit.signed_term lit in
+                        A.P.(lit_mk sign t)))
                in
                lits, p
              ) in
@@ -855,7 +859,9 @@ module Make (A: CC_ARG)
     let proof =
       let lits =
         Iter.of_list lits
-        |> Iter.map (fun lit -> P.lit_st (Lit.signed_term lit))
+        |> Iter.map (fun lit ->
+            let t, sign = Lit.signed_term lit in
+            P.lit_mk sign t)
       in
       P.cc_lemma lits
     in

src/core/Sidekick_core.ml

@@ -172,7 +172,7 @@ module type PROOF = sig
   val pp_lit : lit Fmt.printer
   val lit_a : term -> lit
   val lit_na : term -> lit
-  val lit_st : term * bool -> lit
+  val lit_mk : bool -> term -> lit
   val lit_eq : term -> term -> lit
   val lit_neq : term -> term -> lit
   val lit_not : lit -> lit

src/lra/sidekick_arith_lra.ml

@@ -416,7 +416,9 @@ module Make(A : ARG) : S with module A = A = struct
 
   module Q_map = CCMap.Make(Q)
 
-  let plit_of_lit lit = A.S.P.lit_st (Lit.signed_term lit)
+  let plit_of_lit lit =
+    let t, sign = Lit.signed_term lit in
+    A.S.P.lit_mk sign t
 
   (* raise conflict from certificate *)
   let fail_with_cert si acts cert : 'a =

src/msat-solver/Sidekick_msat_solver.ml

@@ -576,7 +576,7 @@ module Make(A : ARG)
           let tr_atom a : P.lit =
             let sign = Sat_solver.Atom.sign a in
             let t = Lit.term (Sat_solver.Atom.formula a) in
-            P.lit_st (t,sign)
+            P.lit_mk sign t
           in
           let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l c in
 

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -37,7 +37,7 @@ module type ARG = sig
   val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t
 
   (** Basic boolean logic for a clause [|- c] *)
-  val proof_bool_c : string -> S.P.lit list -> S.P.t
+  val proof_bool_c : string -> term list -> S.P.t
 
   val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term
   (** Make a term from the given boolean view. *)
@@ -205,14 +205,8 @@ module Make(A : ARG) : S with module A = A = struct
       end
     | _ -> None
 
-  let[@inline] pr_lit lit = SI.P.(lit_st (Lit.signed_term lit))
   let[@inline] pr_def_refl _proxy t = SI.P.(refl t)
 
-  (* prove clause [l] by boolean lemma *)
-  let pr_bool_c name _proxy l : SI.P.t =
-    let cl = List.rev_map pr_lit l in
-    (A.proof_bool_c name cl)
-
   (* TODO: polarity? *)
   let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
     let rec get_lit_and_proof_ (t:T.t) : Lit.t * SI.P.t =
@@ -242,16 +236,24 @@ module Make(A : ARG) : S with module A = A = struct
       let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
 
       SI.define_const si ~const:t_proxy ~rhs:for_;
-      let add_clause ~elim c =
+      let add_clause c pr =
-        add_clause c (pr_bool_c (if elim then "eq-e" else "eq-i") t_proxy c)
+        add_clause c pr
       in
 
       (* proxy => a<=> b,
          ¬proxy => a xor b *)
-      add_clause ~elim:true [Lit.neg proxy; Lit.neg a; b];
+      add_clause [Lit.neg proxy; Lit.neg a; b]
-      add_clause ~elim:true [Lit.neg proxy; Lit.neg b; a];
+        (if is_xor then A.proof_bool_c "xor-e+" [t_proxy]
-      add_clause ~elim:false [proxy; a; b];
+         else A.proof_bool_c "eq-e" [t_proxy; t_a]);
-      add_clause ~elim:false [proxy; Lit.neg a; Lit.neg b];
+      add_clause [Lit.neg proxy; Lit.neg b; a]
+        (if is_xor then A.proof_bool_c "xor-e-" [t_proxy]
+         else A.proof_bool_c "eq-e" [t_proxy; t_b]);
+      add_clause [proxy; a; b]
+        (if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_a]
+         else A.proof_bool_c "eq-i+" [t_proxy]);
+      add_clause [proxy; Lit.neg a; Lit.neg b]
+        (if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_b]
+         else A.proof_bool_c "eq-i-" [t_proxy]);
       proxy, pr_def_refl t_proxy for_
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
@@ -266,11 +268,6 @@ module Make(A : ARG) : S with module A = A = struct
         lit
       in
 
-      let add_clause_by_def_ name proxy c : unit =
-        let pr = pr_bool_c name proxy c in
-        add_clause c pr
-      in
-
       match A.view_as_bool t with
       | B_bool b -> mk_lit (T.bool self.tst b), SI.P.refl t
       | B_opaque_bool t -> mk_lit t, SI.P.refl t
@@ -279,29 +276,41 @@ module Make(A : ARG) : S with module A = A = struct
         Lit.neg lit, pr
 
       | B_and l ->
-        let subs = l |> Iter.map get_lit |> Iter.to_list in
+        let t_subs = Iter.to_list l in
+        let subs = List.map get_lit t_subs in
         let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
         (* add clauses *)
-        List.iter
+        List.iter2
-          (fun u -> add_clause_by_def_ "and-e" t_proxy [Lit.neg proxy; u])
+          (fun t_u u ->
-          subs;
+             add_clause
-        add_clause_by_def_ "and-i" t_proxy (proxy :: List.map Lit.neg subs);
+               [Lit.neg proxy; u]
+               (A.proof_bool_c "and-i" [t_proxy; t_u]))
+          t_subs subs;
+        add_clause (proxy :: List.map Lit.neg subs)
+          (A.proof_bool_c "and-e" [t_proxy]);
         proxy, pr_def_refl t_proxy t
 
       | B_or l ->
-        let subs = l |> Iter.map get_lit |> Iter.to_list in
+        let t_subs = Iter.to_list l in
+        let subs = List.map get_lit t_subs in
         let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
         SI.define_const si ~const:t_proxy ~rhs:t;
         (* add clauses *)
-        List.iter (fun u -> add_clause_by_def_ "or-i" t_proxy [Lit.neg u; proxy]) subs;
+        List.iter2
-        add_clause_by_def_ "or-e" t_proxy (Lit.neg proxy :: subs);
+          (fun t_u u ->
+             add_clause [Lit.neg u; proxy]
+               (A.proof_bool_c "or-i" [t_proxy; t_u]))
+          t_subs subs;
+        add_clause (Lit.neg proxy :: subs)
+          (A.proof_bool_c "or-e" [t_proxy]);
         proxy, pr_def_refl t_proxy t
 
-      | B_imply (args, u) ->
+      | B_imply (t_args, t_u) ->
         (* transform into [¬args \/ u] on the fly *)
-        let args = args |> Iter.map get_lit |> Iter.map Lit.neg |> Iter.to_list in
+        let t_args = Iter.to_list t_args in
-        let u = get_lit u in
+        let args = List.map (fun t -> Lit.neg (get_lit t)) t_args in
+        let u = get_lit t_u in
         let subs = u :: args in
 
         (* now the or-encoding *)
@@ -309,8 +318,13 @@ module Make(A : ARG) : S with module A = A = struct
         SI.define_const si ~const:t_proxy ~rhs:t;
 
         (* add clauses *)
-        List.iter (fun u -> add_clause_by_def_ "imp-i" t_proxy [Lit.neg u; proxy]) subs;
+        List.iter2
-        add_clause_by_def_ "imp-e" t_proxy (Lit.neg proxy :: subs);
+          (fun t_u u ->
+             add_clause [Lit.neg u; proxy]
+               (A.proof_bool_c "imp-i" [t_proxy; t_u]))
+          (t_u::t_args) subs;
+        add_clause (Lit.neg proxy :: subs)
+          (A.proof_bool_c "imp-e" [t_proxy]);
         proxy, pr_def_refl t_proxy t
 
       | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t