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

refactor: use abstract-solver in smtlib driver; CDCL(T) implements asolver

Browse source 
this way we can add new SMT techniques without changing (much) the
driver.
This commit is contained in:
Simon Cruanes 2022-10-10 15:44:13 -04:00
parent d08c8fe165
commit a47bbf45e8
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
10 changed files with 83 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/main/main.ml
View file

@ -199,11 +199,12 @@ let main_smt ~config () : _ result =
(Sidekick_smt_solver.Theory.name th_bool));
[ th_bool; Driver.th_ty_unin; Driver.th_data; Driver.th_lra ]
in
Solver.create_default ~tracer ~proof ~theories tst
Solver.Smt_solver.Solver.create_default ~tracer ~proof ~theories tst ()
in
let finally () =
if !p_stat then Format.printf "%a@." Solver.pp_stats solver
if !p_stat then
Format.printf "%a@." Solver.Smt_solver.Solver.pp_stats solver
in
CCFun.protect ~finally @@ fun () ->
(* FIXME: emit an actual proof *)
@ -215,7 +216,7 @@ let main_smt ~config () : _ result =
in
if !check then
(* might have to check conflicts *)
Solver.add_theory solver Sidekick_smtlib.Check_cc.theory;
Solver.Smt_solver.Solver.add_theory solver Sidekick_smtlib.Check_cc.theory;
let parse_res =
let@ () = Profile.with_ "parse" ~args:[ "file", !file ] in
@ -224,9 +225,10 @@ let main_smt ~config () : _ result =
parse_res >>= fun input ->
let driver =
let asolver = Solver.Smt_solver.Solver.as_asolver solver in
Driver.create ~restarts:!restarts ~pp_cnf:!p_cnf ~time:!time_limit
~memory:!mem_limit ~pp_model:!p_model ?proof_file ~check:!check
~progress:!p_progress solver
~progress:!p_progress asolver
in
(* process statements *)

3
src/smt/dune
View file

@ -3,5 +3,6 @@
(public_name sidekick.smt-solver)
(synopsis "main SMT solver")
(libraries containers iter sidekick.core sidekick.util sidekick.cc
sidekick.sat sidekick.simplify sidekick.model sidekick.trace)
sidekick.sat sidekick.abstract-solver sidekick.simplify
sidekick.model sidekick.trace)
(flags :standard -w +32 -open Sidekick_util))

46
src/smt/solver.ml
View file

@ -6,32 +6,25 @@ open struct
module Rule_ = Proof_core
end
module Check_res = Sidekick_abstract_solver.Check_res
module Sat_solver = Sidekick_sat
(** the parametrized SAT Solver *)
(** {2 Result} *)
module Unknown = struct
type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop
module Unknown = Sidekick_abstract_solver.Unknown [@@ocaml.warning "-37"]
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
type res = Check_res.t =
| 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
(** Result of solving for the current set of clauses *)
(** Unknown, obtained after a timeout, memory limit, etc. *)
(* main solver state *)
type t = {
@ -175,8 +168,8 @@ let assert_terms self c =
let assert_term self t = assert_terms self [ t ]
let add_ty (self : t) ty = SI.add_ty self.si ~ty
let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
?(should_stop = fun _ _ -> false) ~assumptions (self : t) : res =
let solve ?(on_exit = []) ?(on_progress = fun _ -> ())
?(should_stop = fun _ -> false) ~assumptions (self : t) : res =
let@ () = Profile.with_ "smt-solver.solve" in
let do_on_exit () = List.iter (fun f -> f ()) on_exit in
@ -184,9 +177,8 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
let resource_counter = ref 0 in
fun () ->
incr resource_counter;
on_progress self;
if should_stop self !resource_counter then
raise_notrace Resource_exhausted
on_progress ();
if should_stop !resource_counter then raise_notrace Resource_exhausted
in
Event.on ~f:on_progress (SI.on_progress self.si);
@ -218,8 +210,6 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
| Some m -> m
| None -> assert false
in
(* TODO: check model *)
let _ = check in
do_on_exit ();
Sat m
@ -233,6 +223,20 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
self.last_res <- Some res;
res
let as_asolver (self : t) : Sidekick_abstract_solver.Asolver.t =
object
method assert_term t : unit = assert_term self t
method assert_clause c p : unit = add_clause self c p
method assert_clause_l c p : unit = add_clause_l self c p
method lit_of_term ?sign t : Lit.t = mk_lit_t self ?sign t
method proof = self.proof
method last_res = last_res self
method add_ty ~ty = add_ty self ty
method solve ?on_exit ?on_progress ?should_stop ~assumptions () : res =
solve ?on_exit ?on_progress ?should_stop ~assumptions self
end
let push_assumption self a =
reset_last_res_ self;
Sat_solver.push_assumption self.solver a

32
src/smt/solver.mli
View file

@ -7,6 +7,8 @@
Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *)
open Sigs
module Check_res = Sidekick_abstract_solver.Check_res
module Unknown = Sidekick_abstract_solver.Unknown
type t
(** The solver's state. *)
@ -25,19 +27,6 @@ val mk_theory :
Theory.t
(** Helper to create a theory. *)
(* 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
@ -116,7 +105,7 @@ val assert_term : t -> term -> unit
val add_ty : t -> ty -> unit
(** Result of solving for the current set of clauses *)
type res =
type res = Check_res.t =
| Sat of Model.t (** Satisfiable *)
| Unsat of {
unsat_core: unit -> lit Iter.t;
@ -131,24 +120,25 @@ type res =
val solve :
?on_exit:(unit -> unit) list ->
?check:bool ->
?on_progress:(t -> unit) ->
?should_stop:(t -> int -> bool) ->
?on_progress:(unit -> unit) ->
?should_stop:(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
@param should_stop a callback regularly called from within the solver.
It is given 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 as_asolver : t -> Sidekick_abstract_solver.Asolver.t
(** Comply to the abstract solver interface *)
val last_res : t -> res option
(** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *)
@ -184,7 +174,5 @@ val check_sat_propagations_only :
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. *)

58
src/smtlib/Driver.ml
View file

@ -1,5 +1,6 @@
open Sidekick_core
module Profile = Sidekick_util.Profile
module Asolver = Solver.Asolver
open! Sidekick_base
open Common_
@ -55,7 +56,7 @@ module Fmt = CCFormat
type t = {
progress: Progress_bar.t option;
solver: Solver.t;
solver: Asolver.t;
time_start: float;
time_limit: float;
memory_limit: float;
@ -68,7 +69,8 @@ type t = {
(* call the solver to check-sat *)
let create ?(restarts = true) ?(pp_cnf = false) ?proof_file ?(pp_model = false)
?(check = false) ?time ?memory ?(progress = false) (solver : Solver.t) : t =
?(check = false) ?time ?memory ?(progress = false) (solver : Asolver.t) : t
=
let time_start = now () in
let progress =
if progress then
@ -107,7 +109,7 @@ let decl_fun (_self : t) id args ret : unit =
(* call the solver to check satisfiability *)
let solve (self : t) ~assumptions () : Solver.res =
let t1 = now () in
let should_stop _ _ =
let should_stop _n =
if now () -. self.time_start > self.time_limit then (
Log.debugf 0 (fun k -> k "timeout");
true
@ -125,12 +127,12 @@ let solve (self : t) ~assumptions () : Solver.res =
let res =
let@ () = Profile.with_ "process.solve" in
Solver.solve ~assumptions ?on_progress ~should_stop self.solver
Asolver.solve ~assumptions ?on_progress ~should_stop self.solver ()
in
let t2 = now () in
flush stdout;
(match res with
| Solver.Sat m ->
| Asolver.Check_res.Sat m ->
if self.pp_model then
(* TODO: use actual {!Model} in the solver? or build it afterwards *)
Format.printf "(@[<hv1>model@ %a@])@." Sidekick_smt_solver.Model.pp m;
@ -143,7 +145,7 @@ let solve (self : t) ~assumptions () : Solver.res =
let t3 = now () in
Fmt.printf "sat@.";
Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. time_start) (t2 -. t1) (t3 -. t2)
| Solver.Unsat { unsat_step_id; unsat_core = _ } ->
| Asolver.Check_res.Unsat { unsat_step_id; unsat_core = _ } ->
if self.check then
()
(* FIXME: check trace?
@ -158,19 +160,17 @@ let solve (self : t) ~assumptions () : Solver.res =
(match unsat_step_id () with
| None -> ()
| Some step_id ->
let proof = Solver.proof self.solver in
let proof_quip =
Profile.with_ "proof.to-quip" @@ fun () -> assert false
(* TODO
Proof_quip.of_proof proof ~unsat:step_id
*)
in
Profile.with_ "proof.write-file" @@ fun () ->
with_file_out file @@ fun oc ->
(* TODO
Proof_quip.output oc proof_quip;
(* TODO: read trace; emit proof
let proof = Solver.proof self.solver in
let proof_quip =
Profile.with_ "proof.to-quip" @@ fun () -> assert false
Proof_quip.of_proof proof ~unsat:step_id
Profile.with_ "proof.write-file" @@ fun () ->
with_file_out file @@ fun oc ->
Proof_quip.output oc proof_quip;
flush oc
*)
flush oc)
())
| _ -> ());
let t3 = now () in
@ -193,7 +193,7 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
Log.debugf 5 (fun k ->
k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt);
let add_step r = Proof_trace.add_step (Solver.proof self.solver) r in
let add_step r = Proof_trace.add_step (Asolver.proof self.solver) r in
match stmt with
| Statement.Stmt_set_logic logic ->
@ -211,7 +211,7 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
| Statement.Stmt_check_sat l ->
(* FIXME: how to map [l] to [assumptions] in proof? *)
let assumptions =
List.map (fun (sign, t) -> Solver.mk_lit_t self.solver ~sign t) l
List.map (fun (sign, t) -> Asolver.lit_of_term self.solver ~sign t) l
in
ignore (solve self ~assumptions () : Solver.res);
E.return ()
@ -223,32 +223,32 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
E.return ()
| Statement.Stmt_assert t ->
if self.pp_cnf then Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t;
let lit = Solver.mk_lit_t self.solver t in
Solver.add_clause self.solver [| lit |]
let lit = Asolver.lit_of_term self.solver t in
Asolver.assert_clause self.solver [| lit |]
(add_step @@ fun () -> Proof_sat.sat_input_clause [ lit ]);
E.return ()
| Statement.Stmt_assert_clause c_ts ->
if self.pp_cnf then
Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts;
let c = CCList.map (fun t -> Solver.mk_lit_t self.solver t) c_ts in
let c = CCList.map (fun t -> Asolver.lit_of_term self.solver t) c_ts in
(* proof of assert-input + preprocessing *)
let pr =
add_step @@ fun () ->
let lits = List.map (Solver.mk_lit_t self.solver) c_ts in
let lits = List.map (Asolver.lit_of_term self.solver) c_ts in
Proof_sat.sat_input_clause lits
in
Solver.add_clause self.solver (CCArray.of_list c) pr;
Asolver.assert_clause self.solver (CCArray.of_list c) pr;
E.return ()
| Statement.Stmt_get_model ->
(match Solver.last_res self.solver with
(match Asolver.last_res self.solver with
| Some (Solver.Sat m) -> Fmt.printf "%a@." Sidekick_smt_solver.Model.pp m
| _ -> Error.errorf "cannot access model");
E.return ()
| Statement.Stmt_get_value l ->
(match Solver.last_res self.solver with
(match Asolver.last_res self.solver with
| Some (Solver.Sat m) ->
let l =
List.map
@ -265,7 +265,9 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
| _ -> Error.errorf "cannot access model");
E.return ()
| Statement.Stmt_data ds ->
List.iter (fun d -> Solver.add_ty self.solver (Data_ty.data_as_ty d)) ds;
List.iter
(fun d -> Asolver.add_ty self.solver ~ty:(Data_ty.data_as_ty d))
ds;
E.return ()
| Statement.Stmt_define _ ->
(* TODO *)

3
src/smtlib/Driver.mli
View file

@ -5,6 +5,7 @@
calling "solve", etc.)
*)
module Asolver = Solver.Asolver
open Sidekick_base
val th_bool_dyn : Solver.theory
@ -28,7 +29,7 @@ val create :
?time:float ->
?memory:float ->
?progress:bool ->
Solver.t ->
Asolver.t ->
t
val process_stmt : t -> Statement.t -> unit or_error

2
src/smtlib/check_cc.ml
View file

@ -44,7 +44,7 @@ let check_propagation si _cc p reason : unit =
k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p)
let theory =
Solver.mk_theory ~name:"cc-check"
Solver.Smt_solver.Solver.mk_theory ~name:"cc-check"
~create_and_setup:(fun ~id:_ si ->
let n_calls = Stat.mk_int (SI.stats si) "check-cc.call" in
SI.on_cc_conflict si (fun { cc; th; c } ->

2
src/smtlib/check_cc.mli
View file

@ -1,2 +1,2 @@
val theory : Solver.theory
val theory : Solver.cdcl_theory
(** theory that check validity of EUF conflicts, on the fly *)

1
src/smtlib/dune
View file

@ -4,5 +4,6 @@
(synopsis "SMTLIB 2.6 driver for Sidekick")
(private_modules Common_)
(libraries containers zarith sidekick.core sidekick.util sidekick-base
sidekick.abstract-solver
sidekick.mini-cc smtlib-utils sidekick.tef)
(flags :standard -warn-error -a+8 -open Sidekick_util))

6
src/smtlib/solver.ml
View file

@ -1 +1,5 @@
include Sidekick_base.Solver
module Asolver = Sidekick_abstract_solver.Asolver
module Smt_solver = Sidekick_smt_solver
type t = Asolver.t
type cdcl_theory = Smt_solver.theory