From 36204c5e5efa7d8329781e2826fcd917d9bc3619 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 30 Jul 2022 23:04:49 -0400 Subject: [PATCH] refactor some more --- src/algos/lra/dune | 7 - src/algos/lra/sidekick_arith_lra.ml | 819 ------------------ src/core-logic/t_builtins.ml | 6 + src/core-logic/t_builtins.mli | 2 + src/sigs/smt/Sidekick_sigs_smt.ml | 606 ------------- src/sigs/smt/dune | 8 - src/smt-solver/Sidekick_smt_solver.ml | 1156 ------------------------- src/smt-solver/dune | 6 - src/smt-solver/th_key.ml.bak | 145 ---- src/smt/Sidekick_smt_solver.ml | 5 +- src/th-cstor/Sidekick_th_cstor.mli | 13 + 11 files changed, 25 insertions(+), 2748 deletions(-) delete mode 100644 src/algos/lra/dune delete mode 100644 src/algos/lra/sidekick_arith_lra.ml delete mode 100644 src/sigs/smt/Sidekick_sigs_smt.ml delete mode 100644 src/sigs/smt/dune delete mode 100644 src/smt-solver/Sidekick_smt_solver.ml delete mode 100644 src/smt-solver/dune delete mode 100644 src/smt-solver/th_key.ml.bak create mode 100644 src/th-cstor/Sidekick_th_cstor.mli diff --git a/src/algos/lra/dune b/src/algos/lra/dune deleted file mode 100644 index 3e1f839c..00000000 --- a/src/algos/lra/dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name sidekick_arith_lra) - (public_name sidekick.arith-lra) - (synopsis "Solver for LRA (real arithmetic)") - (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util) - (libraries containers sidekick.sigs.smt sidekick.arith sidekick.simplex - sidekick.cc.plugin)) diff --git a/src/algos/lra/sidekick_arith_lra.ml b/src/algos/lra/sidekick_arith_lra.ml deleted file mode 100644 index ee3b990a..00000000 --- a/src/algos/lra/sidekick_arith_lra.ml +++ /dev/null @@ -1,819 +0,0 @@ -(** Linear Rational Arithmetic *) - -(* Reference: - http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LRA *) - -open Sidekick_sigs_smt -module Predicate = Sidekick_simplex.Predicate -module Linear_expr = Sidekick_simplex.Linear_expr -module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf - -module type INT = Sidekick_arith.INT -module type RATIONAL = Sidekick_arith.RATIONAL - -module S_op = Sidekick_simplex.Op - -type pred = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq -type op = Linear_expr_intf.op = Plus | Minus - -type ('num, 'a) lra_view = - | LRA_pred of pred * 'a * 'a - | LRA_op of op * 'a * 'a - | LRA_mult of 'num * 'a - | LRA_const of 'num - | LRA_other of 'a - -let map_view f (l : _ lra_view) : _ lra_view = - match l with - | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b) - | LRA_op (p, a, b) -> LRA_op (p, f a, f b) - | LRA_mult (n, a) -> LRA_mult (n, f a) - | LRA_const q -> LRA_const q - | LRA_other x -> LRA_other (f x) - -module type ARG = sig - module S : SOLVER - module Z : INT - module Q : RATIONAL with type bigint = Z.t - - type term = S.T.Term.t - type ty = S.T.Ty.t - - val view_as_lra : term -> (Q.t, term) lra_view - (** Project the term into the theory view *) - - val mk_bool : S.T.Term.store -> bool -> term - - val mk_lra : S.T.Term.store -> (Q.t, term) lra_view -> term - (** Make a term from the given theory view *) - - val ty_lra : S.T.Term.store -> ty - - val mk_eq : S.T.Term.store -> term -> term -> term - (** syntactic equality *) - - val has_ty_real : term -> bool - (** Does this term have the type [Real] *) - - val lemma_lra : S.Lit.t Iter.t -> S.Proof_trace.A.rule - - module Gensym : sig - type t - - val create : S.T.Term.store -> t - val tst : t -> S.T.Term.store - val copy : t -> t - - val fresh_term : t -> pre:string -> S.T.Ty.t -> term - (** Make a fresh term of the given type *) - end -end - -module type S = sig - module A : ARG - - (* - module SimpVar : Sidekick_simplex.VAR with type lit = A.S.Lit.t - module LE_ : Linear_expr_intf.S with module Var = SimpVar - module LE = LE_.Expr - *) - - module SimpSolver : Sidekick_simplex.S - (** Simplexe *) - - type state - - val create : ?stat:Stat.t -> A.S.Solver_internal.t -> state - - (* TODO: be able to declare some variables as ints *) - - (* - val simplex : state -> Simplex.t - *) - - val k_state : state A.S.Solver_internal.Registry.key - (** Key to access the state from outside, - available when the theory has been setup *) - - val theory : A.S.theory -end - -module Make (A : ARG) : S with module A = A = struct - module A = A - module Ty = A.S.T.Ty - module T = A.S.T.Term - module Lit = A.S.Solver_internal.Lit - module SI = A.S.Solver_internal - module N = SI.CC.E_node - - open struct - module Pr = SI.Proof_trace - end - - module Tag = struct - type t = Lit of Lit.t | CC_eq of N.t * N.t - - let pp out = function - | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l - | CC_eq (n1, n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2 - - let to_lits si = function - | Lit l -> [ l ] - | CC_eq (n1, n2) -> - let r = SI.CC.explain_eq (SI.cc si) n1 n2 in - (* FIXME - assert (not (SI.CC.Resolved_expl.is_semantic r)); - *) - r.lits - end - - module SimpVar : Linear_expr.VAR with type t = A.term and type lit = Tag.t = - struct - type t = A.term - - let pp = A.S.T.Term.pp - let compare = A.S.T.Term.compare - - type lit = Tag.t - - let pp_lit = Tag.pp - - let not_lit = function - | Tag.Lit l -> Some (Tag.Lit (Lit.neg l)) - | _ -> None - end - - module LE_ = Linear_expr.Make (A.Q) (SimpVar) - module LE = LE_.Expr - - module SimpSolver = Sidekick_simplex.Make (struct - module Z = A.Z - module Q = A.Q - module Var = SimpVar - - let mk_lit _ _ _ = assert false - end) - - module Subst = SimpSolver.Subst - module Comb_map = CCMap.Make (LE_.Comb) - - (* turn the term into a linear expression. Apply [f] on leaves. *) - let rec as_linexp (t : T.t) : LE.t = - let open LE.Infix in - match A.view_as_lra t with - | LRA_other _ -> LE.monomial1 t - | LRA_pred _ -> - Error.errorf "type error: in linexp, LRA predicate %a" T.pp t - | LRA_op (op, t1, t2) -> - let t1 = as_linexp t1 in - let t2 = as_linexp t2 in - (match op with - | Plus -> t1 + t2 - | Minus -> t1 - t2) - | LRA_mult (n, x) -> - let t = as_linexp x in - LE.(n * t) - | LRA_const q -> LE.of_const q - - (* monoid to track linear expressions in congruence classes, to clash on merge *) - module Monoid_exprs = struct - module CC = SI.CC - - let name = "lra.const" - - type single = { le: LE.t; n: N.t } - type t = single list - - let pp_single out { le = _; n } = N.pp out n - - let pp out self = - match self with - | [] -> () - | [ x ] -> pp_single out x - | _ -> Fmt.fprintf out "(@[exprs@ %a@])" (Util.pp_list pp_single) self - - let of_term _cc n t = - match A.view_as_lra t with - | LRA_const _ | LRA_op _ | LRA_mult _ -> - let le = as_linexp t in - Some [ { n; le } ], [] - | LRA_other _ | LRA_pred _ -> None, [] - - exception Confl of SI.CC.Expl.t - - (* merge lists. If two linear expressions equal up to a constant are - merged, conflict. *) - let merge _cc n1 l1 n2 l2 expl_12 : _ result = - try - let i = Iter.(product (of_list l1) (of_list l2)) in - i (fun (s1, s2) -> - let le = LE.(s1.le - s2.le) in - if LE.is_const le && not (LE.is_zero le) then ( - (* conflict: [le+c = le + d] is impossible *) - let expl = - let open SI.CC.Expl in - mk_list [ mk_merge s1.n n1; mk_merge s2.n n2; expl_12 ] - in - raise (Confl expl) - )); - Ok (List.rev_append l1 l2, []) - with Confl expl -> Error (SI.CC.Handler_action.Conflict expl) - end - - module ST_exprs = Sidekick_cc_plugin.Make (Monoid_exprs) - - type state = { - tst: T.store; - ty_st: Ty.store; - proof: SI.Proof_trace.t; - gensym: A.Gensym.t; - in_model: unit T.Tbl.t; (* terms to add to model *) - encoded_eqs: unit T.Tbl.t; - (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) - needs_th_combination: unit T.Tbl.t; - (* terms that require theory combination *) - simp_preds: (T.t * S_op.t * A.Q.t) T.Tbl.t; - (* term -> its simplex meaning *) - simp_defined: LE.t T.Tbl.t; - (* (rational) terms that are equal to a linexp *) - st_exprs: ST_exprs.t; - mutable encoded_le: T.t Comb_map.t; (* [le] -> var encoding [le] *) - simplex: SimpSolver.t; - mutable last_res: SimpSolver.result option; - } - - let create ?(stat = Stat.create ()) (si : SI.t) : state = - let proof = SI.proof si in - let tst = SI.tst si in - let ty_st = SI.ty_st si in - { - tst; - ty_st; - proof; - in_model = T.Tbl.create 8; - st_exprs = ST_exprs.create_and_setup (SI.cc si); - gensym = A.Gensym.create tst; - simp_preds = T.Tbl.create 32; - simp_defined = T.Tbl.create 16; - encoded_eqs = T.Tbl.create 8; - needs_th_combination = T.Tbl.create 8; - encoded_le = Comb_map.empty; - simplex = SimpSolver.create ~stat (); - last_res = None; - } - - let[@inline] reset_res_ (self : state) : unit = self.last_res <- None - let[@inline] n_levels self : int = ST_exprs.n_levels self.st_exprs - - let push_level self = - ST_exprs.push_level self.st_exprs; - SimpSolver.push_level self.simplex; - () - - let pop_levels self n = - reset_res_ self; - ST_exprs.pop_levels self.st_exprs n; - SimpSolver.pop_levels self.simplex n; - () - - let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty - - let fresh_lit (self : state) ~mk_lit ~pre : Lit.t = - let t = fresh_term ~pre self (Ty.bool self.ty_st) in - mk_lit t - - let pp_pred_def out (p, l1, l2) : unit = - Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" Predicate.pp p LE.pp l1 LE.pp l2 - - let[@inline] t_const self n : T.t = A.mk_lra self.tst (LRA_const n) - let[@inline] t_zero self : T.t = t_const self A.Q.zero - - let[@inline] is_const_ t = - match A.view_as_lra t with - | LRA_const _ -> true - | _ -> false - - let[@inline] as_const_ t = - match A.view_as_lra t with - | LRA_const n -> Some n - | _ -> None - - let[@inline] is_zero t = - match A.view_as_lra t with - | LRA_const n -> A.Q.(n = zero) - | _ -> false - - let t_of_comb (self : state) (comb : LE_.Comb.t) ~(init : T.t) : T.t = - let[@inline] ( + ) a b = A.mk_lra self.tst (LRA_op (Plus, a, b)) in - let[@inline] ( * ) a b = A.mk_lra self.tst (LRA_mult (a, b)) in - - let cur = ref init in - LE_.Comb.iter - (fun t c -> - let tc = - if A.Q.(c = of_int 1) then - t - else - c * t - in - cur := - if is_zero !cur then - tc - else - !cur + tc) - comb; - !cur - - (* encode back into a term *) - let t_of_linexp (self : state) (le : LE.t) : T.t = - let comb = LE.comb le in - let const = LE.const le in - t_of_comb self comb ~init:(A.mk_lra self.tst (LRA_const const)) - - (* return a variable that is equal to [le_comb] in the simplex. *) - let var_encoding_comb ~pre self (le_comb : LE_.Comb.t) : T.t = - assert (not (LE_.Comb.is_empty le_comb)); - match LE_.Comb.as_singleton le_comb with - | Some (c, x) when A.Q.(c = one) -> x (* trivial linexp *) - | _ -> - (match Comb_map.find le_comb self.encoded_le with - | x -> x (* already encoded that *) - | exception Not_found -> - (* new variable to represent [le_comb] *) - let proxy = fresh_term self ~pre (A.ty_lra self.tst) in - (* TODO: define proxy *) - self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; - Log.debugf 50 (fun k -> - k "(@[lra.encode-linexp@ `@[%a@]`@ :into-var %a@])" LE_.Comb.pp - le_comb T.pp proxy); - - LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; - SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb); - proxy) - - let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits = - let pr = Pr.add_step PA.proof @@ A.lemma_lra (Iter.of_list lits) in - let pr = - match using with - | None -> pr - | Some using -> - Pr.add_step PA.proof - @@ SI.P_core_rules.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using - in - PA.add_clause lits pr - - let s_op_of_pred pred : S_op.t = - match pred with - | Eq | Neq -> assert false (* unreachable *) - | Leq -> S_op.Leq - | Lt -> S_op.Lt - | Geq -> S_op.Geq - | Gt -> S_op.Gt - - (* TODO: refactor that and {!var_encoding_comb} *) - (* turn a linear expression into a single constant and a coeff. - This might define a side variable in the simplex. *) - let le_comb_to_singleton_ (self : state) (le_comb : LE_.Comb.t) : T.t * A.Q.t - = - match LE_.Comb.as_singleton le_comb with - | Some (coeff, v) -> v, coeff - | None -> - (* non trivial linexp, give it a fresh name in the simplex *) - (match Comb_map.get le_comb self.encoded_le with - | Some x -> x, A.Q.one (* already encoded that *) - | None -> - let proxy = fresh_term self ~pre:"_le_comb" (A.ty_lra self.tst) in - - self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; - LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; - SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb); - - Log.debugf 50 (fun k -> - k "(@[lra.encode-linexp.to-term@ `@[%a@]`@ :new-t %a@])" LE_.Comb.pp - le_comb T.pp proxy); - - proxy, A.Q.one) - - (* look for subterms of type Real, for they will need theory combination *) - let on_subterm (self : state) (t : T.t) : unit = - Log.debugf 50 (fun k -> k "(@[lra.cc-on-subterm@ %a@])" T.pp t); - match A.view_as_lra t with - | LRA_other _ when not (A.has_ty_real t) -> () - | LRA_pred _ | LRA_const _ -> () - | LRA_op _ | LRA_other _ | LRA_mult _ -> - if not (T.Tbl.mem self.needs_th_combination t) then ( - Log.debugf 5 (fun k -> k "(@[lra.needs-th-combination@ %a@])" T.pp t); - T.Tbl.add self.needs_th_combination t () - ) - - (* preprocess linear expressions away *) - let preproc_lra (self : state) si (module PA : SI.PREPROCESS_ACTS) (t : T.t) : - unit = - Log.debugf 50 (fun k -> k "(@[lra.preprocess@ %a@])" T.pp t); - let tst = SI.tst si in - - (* tell the CC this term exists *) - let declare_term_to_cc ~sub t = - Log.debugf 50 (fun k -> k "(@[lra.declare-term-to-cc@ %a@])" T.pp t); - ignore (SI.CC.add_term (SI.cc si) t : N.t); - if sub then on_subterm self t - in - - match A.view_as_lra t with - | _ when T.Tbl.mem self.simp_preds t -> - () (* already turned into a simplex predicate *) - | LRA_pred (((Eq | Neq) as pred), t1, t2) when is_const_ t1 && is_const_ t2 - -> - (* comparison of constants: can decide right now *) - (match A.view_as_lra t1, A.view_as_lra t2 with - | LRA_const n1, LRA_const n2 -> - let is_eq = pred = Eq in - let t_is_true = is_eq = A.Q.equal n1 n2 in - let lit = PA.mk_lit ~sign:t_is_true t in - add_clause_lra_ (module PA) [ lit ] - | _ -> assert false) - | LRA_pred ((Eq | Neq), t1, t2) -> - (* equality: just punt to [t1 = t2 <=> (t1 <= t2 /\ t1 >= t2)] *) - let t, _ = T.abs tst t in - if not (T.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 - - T.Tbl.add self.encoded_eqs t (); - - (* encode [t <=> (u1 /\ u2)] *) - let lit_t = PA.mk_lit t in - let lit_u1 = PA.mk_lit u1 in - let lit_u2 = PA.mk_lit u2 in - add_clause_lra_ (module PA) [ SI.Lit.neg lit_t; lit_u1 ]; - add_clause_lra_ (module PA) [ SI.Lit.neg lit_t; lit_u2 ]; - add_clause_lra_ - (module PA) - [ SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t ] - ) - | LRA_pred (pred, t1, t2) -> - let l1 = as_linexp t1 in - let l2 = as_linexp t2 in - let le = LE.(l1 - l2) in - let le_comb, le_const = LE.comb le, LE.const le in - let le_const = A.Q.neg le_const in - let op = s_op_of_pred pred in - - (* now we have [le_comb op le_const] *) - - (* obtain a single variable for the linear combination *) - let v, c_v = le_comb_to_singleton_ self le_comb in - declare_term_to_cc ~sub:false v; - LE_.Comb.iter (fun v _ -> declare_term_to_cc ~sub:true v) le_comb; - - (* turn into simplex constraint. For example, - [c . v <= const] becomes a direct simplex constraint [v <= const/c] - (beware the sign) *) - - (* make sure to swap sides if multiplying with a negative coeff *) - let q = A.Q.(le_const / c_v) in - let op = - if A.Q.(c_v < zero) then - S_op.neg_sign op - else - op - in - - let lit = PA.mk_lit t in - let constr = SimpSolver.Constraint.mk v op q in - SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); - T.Tbl.add self.simp_preds t (v, op, q); - - Log.debugf 50 (fun k -> - k "(@[lra.preproc@ :t %a@ :to-constr %a@])" T.pp t - SimpSolver.Constraint.pp constr) - | LRA_op _ | LRA_mult _ -> - if not (T.Tbl.mem self.simp_defined t) then ( - (* we define these terms so their value in the model make sense *) - let le = as_linexp t in - T.Tbl.add self.simp_defined t le - ) - | LRA_const _n -> () - | LRA_other t when A.has_ty_real t -> () - | LRA_other _ -> () - - let simplify (self : state) (_recurse : _) (t : T.t) : - (T.t * SI.step_id Iter.t) option = - let proof_eq t u = - Pr.add_step self.proof - @@ A.lemma_lra (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) - in - let proof_bool t ~sign:b = - let lit = SI.Lit.atom ~sign:b self.tst t in - Pr.add_step self.proof @@ A.lemma_lra (Iter.return lit) - in - - match A.view_as_lra t with - | LRA_op _ | LRA_mult _ -> - let le = as_linexp t in - if LE.is_const le then ( - let c = LE.const le in - let u = A.mk_lra self.tst (LRA_const c) in - let pr = proof_eq t u in - Some (u, Iter.return pr) - ) else ( - let u = t_of_linexp self le in - if t != u then ( - let pr = proof_eq t u in - Some (u, Iter.return pr) - ) else - None - ) - | LRA_pred ((Eq | Neq), _, _) -> - (* never change equalities, it can affect theory combination *) - None - | LRA_pred (pred, l1, l2) -> - let le = LE.(as_linexp l1 - as_linexp l2) in - - if LE.is_const le then ( - let c = LE.const le in - let is_true = - match pred with - | Leq -> A.Q.(c <= zero) - | Geq -> A.Q.(c >= zero) - | Lt -> A.Q.(c < zero) - | Gt -> A.Q.(c > zero) - | Eq -> A.Q.(c = zero) - | Neq -> A.Q.(c <> zero) - in - let u = A.mk_bool self.tst is_true in - let pr = proof_bool t ~sign:is_true in - Some (u, Iter.return pr) - ) else ( - (* le <= const *) - let u = - A.mk_lra self.tst - (LRA_pred - ( pred, - t_of_comb self (LE.comb le) ~init:(t_zero self), - t_const self (A.Q.neg @@ LE.const le) )) - in - - if t != u then ( - let pr = proof_eq t u in - Some (u, Iter.return pr) - ) else - None - ) - | _ -> None - - (* raise conflict from certificate *) - let fail_with_cert si acts cert : 'a = - Profile.with1 "lra.simplex.check-cert" SimpSolver._check_cert cert; - let confl = - SimpSolver.Unsat_cert.lits cert - |> CCList.flat_map (Tag.to_lits si) - |> List.rev_map SI.Lit.neg - in - let pr = Pr.add_step (SI.proof si) @@ A.lemma_lra (Iter.of_list confl) in - SI.raise_conflict si acts confl pr - - let on_propagate_ si acts lit ~reason = - match lit with - | Tag.Lit lit -> - (* TODO: more detailed proof certificate *) - SI.propagate si acts lit ~reason:(fun () -> - let lits = CCList.flat_map (Tag.to_lits si) reason in - let pr = - Pr.add_step (SI.proof si) - @@ A.lemma_lra Iter.(cons lit (of_list lits)) - in - CCList.flat_map (Tag.to_lits si) reason, pr) - | _ -> () - - (** Check satisfiability of simplex, and sets [self.last_res] *) - let check_simplex_ self si acts : SimpSolver.Subst.t = - Log.debugf 5 (fun k -> - k "(@[lra.check-simplex@ :n-vars %d :n-rows %d@])" - (SimpSolver.n_vars self.simplex) - (SimpSolver.n_rows self.simplex)); - let res = - Profile.with_ "lra.simplex.solve" @@ fun () -> - SimpSolver.check self.simplex ~on_propagate:(on_propagate_ si acts) - in - Log.debug 5 "(lra.check-simplex.done)"; - self.last_res <- Some res; - match res with - | SimpSolver.Sat m -> m - | SimpSolver.Unsat cert -> - Log.debugf 10 (fun k -> - k "(@[lra.check.unsat@ :cert %a@])" SimpSolver.Unsat_cert.pp cert); - fail_with_cert si acts cert - - (* TODO: trivial propagations *) - - let add_local_eq_t (self : state) si acts t1 t2 ~tag : unit = - Log.debugf 20 (fun k -> k "(@[lra.add-local-eq@ %a@ %a@])" T.pp t1 T.pp t2); - reset_res_ self; - let t1, t2 = - if T.compare t1 t2 > 0 then - t2, t1 - else - t1, t2 - in - - let le = LE.(as_linexp t1 - as_linexp t2) in - let le_comb, le_const = LE.comb le, LE.const le in - let le_const = A.Q.neg le_const in - - if LE_.Comb.is_empty le_comb then ( - if A.Q.(le_const <> zero) then ( - (* [c=0] when [c] is not 0 *) - let lit = SI.Lit.neg @@ SI.mk_lit si acts @@ A.mk_eq self.tst t1 t2 in - let pr = Pr.add_step self.proof @@ A.lemma_lra (Iter.return lit) in - SI.add_clause_permanent si acts [ lit ] pr - ) - ) else ( - let v = var_encoding_comb ~pre:"le_local_eq" self le_comb in - try - let c1 = SimpSolver.Constraint.geq v le_const in - SimpSolver.add_constraint self.simplex c1 tag - ~on_propagate:(on_propagate_ si acts); - let c2 = SimpSolver.Constraint.leq v le_const in - SimpSolver.add_constraint self.simplex c2 tag - ~on_propagate:(on_propagate_ si acts) - with SimpSolver.E_unsat cert -> fail_with_cert si acts cert - ) - - let add_local_eq (self : state) si acts n1 n2 : unit = - let t1 = N.term n1 in - let t2 = N.term n2 in - add_local_eq_t self si acts t1 t2 ~tag:(Tag.CC_eq (n1, n2)) - - (* evaluate a term directly, as a variable *) - let eval_in_subst_ subst t = - match A.view_as_lra t with - | LRA_const n -> n - | _ -> Subst.eval subst t |> Option.value ~default:A.Q.zero - - (* evaluate a linear expression *) - let eval_le_in_subst_ subst (le : LE.t) = LE.eval (eval_in_subst_ subst) le - - (* FIXME: rename, this is more "provide_model_to_cc" *) - let do_th_combination (self : state) _si _acts : _ Iter.t = - Log.debug 1 "(lra.do-th-combinations)"; - let model = - match self.last_res with - | Some (SimpSolver.Sat m) -> m - | _ -> assert false - in - - let vals = Subst.to_iter model |> T.Tbl.of_iter in - - (* also include terms that occur under function symbols, if they're - not in the model already *) - T.Tbl.iter - (fun t () -> - if not (T.Tbl.mem vals t) then ( - let v = eval_in_subst_ model t in - T.Tbl.add vals t v - )) - self.needs_th_combination; - - (* also consider subterms that are linear expressions, - and evaluate them using the value of each variable - in that linear expression. For example a term [a + 2b] - is evaluated as [eval(a) + 2 × eval(b)]. *) - T.Tbl.iter - (fun t le -> - if not (T.Tbl.mem vals t) then ( - let v = eval_le_in_subst_ model le in - T.Tbl.add vals t v - )) - self.simp_defined; - - (* return whole model *) - T.Tbl.to_iter vals |> Iter.map (fun (t, v) -> t, t_const self v) - - (* partial checks is where we add literals from the trail to the - simplex. *) - let partial_check_ self si acts trail : unit = - Profile.with_ "lra.partial-check" @@ fun () -> - reset_res_ self; - let changed = ref false in - - let examine_lit lit = - let sign = SI.Lit.sign lit in - let lit_t = SI.Lit.term lit in - match T.Tbl.get self.simp_preds lit_t, A.view_as_lra lit_t with - | Some (v, op, q), _ -> - Log.debugf 50 (fun k -> - k "(@[lra.partial-check.add@ :lit %a@ :lit-t %a@])" SI.Lit.pp lit - T.pp lit_t); - - (* need to account for the literal's sign *) - let op = - if sign then - op - else - S_op.not_ op - in - - (* assert new constraint to Simplex *) - let constr = SimpSolver.Constraint.mk v op q in - Log.debugf 10 (fun k -> - k "(@[lra.partial-check.assert@ %a@])" SimpSolver.Constraint.pp - constr); - changed := true; - (try - SimpSolver.add_var self.simplex v; - SimpSolver.add_constraint self.simplex constr (Tag.Lit lit) - ~on_propagate:(on_propagate_ si acts) - with SimpSolver.E_unsat cert -> - Log.debugf 10 (fun k -> - k "(@[lra.partial-check.unsat@ :cert %a@])" - SimpSolver.Unsat_cert.pp cert); - fail_with_cert si acts cert) - | None, LRA_pred (Eq, t1, t2) when sign -> - add_local_eq_t self si acts t1 t2 ~tag:(Tag.Lit lit) - | None, LRA_pred (Neq, t1, t2) when not sign -> - add_local_eq_t self si acts t1 t2 ~tag:(Tag.Lit lit) - | None, _ -> () - in - - Iter.iter examine_lit trail; - - (* incremental check *) - if !changed then ignore (check_simplex_ self si acts : SimpSolver.Subst.t); - () - - let final_check_ (self : state) si (acts : SI.theory_actions) - (_trail : _ Iter.t) : unit = - Log.debug 5 "(th-lra.final-check)"; - Profile.with_ "lra.final-check" @@ fun () -> - reset_res_ self; - - (* add equalities between linear-expressions merged in the congruence closure *) - ST_exprs.iter_all self.st_exprs (fun (_, l) -> - Iter.diagonal_l l (fun (s1, s2) -> add_local_eq self si acts s1.n s2.n)); - - (* TODO: jiggle model to reduce the number of variables that - have the same value *) - let model = check_simplex_ self si acts in - Log.debugf 20 (fun k -> k "(@[lra.model@ %a@])" SimpSolver.Subst.pp model); - Log.debug 5 "(lra: solver returns SAT)"; - () - - (* help generating model *) - let model_ask_ (self : state) ~recurse:_ _si n : _ option = - let t = N.term n in - match self.last_res with - | Some (SimpSolver.Sat m) -> - Log.debugf 50 (fun k -> k "(@[lra.model-ask@ %a@])" T.pp t); - (match A.view_as_lra t with - | LRA_const n -> Some n (* always eval constants to themselves *) - | _ -> SimpSolver.V_map.get t m) - |> Option.map (t_const self) - | _ -> None - - (* help generating model *) - let model_complete_ (self : state) _si ~add : unit = - Log.debugf 30 (fun k -> k "(lra.model-complete)"); - match self.last_res with - | Some (SimpSolver.Sat m) when T.Tbl.length self.in_model > 0 -> - Log.debugf 50 (fun k -> - k "(@[lra.in_model@ %a@])" (Util.pp_iter T.pp) - (T.Tbl.keys self.in_model)); - - let add_t t () = - match SimpSolver.V_map.get t m with - | None -> () - | Some u -> add t (t_const self u) - in - T.Tbl.iter add_t self.in_model - | _ -> () - - let k_state = SI.Registry.create_key () - - let create_and_setup si = - Log.debug 2 "(th-lra.setup)"; - let stat = SI.stats si in - let st = create ~stat si in - SI.Registry.set (SI.registry si) k_state st; - SI.add_simplifier si (simplify st); - SI.on_preprocess si (preproc_lra st); - SI.on_final_check si (final_check_ st); - SI.on_partial_check si (partial_check_ st); - SI.on_model si ~ask:(model_ask_ st) ~complete:(model_complete_ st); - SI.on_cc_is_subterm si (fun (_, _, t) -> - on_subterm st t; - []); - SI.on_cc_pre_merge si (fun (_cc, n1, n2, expl) -> - match as_const_ (N.term n1), as_const_ (N.term n2) with - | Some q1, Some q2 when A.Q.(q1 <> q2) -> - (* classes with incompatible constants *) - Log.debugf 30 (fun k -> - k "(@[lra.merge-incompatible-consts@ %a@ %a@])" N.pp n1 N.pp n2); - Error (SI.CC.Handler_action.Conflict expl) - | _ -> Ok []); - SI.on_th_combination si (do_th_combination st); - st - - let theory = - A.S.mk_theory ~name:"th-lra" ~create_and_setup ~push_level ~pop_levels () -end diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml index 3bc09bd0..b5b1e923 100644 --- a/src/core-logic/t_builtins.ml +++ b/src/core-logic/t_builtins.ml @@ -88,3 +88,9 @@ let rec abs t = let sign, v = abs u in Stdlib.not sign, v | _ -> true, t + +let as_bool_val t = + match Term.view t with + | Term.E_const { c_view = C_true; _ } -> Some true + | Term.E_const { c_view = C_false; _ } -> Some false + | _ -> None diff --git a/src/core-logic/t_builtins.mli b/src/core-logic/t_builtins.mli index 8ae490ee..5ffd27b3 100644 --- a/src/core-logic/t_builtins.mli +++ b/src/core-logic/t_builtins.mli @@ -31,3 +31,5 @@ val abs : t -> bool * 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 diff --git a/src/sigs/smt/Sidekick_sigs_smt.ml b/src/sigs/smt/Sidekick_sigs_smt.ml deleted file mode 100644 index ddeb5b71..00000000 --- a/src/sigs/smt/Sidekick_sigs_smt.ml +++ /dev/null @@ -1,606 +0,0 @@ -(** Signature for the main SMT solver types. - - Theories and concrete solvers rely on an environment that defines - several important types: - - - sorts - - terms (to represent logic expressions and formulas) - - a congruence closure instance - - a bridge to some SAT solver - - In this module we collect signatures defined elsewhere and define - the module types for the main SMT solver. -*) - -module type TERM = Sidekick_sigs_term.S -module type LIT = Sidekick_sigs_lit.S -module type PROOF_TRACE = Sidekick_sigs_proof_trace.S - -module type SAT_PROOF_RULES = Sidekick_sigs_proof_sat.S -(** Signature for SAT-solver proof emission. *) - -module type PROOF_CORE = Sidekick_sigs_proof_core.S -(** Proofs of unsatisfiability. *) - -(** Registry to extract values *) -module type REGISTRY = sig - type t - type 'a key - - val create_key : unit -> 'a key - (** Call this statically, typically at program initialization, for - each distinct key. *) - - val create : unit -> t - val get : t -> 'a key -> 'a option - val set : t -> 'a key -> 'a -> unit -end - -(** A view of the solver from a theory's point of view. - - Theories should interact with the solver via this module, to assert - new lemmas, propagate literals, access the congruence closure, etc. *) -module type SOLVER_INTERNAL = sig - module T : TERM - module Lit : LIT with module T = T - module Proof_trace : PROOF_TRACE - - type ty = T.Ty.t - type term = T.Term.t - type value = T.Term.t - type lit = Lit.t - type term_store = T.Term.store - type ty_store = T.Ty.store - type clause_pool - type proof_trace = Proof_trace.t - type step_id = Proof_trace.A.step_id - - type t - (** {3 Main type for a solver} *) - - type solver = t - - val tst : t -> term_store - val ty_st : t -> ty_store - val stats : t -> Stat.t - - val proof : t -> proof_trace - (** Access the proof object *) - - (** {3 Registry} *) - - module Registry : REGISTRY - - val registry : t -> Registry.t - (** A solver contains a registry so that theories can share data *) - - (** {3 Exported Proof rules} *) - - module P_core_rules : - Sidekick_sigs_proof_core.S - with type rule = Proof_trace.A.rule - and type step_id = Proof_trace.A.step_id - and type term = term - and type lit = lit - - (** {3 Actions for the theories} *) - - type theory_actions - (** Handle that the theories can use to perform actions. *) - - (** {3 Congruence Closure} *) - - (** Congruence closure instance *) - module CC : - Sidekick_sigs_cc.S - with module T = T - and module Lit = Lit - and module Proof_trace = Proof_trace - - val cc : t -> CC.t - (** Congruence closure for this solver *) - - (** {3 Simplifiers} *) - - (* TODO: move into its own library *) - - (** Simplify terms *) - module Simplify : sig - type t - - val tst : t -> term_store - val ty_st : t -> ty_store - - val clear : t -> unit - (** Reset internal cache, etc. *) - - val proof : t -> proof_trace - (** Access proof *) - - type hook = t -> term -> (term * step_id Iter.t) option - (** Given a term, try to simplify it. Return [None] if it didn't change. - - A simple example could be a hook that takes a term [t], - and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, - returns [Some (const (x+y))], and [None] otherwise. - - The simplifier will take care of simplifying the resulting term further, - caching (so that work is not duplicated in subterms), etc. - *) - - val normalize : t -> term -> (term * step_id) option - (** Normalize a term using all the hooks. This performs - a fixpoint, i.e. it only stops when no hook applies anywhere inside - the term. *) - - val normalize_t : t -> term -> term * step_id option - (** Normalize a term using all the hooks, along with a proof that the - simplification is correct. - returns [t, ø] if no simplification occurred. *) - end - - type simplify_hook = Simplify.hook - - val add_simplifier : t -> Simplify.hook -> unit - (** Add a simplifier hook for preprocessing. *) - - val simplify_t : t -> term -> (term * step_id) option - (** Simplify input term, returns [Some u] if some - simplification occurred. *) - - val simp_t : t -> term -> term * step_id option - (** [simp_t si t] returns [u] even if no simplification occurred - (in which case [t == u] syntactically). - It emits [|- t=u]. - (see {!simplifier}) *) - - (** {3 Preprocessors} - These preprocessors turn mixed, raw literals (possibly simplified) into - literals suitable for reasoning. - Typically some clauses are also added to the solver. *) - - (* TODO: move into its own sig + library *) - module type PREPROCESS_ACTS = sig - val proof : proof_trace - - val mk_lit : ?sign:bool -> term -> lit - (** [mk_lit t] creates a new literal for a boolean term [t]. *) - - val add_clause : lit list -> step_id -> unit - (** pushes a new clause into the SAT solver. *) - - val add_lit : ?default_pol:bool -> lit -> unit - (** Ensure the literal will be decided/handled by the SAT solver. *) - end - - type preprocess_actions = (module PREPROCESS_ACTS) - (** Actions available to the preprocessor *) - - type preprocess_hook = t -> preprocess_actions -> term -> unit - (** Given a term, preprocess it. - - The idea is to add literals and clauses to help define the meaning of - the term, if needed. For example for boolean formulas, clauses - for their Tseitin encoding can be added, with the formula acting - as its own proxy symbol. - - @param preprocess_actions actions available during preprocessing. - *) - - val on_preprocess : t -> preprocess_hook -> unit - (** Add a hook that will be called when terms are preprocessed *) - - (** {3 hooks for the theory} *) - - val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a - (** Give a conflict clause to the solver *) - - val push_decision : t -> theory_actions -> lit -> unit - (** Ask the SAT solver to decide the given literal in an extension of the - current trail. This is useful for theory combination. - If the SAT solver backtracks, this (potential) decision is removed - and forgotten. *) - - val propagate : - t -> theory_actions -> lit -> reason:(unit -> lit list * step_id) -> unit - (** Propagate a boolean using a unit clause. - [expl => lit] must be a theory lemma, that is, a T-tautology *) - - val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> unit - (** Propagate a boolean using a unit clause. - [expl => lit] must be a theory lemma, that is, a T-tautology *) - - val add_clause_temp : t -> theory_actions -> lit list -> step_id -> unit - (** Add local clause to the SAT solver. This clause will be - removed when the solver backtracks. *) - - val add_clause_permanent : t -> theory_actions -> lit list -> step_id -> unit - (** Add toplevel clause to the SAT solver. This clause will - not be backtracked. *) - - val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit - (** Create a literal. This automatically preprocesses the term. *) - - val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit - (** Add the given literal to the SAT solver, so it gets assigned - a boolean value. - @param default_pol default polarity for the corresponding atom *) - - val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit - (** Add the given (signed) bool term to the SAT solver, so it gets assigned - a boolean value *) - - val cc_find : t -> CC.E_node.t -> CC.E_node.t - (** Find representative of the node *) - - val cc_are_equal : t -> term -> term -> bool - (** Are these two terms equal in the congruence closure? *) - - val cc_resolve_expl : t -> CC.Expl.t -> lit list * step_id - - (* - val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'a - (** Raise a conflict with the given congruence closure explanation. - it must be a theory tautology that [expl ==> absurd]. - To be used in theories. *) - - val cc_merge : - t -> theory_actions -> CC.E_node.t -> CC.E_node.t -> CC.Expl.t -> unit - (** Merge these two nodes in the congruence closure, given this explanation. - It must be a theory tautology that [expl ==> n1 = n2]. - To be used in theories. *) - - val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unit - (** Merge these two terms in the congruence closure, given this explanation. - See {!cc_merge} *) - *) - - val cc_add_term : t -> term -> CC.E_node.t - (** Add/retrieve congruence closure node for this term. - To be used in theories *) - - val cc_mem_term : t -> term -> bool - (** Return [true] if the term is explicitly in the congruence closure. - To be used in theories *) - - val on_cc_pre_merge : - t -> - (CC.t * CC.E_node.t * CC.E_node.t * CC.Expl.t -> - CC.Handler_action.or_conflict) -> - unit - (** Callback for when two classes containing data for this key are merged (called before) *) - - val on_cc_post_merge : - t -> (CC.t * CC.E_node.t * CC.E_node.t -> CC.Handler_action.t list) -> unit - (** Callback for when two classes containing data for this key are merged (called after)*) - - val on_cc_new_term : - t -> (CC.t * CC.E_node.t * term -> CC.Handler_action.t list) -> unit - (** Callback to add data on terms when they are added to the congruence - closure *) - - val on_cc_is_subterm : - t -> (CC.t * CC.E_node.t * term -> CC.Handler_action.t list) -> unit - (** Callback for when a term is a subterm of another term in the - congruence closure *) - - val on_cc_conflict : t -> (CC.ev_on_conflict -> unit) -> unit - (** Callback called on every CC conflict *) - - val on_cc_propagate : - t -> - (CC.t * lit * (unit -> lit list * step_id) -> CC.Handler_action.t list) -> - unit - (** Callback called on every CC propagation *) - - val on_partial_check : - t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit - (** Register callbacked to be called with the slice of literals - newly added on the trail. - - This is called very often and should be efficient. It doesn't have - to be complete, only correct. It's given only the slice of - the trail consisting in new literals. *) - - val on_final_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit - (** Register callback to be called during the final check. - - Must be complete (i.e. must raise a conflict if the set of literals is - not satisfiable) and can be expensive. The function - is given the whole trail. - *) - - val on_th_combination : - t -> (t -> theory_actions -> (term * value) Iter.t) -> unit - (** Add a hook called during theory combination. - The hook must return an iterator of pairs [(t, v)] - which mean that term [t] has value [v] in the model. - - Terms with the same value (according to {!Term.equal}) will be - merged in the CC; if two terms with different values are merged, - we get a semantic conflict and must pick another model. *) - - val declare_pb_is_incomplete : t -> unit - (** Declare that, in some theory, the problem is outside the logic fragment - that is decidable (e.g. if we meet proper NIA formulas). - The solver will not reply "SAT" from now on. *) - - (** {3 Model production} *) - - type model_ask_hook = - recurse:(t -> CC.E_node.t -> term) -> t -> CC.E_node.t -> term option - (** A model-production hook to query values from a theory. - - It takes the solver, a class, and returns - a term for this class. For example, an arithmetic theory - might detect that a class contains a numeric constant, and return - this constant as a model value. - - If no hook assigns a value to a class, a fake value is created for it. - *) - - type model_completion_hook = t -> add:(term -> term -> unit) -> unit - (** A model production hook, for the theory to add values. - The hook is given a [add] function to add bindings to the model. *) - - val on_model : - ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit - (** Add model production/completion hooks. *) -end - -(** User facing view of the solver. - - This is the solver a user of sidekick can see, after instantiating - everything. The user can add some theories, clauses, etc. and asks - the solver to check satisfiability. - - Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *) -module type SOLVER = sig - module T : TERM - module Lit : LIT with module T = T - module Proof_trace : PROOF_TRACE - - (** Internal solver, available to theories. *) - module Solver_internal : - SOLVER_INTERNAL - with module T = T - and module Lit = Lit - and module Proof_trace = Proof_trace - - type t - (** The solver's state. *) - - type solver = t - type term = T.Term.t - type ty = T.Ty.t - type lit = Lit.t - type proof_trace = Proof_trace.t - type step_id = Proof_trace.A.step_id - - (** {3 Value registry} *) - - module Registry : REGISTRY - - val registry : t -> Registry.t - (** A solver contains a registry so that theories can share data *) - - (** {3 A theory} - - Theories are abstracted over the concrete implementation of the solver, - so they can work with any implementation. - - Typically a theory should be a functor taking an argument containing - a [SOLVER_INTERNAL] or even a full [SOLVER], - and some additional views on terms, literals, etc. - that are specific to the theory (e.g. to map terms to linear - expressions). - The theory can then be instantiated on any kind of solver for any - term representation that also satisfies the additional theory-specific - requirements. Instantiated theories (ie values of type {!SOLVER.theory}) - can be added to the solver. - *) - module type THEORY = sig - type t - (** The theory's state *) - - val name : string - (** Name of the theory (ideally, unique and short) *) - - val create_and_setup : Solver_internal.t -> t - (** Instantiate the theory's state for the given (internal) solver, - register callbacks, create keys, etc. - - Called once for every solver this theory is added to. *) - - val push_level : t -> unit - (** Push backtracking level. When the corresponding pop is called, - the theory's state should be restored to a state {b equivalent} - to what it was just before [push_level]. - - it does not have to be exactly the same state, it just needs to - be equivalent. *) - - val pop_levels : t -> int -> unit - (** [pop_levels theory n] pops [n] backtracking levels, - restoring [theory] to its state before calling [push_level] n times. *) - end - - type theory = (module THEORY) - (** A theory that can be used for this particular solver. *) - - type 'a theory_p = (module THEORY with type t = 'a) - (** A theory that can be used for this particular solver, with state - of type ['a]. *) - - val mk_theory : - name:string -> - create_and_setup:(Solver_internal.t -> 'th) -> - ?push_level:('th -> unit) -> - ?pop_levels:('th -> int -> unit) -> - unit -> - theory - (** Helper to create a theory. *) - - (** Models - - A model can be produced when the solver is found to be in a - satisfiable state after a call to {!solve}. *) - module Model : sig - type t - - val empty : t - val mem : t -> term -> bool - val find : t -> term -> term option - val eval : t -> term -> term option - val pp : t Fmt.printer - end - - (* TODO *) - module Unknown : sig - type t - - val pp : t CCFormat.printer - - (* - type unknown = - | U_timeout - | U_incomplete - *) - end - - (** {3 Main API} *) - - val stats : t -> Stat.t - val tst : t -> T.Term.store - val ty_st : t -> T.Ty.store - val proof : t -> proof_trace - - val create : - ?stat:Stat.t -> - ?size:[ `Big | `Tiny | `Small ] -> - (* TODO? ?config:Config.t -> *) - proof:proof_trace -> - theories:theory list -> - T.Term.store -> - T.Ty.store -> - unit -> - t - (** Create a new solver. - - It needs a term state and a type state to manipulate terms and types. - All terms and types interacting with this solver will need to come - from these exact states. - - @param store_proof if true, proofs from the SAT solver and theories - are retained and potentially accessible after {!solve} - returns UNSAT. - @param size influences the size of initial allocations. - @param theories theories to load from the start. Other theories - can be added using {!add_theory}. *) - - val add_theory : t -> theory -> unit - (** Add a theory to the solver. This should be called before - any call to {!solve} or to {!add_clause} and the likes (otherwise - the theory will have a partial view of the problem). *) - - val add_theory_p : t -> 'a theory_p -> 'a - (** Add the given theory and obtain its state *) - - val add_theory_l : t -> theory list -> unit - - val mk_lit_t : t -> ?sign:bool -> term -> lit - (** [mk_lit_t _ ~sign t] returns [lit'], - where [lit'] is [preprocess(lit)] and [lit] is - an internal representation of [± t]. - - The proof of [|- lit = lit'] is directly added to the solver's proof. *) - - val add_clause : t -> lit array -> step_id -> 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 -> lit list -> step_id -> unit - (** Add a clause to the solver, given as a list. *) - - val assert_terms : t -> term list -> unit - (** Helper that turns each term into an atom, before adding the result - to the solver as an assertion *) - - val assert_term : t -> term -> unit - (** Helper that turns the term into an atom, before adding the result - to the solver as a unit clause assertion *) - - (** Result of solving for the current set of clauses *) - type res = - | Sat of Model.t (** Satisfiable *) - | Unsat of { - unsat_core: unit -> lit Iter.t; - (** Unsat core (subset of assumptions), or empty *) - unsat_step_id: unit -> step_id option; - (** Proof step for the empty clause *) - } (** 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) -> - ?should_stop:(t -> int -> bool) -> - assumptions:lit list -> - t -> - res - (** [solve s] checks the satisfiability of the clauses added so far to [s]. - @param check if true, the model is checked before returning. - @param on_progress called regularly during solving. - @param assumptions a set of atoms held to be true. The unsat core, - if any, will be a subset of [assumptions]. - @param should_stop a callback regularly called with the solver, - and with a number of "steps" done since last call. The exact notion - of step is not defined, but is guaranteed to increase regularly. - The function should return [true] if it judges solving - must stop (returning [Unknown]), [false] if solving can proceed. - @param on_exit functions to be run before this returns *) - - val last_res : t -> res option - (** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *) - - val push_assumption : t -> lit -> unit - (** Pushes an assumption onto the assumption stack. It will remain - there until it's pop'd by {!pop_assumptions}. *) - - val pop_assumptions : t -> int -> unit - (** [pop_assumptions solver n] removes [n] assumptions from the stack. - It removes the assumptions that were the most - recently added via {!push_assumptions}. - Note that {!check_sat_propagations_only} can call this if it meets - a conflict. *) - - type propagation_result = - | PR_sat - | PR_conflict of { backtracked: int } - | PR_unsat of { unsat_core: unit -> lit Iter.t } - - val check_sat_propagations_only : - assumptions:lit list -> t -> propagation_result - (** [check_sat_propagations_only solver] uses assumptions (including - the [assumptions] parameter, and atoms previously added via {!push_assumptions}) - and boolean+theory propagation to quickly assess satisfiability. - It is not complete; calling {!solve} is required to get an accurate - result. - @returns one of: - - - [PR_sat] if the current state seems satisfiable - - [PR_conflict {backtracked=n}] if a conflict was found and resolved, - leading to backtracking [n] levels of assumptions - - [PR_unsat …] if the assumptions were found to be unsatisfiable, with - the given core. - *) - - (* TODO: allow on_progress to return a bool to know whether to stop? *) - - val pp_stats : t CCFormat.printer - (** Print some statistics. What it prints exactly is unspecified. *) -end diff --git a/src/sigs/smt/dune b/src/sigs/smt/dune deleted file mode 100644 index 063ba7ce..00000000 --- a/src/sigs/smt/dune +++ /dev/null @@ -1,8 +0,0 @@ -(library - (name sidekick_sigs_smt) - (public_name sidekick.sigs.smt) - (synopsis "Signatures for the SMT solver") - (flags :standard -open Sidekick_util) - (libraries containers iter sidekick.sigs sidekick.sigs.term - sidekick.sigs.lit sidekick.sigs.proof-trace sidekick.sigs.proof.core - sidekick.sigs.proof.sat sidekick.util sidekick.sigs.cc)) diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml deleted file mode 100644 index c44b5f83..00000000 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ /dev/null @@ -1,1156 +0,0 @@ -(** Core of the SMT solver using Sidekick_sat - - Sidekick_sat (in src/sat/) is a modular SAT solver in - pure OCaml. - - This builds a SMT solver on top of it. -*) - -(** Argument to pass to the functor {!Make} in order to create a - new Msat-based SMT solver. *) -module type ARG = sig - open Sidekick_core - module T : TERM - module Lit : LIT with module T = T - module Proof_trace : PROOF_TRACE - - type step_id = Proof_trace.A.step_id - type rule = Proof_trace.A.rule - - module Rule_core : - Sidekick_sigs_proof_core.S - with type term = T.Term.t - and type lit = Lit.t - and type step_id = step_id - and type rule = rule - - module Rule_sat : - Sidekick_sigs_proof_sat.S - with type lit = Lit.t - and type step_id = step_id - and type rule = rule - - val view_as_cc : - T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) Sidekick_sigs_cc.View.t - - val mk_eq : T.Term.store -> T.Term.t -> T.Term.t -> T.Term.t - (** [mk_eq store t u] builds the term [t=u] *) - - val is_valid_literal : T.Term.t -> bool - (** Is this a valid boolean literal? (e.g. is it a closed term, not inside - a quantifier) *) -end - -module type S = Sidekick_sigs_smt.SOLVER - -module Registry : Sidekick_sigs_smt.REGISTRY = struct - (* registry keys *) - module type KEY = sig - type elt - - val id : int - - exception E of elt - end - - type 'a key = (module KEY with type elt = 'a) - type t = { tbl: exn Util.Int_tbl.t } [@@unboxed] - - let create () : t = { tbl = Util.Int_tbl.create 8 } - let n_ = ref 0 - - let create_key (type a) () : a key = - let id = !n_ in - incr n_; - let module K = struct - type elt = a - - exception E of a - - let id = id - end in - (module K) - - let get (type a) (self : t) (k : a key) : _ option = - let (module K : KEY with type elt = a) = k in - match Util.Int_tbl.get self.tbl K.id with - | Some (K.E x) -> Some x - | _ -> None - - let set (type a) (self : t) (k : a key) (v : a) : unit = - let (module K) = k in - Util.Int_tbl.replace self.tbl K.id (K.E v) -end - -(** Main functor to get a solver. *) -module Make (A : ARG) : - S - with module T = A.T - and module Lit = A.Lit - and module Proof_trace = A.Proof_trace = struct - module T = A.T - module Proof_trace = A.Proof_trace - module Lit = A.Lit - module Ty = T.Ty - module Term = T.Term - - open struct - module P = Proof_trace - module Rule_ = A.Rule_core - end - - type term = Term.t - type ty = Ty.t - type lit = Lit.t - type step_id = Proof_trace.A.step_id - type proof_trace = Proof_trace.t - - (* actions from the sat solver *) - type sat_acts = (lit, Proof_trace.t, step_id) Sidekick_sat.acts - - type th_combination_conflict = { - lits: lit list; - semantic: (bool * term * term) list; - (* set of semantic eqns/diseqns (ie true only in current model) *) - } - (** Conflict obtained during theory combination. It involves equalities - merged because of the current model so it's not a "true" conflict - and doesn't need to kill the current trail. *) - - (* the full argument to the congruence closure *) - module CC_arg = struct - module T = T - module Lit = Lit - module Proof_trace = Proof_trace - module Rule_core = A.Rule_core - - let view_as_cc = A.view_as_cc - - let[@inline] mk_lit_eq ?sign store t u = - A.Lit.atom ?sign store (A.mk_eq store t u) - end - - module CC = Sidekick_cc.Make (CC_arg) - module N = CC.E_node - - module Model = struct - type t = Empty | Map of term Term.Tbl.t - - let empty = Empty - - let mem = function - | Empty -> fun _ -> false - | Map tbl -> Term.Tbl.mem tbl - - let find = function - | Empty -> fun _ -> None - | Map tbl -> Term.Tbl.get tbl - - let eval = find - - let pp out = function - | Empty -> Fmt.string out "(model)" - | Map tbl -> - let pp_pair out (t, v) = - Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Term.pp v - in - Fmt.fprintf out "(@[model@ %a@])" (Util.pp_iter pp_pair) - (Term.Tbl.to_iter tbl) - end - - (* delayed actions. We avoid doing them on the spot because, when - triggered by a theory, they might go back to the theory "too early". *) - type delayed_action = - | DA_add_clause of { c: lit list; pr: step_id; keep: bool } - | DA_add_lit of { default_pol: bool option; lit: lit } - - (* TODO - let mk_cc_acts_ (pr : P.t) (a : sat_acts) : CC.actions = - let (module A) = a in - - (module struct - module T = T - module Lit = Lit - - type nonrec lit = lit - type nonrec term = term - type nonrec proof_trace = Proof_trace.t - type nonrec step_id = step_id - - let proof_trace () = pr - let[@inline] raise_conflict lits (pr : step_id) = A.raise_conflict lits pr - - let[@inline] raise_semantic_conflict lits semantic = - raise (Semantic_conflict { lits; semantic }) - - let[@inline] propagate lit ~reason = - let reason = Sidekick_sat.Consequence reason in - A.propagate lit reason - end) - *) - - (** Internal solver, given to theories and to Msat *) - module Solver_internal = struct - module T = T - module Proof_trace = Proof_trace - module Proof_rules = A.Rule_sat - module P_core_rules = A.Rule_core - module Lit = Lit - module CC = CC - module N = CC.E_node - - type nonrec proof_trace = Proof_trace.t - type nonrec step_id = step_id - type term = Term.t - type value = term - type ty = Ty.t - type lit = Lit.t - type term_store = Term.store - type clause_pool - type ty_store = Ty.store - - type th_states = - | Ths_nil - | Ths_cons : { - st: 'a; - push_level: 'a -> unit; - pop_levels: 'a -> int -> unit; - next: th_states; - } - -> th_states - - type theory_actions = sat_acts - - module Simplify = struct - type t = { - tst: term_store; - ty_st: ty_store; - proof: proof_trace; - mutable hooks: hook list; - (* store [t --> u by step_ids] in the cache. - We use a bag for the proof steps because it gives us structural - sharing of subproofs. *) - cache: (Term.t * step_id Bag.t) Term.Tbl.t; - } - - and hook = t -> term -> (term * step_id Iter.t) option - - let create tst ty_st ~proof : t = - { tst; ty_st; proof; hooks = []; cache = Term.Tbl.create 32 } - - let[@inline] tst self = self.tst - let[@inline] ty_st self = self.ty_st - let[@inline] proof self = self.proof - let add_hook self f = self.hooks <- f :: self.hooks - let clear self = Term.Tbl.clear self.cache - - let normalize (self : t) (t : Term.t) : (Term.t * step_id) option = - (* compute and cache normal form of [t] *) - let rec loop t : Term.t * _ Bag.t = - match Term.Tbl.find self.cache t with - | res -> res - | exception Not_found -> - let steps_u = ref Bag.empty in - let u = aux_rec ~steps:steps_u t self.hooks in - Term.Tbl.add self.cache t (u, !steps_u); - u, !steps_u - and loop_add ~steps t = - let u, pr_u = loop t in - steps := Bag.append !steps pr_u; - u - (* try each function in [hooks] successively, and rewrite subterms *) - and aux_rec ~steps t hooks : Term.t = - match hooks with - | [] -> - let u = Term.map_shallow self.tst (loop_add ~steps) t in - if Term.equal t u then - t - else - loop_add ~steps u - | h :: hooks_tl -> - (match h self t with - | None -> aux_rec ~steps t hooks_tl - | Some (u, _) when Term.equal t u -> aux_rec ~steps t hooks_tl - | Some (u, pr_u) -> - let bag_u = Bag.of_iter pr_u in - steps := Bag.append !steps bag_u; - let v, pr_v = loop u in - (* fixpoint *) - steps := Bag.append !steps pr_v; - v) - in - let u, pr_u = loop t in - if Term.equal t u then - None - else ( - (* proof: [sub_proofs |- t=u] by CC + subproof *) - let step = - P.add_step self.proof - @@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u) - in - Some (u, step) - ) - - let normalize_t self t = - match normalize self t with - | Some (u, pr_u) -> u, Some pr_u - | None -> t, None - end - - type simplify_hook = Simplify.hook - - module type PREPROCESS_ACTS = sig - val proof : proof_trace - val mk_lit : ?sign:bool -> term -> lit - val add_clause : lit list -> step_id -> unit - val add_lit : ?default_pol:bool -> lit -> unit - end - - type preprocess_actions = (module PREPROCESS_ACTS) - - module Registry = Registry - - type t = { - tst: Term.store; (** state for managing terms *) - ty_st: Ty.store; - cc: CC.t lazy_t; (** congruence closure *) - proof: proof_trace; (** proof logger *) - registry: Registry.t; - mutable on_progress: unit -> unit; - mutable on_partial_check: - (t -> theory_actions -> lit Iter.t -> unit) list; - mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list; - mutable on_th_combination: - (t -> theory_actions -> (term * value) Iter.t) list; - mutable preprocess: preprocess_hook list; - mutable model_ask: model_ask_hook list; - mutable model_complete: model_completion_hook list; - simp: Simplify.t; - preprocessed: unit Term.Tbl.t; - delayed_actions: delayed_action Queue.t; - mutable last_model: Model.t option; - mutable th_states: th_states; (** Set of theories *) - mutable level: int; - mutable complete: bool; - stat: Stat.t; - count_axiom: int Stat.counter; - count_preprocess_clause: int Stat.counter; - count_conflict: int Stat.counter; - count_propagate: int Stat.counter; - } - - and preprocess_hook = t -> preprocess_actions -> term -> unit - and model_ask_hook = recurse:(t -> N.t -> term) -> t -> N.t -> term option - and model_completion_hook = t -> add:(term -> term -> unit) -> unit - - type solver = t - - let[@inline] cc (t : t) = Lazy.force t.cc - let[@inline] tst t = t.tst - let[@inline] ty_st t = t.ty_st - let[@inline] proof self = self.proof - let stats t = t.stat - - let[@inline] has_delayed_actions self = - not (Queue.is_empty self.delayed_actions) - - let registry self = self.registry - let simplifier self = self.simp - let simplify_t self (t : Term.t) : _ option = Simplify.normalize self.simp t - let simp_t self (t : Term.t) : Term.t * _ = Simplify.normalize_t self.simp t - let add_simplifier (self : t) f : unit = Simplify.add_hook self.simp f - - let on_th_combination self f = - self.on_th_combination <- f :: self.on_th_combination - - let on_preprocess self f = self.preprocess <- f :: self.preprocess - - let on_model ?ask ?complete self = - Option.iter (fun f -> self.model_ask <- f :: self.model_ask) ask; - Option.iter - (fun f -> self.model_complete <- f :: self.model_complete) - complete; - () - - let[@inline] raise_conflict self (acts : theory_actions) c proof : 'a = - let (module A) = acts in - Stat.incr self.count_conflict; - A.raise_conflict c proof - - let[@inline] propagate self (acts : theory_actions) p ~reason : unit = - let (module A) = acts in - Stat.incr self.count_propagate; - A.propagate p (Sidekick_sat.Consequence reason) - - let[@inline] propagate_l self acts p cs proof : unit = - propagate self acts p ~reason:(fun () -> cs, proof) - - let add_sat_clause_ self (acts : theory_actions) ~keep lits - (proof : step_id) : unit = - let (module A) = acts in - Stat.incr self.count_axiom; - A.add_clause ~keep lits proof - - let add_sat_lit_ _self ?default_pol (acts : theory_actions) (lit : Lit.t) : - unit = - let (module A) = acts in - A.add_lit ?default_pol lit - - let delayed_add_lit (self : t) ?default_pol (lit : Lit.t) : unit = - Queue.push (DA_add_lit { default_pol; lit }) self.delayed_actions - - let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : - unit = - Queue.push (DA_add_clause { c; pr; keep }) self.delayed_actions - - (* preprocess a term. We assume the term has been simplified already. *) - 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 self.tst ?sign 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 - let acts = (module A : PREPROCESS_ACTS) in - - (* how to preprocess a term and its subterms *) - let rec preproc_rec_ t = - if not (Term.Tbl.mem self.preprocessed t) then ( - Term.Tbl.add self.preprocessed t (); - - (* process sub-terms first *) - Term.iter_shallow self.tst preproc_rec_ t; - - Log.debugf 50 (fun k -> k "(@[smt.preprocess@ %a@])" Term.pp t); - - (* signal boolean subterms, so as to decide them - in the SAT solver *) - if Ty.is_bool (Term.ty t) then ( - Log.debugf 5 (fun k -> - k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp t); - - (* make a literal *) - let lit = Lit.atom self.tst t in - (* ensure that SAT solver has a boolean atom for [u] *) - delayed_add_lit self lit; - - (* also map [sub] to this atom in the congruence closure, for propagation *) - let cc = cc self in - CC.set_as_lit cc (CC.add_term cc t) lit - ); - - List.iter (fun f -> f self acts t) self.preprocess - ) - in - preproc_rec_ t0 - - (* simplify literal, then preprocess the result *) - let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : - Lit.t * step_id option = - let t = Lit.term lit in - let sign = Lit.sign lit in - let u, pr = - match simplify_t self t with - | None -> t, None - | Some (u, pr_t_u) -> - Log.debugf 30 (fun k -> - k "(@[smt-solver.simplify@ :t %a@ :into %a@])" Term.pp t Term.pp u); - u, Some pr_t_u - in - preprocess_term_ self u; - Lit.atom self.tst ~sign u, pr - - let push_decision (self : t) (acts : theory_actions) (lit : lit) : unit = - let (module A) = acts in - (* make sure the literal is preprocessed *) - let lit, _ = simplify_and_preproc_lit_ self lit in - let sign = Lit.sign lit in - A.add_decision_lit (Lit.abs lit) sign - - module type ARR = sig - type 'a t - - val map : ('a -> 'b) -> 'a t -> 'b t - val to_iter : 'a t -> 'a Iter.t - end - - module Preprocess_clause (A : ARR) = struct - (* preprocess a clause's literals, possibly emitting a proof - for the preprocessing. *) - let top (self : t) (c : lit A.t) (pr_c : step_id) : lit A.t * step_id = - let steps = ref [] in - - (* simplify a literal, then preprocess it *) - let[@inline] simp_lit lit = - let lit, pr = simplify_and_preproc_lit_ self lit in - Option.iter (fun pr -> steps := pr :: !steps) pr; - lit - in - let c' = A.map simp_lit c in - - let pr_c' = - if !steps = [] then - pr_c - else ( - Stat.incr self.count_preprocess_clause; - P.add_step self.proof - @@ Rule_.lemma_rw_clause pr_c ~res:(A.to_iter c') - ~using:(Iter.of_list !steps) - ) - in - c', pr_c' - end - [@@inline] - - module PC_list = Preprocess_clause (CCList) - module PC_arr = Preprocess_clause (CCArray) - - let preprocess_clause_ = PC_list.top - let preprocess_clause_iarray_ = PC_arr.top - - module type PERFORM_ACTS = sig - type t - - val add_clause : solver -> t -> keep:bool -> lit list -> step_id -> unit - val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit - end - - module Perform_delayed (A : PERFORM_ACTS) = struct - (* perform actions that were delayed *) - let top (self : t) (acts : A.t) : unit = - while not (Queue.is_empty self.delayed_actions) do - let act = Queue.pop self.delayed_actions in - match act with - | DA_add_clause { c; pr = pr_c; keep } -> - let c', pr_c' = preprocess_clause_ self c pr_c in - A.add_clause self acts ~keep c' pr_c' - | DA_add_lit { default_pol; lit } -> - preprocess_term_ self (Lit.term lit); - A.add_lit self acts ?default_pol lit - done - end - [@@inline] - - module Perform_delayed_th = Perform_delayed (struct - type t = theory_actions - - let add_clause self acts ~keep c pr : unit = - add_sat_clause_ self acts ~keep c pr - - let add_lit self acts ?default_pol lit : unit = - add_sat_lit_ self acts ?default_pol lit - end) - - let[@inline] add_clause_temp self _acts c (proof : step_id) : unit = - let c, proof = preprocess_clause_ self c proof in - delayed_add_clause self ~keep:false c proof - - 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 (self : t) (_acts : theory_actions) ?sign t : lit = - Lit.atom self.tst ?sign 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 self.tst ?sign t in - let lit, _ = simplify_and_preproc_lit_ self lit in - delayed_add_lit self lit - - let on_final_check self f = self.on_final_check <- f :: self.on_final_check - - let on_partial_check self f = - self.on_partial_check <- f :: self.on_partial_check - - let on_cc_new_term self f = Event.on (CC.on_new_term (cc self)) ~f - let on_cc_pre_merge self f = Event.on (CC.on_pre_merge (cc self)) ~f - let on_cc_post_merge self f = Event.on (CC.on_post_merge (cc self)) ~f - let on_cc_conflict self f = Event.on (CC.on_conflict (cc self)) ~f - let on_cc_propagate self f = Event.on (CC.on_propagate (cc self)) ~f - let on_cc_is_subterm self f = Event.on (CC.on_is_subterm (cc self)) ~f - let cc_add_term self t = CC.add_term (cc self) t - let cc_mem_term self t = CC.mem_term (cc self) t - let cc_find self n = CC.find (cc self) n - - let cc_are_equal self t1 t2 = - let n1 = cc_add_term self t1 in - let n2 = cc_add_term self t2 in - N.equal (cc_find self n1) (cc_find self n2) - - let cc_resolve_expl self e : lit list * _ = - let r = CC.explain_expl (cc self) e in - r.lits, r.pr self.proof - - (* - let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e - - let cc_merge_t self acts t1 t2 e = - let cc_acts = mk_cc_acts_ self.proof acts in - cc_merge self cc_acts (cc_add_term self t1) (cc_add_term self t2) e - - let cc_raise_conflict_expl self acts e = - let cc_acts = mk_cc_acts_ self.proof acts in - CC.raise_conflict_from_expl (cc self) cc_acts e - *) - - (** {2 Interface with the SAT solver} *) - - let rec push_lvl_ = function - | Ths_nil -> () - | Ths_cons r -> - r.push_level r.st; - push_lvl_ r.next - - let rec pop_lvls_ n = function - | Ths_nil -> () - | Ths_cons r -> - r.pop_levels r.st n; - pop_lvls_ n r.next - - let push_level (self : t) : unit = - self.level <- 1 + self.level; - CC.push_level (cc self); - push_lvl_ self.th_states - - let pop_levels (self : t) n : unit = - self.last_model <- None; - self.level <- self.level - n; - CC.pop_levels (cc self) n; - pop_lvls_ n self.th_states - - (** {2 Model construction and theory combination} *) - - (* make model from the congruence closure *) - let mk_model_ (self : t) (lits : lit Iter.t) : Model.t = - Log.debug 1 "(smt.solver.mk-model)"; - Profile.with_ "smt-solver.mk-model" @@ fun () -> - let module M = Term.Tbl in - let { - cc = (lazy cc); - tst; - model_ask = model_ask_hooks; - model_complete; - _; - } = - self - in - - let model = M.create 128 in - - (* first, add all literals to the model using the given propositional model - [lits]. *) - lits (fun lit -> - let t, sign = Lit.signed_term lit in - M.replace model t (Term.bool tst sign)); - - (* populate with information from the CC *) - (* FIXME - CC.get_model_for_each_class cc (fun (_, ts, v) -> - Iter.iter - (fun n -> - let t = N.term n in - M.replace model t v) - ts); - *) - - (* complete model with theory specific values *) - let complete_with f = - f self ~add:(fun t u -> - if not (M.mem model t) then ( - Log.debugf 20 (fun k -> - k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp t - Term.pp u); - M.replace model t u - )) - in - List.iter complete_with model_complete; - - (* compute a value for [n]. *) - let rec val_for_class (n : N.t) : term = - Log.debugf 5 (fun k -> k "val-for-term %a" N.pp n); - let repr = CC.find cc n in - Log.debugf 5 (fun k -> k "val-for-term.repr %a" N.pp repr); - - (* see if a value is found already (always the case if it's a boolean) *) - match M.get model (N.term repr) with - | Some t_val -> - Log.debugf 5 (fun k -> k "cached val is %a" Term.pp t_val); - t_val - | None -> - (* try each model hook *) - let rec try_hooks_ = function - | [] -> N.term repr - | h :: hooks -> - (match h ~recurse:(fun _ n -> val_for_class n) self repr with - | None -> try_hooks_ hooks - | Some t -> t) - in - - let t_val = - try_hooks_ model_ask_hooks - (* FIXME: the more complete version? - match - (* look for a value in the model for any term in the class *) - N.iter_class repr - |> Iter.find_map (fun n -> M.get model (N.term n)) - with - | Some v -> v - | None -> try_hooks_ model_ask_hooks - *) - in - - M.replace model (N.term repr) t_val; - (* be sure to cache the value *) - Log.debugf 5 (fun k -> k "val is %a" Term.pp t_val); - t_val - in - - (* map terms of each CC class to the value computed for their class. *) - CC.all_classes cc (fun repr -> - let t_val = val_for_class repr in - (* value for this class *) - N.iter_class repr (fun u -> - let t_u = N.term u in - if (not (N.equal u repr)) && not (Term.equal t_u t_val) then - M.replace model t_u t_val)); - Model.Map model - - (* do theory combination using the congruence closure. Each theory - can merge classes, *) - let check_th_combination_ (self : t) (_acts : theory_actions) lits : - (Model.t, th_combination_conflict) result = - (* FIXME - - (* enter model mode, disabling most of congruence closure *) - CC.with_model_mode cc @@ fun () -> - let set_val (t, v) : unit = - Log.debugf 50 (fun k -> - k "(@[solver.th-comb.cc-set-term-value@ %a@ :val %a@])" Term.pp t - Term.pp v); - CC.set_model_value cc t v - in - - (* obtain assignments from the hook, and communicate them to the CC *) - let add_th_values f : unit = - let vals = f self acts in - Iter.iter set_val vals - in - try - List.iter add_th_values self.on_th_combination; - CC.check cc; - let m = mk_model_ self in - Ok m - with Semantic_conflict c -> Error c - *) - let m = mk_model_ self lits in - Ok m - - (* call congruence closure, perform the actions it scheduled *) - let check_cc_with_acts_ (self : t) (acts : theory_actions) = - let (module A) = acts in - let cc = cc self in - match CC.check cc with - | Ok acts -> - List.iter - (function - | CC.Result_action.Act_propagate { lit; reason } -> - let reason = Sidekick_sat.Consequence reason in - A.propagate lit reason) - acts - | Error (CC.Result_action.Conflict (lits, pr)) -> A.raise_conflict lits pr - - (* handle a literal assumed by the SAT solver *) - let assert_lits_ ~final (self : t) (acts : theory_actions) - (lits : Lit.t Iter.t) : unit = - Log.debugf 2 (fun k -> - k "(@[@{smt-solver.assume_lits@}%s[lvl=%d]@ %a@])" - (if final then - "[final]" - else - "") - self.level - (Util.pp_iter ~sep:"; " Lit.pp) - lits); - (* transmit to CC *) - let cc = cc self in - - if not final then CC.assert_lits cc lits; - (* transmit to theories. *) - check_cc_with_acts_ self acts; - if final then ( - List.iter (fun f -> f self acts lits) self.on_final_check; - check_cc_with_acts_ self acts; - - (match check_th_combination_ self acts lits with - | Ok m -> self.last_model <- Some m - | Error { lits; semantic } -> - (* bad model, we add a clause to remove it *) - Log.debugf 5 (fun k -> - k - "(@[solver.th-comb.conflict@ :lits (@[%a@])@ :same-val \ - (@[%a@])@])" - (Util.pp_list Lit.pp) lits - (Util.pp_list @@ Fmt.Dump.(triple bool Term.pp Term.pp)) - semantic); - - let c1 = List.rev_map Lit.neg lits in - let c2 = - semantic - |> List.rev_map (fun (sign, t, u) -> - let eqn = A.mk_eq self.tst t u 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) - in - - let c = List.rev_append c1 c2 in - let pr = P.add_step self.proof @@ Rule_.lemma_cc (Iter.of_list c) in - - Log.debugf 20 (fun k -> - k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])" - (Util.pp_list Lit.pp) c); - (* will add a delayed action *) - add_clause_temp self acts c pr); - - Perform_delayed_th.top self acts - ) else ( - List.iter (fun f -> f self acts lits) self.on_partial_check; - Perform_delayed_th.top self acts - ); - () - - let[@inline] iter_atoms_ (acts : theory_actions) : _ Iter.t = - fun f -> - let (module A) = acts in - A.iter_assumptions f - - (* propagation from the bool solver *) - let check_ ~final (self : t) (acts : sat_acts) = - let pb = - if final then - Profile.begin_ "solver.final-check" - else - Profile.null_probe - in - let iter = iter_atoms_ acts in - Log.debugf 5 (fun k -> k "(smt-solver.assume :len %d)" (Iter.length iter)); - self.on_progress (); - assert_lits_ ~final self acts iter; - Profile.exit pb - - (* propagation from the bool solver *) - let[@inline] partial_check (self : t) (acts : _ Sidekick_sat.acts) : unit = - check_ ~final:false self acts - - (* perform final check of the model *) - let[@inline] final_check (self : t) (acts : _ Sidekick_sat.acts) : unit = - check_ ~final:true self acts - - let declare_pb_is_incomplete self = - if self.complete then Log.debug 1 "(solver.declare-pb-is-incomplete)"; - self.complete <- false - - let create ~stat ~proof (tst : Term.store) (ty_st : Ty.store) () : t = - let rec self = - { - tst; - ty_st; - cc = - lazy - ((* lazily tie the knot *) - CC.create ~size:`Big self.tst self.proof); - proof; - th_states = Ths_nil; - stat; - simp = Simplify.create tst ty_st ~proof; - last_model = None; - on_progress = (fun () -> ()); - preprocess = []; - model_ask = []; - model_complete = []; - registry = Registry.create (); - preprocessed = Term.Tbl.create 32; - delayed_actions = Queue.create (); - count_axiom = Stat.mk_int stat "solver.th-axioms"; - count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause"; - count_propagate = Stat.mk_int stat "solver.th-propagations"; - count_conflict = Stat.mk_int stat "solver.th-conflicts"; - on_partial_check = []; - on_final_check = []; - on_th_combination = []; - level = 0; - complete = true; - } - in - ignore (Lazy.force @@ self.cc : CC.t); - self - end - - module Sat_solver = Sidekick_sat.Make_cdcl_t (Solver_internal) - (** the parametrized SAT Solver *) - - module Registry = Solver_internal.Registry - - module type THEORY = sig - type t - - val name : string - val create_and_setup : Solver_internal.t -> t - val push_level : t -> unit - val pop_levels : t -> int -> unit - end - - type theory = (module THEORY) - type 'a theory_p = (module THEORY with type t = 'a) - - (** {2 Result} *) - - module Unknown = struct - type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop - - let pp out = function - | U_timeout -> Fmt.string out {|"timeout"|} - | U_max_depth -> Fmt.string out {|"max depth reached"|} - | U_incomplete -> Fmt.string out {|"incomplete fragment"|} - | U_asked_to_stop -> Fmt.string out {|"asked to stop by callback"|} - end - [@@ocaml.warning "-37"] - - type res = - | Sat of Model.t - | Unsat of { - unsat_core: unit -> lit Iter.t; - (** Unsat core (subset of assumptions), or empty *) - unsat_step_id: unit -> step_id option; - (** Proof step for the empty clause *) - } - | Unknown of Unknown.t - (** Result of solving for the current set of clauses *) - - (* main solver state *) - type t = { - si: Solver_internal.t; - solver: Sat_solver.t; - mutable last_res: res option; - stat: Stat.t; - proof: P.t; - count_clause: int Stat.counter; - count_solve: int Stat.counter; (* config: Config.t *) - } - - type solver = t - - (** {2 Main} *) - - let add_theory_p (type a) (self : t) (th : a theory_p) : a = - let (module Th) = th in - Log.debugf 2 (fun k -> k "(@[smt-solver.add-theory@ :name %S@])" Th.name); - let st = Th.create_and_setup self.si in - (* add push/pop to the internal solver *) - (let open Solver_internal in - self.si.th_states <- - Ths_cons - { - st; - push_level = Th.push_level; - pop_levels = Th.pop_levels; - next = self.si.th_states; - }); - st - - let add_theory (self : t) (th : theory) : unit = - let (module Th) = th in - ignore (add_theory_p self (module Th)) - - let add_theory_l self = List.iter (add_theory self) - - (* create a new solver *) - let create ?(stat = Stat.global) ?size ~proof ~theories tst ty_st () : t = - Log.debug 5 "smt-solver.create"; - let si = Solver_internal.create ~stat ~proof tst ty_st () in - let self = - { - si; - proof; - last_res = None; - solver = Sat_solver.create ~proof ?size ~stat si; - stat; - count_clause = Stat.mk_int stat "solver.add-clause"; - count_solve = Stat.mk_int stat "solver.solve"; - } - in - add_theory_l self theories; - (* assert [true] and [not false] *) - (let tst = Solver_internal.tst self.si in - let t_true = Term.bool tst true in - Sat_solver.add_clause self.solver - [ Lit.atom tst t_true ] - (P.add_step self.proof @@ Rule_.lemma_true t_true)); - self - - let[@inline] solver self = self.solver - let[@inline] cc self = Solver_internal.cc self.si - let[@inline] stats self = self.stat - let[@inline] tst self = Solver_internal.tst self.si - let[@inline] ty_st self = Solver_internal.ty_st self.si - let[@inline] proof self = self.si.proof - let[@inline] last_res self = self.last_res - let[@inline] registry self = Solver_internal.registry self.si - let reset_last_res_ self = self.last_res <- None - - (* preprocess clause, return new proof *) - let preprocess_clause_ (self : t) (c : lit array) (pr : step_id) : - lit array * step_id = - Solver_internal.preprocess_clause_iarray_ self.si c pr - - let mk_lit_t (self : t) ?sign (t : term) : lit = - let lit = Lit.atom self.si.tst ?sign t in - let lit, _ = Solver_internal.simplify_and_preproc_lit_ self.si lit in - lit - - (** {2 Main} *) - - let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self) - - (* add [c], without preprocessing its literals *) - let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit - = - Stat.incr self.count_clause; - reset_last_res_ self; - Log.debugf 50 (fun k -> - k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c); - let pb = Profile.begin_ "add-clause" in - Sat_solver.add_clause_a self.solver (c :> lit array) proof; - Profile.exit pb - - let add_clause_nopreproc_l_ self c p = - add_clause_nopreproc_ self (CCArray.of_list c) p - - module Perform_delayed_ = Solver_internal.Perform_delayed (struct - type nonrec t = t - - let add_clause _si solver ~keep:_ c pr : unit = - add_clause_nopreproc_l_ solver c pr - - let add_lit _si solver ?default_pol lit : unit = - Sat_solver.add_lit solver.solver ?default_pol lit - end) - - let add_clause (self : t) (c : lit array) (proof : step_id) : unit = - let c, proof = preprocess_clause_ self c proof in - add_clause_nopreproc_ self c proof; - Perform_delayed_.top self.si self; - (* finish preproc *) - () - - let add_clause_l self c p = add_clause self (CCArray.of_list c) p - - let assert_terms self c = - let c = CCList.map (fun t -> Lit.atom (tst self) t) c in - let pr_c = - P.add_step self.proof @@ A.Rule_sat.sat_input_clause (Iter.of_list c) - in - add_clause_l self c pr_c - - let assert_term self t = assert_terms self [ t ] - - exception Resource_exhausted = Sidekick_sat.Resource_exhausted - - let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ()) - ?(should_stop = fun _ _ -> false) ~assumptions (self : t) : res = - Profile.with_ "smt-solver.solve" @@ fun () -> - let do_on_exit () = List.iter (fun f -> f ()) on_exit in - - let on_progress = - let resource_counter = ref 0 in - fun () -> - incr resource_counter; - on_progress self; - if should_stop self !resource_counter then - raise_notrace Resource_exhausted - in - self.si.on_progress <- on_progress; - - let res = - match - Stat.incr self.count_solve; - Sat_solver.solve ~on_progress ~assumptions (solver self) - with - | Sat_solver.Sat _ when not self.si.complete -> - Log.debugf 1 (fun k -> - k - "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason \ - incomplete-fragment@])"); - Unknown Unknown.U_incomplete - | Sat_solver.Sat _ -> - Log.debug 1 "(sidekick.smt-solver: SAT)"; - - Log.debugf 5 (fun k -> - let ppc out n = - Fmt.fprintf out "{@[class@ %a@]}" (Util.pp_iter N.pp) - (N.iter_class n) - in - k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" (Util.pp_iter ppc) - (CC.all_classes @@ Solver_internal.cc self.si)); - - let m = - match self.si.last_model with - | Some m -> m - | None -> assert false - in - (* TODO: check model *) - let _ = check in - - do_on_exit (); - Sat m - | Sat_solver.Unsat (module UNSAT) -> - let unsat_core () = UNSAT.unsat_assumptions () in - let unsat_step_id () = Some (UNSAT.unsat_proof ()) in - do_on_exit (); - Unsat { unsat_core; unsat_step_id } - | exception Resource_exhausted -> Unknown Unknown.U_asked_to_stop - in - self.last_res <- Some res; - res - - let push_assumption self a = - reset_last_res_ self; - Sat_solver.push_assumption self.solver a - - let pop_assumptions self n = - reset_last_res_ self; - Sat_solver.pop_assumptions self.solver n - - type propagation_result = - | PR_sat - | PR_conflict of { backtracked: int } - | PR_unsat of { unsat_core: unit -> lit Iter.t } - - let check_sat_propagations_only ~assumptions self : propagation_result = - reset_last_res_ self; - match Sat_solver.check_sat_propagations_only ~assumptions self.solver with - | Sat_solver.PR_sat -> PR_sat - | Sat_solver.PR_conflict { backtracked } -> PR_conflict { backtracked } - | Sat_solver.PR_unsat (module UNSAT) -> - let unsat_core () = UNSAT.unsat_assumptions () in - PR_unsat { unsat_core } - - let mk_theory (type st) ~name ~create_and_setup ?(push_level = fun _ -> ()) - ?(pop_levels = fun _ _ -> ()) () : theory = - let module Th = struct - type t = st - - let name = name - let create_and_setup = create_and_setup - let push_level = push_level - let pop_levels = pop_levels - end in - (module Th : THEORY) -end diff --git a/src/smt-solver/dune b/src/smt-solver/dune deleted file mode 100644 index 42a88c50..00000000 --- a/src/smt-solver/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name Sidekick_smt_solver) - (public_name sidekick.smt-solver) - (libraries containers iter sidekick.sigs.smt sidekick.util sidekick.cc - sidekick.sat) - (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/smt-solver/th_key.ml.bak b/src/smt-solver/th_key.ml.bak deleted file mode 100644 index cd8c7194..00000000 --- a/src/smt-solver/th_key.ml.bak +++ /dev/null @@ -1,145 +0,0 @@ - - -module type S = sig - type ('term,'lit,'a) t - (** An access key for theories which have per-class data ['a] *) - - val create : - ?pp:'a Fmt.printer -> - name:string -> - eq:('a -> 'a -> bool) -> - merge:('a -> 'a -> 'a) -> - unit -> - ('term,'lit,'a) t - (** Generative creation of keys for the given theory data. - - @param eq : Equality. This is used to optimize backtracking info. - - @param merge : - [merge d1 d2] is called when merging classes with data [d1] and [d2] - respectively. The theory should already have checked that the merge - is compatible, and this produces the combined data for terms in the - merged class. - @param name name of the theory which owns this data - @param pp a printer for the data - *) - - val equal : ('t,'lit,_) t -> ('t,'lit,_) t -> bool - (** Checks if two keys are equal (generatively) *) - - val pp : _ t Fmt.printer - (** Prints the name of the key. *) -end - - -(** Custom keys for theory data. - This imitates the classic tricks for heterogeneous maps - https://blog.janestreet.com/a-universal-type/ - - It needs to form a commutative monoid where values are persistent so - they can be restored during backtracking. -*) -module Key = struct - module type KEY_IMPL = sig - type term - type lit - type t - val id : int - val name : string - val pp : t Fmt.printer - val equal : t -> t -> bool - val merge : t -> t -> t - exception Store of t - end - - type ('term,'lit,'a) t = - (module KEY_IMPL with type term = 'term and type lit = 'lit and type t = 'a) - - let n_ = ref 0 - - let create (type term)(type lit)(type d) - ?(pp=fun out _ -> Fmt.string out "") - ~name ~eq ~merge () : (term,lit,d) t = - let module K = struct - type nonrec term = term - type nonrec lit = lit - type t = d - let id = !n_ - let name = name - let pp = pp - let merge = merge - let equal = eq - exception Store of d - end in - incr n_; - (module K) - - let[@inline] id - : type term lit a. (term,lit,a) t -> int - = fun (module K) -> K.id - - let[@inline] equal - : type term lit a b. (term,lit,a) t -> (term,lit,b) t -> bool - = fun (module K1) (module K2) -> K1.id = K2.id - - let pp - : type term lit a. (term,lit,a) t Fmt.printer - = fun out (module K) -> Fmt.string out K.name -end - - - -(* - (** Map for theory data associated with representatives *) - module K_map = struct - type 'a key = (term,lit,'a) Key.t - type pair = Pair : 'a key * exn -> pair - - type t = pair IM.t - - let empty = IM.empty - - let[@inline] mem k t = IM.mem (Key.id k) t - - let find (type a) (k : a key) (self:t) : a option = - let (module K) = k in - match IM.find K.id self with - | Pair (_, K.Store v) -> Some v - | _ -> None - | exception Not_found -> None - - let add (type a) (k : a key) (v:a) (self:t) : t = - let (module K) = k in - IM.add K.id (Pair (k, K.Store v)) self - - let remove (type a) (k: a key) self : t = - let (module K) = k in - IM.remove K.id self - - let equal (m1:t) (m2:t) : bool = - IM.equal - (fun p1 p2 -> - let Pair ((module K1), v1) = p1 in - let Pair ((module K2), v2) = p2 in - assert (K1.id = K2.id); - match v1, v2 with K1.Store v1, K1.Store v2 -> K1.equal v1 v2 | _ -> false) - m1 m2 - - let merge ~f_both (m1:t) (m2:t) : t = - IM.merge - (fun _ p1 p2 -> - match p1, p2 with - | None, None -> None - | Some v, None - | None, Some v -> Some v - | Some (Pair ((module K1) as key1, pair1)), Some (Pair (_, pair2)) -> - match pair1, pair2 with - | K1.Store v1, K1.Store v2 -> - f_both K1.id pair1 pair2; (* callback for checking compat *) - let v12 = K1.merge v1 v2 in (* merge content *) - Some (Pair (key1, K1.Store v12)) - | _ -> assert false - ) - m1 m2 - end - *) diff --git a/src/smt/Sidekick_smt_solver.ml b/src/smt/Sidekick_smt_solver.ml index 9ab1530d..a0e5b0c7 100644 --- a/src/smt/Sidekick_smt_solver.ml +++ b/src/smt/Sidekick_smt_solver.ml @@ -9,6 +9,9 @@ module Sigs = Sigs module Model = Model module Registry = Registry -module Simplify = Simplify module Solver_internal = Solver_internal module Solver = Solver +module Theory = Theory + +type theory = Theory.t +type solver = Solver.t diff --git a/src/th-cstor/Sidekick_th_cstor.mli b/src/th-cstor/Sidekick_th_cstor.mli new file mode 100644 index 00000000..0cf658a9 --- /dev/null +++ b/src/th-cstor/Sidekick_th_cstor.mli @@ -0,0 +1,13 @@ +(** Theory for constructors *) + +open Sidekick_core +module SMT = Sidekick_smt_solver + +type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't + +module type ARG = sig + val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view + val lemma_cstor : Lit.t Iter.t -> Proof_term.t +end + +val make : (module ARG) -> SMT.theory