From a499d65fdebc075023d6a2e1fdcb8f3072f42ae5 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 9 Jan 2015 14:53:46 +0100 Subject: [PATCH 1/2] Added model output for Mcsolver --- solver/mcsolver.ml | 7 +++++++ solver/mcsolver.mli | 3 +++ 2 files changed, 10 insertions(+) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 83d49550..32267300 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -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 diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index 120077f8..83a9e6b9 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -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. *) From ff25fae1921f4b26b0dcdadfbf2ddda2315bffcb Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 9 Jan 2015 15:04:06 +0100 Subject: [PATCH 2/2] Fixed an interface omission --- solver/mcsolver.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index 83a9e6b9..261fe622 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -11,7 +11,8 @@ module Make (E : Expr_intf.S) exception Unsat 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 with type atom = St.atom