refactor: require state in Lit.atom, and in Term.abs

allows abs(false)=true

src/smt/Lit.ml

@@ -14,8 +14,8 @@ let[@inline] abs t: t = {t with lit_sign=true}
 
 let make ~sign t = {lit_sign=sign; lit_term=t}
 
-let atom ?(sign=true) (t:term) : t =
+let atom tst ?(sign=true) (t:term) : t =
-  let t, sign' = Term.abs t in
+  let t, sign' = Term.abs tst t in
   let sign = if not sign' then not sign else sign in
   make ~sign t
 

src/smt/Lit.mli

@@ -12,7 +12,7 @@ val abs : t -> t
 val sign : t -> bool
 val term : t -> term
 val as_atom : t -> term * bool
-val atom : ?sign:bool -> term -> t
+val atom : Term.state -> ?sign:bool -> term -> t
 val hash : t -> int
 val compare : t -> t -> int
 val equal : t -> t -> bool

src/smt/Solver.ml

@@ -35,7 +35,7 @@ let[@inline] tst self = Theory_combine.tst (th_combine self)
 
 let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
 let[@inline] mk_atom_t self ?sign t : Atom.t =
-  let lit = Lit.atom ?sign t in
+  let lit = Lit.atom (tst self)  ?sign t in
   mk_atom_lit self lit
 
 let create ?size ?(config=Config.empty) ?store_proof ~theories () : t =
@@ -50,17 +50,15 @@ let create ?size ?(config=Config.empty) ?store_proof ~theories () : t =
   (* assert [true] and [not false] *)
   let tst = tst self in
   Sat_solver.assume self.solver [
-    [Lit.atom @@ Term.true_ tst];
+    [Lit.atom tst @@ Term.true_ tst];
-    [Lit.atom ~sign:false @@ Term.false_ tst];
   ] Proof_default;
   self
 
 (** {2 Sat Solver} *)
 
 let print_progress (st:t) : unit =
-  Printf.printf "\r[%.2f] expanded %d | clauses %d | lemmas %d%!"
+  Printf.printf "\r[%.2f] clauses %d | lemmas %d%!"
     (get_time())
-    st.stat.Stat.num_cst_expanded
     st.stat.Stat.num_clause_push
     st.stat.Stat.num_clause_tautology
 
@@ -160,19 +158,13 @@ let pp_term_graph _out (_:t) =
 let pp_stats out (s:t) : unit =
   Format.fprintf out
     "(@[<hv1>stats@ \
-     :num_expanded %d@ \
-     :num_uty_expanded %d@ \
      :num_clause_push %d@ \
      :num_clause_tautology %d@ \
      :num_propagations %d@ \
-     :num_unif %d@ \
      @])"
-    s.stat.Stat.num_cst_expanded
-    s.stat.Stat.num_uty_expanded
     s.stat.Stat.num_clause_push
     s.stat.Stat.num_clause_tautology
     s.stat.Stat.num_propagations
-    s.stat.Stat.num_unif
 
 let do_on_exit ~on_exit =
   List.iter (fun f->f()) on_exit;

src/smt/Stat.ml

@@ -1,18 +1,12 @@
 
 type t = {
-  mutable num_cst_expanded  : int;
-  mutable num_uty_expanded  : int;
   mutable num_clause_push  : int;
   mutable num_clause_tautology  : int;
   mutable num_propagations  : int;
-  mutable num_unif  : int;
 }
 
 let create () : t = {
-  num_cst_expanded = 0;
-  num_uty_expanded = 0;
   num_clause_push = 0;
   num_clause_tautology = 0;
   num_propagations = 0;
-  num_unif = 0;
 }

src/smt/Term.ml

@@ -72,9 +72,10 @@ let[@inline] eq st a b = make st (Term_cell.eq a b)
 let and_eager st a b = if_ st a b (false_ st)
 
 (* might need to tranfer the negation from [t] to [sign] *)
-let abs t : t * bool = match view t with
+let abs tst t : t * bool = match view t with
+  | Bool false -> true_ tst, false
   | App_cst ({cst_view=Cst_def def; _}, args) ->
-    def.abs ~self:t args
+    def.abs ~self:t args (* TODO: pass state *)
   | _ -> t, true
 
 let[@inline] is_true t = match view t with Bool true -> true | _ -> false

src/smt/Term.mli

@@ -35,7 +35,7 @@ val if_: state -> t -> t -> t -> t
 val and_eager : state -> t -> t -> t (* evaluate left argument first *)
 
 (** Obtain unsigned version of [t], + the sign as a boolean *)
-val abs : t -> t * bool
+val abs : state -> t -> t * bool
 
 val to_seq : t -> t Sequence.t
 

src/smtlib/Process.ml

@@ -316,7 +316,7 @@ let mk_iatom =
   fun tst i ->
     let c = Util.Int_tbl.get_or_add tbl ~k:(abs i) 
         ~f:(fun i -> Cst.mk_undef_const (ID.makef "a_%d" i) Ty.prop) in
-    Lit.atom ~sign:(i>0) @@ Term.const tst c
+    Lit.atom tst ~sign:(i>0) @@ Term.const tst c
 
 (* process a single statement *)
 let process_stmt
@@ -370,7 +370,7 @@ let process_stmt
       if pp_cnf then (
         Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
       );
-      let atom = Lit.atom t in
+      let atom = Lit.atom tst t in
       CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
       Solver.assume solver (IArray.singleton atom);
       E.return()

src/th-bool/Th_dyn_tseitin.ml

@@ -18,7 +18,7 @@ module Make(Term : ARG) = struct
 
   module Lit = struct
     include Sidekick_smt.Lit
-    let eq tst a b = atom ~sign:true (Term.make tst (B_eq (a,b)))
+    let eq tst a b = atom tst ~sign:true @@ Term.make tst (B_eq (a,b))
     let neq tst a b = neg @@ eq tst a b
   end
 
@@ -60,13 +60,13 @@ module Make(Term : ARG) = struct
         (* propagate [lit => subs_i] *)
         IArray.iter
           (fun sub ->
-             let sublit = Lit.atom sub in
+             let sublit = Lit.atom self.tst sub in
              A.propagate sublit [lit])
           subs
       ) else if final && not @@ expanded () then (
         (* axiom [¬lit => ∨_i ¬ subs_i] *)
         let subs = IArray.to_list subs in
-        let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
+        let c = Lit.neg lit :: List.map (Lit.atom self.tst ~sign:false) subs in
         add_axiom c
       )
     | B_or subs ->
@@ -74,28 +74,28 @@ module Make(Term : ARG) = struct
         (* propagate [¬lit => ¬subs_i] *)
         IArray.iter
           (fun sub ->
-             let sublit = Lit.atom ~sign:false sub in
+             let sublit = Lit.atom self.tst ~sign:false sub in
              A.add_local_axiom [Lit.neg lit; sublit])
           subs
       ) else if final && not @@ expanded () then (
         (* axiom [lit => ∨_i subs_i] *)
         let subs = IArray.to_list subs in
-        let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
+        let c = Lit.neg lit :: List.map (Lit.atom self.tst ~sign:true) subs in
         add_axiom c
       )
     | B_imply (guard,concl) ->
       if Lit.sign lit && final && not @@ expanded () then (
         (* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
         let guard = IArray.to_list guard in
-        let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
+        let c = Lit.atom self.tst concl :: Lit.neg lit :: List.map (Lit.atom self.tst ~sign:false) guard in
         add_axiom c
       ) else if not @@ Lit.sign lit then (
         (* propagate [¬lit => ¬concl] *)
-        A.propagate (Lit.atom ~sign:false concl) [lit];
+        A.propagate (Lit.atom self.tst ~sign:false concl) [lit];
         (* propagate [¬lit => ∧_i guard_i] *)
         IArray.iter
           (fun sub ->
-             let sublit = Lit.atom ~sign:true sub in
+             let sublit = Lit.atom self.tst ~sign:true sub in
              A.propagate sublit [lit])
           guard
       )