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

Added model output for Mcsolver

Browse source
This commit is contained in:
Guillaume Bury 2015-01-09 14:53:46 +01:00
parent fe41b38501
commit a499d65fde
2 changed files with 10 additions and 0 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 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 *)
type level = int

3
solver/mcsolver.mli
View file

@ -39,6 +39,9 @@ module Make (E : Expr_intf.S)
(** Returns the unsat clause found at the toplevel, if it exists (i.e if
[solve] has raised [Unsat]) *)
val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *)
type level
(** Abstract notion of assumption level. *)