mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
refactor some more
This commit is contained in:
Simon Cruanes
parent
0ff5ac9a3f
commit
36204c5e5e
11 changed files with 25 additions and 2748 deletions
|
|
@ -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))
|
|
||||||
|
|
@ -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
|
|
||||||
|
|
@ -88,3 +88,9 @@ let rec abs t =
|
||||||
let sign, v = abs u in
|
let sign, v = abs u in
|
||||||
Stdlib.not sign, v
|
Stdlib.not sign, v
|
||||||
| _ -> true, t
|
| _ -> 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
|
||||||
|
|
|
||||||
|
|
@ -31,3 +31,5 @@ val abs : t -> bool * t
|
||||||
The idea is that we want to turn [not a] into [(false, a)],
|
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
|
or [(a != b)] into [(false, a=b)]. For terms without a negation this
|
||||||
should return [(true, t)]. *)
|
should return [(true, t)]. *)
|
||||||
|
|
||||||
|
val as_bool_val : t -> bool option
|
||||||
|
|
|
||||||
|
|
@ -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
|
|
||||||
|
|
@ -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))
|
|
||||||
File diff suppressed because it is too large
Load diff
|
|
@ -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))
|
|
||||||
|
|
@ -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 "<opaque>")
|
|
||||||
~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
|
|
||||||
*)
|
|
||||||
|
|
@ -9,6 +9,9 @@
|
||||||
module Sigs = Sigs
|
module Sigs = Sigs
|
||||||
module Model = Model
|
module Model = Model
|
||||||
module Registry = Registry
|
module Registry = Registry
|
||||||
module Simplify = Simplify
|
|
||||||
module Solver_internal = Solver_internal
|
module Solver_internal = Solver_internal
|
||||||
module Solver = Solver
|
module Solver = Solver
|
||||||
|
module Theory = Theory
|
||||||
|
|
||||||
|
type theory = Theory.t
|
||||||
|
type solver = Solver.t
|
||||||
|
|
|
||||||
13
src/th-cstor/Sidekick_th_cstor.mli
Normal file
13
src/th-cstor/Sidekick_th_cstor.mli
Normal file
|
|
@ -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
|
||||||
Loading…
Add table
Reference in a new issue