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

expose tag_clause in Solver.Make

Browse source
This commit is contained in:
Simon Cruanes 2016-01-29 14:59:48 +01:00
parent f348dcd5ae
commit f088ef73e1
3 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
sat/sat.ml
View file

@ -71,7 +71,7 @@ module Make(Dummy : sig end) = struct
type clause = SatSolver.St.clause
type proof = SatSolver.Proof.proof
let tag_clause cl = SatSolver.St.(cl.tag)
let tag_clause = SatSolver.tag_clause
type res =
| Sat

1
solver/solver.ml
View file

@ -101,5 +101,6 @@ module Make (E : Formula_intf.S)
include S
let tag_clause cl = St.(cl.tag)
end

3
solver/solver.mli
View file

@ -38,6 +38,9 @@ module Make (F : Formula_intf.S)
Modifies the sat solver state in place.
@raise Unsat if a conflict is detect when adding the clauses *)
val tag_clause : St.clause -> int option
(** Recover tag from a clause, if any *)
val eval : F.t -> bool
(** Returns the valuation of a formula in the current state
of the sat solver. *)