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

Merge branch 'master' of github.com:Gbury/mSAT

Browse source
This commit is contained in:
Guillaume Bury 2015-01-13 17:37:11 +01:00
commit 017bcaad78
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
solver/mcsolver.ml
View file

@ -858,6 +858,13 @@ module Make (E : Expr_intf.S)
let unsat_conflict () = env.unsat_conflict let unsat_conflict () = env.unsat_conflict
let model () =
let opt = function Some a -> a | None -> assert false in
Vec.fold (fun acc e -> Either.destruct e
(fun v -> (v.tag.term, opt v.tag.assigned) :: acc)
(fun _ -> acc)
) [] env.trail
(* Push/Pop *) (* Push/Pop *)
type level = int type level = int

6
solver/mcsolver.mli
View file

@ -11,7 +11,8 @@ module Make (E : Expr_intf.S)
exception Unsat exception Unsat
module St : Mcsolver_types.S module St : Mcsolver_types.S
with type formula = E.Formula.t with type term = E.Term.t
and type formula = E.Formula.t
module Proof : Res.S module Proof : Res.S
with type atom = St.atom with type atom = St.atom
@ -39,6 +40,9 @@ module Make (E : Expr_intf.S)
(** Returns the unsat clause found at the toplevel, if it exists (i.e if (** Returns the unsat clause found at the toplevel, if it exists (i.e if
[solve] has raised [Unsat]) *) [solve] has raised [Unsat]) *)
val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *)
type level type level
(** Abstract notion of assumption level. *) (** Abstract notion of assumption level. *)