From d08c8fe16551856210f60a098112b474cc4a706e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 10 Oct 2022 15:43:37 -0400 Subject: [PATCH] feat: add sidekick.abstract solver this library provides an abstract interface for what a SMT solver provides, independently of the underlying implementation technology. --- src/abstract-solver/asolver.ml | 65 +++++++++++++++++++ src/abstract-solver/check_res.ml | 21 ++++++ src/abstract-solver/dune | 7 ++ .../sidekick_abstract_solver.ml | 8 +++ src/abstract-solver/unknown.ml | 7 ++ src/abstract-solver/unknown.mli | 3 + 6 files changed, 111 insertions(+) create mode 100644 src/abstract-solver/asolver.ml create mode 100644 src/abstract-solver/check_res.ml create mode 100644 src/abstract-solver/dune create mode 100644 src/abstract-solver/sidekick_abstract_solver.ml create mode 100644 src/abstract-solver/unknown.ml create mode 100644 src/abstract-solver/unknown.mli diff --git a/src/abstract-solver/asolver.ml b/src/abstract-solver/asolver.ml new file mode 100644 index 00000000..eb5f6aa9 --- /dev/null +++ b/src/abstract-solver/asolver.ml @@ -0,0 +1,65 @@ +(** Abstract interface for a solver *) + +open Sidekick_core +module Unknown = Unknown +module Check_res = Check_res + +class type t = + object + method assert_term : Term.t -> unit + (** Helper that turns the term into an atom, before adding the result + to the solver as a unit clause assertion. + + This uses {!Proof_sat.sat_input_clause} to justify the assertion. *) + + method assert_clause : Lit.t array -> Proof_step.id -> unit + (** [add_clause solver cs] adds a boolean clause to the solver. + Subsequent calls to {!solve} will need to satisfy this clause. *) + + method assert_clause_l : Lit.t list -> Proof_step.id -> unit + (** Add a clause to the solver, given as a list. *) + + method add_ty : ty:Term.t -> unit + (** Add a new sort/atomic type. *) + + method lit_of_term : ?sign:bool -> Term.t -> Lit.t + (** Convert a term into a simplified literal. *) + + method solve : + ?on_exit:(unit -> unit) list -> + ?on_progress:(unit -> unit) -> + ?should_stop:(int -> bool) -> + assumptions:Lit.t list -> + unit -> + Check_res.t + (** Checks the satisfiability of the clauses added so far to the solver. + @param assumptions a set of atoms held to be true. The unsat core, + if any, will be a subset of [assumptions]. + @param on_progress called regularly during solving. + @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 *) + + method last_res : Check_res.t option + (** Returns the result of the last call to {!solve}, if the logic statee + has not changed (mostly by asserting new clauses). *) + + method proof : Proof_trace.t + (** TODO: remove, use Tracer instead *) + end + +let assert_term (self : #t) t : unit = self#assert_term t +let assert_clause (self : #t) c p : unit = self#assert_clause c p +let assert_clause_l (self : #t) c p : unit = self#assert_clause_l c p +let add_ty (self : #t) ~ty : unit = self#add_ty ~ty +let lit_of_term (self : #t) ?sign t : Lit.t = self#lit_of_term ?sign t + +let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () : + Check_res.t = + self#solve ?on_exit ?on_progress ?should_stop ~assumptions () + +let last_res (self : #t) = self#last_res +let proof (self : #t) : Proof_trace.t = self#proof diff --git a/src/abstract-solver/check_res.ml b/src/abstract-solver/check_res.ml new file mode 100644 index 00000000..17dbbc91 --- /dev/null +++ b/src/abstract-solver/check_res.ml @@ -0,0 +1,21 @@ +(** Result of solving for the current set of clauses *) + +module Model = Sidekick_model + +(** Result of calling "check" *) +type t = + | Sat of Model.t (** Satisfiable *) + | Unsat of { + unsat_core: unit -> Lit.t Iter.t; + (** Unsat core (subset of assumptions), or empty *) + unsat_step_id: unit -> Proof_trace.step_id option; + (** Proof step for the empty clause *) + } (** Unsatisfiable *) + | Unknown of Unknown.t + (** Unknown, obtained after a timeout, memory limit, etc. *) + +let pp out (self : t) = + match self with + | Sat _ -> Fmt.string out "Sat" + | Unsat _ -> Fmt.string out "Unsat" + | Unknown u -> Fmt.fprintf out "Unknown(%a)" Unknown.pp u diff --git a/src/abstract-solver/dune b/src/abstract-solver/dune new file mode 100644 index 00000000..440f122f --- /dev/null +++ b/src/abstract-solver/dune @@ -0,0 +1,7 @@ + +(library + (name sidekick_abstract_solver) + (public_name sidekick.abstract-solver) + (flags :standard -open Sidekick_util -open Sidekick_core) + (libraries containers iter + sidekick.core sidekick.model)) diff --git a/src/abstract-solver/sidekick_abstract_solver.ml b/src/abstract-solver/sidekick_abstract_solver.ml new file mode 100644 index 00000000..b3a6f162 --- /dev/null +++ b/src/abstract-solver/sidekick_abstract_solver.ml @@ -0,0 +1,8 @@ +(** Abstract interface for a solver *) + +module Unknown = Unknown +module Check_res = Check_res +module Asolver = Asolver + +class type t = Asolver.t +(** Main abstract solver type *) diff --git a/src/abstract-solver/unknown.ml b/src/abstract-solver/unknown.ml new file mode 100644 index 00000000..cfd53a6d --- /dev/null +++ b/src/abstract-solver/unknown.ml @@ -0,0 +1,7 @@ +type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop + +let pp out = function + | U_timeout -> Fmt.string out {|"timeout"|} + | U_max_depth -> Fmt.string out {|"max depth reached"|} + | U_incomplete -> Fmt.string out {|"incomplete fragment"|} + | U_asked_to_stop -> Fmt.string out {|"asked to stop by callback"|} diff --git a/src/abstract-solver/unknown.mli b/src/abstract-solver/unknown.mli new file mode 100644 index 00000000..5fbf5415 --- /dev/null +++ b/src/abstract-solver/unknown.mli @@ -0,0 +1,3 @@ +type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop + +val pp : t Fmt.printer