refactor: Term.abs takes store again, so abs false can be false,true

examples/sudoku/sudoku_solve.ml

@@ -174,7 +174,7 @@ end = struct
     @@ Const.make (Cell_is { x; y; value }) ops ~ty:(Term.bool tst)
 
   let mk_cell_lit ?sign tst x y value : Lit.t =
-    Lit.atom ?sign @@ mk_cell tst x y value
+    Lit.atom ?sign tst @@ mk_cell tst x y value
 
   module Theory : sig
     type t

src/core-logic/t_builtins.ml

@@ -101,11 +101,12 @@ let is_eq t =
   | E_const { c_view = C_eq; _ } -> true
   | _ -> false
 
-let rec abs t =
+let rec abs tst t =
   match view t with
   | E_app ({ view = E_const { c_view = C_not; _ }; _ }, u) ->
-    let sign, v = abs u in
+    let sign, v = abs tst u in
     Stdlib.not sign, v
+  | E_const { c_view = C_false; _ } -> false, true_ tst
   | _ -> true, t
 
 let as_bool_val t =

src/core-logic/t_builtins.mli

@@ -24,12 +24,12 @@ val ite : store -> t -> t -> t -> t
 val is_eq : t -> bool
 val is_bool : t -> bool
 
-val abs : t -> bool * t
+val abs : store -> t -> bool * t
 (** [abs t] returns an "absolute value" for the term, along with the
-      sign of [t].
+    sign of [t].
 
-      The idea is that we want to turn [not a] into [(false, a)],
-      or [(a != b)] into [(false, a=b)]. For terms without a negation this
-      should return [(true, t)]. *)
+    The idea is that we want to turn [not a] into [(false, a)],
+    or [(a != b)] into [(false, a=b)]. For terms without a negation this
+    should return [(true, t)]. *)
 
 val as_bool_val : t -> bool option

src/core/lit.ml

@@ -11,17 +11,23 @@ let[@inline] term (l : t) : term = l.lit_term
 let[@inline] signed_term l = term l, sign l
 let[@inline] make_ ~sign t : t = { lit_sign = sign; lit_term = t }
 
-let atom ?(sign = true) (t : term) : t =
-  let sign', t = T_builtins.abs t in
+let atom ?(sign = true) tst (t : term) : t =
+  let sign', t = T_builtins.abs tst t in
   let sign = sign = sign' in
   make_ ~sign t
 
 let make_eq ?sign store t u : t =
   let p = T_builtins.eq store t u in
-  atom ?sign p
+  atom ?sign store p
 
 let equal a b = a.lit_sign = b.lit_sign && T.equal a.lit_term b.lit_term
 
+let compare a b =
+  if a.lit_sign = b.lit_sign then
+    T.compare a.lit_term b.lit_term
+  else
+    CCOrd.bool a.lit_sign b.lit_sign
+
 let hash a =
   let sign = a.lit_sign in
   CCHash.combine3 2 (CCHash.bool sign) (T.hash a.lit_term)

src/core/lit.mli

@@ -14,7 +14,7 @@ type term = Term.t
 type t
 (** A literal *)
 
-include Sidekick_sigs.EQ_HASH_PRINT with type t := t
+include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
 
 val term : t -> term
 (** Get the (positive) term *)
@@ -31,7 +31,7 @@ val abs : t -> t
 val signed_term : t -> term * bool
 (** Return the atom and the sign *)
 
-val atom : ?sign:bool -> term -> t
+val atom : ?sign:bool -> Term.store -> term -> t
 (** [atom store t] makes a literal out of a term, possibly normalizing
       its sign in the process.
       @param sign if provided, and [sign=false], negate the resulting lit. *)

src/main/pure_sat_solver.ml

@@ -181,7 +181,7 @@ end = struct
 
   let make tst i : Lit.t =
     let t = Term.const tst @@ Const.make (I (abs i)) ops ~ty:(Term.bool tst) in
-    Lit.atom ~sign:(i > 0) t
+    Lit.atom ~sign:(i > 0) tst t
 end
 
 module SAT = Sidekick_sat

src/smt/solver.ml

@@ -112,7 +112,7 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
   (let tst = Solver_internal.tst self.si in
    let t_true = Term.true_ tst in
    Sat_solver.add_clause self.solver
-     [ Lit.atom t_true ]
+     [ Lit.atom tst t_true ]
      (P.add_step self.proof @@ fun () -> Rule_.lemma_true t_true));
   self
 
@@ -130,7 +130,7 @@ let preprocess_clause_ (self : t) (c : lit array) (pr : step_id) :
   Solver_internal.preprocess_clause_array self.si c pr
 
 let mk_lit_t (self : t) ?sign (t : term) : lit =
-  let lit = Lit.atom ?sign t in
+  let lit = Lit.atom ?sign (tst self) t in
   let lit, _ = Solver_internal.simplify_and_preproc_lit self.si lit in
   lit
 
@@ -175,7 +175,7 @@ let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
 let add_clause_l self c p = add_clause self (CCArray.of_list c) p
 
 let assert_terms self c =
-  let c = CCList.map Lit.atom c in
+  let c = CCList.map (Lit.atom (tst self)) c in
   let pr_c = P.add_step self.proof @@ fun () -> Proof_sat.sat_input_clause c in
   add_clause_l self c pr_c
 

src/smt/solver_internal.ml

@@ -127,7 +127,7 @@ let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : unit =
 let preprocess_term_ (self : t) (t0 : term) : unit =
   let module A = struct
     let proof = self.proof
-    let mk_lit ?sign t : Lit.t = Lit.atom ?sign t
+    let mk_lit ?sign t : Lit.t = Lit.atom ?sign self.tst t
     let add_lit ?default_pol lit : unit = delayed_add_lit self ?default_pol lit
     let add_clause c pr : unit = delayed_add_clause self ~keep:true c pr
   end in
@@ -151,7 +151,7 @@ let preprocess_term_ (self : t) (t0 : term) : unit =
               t);
 
         (* make a literal *)
-        let lit = Lit.atom t in
+        let lit = Lit.atom self.tst t in
         (* ensure that SAT solver has a boolean atom for [u] *)
         delayed_add_lit self lit;
 
@@ -179,7 +179,7 @@ let simplify_and_preproc_lit (self : t) (lit : Lit.t) : Lit.t * step_id option =
       u, Some pr_t_u
   in
   preprocess_term_ self u;
-  Lit.atom ~sign u, pr
+  Lit.atom ~sign self.tst u, pr
 
 let push_decision (self : t) (acts : theory_actions) (lit : lit) : unit =
   let (module A) = acts in
@@ -275,13 +275,13 @@ let[@inline] add_clause_permanent self _acts c (proof : step_id) : unit =
   let c, proof = preprocess_clause self c proof in
   delayed_add_clause self ~keep:true c proof
 
-let[@inline] mk_lit _ ?sign t : lit = Lit.atom ?sign t
+let[@inline] mk_lit self ?sign t : lit = Lit.atom ?sign self.tst t
 
 let[@inline] add_lit self _acts ?default_pol lit =
   delayed_add_lit self ?default_pol lit
 
 let add_lit_t self _acts ?sign t =
-  let lit = Lit.atom ?sign t in
+  let lit = Lit.atom ?sign self.tst t in
   let lit, _ = simplify_and_preproc_lit self lit in
   delayed_add_lit self lit
 
@@ -506,7 +506,7 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
           semantic
           |> List.rev_map (fun (sign, t, u) ->
                  let eqn = Term.eq self.tst t u in
-                 let lit = Lit.atom ~sign:(not sign) eqn in
+                 let lit = Lit.atom ~sign:(not sign) self.tst eqn in
                  (* make sure to consider the new lit *)
                  add_lit self acts lit;
                  lit)

src/smtlib/Process.ml

@@ -305,7 +305,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
     (* proof of assert-input + preprocessing *)
     let pr =
       add_step @@ fun () ->
-      let lits = List.map Lit.atom c_ts in
+      let lits = List.map (Solver.mk_lit_t solver) c_ts in
       Proof_sat.sat_input_clause lits
     in
 

src/th-bool-dyn/Sidekick_th_bool_dyn.ml

@@ -61,7 +61,7 @@ end = struct
       add_step_ @@ mk_step_
       @@ fun () ->
       Proof_core.lemma_rw_clause c0 ~using
-        ~res:[ Lit.atom (A.mk_bool tst (B_eq (a, b))) ]
+        ~res:[ Lit.atom tst (A.mk_bool tst (B_eq (a, b))) ]
     in
 
     let[@inline] ret u =
@@ -227,7 +227,7 @@ end = struct
         (mk_step_ @@ fun () -> Proof_core.lemma_true (Lit.term lit))
     | _ when expanded self lit -> () (* already done *)
     | B_and (a, b) ->
-      let subs = List.map Lit.atom [ a; b ] in
+      let subs = List.map (Lit.atom self.tst) [ a; b ] in
 
       if Lit.sign lit then
         (* assert [(and …t_i) => t_i] *)
@@ -245,7 +245,7 @@ end = struct
           (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ])
       )
     | B_or (a, b) ->
-      let subs = List.map Lit.atom [ a; b ] in
+      let subs = List.map (Lit.atom self.tst) [ a; b ] in
 
       if not @@ Lit.sign lit then
         (* propagate [¬sub_i \/ lit] *)
@@ -262,8 +262,8 @@ end = struct
         add_axiom c (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ])
       )
     | B_imply (a, b) ->
-      let a = Lit.atom a in
-      let b = Lit.atom b in
+      let a = Lit.atom self.tst a in
+      let b = Lit.atom self.tst b in
       if Lit.sign lit then (
         (* axiom [lit => a => b] *)
         let c = [ Lit.neg lit; Lit.neg a; b ] in
@@ -286,7 +286,7 @@ end = struct
       (* boolean ite:
          just add [a => (ite a b c <=> b)]
          and [¬a => (ite a b c <=> c)] *)
-      let lit_a = Lit.atom a in
+      let lit_a = Lit.atom self.tst a in
       add_axiom
         [ Lit.neg lit_a; Lit.make_eq self.tst t b ]
         (mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
@@ -294,20 +294,20 @@ end = struct
         [ Lit.neg lit; lit_a; Lit.make_eq self.tst t c ]
         (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
     | B_equiv (a, b) ->
-      let a = Lit.atom a in
-      let b = Lit.atom b in
+      let a = Lit.atom self.tst a in
+      let b = Lit.atom self.tst b in
       equiv_ ~is_xor:false a b
     | B_eq (a, b) when T.is_bool a ->
-      let a = Lit.atom a in
-      let b = Lit.atom b in
+      let a = Lit.atom self.tst a in
+      let b = Lit.atom self.tst b in
       equiv_ ~is_xor:false a b
     | B_xor (a, b) ->
-      let a = Lit.atom a in
-      let b = Lit.atom b in
+      let a = Lit.atom self.tst a in
+      let b = Lit.atom self.tst b in
       equiv_ ~is_xor:true a b
     | B_neq (a, b) when T.is_bool a ->
-      let a = Lit.atom a in
-      let b = Lit.atom b in
+      let a = Lit.atom self.tst a in
+      let b = Lit.atom self.tst b in
       equiv_ ~is_xor:true a b
     | B_eq _ | B_neq _ -> ()
 

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -51,7 +51,7 @@ end = struct
       add_step_ @@ mk_step_
       @@ fun () ->
       Proof_core.lemma_rw_clause c0 ~using
-        ~res:[ Lit.atom (A.mk_bool tst (B_eq (a, b))) ]
+        ~res:[ Lit.atom tst (A.mk_bool tst (B_eq (a, b))) ]
     in
 
     let[@inline] ret u =

src/th-data/Sidekick_th_data.ml

@@ -354,7 +354,7 @@ end = struct
           let pr_isa =
             Proof_trace.add_step self.proof @@ fun () ->
             Proof_rules.lemma_isa_split t
-              [ Lit.atom (A.mk_is_a self.tst cstor t) ]
+              [ Lit.atom self.tst (A.mk_is_a self.tst cstor t) ]
           and pr_eq_sel =
             Proof_trace.add_step self.proof @@ fun () ->
             Proof_rules.lemma_select_cstor ~cstor_t:u t

src/th-lra/sidekick_th_lra.ml

@@ -335,7 +335,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       | _ -> assert false)
     | LRA_pred ((Eq | Neq), t1, t2) ->
       (* equality: just punt to [t1 = t2 <=> (t1 <= t2 /\ t1 >= t2)] *)
-      let _, t = Term.abs t in
+      let _, t = Term.abs self.tst t in
       if not (Term.Tbl.mem self.encoded_eqs t) then (
         let u1 = A.mk_lra tst (LRA_pred (Leq, t1, t2)) in
         let u2 = A.mk_lra tst (LRA_pred (Geq, t1, t2)) in
@@ -400,10 +400,10 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       (Term.t * Proof_step.id Iter.t) option =
     let proof_eq t u =
       Proof_trace.add_step self.proof @@ fun () ->
-      A.lemma_lra [ Lit.atom (Term.eq self.tst t u) ]
+      A.lemma_lra [ Lit.atom self.tst (Term.eq self.tst t u) ]
     in
     let proof_bool t ~sign:b =
-      let lit = Lit.atom ~sign:b t in
+      let lit = Lit.atom ~sign:b self.tst t in
       Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
     in
 
@@ -526,7 +526,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     if LE_.Comb.is_empty le_comb then (
       if A.Q.(le_const <> zero) then (
         (* [c=0] when [c] is not 0 *)
-        let lit = Lit.atom ~sign:false @@ Term.eq self.tst t1 t2 in
+        let lit = Lit.atom ~sign:false self.tst @@ Term.eq self.tst t1 t2 in
         let pr =
           Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
         in