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(asolver): use new proof tracer from sidekick.proof

Browse source
This commit is contained in:
Simon Cruanes 2022-10-12 12:21:20 -04:00
parent ef3f2713dc
commit 5135d9920a
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 10 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/abstract-solver/asolver.ml
View file

@ -3,6 +3,7 @@
open Sidekick_core open Sidekick_core
module Unknown = Unknown module Unknown = Unknown
module Check_res = Check_res module Check_res = Check_res
module Proof = Sidekick_proof
class type t = class type t =
object object
@ -12,11 +13,11 @@ class type t =
This uses {!Proof_sat.sat_input_clause} to justify the assertion. *) This uses {!Proof_sat.sat_input_clause} to justify the assertion. *)
method assert_clause : Lit.t array -> Proof_step.id -> unit method assert_clause : Lit.t array -> Proof.Pterm.delayed -> unit
(** [add_clause solver cs] adds a boolean clause to the solver. (** [add_clause solver cs] adds a boolean clause to the solver.
Subsequent calls to {!solve} will need to satisfy this clause. *) Subsequent calls to {!solve} will need to satisfy this clause. *)
method assert_clause_l : Lit.t list -> Proof_step.id -> unit method assert_clause_l : Lit.t list -> Proof.Pterm.delayed -> unit
(** Add a clause to the solver, given as a list. *) (** Add a clause to the solver, given as a list. *)
method add_ty : ty:Term.t -> unit method add_ty : ty:Term.t -> unit
@ -47,7 +48,7 @@ class type t =
(** Returns the result of the last call to {!solve}, if the logic statee (** Returns the result of the last call to {!solve}, if the logic statee
has not changed (mostly by asserting new clauses). *) has not changed (mostly by asserting new clauses). *)
method proof : Proof_trace.t method proof_tracer : #Proof.Tracer.t
(** TODO: remove, use Tracer instead *) (** TODO: remove, use Tracer instead *)
end end
@ -62,4 +63,4 @@ let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () :
self#solve ?on_exit ?on_progress ?should_stop ~assumptions () self#solve ?on_exit ?on_progress ?should_stop ~assumptions ()
let last_res (self : #t) = self#last_res let last_res (self : #t) = self#last_res
let proof (self : #t) : Proof_trace.t = self#proof let proof (self : #t) : #Proof.Tracer.t = self#proof

2
src/abstract-solver/check_res.ml
View file

@ -8,7 +8,7 @@ type t =
| Unsat of { | Unsat of {
unsat_core: unit -> Lit.t Iter.t; unsat_core: unit -> Lit.t Iter.t;
(** Unsat core (subset of assumptions), or empty *) (** Unsat core (subset of assumptions), or empty *)
unsat_step_id: unit -> Proof_trace.step_id option; unsat_step_id: unit -> Sidekick_proof.Step.id option;
(** Proof step for the empty clause *) (** Proof step for the empty clause *)
} (** Unsatisfiable *) } (** Unsatisfiable *)
| Unknown of Unknown.t | Unknown of Unknown.t

4
src/abstract-solver/dune
View file

@ -1,7 +1,5 @@
(library (library
(name sidekick_abstract_solver) (name sidekick_abstract_solver)
(public_name sidekick.abstract-solver) (public_name sidekick.abstract-solver)
(flags :standard -open Sidekick_util -open Sidekick_core) (flags :standard -open Sidekick_util -open Sidekick_core)
(libraries containers iter (libraries containers iter sidekick.core sidekick.model sidekick.proof))
sidekick.core sidekick.model))