simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: use msat 0.8

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 20:57:44 -06:00
parent 27d1841f6b
commit a57fdcdeda
11 changed files with 133 additions and 130 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/main/main.ml
View file

@ -12,6 +12,7 @@ module Term = Sidekick_smt.Term
module Ast = Sidekick_smt.Ast
module Solver = Sidekick_smt.Solver
module Process = Sidekick_smtlib.Process
module Vec = Msat.Vec
type 'a or_error = ('a, string) E.t
@ -78,7 +79,7 @@ let argspec = Arg.align [
"-no-p", Arg.Clear p_progress, " no progress bar";
"-size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
"-time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
"-v", Arg.Int Sidekick_sat.Log.set_debug, "<lvl> sets the debug verbose level";
"-v", Arg.Int Sidekick_smt.Log.set_debug, "<lvl> sets the debug verbose level";
]
type syntax =
@ -123,7 +124,7 @@ let main () =
(* process statements *)
let res =
try
let hyps = Vec.make_empty [] in
let hyps = Vec.create() in
E.fold_l
(fun () ->
Process.process_stmt
@ -160,6 +161,9 @@ let () = match main() with
| Out_of_space ->
Format.printf "Spaceout@.";
exit 3
| Invalid_argument e ->
Format.printf "invalid argument:\n%s@." e;
exit 127
| _ -> raise e
end;
if Printexc.backtrace_status () then (

9
src/smt/Congruence_closure.ml
View file

@ -68,6 +68,8 @@ let rec find_rec cc (n:node) : repr =
if n==n.n_root then (
n
) else (
(* TODO: path compression, assuming backtracking restores equiv classes
properly *)
let root = find_rec cc n.n_root in
root
)
@ -127,7 +129,7 @@ let signature cc (t:term): node Term.view option =
| App_cst (f, a) -> Some (App_cst (f, IArray.map find a)) (* FIXME: relevance? *)
| Bool _ | If _
-> None (* no congruence for these *)
end
end
(* find whether the given (parent) term corresponds to some signature
in [signatures_] *)
@ -193,6 +195,7 @@ let[@inline][@unroll 2] rec distance_to_root (n:node): int = match n.n_expl with
| E_none -> 0
| E_some {next=t'; _} -> 1 + distance_to_root t'
(* TODO: bool flag on nodes + stepwise progress + cleanup *)
(* find the closest common ancestor of [a] and [b] in the proof forest *)
let find_common_ancestor (a:node) (b:node) : node =
let d_a = distance_to_root a in
@ -647,6 +650,10 @@ let create ?on_merge ?(size=`Big) (tst:Term.state) : t =
ignore (Lazy.force false_ : node);
cc
let[@inline] find_t cc t : repr =
let n = Term.Tbl.find cc.tbl t in
find cc n
let[@inline] check cc acts : unit =
Log.debug 5 "(CC.check)";
update_tasks cc acts

4
src/smt/Congruence_closure.mli
View file

@ -29,6 +29,10 @@ val add : t -> term -> node
(** Add the term to the congruence closure, if not present already.
Will be backtracked. *)
val find_t : t -> term -> repr
(** Current representative of the term.
@raise Not_found if the term is not already {!add}-ed. *)
val add_seq : t -> term Sequence.t -> unit
(** Add a sequence of terms to the congruence closure *)

26
src/smt/Sidekick_smt.ml Normal file
View file

@ -0,0 +1,26 @@
module ID = ID
module Ty_card = Ty_card
module Cst = Cst
module Stat = Stat
module Model = Model
module Ast = Ast
module Term = Term
module Value = Value
module Term_cell = Term_cell
module Ty = Ty
module Equiv_class = Equiv_class
module Lit = Lit
module Explanation = Explanation
module Congruence_closure = Congruence_closure
module Theory_combine = Theory_combine
module Theory = Theory
module Solver = Solver
module Solver_types = Solver_types
(**/**)
module Bag = Bag
module Vec = Msat.Vec
module Log = Msat.Log
(**/**)

11
src/smt/Solver.ml
View file

@ -16,6 +16,7 @@ module Sat_solver = Msat.Make_cdcl_t(Theory_combine)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
module Atom = Sat_solver.Atom
module Proof = struct
type t = Sat_solver.Proof.t
@ -41,7 +42,6 @@ module Proof = struct
() p;
Format.fprintf out "@])";
()
end
(* main solver state *)
@ -58,6 +58,11 @@ let[@inline] cc self = Theory_combine.cc (th_combine self)
let stats self = self.stat
let[@inline] tst self = Theory_combine.tst (th_combine self)
let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
let[@inline] mk_atom_t self ?sign t : Atom.t =
let lit = Lit.atom ?sign t in
mk_atom_lit self lit
let create ?size ?(config=Config.empty) ~theories () : t =
let th_combine = Theory_combine.create() in
let self = {
@ -212,13 +217,14 @@ let check_model (_s:t) : unit =
(* TODO: main loop with iterative deepening of the unrolling limit
(not the value depth limit) *)
let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res =
let solve ?(on_exit=[]) ?check:(_=true) ~assumptions (self:t) : res =
let r = Sat_solver.solve ~assumptions (solver self) in
match r with
| Sat_solver.Sat st ->
Log.debugf 0 (fun k->k "SAT");
let lits f = st.iter_trail f (fun _ -> ()) in
let m = Theory_combine.mk_model (th_combine self) lits in
do_on_exit ~on_exit;
Sat m
(*
let env = Ast.env_empty in
@ -228,6 +234,7 @@ let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res =
*)
| Sat_solver.Unsat us ->
let pr = us.get_proof () in
do_on_exit ~on_exit;
Unsat pr
(* FIXME:

10
src/smt/Solver.mli
View file

@ -6,7 +6,7 @@
The solving algorithm, based on MCSat *)
module Sat_solver : Msat.S
with module Formula = Lit
with type Formula.t = Lit.t
and type theory = Theory_combine.t
and type lemma = Theory_combine.proof
@ -14,6 +14,8 @@ module Sat_solver : Msat.S
type model = Model.t
module Atom = Sat_solver.Atom
module Proof : sig
type t = Sat_solver.Proof.t
@ -49,16 +51,18 @@ val cc : t -> Congruence_closure.t
val stats : t -> Stat.t
val tst : t -> Term.state
val mk_atom_lit : t -> Lit.t -> Atom.t
val mk_atom_t : t -> ?sign:bool -> Term.t -> Atom.t
val assume : t -> Lit.t IArray.t -> unit
val assume_eq : t -> Term.t -> Term.t -> Lit.t -> unit
val assume_distinct : t -> Term.t list -> neq:Term.t -> Lit.t -> unit
val solve :
?restarts:bool ->
?on_exit:(unit -> unit) list ->
?check:bool ->
assumptions:Lit.t list ->
assumptions:Atom.t list ->
t ->
res
(** [solve s] checks the satisfiability of the statement added so far to [s]

2
src/smt/Solver_types.ml
View file

@ -140,7 +140,7 @@ and value_custom_view = ..
type proof = Proof_default
type sat_actions = (Msat.void, lit, value, proof) Msat.acts
type sat_actions = (Msat.void, lit, Msat.void, proof) Msat.acts
let[@inline] term_equal_ (a:term) b = a==b
let[@inline] term_hash_ a = a.term_id

7
src/smt/Theory.ml
View file

@ -20,9 +20,6 @@ type conflict = Lit.t list
(** Actions available to a theory during its lifetime *)
module type ACTIONS = sig
val on_backtrack: (unit -> unit) -> unit
(** Register an action to do when we backtrack *)
val raise_conflict: conflict -> 'a
(** Give a conflict clause to the solver *)
@ -36,11 +33,11 @@ module type ACTIONS = sig
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_local_axiom: Lit.t IArray.t -> unit
val add_local_axiom: Lit.t list -> unit
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
val add_persistent_axiom: Lit.t IArray.t -> unit
val add_persistent_axiom: Lit.t list -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)

147
src/smt/Theory_combine.ml
View file

@ -11,7 +11,7 @@ module Proof = struct
let default = Proof_default
end
module Form = Lit
module Formula = Lit
type formula = Lit.t
type proof = Proof.t
@ -28,39 +28,46 @@ type t = {
(** congruence closure *)
mutable theories : theory_state list;
(** Set of theories *)
new_merges: (Equiv_class.t * Equiv_class.t * explanation) Vec.t;
}
let[@inline] cc t = Lazy.force t.cc
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let[@inline] theories (self:t) : theory_state Sequence.t =
fun k -> List.iter k self.theories
(** {2 Interface with the SAT solver} *)
module Plugin = struct
(* handle a literal assumed by the SAT solver *)
let assert_lits (self:t) acts (lits:Lit.t Sequence.t) : unit =
let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit =
Msat.Log.debugf 2
(fun k->k "(@[<1>@{<green>th_combine.assume_lits@}@ @[%a@]@])" (Fmt.seq Lit.pp) lits);
(* transmit to CC *)
Vec.clear self.new_merges;
let cc = cc self in
C_clos.assert_lits cc lits;
(* transmit to theories. *)
C_clos.assert_lits (cc self) lits;
C_clos.check (cc self) acts;
theories self (fun (Th_state ((module Th),st)) -> Th.partial_check st acts lits);
C_clos.check cc acts;
let module A = struct
let[@inline] raise_conflict c : 'a = acts.Msat.acts_raise_conflict c Proof_default
let[@inline] propagate_eq t u expl : unit = C_clos.assert_eq cc t u expl
let propagate_distinct ts ~neq expl = C_clos.assert_distinct cc ts ~neq expl
let[@inline] propagate p cs : unit = acts.Msat.acts_propagate p (Msat.Consequence (cs, Proof_default))
let[@inline] add_local_axiom lits : unit =
acts.Msat.acts_add_clause ~keep:false lits Proof_default
let[@inline] add_persistent_axiom lits : unit =
acts.Msat.acts_add_clause ~keep:true lits Proof_default
let[@inline] find t = C_clos.find_t cc t
let all_classes = C_clos.all_classes cc
end in
let acts = (module A : Theory.ACTIONS) in
theories self
(fun (Th_state ((module Th),st)) ->
(* give new merges, then call {final,partial}-check *)
Vec.iter (fun (r1,r2,e) -> Th.on_merge st acts r1 r2 e) self.new_merges;
if final then Th.final_check st acts lits else Th.partial_check st acts lits);
()
(* TODO: remove
let with_conflict_catch acts f =
try
f ();
with Exn_conflict lit_set ->
let conflict_clause = IArray.of_list_map Lit.neg lit_set in
Msat.Log.debugf 3
(fun k->k "(@[<1>@{<yellow>th_combine.conflict@}@ :clause %a@])"
Theory.Clause.pp conflict_clause);
acts.Msat.acts_raise_conflict (IArray.to_list conflict_clause) Proof.default
*)
let[@inline] iter_atoms_ acts : _ Sequence.t =
fun f ->
acts.Msat.acts_iter_assumptions
@ -69,12 +76,11 @@ let[@inline] iter_atoms_ acts : _ Sequence.t =
| Msat.Assign _ -> assert false)
(* propagation from the bool solver *)
let check_ (self:t) (acts:_ Msat.acts) =
let check_ ~final (self:t) (acts:_ Msat.acts) =
let iter = iter_atoms_ acts in
(* TODO if Config.progress then print_progress(); *)
Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Sequence.length iter));
iter (assume_lit self);
Congruence_closure.check (cc self) acts
assert_lits_ ~final self acts iter
let add_formula (self:t) (lit:Lit.t) =
let t = Lit.view lit in
@ -84,43 +90,35 @@ let add_formula (self:t) (lit:Lit.t) =
()
(* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) =
check_ self acts
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:false self acts
(* perform final check of the model *)
let final_check (self:t) (acts:_ Msat.acts) : unit =
(* all formulas in the SAT solver's trail *)
let iter = iter_atoms_ acts in
(* final check for CC + each theory *)
Congruence_closure.check (cc self) acts;
theories self
(fun (module Th) -> Th.final_check Th.state iter)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:true self acts
let push_level (self:t) : unit =
C_clos.push_level (cc self);
theories self (fun (Th_state ((module Th), st)) -> Th.push_level st)
let pop_levels (self:t) n : unit =
C_clos.pop_levels (cc self) n;
theories self (fun (Th_state ((module Th), st)) -> Th.pop_levels st n)
let mk_model (self:t) lits : Model.t =
let m =
Sequence.fold
(fun m (module Th : Theory.STATE) -> Model.merge m (Th.mk_model Th.state lits))
(fun m (Th_state ((module Th),st)) -> Model.merge m (Th.mk_model st lits))
Model.empty (theories self)
in
(* now complete model using CC *)
Congruence_closure.mk_model (cc self) m
(** {2 Various helpers} *)
(* forward propagations from CC or theories directly to the SMT core *)
let act_propagate acts f guard : unit =
Msat.Log.debugf 2
(fun k->k "(@[@{<green>th.propagate@}@ %a@ :guard %a@])"
Lit.pp f (Util.pp_list Lit.pp) guard);
let reason = Msat.Consequence (guard,Proof.default) in
acts.Msat.acts_propagate f reason
(** {2 Interface to Congruence Closure} *)
(* when CC decided to merge [r1] and [r2], notify theories *)
let on_merge_from_cc (self:t) r1 r2 e : unit =
theories self
(fun (module Th) -> Th.on_merge Th.state r1 r2 e)
let[@inline] on_merge_from_cc (self:t) r1 r2 e : unit =
Vec.push self.new_merges (r1,r2,e)
(** {2 Main} *)
@ -129,6 +127,7 @@ let create () : t =
Log.debug 5 "th_combine.create";
let rec self = {
tst=Term.create ~size:1024 ();
new_merges=Vec.create();
cc = lazy (
(* lazily tie the knot *)
let on_merge = on_merge_from_cc self in
@ -139,61 +138,17 @@ let create () : t =
ignore (Lazy.force @@ self.cc : C_clos.t);
self
(** {2 Interface to individual theories} *)
let act_all_classes self = C_clos.all_classes (cc self)
let act_propagate_eq self t u guard =
C_clos.assert_eq (cc self) t u guard
let act_propagate_distinct self l ~neq guard =
C_clos.assert_distinct (cc self) l ~neq guard
let act_find self t =
C_clos.add (cc self) t
|> C_clos.find (cc self)
(* TODO: remove
let act_add_local_axiom self c : unit =
Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c);
A.push_local c Proof.default
(* push one clause into [M], in the current level (not a lemma but
an axiom) *)
let act_add_persistent_axiom self c : unit =
Log.debugf 5 (fun k->k "(@[<2>th_combine.push_persistent_lemma@ %a@])" Theory.Clause.pp c);
let (module A) = self.cdcl_acts in
A.push_persistent c Proof.default
*)
let check_invariants (self:t) =
if Util._CHECK_INVARIANTS then (
Congruence_closure.check_invariants (cc self);
)
let mk_theory_actions (self:t) : Theory.actions =
let (module A) = self.cdcl_acts in
let module R = struct
let on_backtrack = A.on_backtrack
let raise_conflict = act_raise_conflict
let propagate = act_propagate self
let all_classes = act_all_classes self
let propagate_eq = act_propagate_eq self
let propagate_distinct = act_propagate_distinct self
let add_local_axiom = act_add_local_axiom self
let add_persistent_axiom = act_add_persistent_axiom self
let find = act_find self
end
in (module R)
let add_theory (self:t) (th:Theory.t) : unit =
Sat_solver.Log.debugf 2
(fun k->k "(@[th_combine.add_th@ :name %S@])" th.Theory.name);
let th_s = th.Theory.make self.tst (mk_theory_actions self) in
self.theories <- th_s :: self.theories
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[th_combine.add_th@ :name %S@])" Th.name);
let st = Th.create self.tst in
(* re-pack as a [Theory.t1] *)
self.theories <- (Th_state ((module Th),st)) :: self.theories
let add_theory_l self = List.iter (add_theory self)
let post_backtrack self =
C_clos.post_backtrack (cc self);
theories self (fun (module Th) -> Th.post_backtrack Th.state)

33
src/smtlib/Process.ml
View file

@ -9,7 +9,7 @@ module E = CCResult
module A = Ast
module Form = Sidekick_th_bool
module Fmt = CCFormat
module Dot = Msat_backend.Dot.Simple(Solver.Sat_solver)
module Dot = Msat_backend.Dot.Make(Solver.Sat_solver)(Msat_backend.Dot.Default(Solver.Sat_solver))
module Subst = struct
type 'a t = 'a ID.Map.t
@ -222,19 +222,18 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
Log.debug 1 "(smt.check-smt-model)";
let open Solver_types in
let module S = Solver.Sat_solver in
let check_atom (lit:Lit.t) : bool option =
let check_atom (lit:Lit.t) : Msat.lbool =
Log.debugf 5 (fun k->k "(@[smt.check-smt-model.atom@ %a@])" Lit.pp lit);
let a = S.Atom.make solver lit in
let is_true = S.Atom.is_true a in
let is_false = S.Atom.is_true (S.Atom.neg a) in
let sat_value = if is_true then Some true else if is_false then Some false else None in
let a = S.make_atom solver lit in
let sat_value = S.eval_atom solver a in
let t, sign = Lit.as_atom lit in
begin match Model.eval m t with
| Some (V_bool b) ->
let b = if sign then b else not b in
if (is_true || is_false) && ((b && is_false) || (not b && is_true)) then (
Error.errorf "(@[check-model.error@ :atom %a@ :model-val %B@ :sat-val %B@])"
S.Atom.pp a b (if is_true then true else not is_false)
if (sat_value <> Msat.L_undefined) &&
((b && sat_value=Msat.L_false) || (not b && sat_value=Msat.L_true)) then (
Error.errorf "(@[check-model.error@ :atom %a@ :model-val %B@ :sat-val %a@])"
S.Atom.pp a b Msat.pp_lbool sat_value
) else (
Log.debugf 5
(fun k->k "(@[check-model@ :atom %a@ :model-val %B@ :no-sat-val@])" S.Atom.pp a b);
@ -243,18 +242,18 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
Error.errorf "(@[check-model.error@ :atom %a@ :non-bool-value %a@])"
S.Atom.pp a Value.pp v
| None ->
if is_true || is_false then (
Error.errorf "(@[check-model.error@ :atom %a@ :no-smt-value@ :sat-val %B@])"
S.Atom.pp a is_true
if sat_value <> Msat.L_undefined then (
Error.errorf "(@[check-model.error@ :atom %a@ :no-smt-value@ :sat-val %a@])"
S.Atom.pp a Msat.pp_lbool sat_value
);
end;
sat_value
in
let check_c c =
let bs = List.map check_atom c in
if List.for_all (function Some true -> false | _ -> true) bs then (
if List.for_all (function Msat.L_true -> false | _ -> true) bs then (
Error.errorf "(@[check-model.error.none-true@ :clause %a@ :vals %a@])"
(Fmt.Dump.list Lit.pp) c Fmt.(Dump.list @@ Dump.option bool) bs
(Fmt.Dump.list Lit.pp) c Fmt.(Dump.list @@ Msat.pp_lbool) bs
);
in
Vec.iter check_c hyps
@ -262,7 +261,7 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
(* call the solver to check-sat *)
let solve
?gc:_
?restarts
?restarts:_
?dot_proof
?(pp_model=false)
?(check=false)
@ -272,7 +271,7 @@ let solve
s : unit =
let t1 = Sys.time() in
let res =
Solver.solve ?restarts ~assumptions s
Solver.solve ~assumptions s
(* ?gc ?restarts ?time ?memory ?progress *)
in
let t2 = Sys.time () in
@ -297,7 +296,7 @@ let solve
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.print fmt p;
Dot.pp fmt p;
Format.pp_print_flush fmt (); flush oc)
end
);

6
src/th-bool/Sidekick_th_bool.ml
View file

@ -200,14 +200,14 @@ let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term vie
(* propagate [¬lit => ∨_i ¬ subs_i] *)
let subs = IArray.to_list subs in
let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
A.add_local_axiom (IArray.of_list c)
A.add_local_axiom c
)
| B_or subs ->
if Lit.sign lit then (
(* propagate [lit => ∨_i subs_i] *)
let subs = IArray.to_list subs in
let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
A.add_local_axiom (IArray.of_list c)
A.add_local_axiom c
) else (
(* propagate [¬lit => ¬subs_i] *)
IArray.iter
@ -221,7 +221,7 @@ let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term vie
(* propagate [lit => ∨_i ¬guard_i ∨ concl] *)
let guard = IArray.to_list guard in
let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
A.add_local_axiom (IArray.of_list c)
A.add_local_axiom c
) else (
(* propagate [¬lit => ¬concl] *)
A.propagate (Lit.atom ~sign:false concl) [lit];