refactor: make it compile again

src/base/Proof_stub.mli

@@ -7,6 +7,8 @@ include Sidekick_core.PROOF
   with type lit = Lit.t
    and type term = Term.t
 
+val create : unit -> t
+
 val lemma_bool_tauto : t -> Lit.t Iter.t -> unit
 val lemma_bool_c : t -> string -> term list -> unit
 val lemma_bool_equiv : t -> term -> term -> unit

src/core/Sidekick_core.ml

@@ -972,24 +972,6 @@ module type SOLVER = sig
     theory
   (** Helper to create a theory. *)
 
-  (* TODO: remove? hide? *)
-  (** {3 Boolean Atoms}
-
-      Atoms are the SAT solver's version of our boolean literals
-      (they may have a different representation). *)
-  module Atom : sig
-    type t
-
-    val equal : t -> t -> bool
-    val hash : t -> int
-
-    val pp : solver -> t CCFormat.printer
-    val formula : solver -> t -> lit
-
-    val neg : t -> t
-    val sign : t -> bool
-  end
-
   (** Models
 
       A model can be produced when the solver is found to be in a
@@ -1059,29 +1041,19 @@ module type SOLVER = sig
 
   val add_theory_l : t -> theory list -> unit
 
-  (* FIXME: do not handle atoms here, only lits *)
+  val mk_lit_t : t -> ?sign:bool -> term -> lit * dproof
+  (** [mk_lit_t _ ~sign t] returns [lit, pr]
+      where [lit] is a internal representation of [± t],
+      and [pr] is a proof of [|- lit = (± t)] *)
 
-  val mk_atom_lit : t -> lit -> Atom.t * dproof
+  val mk_lit_t' : t -> ?sign:bool -> term -> lit
-  (** [mk_atom_lit _ lit] returns [atom, pr]
+  (** Like {!mk_lit_t} but skips the proof *)
-      where [atom] is an internal atom for the solver,
-      and [pr] is a proof of [|- lit = atom] *)
 
-  val mk_atom_lit' : t -> lit -> Atom.t
+  val add_clause : t -> lit IArray.t -> dproof -> unit
-  (** Like {!mk_atom_t} but skips the proof *)
-
-  val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * dproof
-  (** [mk_atom_t _ ~sign t] returns [atom, pr]
-      where [atom] is an internal representation of [± t],
-      and [pr] is a proof of [|- atom = (± t)] *)
-
-  val mk_atom_t' : t -> ?sign:bool -> term -> Atom.t
-  (** Like {!mk_atom_t} but skips the proof *)
-
-  val add_clause : t -> Atom.t IArray.t -> dproof -> unit
   (** [add_clause solver cs] adds a boolean clause to the solver.
       Subsequent calls to {!solve} will need to satisfy this clause. *)
 
-  val add_clause_l : t -> Atom.t list -> dproof -> unit
+  val add_clause_l : t -> lit list -> dproof -> unit
   (** Add a clause to the solver, given as a list. *)
 
   val assert_terms : t -> term list -> unit
@@ -1096,16 +1068,18 @@ module type SOLVER = sig
   type res =
     | Sat of Model.t (** Satisfiable *)
     | Unsat of {
-        unsat_core: Atom.t list lazy_t; (** subset of assumptions responsible for unsat *)
+        unsat_core: unit -> lit Iter.t; (** subset of assumptions responsible for unsat *)
       } (** Unsatisfiable *)
     | Unknown of Unknown.t
     (** Unknown, obtained after a timeout, memory limit, etc. *)
 
+  (* TODO: API to push/pop/clear assumptions, in addition to ~assumptions param *)
+
   val solve :
     ?on_exit:(unit -> unit) list ->
     ?check:bool ->
     ?on_progress:(t -> unit) ->
-    assumptions:Atom.t list ->
+    assumptions:lit list ->
     t ->
     res
   (** [solve s] checks the satisfiability of the clauses added so far to [s].

src/main/main.ml

@@ -94,7 +94,12 @@ let check_limits () =
     raise Out_of_space
 
 let main_smt () : _ result =
+  let module Proof = Sidekick_smtlib.Proof in
   let tst = Term.create ~size:4_096 () in
+  (* FIXME: use this to enable/disable actual proof
+    let store_proof = !check || !p_proof || !proof_file <> "" in
+     *)
+  let proof = Proof.create() in
   let solver =
     let theories =
       (* TODO: probes, to load only required theories *)
@@ -104,8 +109,7 @@ let main_smt () : _ result =
         Process.th_lra;
       ]
     in
-    let store_proof = !check || !p_proof || !proof_file <> "" in
+    Process.Solver.create ~proof ~theories tst () ()
-    Process.Solver.create ~store_proof ~theories tst () ()
   in
   let proof_file = if !proof_file ="" then None else Some !proof_file in
   if !check then (
@@ -137,25 +141,31 @@ let main_smt () : _ result =
   res
 
 let main_cnf () : _ result =
+  let module Proof = Pure_sat_solver.Proof in
   let module S = Pure_sat_solver in
+  let proof = Proof.create() in
 
+  (* FIXME: this should go in the proof module *)
   let close_proof_, on_learnt, on_gc =
     if !proof_file ="" then (
       (fun() -> ()), None, None
     ) else (
       let oc = open_out !proof_file in
+      let pp_lits lits =
+        Array.iteri (fun i v ->
+            if i>0 then output_char oc ' ';
+            output_string oc (string_of_int v))
+          lits
+      in
       let pp_c solver c =
         let store = S.SAT.store solver in
-        Array.iteri (fun i a ->
+        let lits = S.SAT.Clause.lits_a store c in
-            if i>0 then output_char oc ' ';
+        pp_lits lits
-            let v = S.SAT.Atom.formula store a in
-            output_string oc (string_of_int v))
-          c
       in
       let on_learnt solver c =
         pp_c solver c; output_string oc " 0\n";
       and on_gc solver c =
-        output_string oc "d "; pp_c solver c; output_string oc " 0\n";
+        output_string oc "d "; pp_lits c; output_string oc " 0\n";
         ()
       and close () =
         flush oc;
@@ -168,8 +178,8 @@ let main_cnf () : _ result =
   let n_atoms = ref 0 in
   let solver =
     S.SAT.create
-      ~on_new_atom:(fun _ _ -> incr n_atoms) ~size:`Big ()
+      ~size:`Big
-      ?on_learnt ?on_gc
+      ?on_learnt ?on_gc ~proof ()
   in
 
   S.Dimacs.parse_file solver !file >>= fun () ->

src/main/pure_sat_solver.ml

@@ -4,9 +4,9 @@
 module E = CCResult
 module SS = Sidekick_sat
 
-module Formula = struct
+module Lit = struct
   type t = int
-  let norm t = if t>0 then t, SS.Same_sign else -t, SS.Negated
+  let norm_sign t = if t>0 then t, true else -t, false
   let abs = abs
   let sign t = t>0
   let equal = CCInt.equal
@@ -17,7 +17,7 @@ end
 
 (* TODO: on the fly compression *)
 module Proof : sig
-  include Sidekick_sat.PROOF with type lit = Formula.t
+  include Sidekick_sat.PROOF with type lit = Lit.t
 
   val dummy : t
   val create : unit -> t
@@ -30,7 +30,7 @@ module Proof : sig
   val iter_events : t -> event Iter.t
 end = struct
   let bpf = Printf.bprintf
-  type lit = Formula.t
+  type lit = Lit.t
   type t =
     | Dummy
     | Inner of {
@@ -93,8 +93,8 @@ end = struct
 end
 
 module Arg = struct
-  module Formula = Formula
+  module Lit = Lit
-  type formula = Formula.t
+  type lit = Lit.t
   module Proof = Proof
   type proof = Proof.t
 end
@@ -107,16 +107,12 @@ module Dimacs = struct
   module T = Term
 
   let parse_file (solver:SAT.t) (file:string) : (unit, string) result =
-    let get_lit i : SAT.atom = SAT.make_atom solver i in
-
     try
       CCIO.with_in file
         (fun ic ->
            let p = BL.Dimacs_parser.create ic in
            BL.Dimacs_parser.iter p
-             (fun c ->
+             (fun c -> SAT.add_input_clause solver c);
-                let atoms = List.rev_map get_lit c in
-                SAT.add_input_clause solver atoms);
            Ok ())
     with e ->
       E.of_exn_trace e

src/sat/Sidekick_sat.ml

@@ -19,12 +19,7 @@ type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
 module type ACTS = Solver_intf.ACTS
 type ('lit, 'proof) acts = ('lit, 'proof) Solver_intf.acts
 
-type negated = Solver_intf.negated = Negated | Same_sign
+type negated = bool
-
-(** Print {!negated} values *)
-let pp_negated out = function
-  | Negated -> Format.fprintf out "negated"
-  | Same_sign -> Format.fprintf out "same-sign"
 
 (** Print {!lbool} values *)
 let pp_lbool out = function

src/sat/Solver.ml

@@ -467,7 +467,7 @@ module Make(Plugin : PLUGIN)
 
     (* create new variable *)
     let alloc_var (self:t) ?default_pol (lit:lit) : var * Solver_intf.negated =
-      let lit, negated = Lit.norm lit in
+      let lit, negated = Lit.norm_sign lit in
       try Lit_tbl.find self.v_of_lit lit, negated
       with Not_found ->
         let v = alloc_var_uncached_ ?default_pol self lit in
@@ -480,16 +480,14 @@ module Make(Plugin : PLUGIN)
       ()
 
     let atom_of_var_ v negated : atom =
-      match negated with
+      if negated then Atom.na v else Atom.pa v
-      | Solver_intf.Same_sign -> Atom.pa v
-      | Solver_intf.Negated -> Atom.na v
 
     let alloc_atom (self:t) ?default_pol lit : atom =
       let var, negated = alloc_var self ?default_pol lit in
       atom_of_var_ var negated
 
     let find_atom (self:t) lit : atom option =
-      let lit, negated = Lit.norm lit in
+      let lit, negated = Lit.norm_sign lit in
       match Lit_tbl.find self.v_of_lit lit with
       | v -> Some (atom_of_var_ v negated)
       | exception Not_found -> None
@@ -1844,6 +1842,8 @@ module Make(Plugin : PLUGIN)
   let[@inline] store st = st.store
   let[@inline] proof st = st.proof
 
+  let[@inline] add_lit self ?default_pol lit =
+    ignore (make_atom_ self lit ?default_pol : atom)
   let[@inline] set_default_pol (self:t) (lit:lit) (pol:bool) : unit =
     let a = make_atom_ self lit ~default_pol:pol in
     Var.set_default_pol self.store (Atom.var a) pol

src/sat/Solver_intf.ml

@@ -53,11 +53,9 @@ type ('lit, 'clause) unsat_state =
                        and type clause = 'clause)
 (** The type of values returned when the solver reaches an UNSAT state. *)
 
-type negated =
+type negated = bool
-  | Negated     (** changed sign *)
-  | Same_sign   (** kept sign *)
 (** This type is used during the normalisation of lits.
-    See {!val:Expr_intf.S.norm} for more details. *)
+    [true] means the literal stayed the same, [false] that its sign was flipped. *)
 
 (** The type of reasons for propagations of a lit [f]. *)
 type ('lit, 'proof) reason =
@@ -147,11 +145,11 @@ module type LIT = sig
   val neg : t -> t
   (** Formula negation *)
 
-  val norm : t -> t * negated
+  val norm_sign : t -> t * negated
   (** Returns a 'normalized' form of the lit, possibly negated
-      (in which case return [Negated]).
+      (in which case return [false]).
       [norm] must be so that [a] and [neg a] normalise to the same lit,
-      but one returns [Negated] and the other [Same_sign]. *)
+      but one returns [false] and the other [true]. *)
 end
 
 module type PROOF = Sidekick_core.SAT_PROOF
@@ -319,6 +317,10 @@ module type S = sig
         The assumptions are just used for this call to [solve], they are
         not saved in the solver's state. *)
 
+  val add_lit : t -> ?default_pol:bool -> lit -> unit
+  (** Ensure the SAT solver handles this particular literal, ie add
+      a boolean variable for it if it's not already there. *)
+
   val set_default_pol : t -> lit -> bool -> unit
   (** Set default polarity for the given boolean variable.
       Sign of the literal is ignored. *)

src/smt-solver/Sidekick_smt_solver.ml

@@ -201,12 +201,6 @@ module Make(A : ARG)
 
     type solver = t
 
-    module Formula = struct
-      include Lit
-      let norm lit =
-        let lit', sign = Lit.norm_sign lit in
-        lit', if sign then Sidekick_sat.Same_sign else Sidekick_sat.Negated
-    end
     module Eq_class = CC.N
     module Expl = CC.Expl
     module Proof = P
@@ -519,12 +513,6 @@ module Make(A : ARG)
   }
   type solver = t
 
-  module Atom = struct
-    include Sat_solver.Atom
-    let pp self out a = pp (Sat_solver.store self.solver) out a
-    let formula self a = formula (Sat_solver.store self.solver) a
-  end
-
   module type THEORY = sig
     type t
     val name : string
@@ -589,12 +577,6 @@ module Make(A : ARG)
   let[@inline] tst self = Solver_internal.tst self.si
   let[@inline] ty_st self = Solver_internal.ty_st self.si
 
-  let[@inline] mk_atom_lit_ self lit : Atom.t = Sat_solver.make_atom self.solver lit
-
-  let mk_atom_t_ self t : Atom.t =
-    let lit = Lit.atom (tst self) t in
-    mk_atom_lit_ self lit
-
   (* map boolean subterms to literals *)
   let add_bool_subterms_ (self:t) (t:Term.t) : unit =
     Term.iter_dag t
@@ -608,28 +590,24 @@ module Make(A : ARG)
       (fun sub ->
          Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp sub);
          (* ensure that SAT solver has a boolean atom for [sub] *)
-         let atom = mk_atom_t_ self sub in
+         let lit = Lit.atom self.si.tst sub in
+         Sat_solver.add_lit self.solver lit;
          (* also map [sub] to this atom in the congruence closure, for propagation *)
          let cc = cc self in
-         let store = Sat_solver.store self.solver in
+         CC.set_as_lit cc (CC.add_term cc sub) lit;
-         CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula store atom);
          ())
 
-  let rec mk_atom_lit self lit : Atom.t * dproof =
+  (* preprocess literals, making them ready for being added to the solver *)
-    let lit, proof = preprocess_lit_ self lit in
+  let rec preprocess_lit_ self lit : Lit.t * dproof =
-    add_bool_subterms_ self (Lit.term lit);
-    Sat_solver.make_atom self.solver lit, proof
-
-  and preprocess_lit_ self lit : Lit.t * dproof =
     Solver_internal.preprocess_lit_
       ~add_clause:(fun lits proof ->
           (* recursively add these sub-literals, so they're also properly processed *)
           Stat.incr self.si.count_preprocess_clause;
           let pr_l = ref [] in
-          let atoms =
+          let lits =
             List.map
               (fun lit ->
-                 let a, pr = mk_atom_lit self lit in
+                 let a, pr = preprocess_lit_ self lit in
                  (* FIXME                 if not (P.is_trivial_refl pr) then ( *)
                    pr_l := pr :: !pr_l;
                    (*                  ); *)
@@ -637,15 +615,22 @@ module Make(A : ARG)
               lits
           in
           let emit_proof p = List.iter (fun dp -> dp p) !pr_l; in
-          Sat_solver.add_clause self.solver atoms emit_proof)
+          Sat_solver.add_clause self.solver lits emit_proof)
       self.si lit
 
-  let[@inline] mk_atom_t self ?sign t : Atom.t * dproof =
+  (* FIXME: should we just add the proof instead? *)
-    let lit = Lit.atom (tst self) ?sign t in
+  let[@inline] preprocess_lit' self lit : Lit.t =
-    mk_atom_lit self lit
+    fst (preprocess_lit_ self lit)
 
-  let mk_atom_t' self ?sign t = mk_atom_t self ?sign t |> fst
+  (* FIXME: should we just assert the proof instead? or do we wait because
-  let mk_atom_lit' self lit = mk_atom_lit self lit |> fst
+     we're most likely in a subproof? *)
+  let rec mk_lit_t (self:t) ?sign (t:term) : lit * dproof =
+    let lit = Lit.atom ?sign self.si.tst t in
+    let lit, proof = preprocess_lit_ self lit in
+    add_bool_subterms_ self (Lit.term lit);
+    lit, proof
+
+  let[@inline] mk_lit_t' self ?sign lit = mk_lit_t self ?sign lit |> fst
 
   (** {2 Result} *)
 
@@ -686,7 +671,7 @@ module Make(A : ARG)
   type res =
     | Sat of Model.t
     | Unsat of {
-        unsat_core: Atom.t list lazy_t;
+        unsat_core: unit -> lit Iter.t;
       }
     | Unknown of Unknown.t
     (** Result of solving for the current set of clauses *)
@@ -696,14 +681,13 @@ module Make(A : ARG)
   let pp_stats out (self:t) : unit =
     Stat.pp_all out (Stat.all @@ stats self)
 
-  let add_clause (self:t) (c:Atom.t IArray.t) (proof:dproof) : unit =
+  let add_clause (self:t) (c:lit IArray.t) (proof:dproof) : unit =
     Stat.incr self.count_clause;
     Log.debugf 50 (fun k->
-        let store = Sat_solver.store self.solver in
         k "(@[solver.add-clause@ %a@])"
-          (Util.pp_iarray (Sat_solver.Atom.pp store)) c);
+          (Util.pp_iarray Lit.pp) c);
     let pb = Profile.begin_ "add-clause" in
-    Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof;
+    Sat_solver.add_clause_a self.solver (c:> lit array) proof;
     Profile.exit pb
 
   let add_clause_l self c p = add_clause self (IArray.of_list c) p
@@ -714,7 +698,7 @@ module Make(A : ARG)
       P.emit_input_clause p (Iter.of_list c)
     in
     (* FIXME: just emit proofs on the fly? *)
-    let c = CCList.map (mk_atom_lit' self) c in
+    let c = CCList.map (preprocess_lit' self) c in
     add_clause_l self c emit_proof
 
   let assert_term self t = assert_terms self [t]
@@ -788,7 +772,7 @@ module Make(A : ARG)
       do_on_exit ();
       Sat m
     | Sat_solver.Unsat (module UNSAT) ->
-      let unsat_core = lazy (UNSAT.unsat_assumptions ()) in
+      let unsat_core () = UNSAT.unsat_assumptions () in
       do_on_exit ();
       Unsat {unsat_core}
 

src/smtlib/Process.ml

@@ -216,8 +216,6 @@ let process_stmt
     (* TODO: more? *)
   in
 
-  let mk_lit ?sign t = Solver.Lit.atom (Solver.tst solver) ?sign t in
-
   begin match stmt with
     | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA"|"QF_DT"|"QF_UFDT") ->
       E.return ()
@@ -235,9 +233,7 @@ let process_stmt
       (* FIXME: how to map [l] to [assumptions] in proof? *)
       let assumptions =
         List.map
-          (fun (sign,t) ->
+          (fun (sign,t) -> Solver.mk_lit_t' solver ~sign t)
-             let a, _pr = Solver.mk_atom_t solver ~sign t in
-             a)
           l
       in
       solve
@@ -257,9 +253,9 @@ let process_stmt
       if pp_cnf then (
         Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
       );
-      let atom, pr_atom = Solver.mk_atom_t solver t in
+      let lit = Solver.mk_lit_t' solver t in
-      Solver.add_clause solver (IArray.singleton atom)
+      Solver.add_clause solver (IArray.singleton lit)
-        (fun p -> Solver.P.emit_input_clause p (Iter.singleton (mk_lit t)));
+        (fun p -> Solver.P.emit_input_clause p (Iter.singleton lit));
       E.return()
 
     | Statement.Stmt_assert_clause c_ts ->
@@ -269,20 +265,20 @@ let process_stmt
       let pr_l = ref [] in
       let c =
         List.map
-          (fun lit ->
+          (fun t ->
-             let a, pr = Solver.mk_atom_t solver lit in
+             let lit, pr = Solver.mk_lit_t solver t in
              pr_l := pr :: !pr_l;
-             a)
+             lit)
           c_ts in
 
       (* proof of assert-input + preprocessing *)
       let emit_proof p =
         let module P = Solver.P in
         P.begin_subproof p;
-        P.emit_input_clause p (Iter.of_list c_ts |> Iter.map mk_lit);
+        let tst = Solver.tst solver in
+        P.emit_input_clause p (Iter.of_list c_ts |> Iter.map (Lit.atom tst));
         List.iter (fun dp -> dp p) !pr_l;
-        P.emit_redundant_clause p
+        P.emit_redundant_clause p (Iter.of_list c);
-          (Iter.of_list c |> Iter.map (Solver.Atom.formula solver));
         P.end_subproof p;
       in
 

src/smtlib/Process.mli

@@ -7,6 +7,7 @@ module Solver
                             and type T.Term.store = Term.store
                             and type T.Ty.t = Ty.t
                             and type T.Ty.store = Ty.store
+                            and type proof = Proof_stub.t
 
 val th_bool : Solver.theory
 val th_data : Solver.theory

src/smtlib/Sidekick_smtlib.ml

@@ -8,6 +8,7 @@ module Process = Process
 module Solver = Process.Solver
 module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
+module Proof = Sidekick_base.Proof_stub
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Sidekick_smtlib.mli

@@ -10,6 +10,7 @@ module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
 module Process = Process
 module Solver = Process.Solver
+module Proof = Sidekick_base.Proof_stub (* FIXME: actual DRUP(T) proof *)
 
 val parse : Term.store -> string -> Stmt.t list or_error