From 9eee458c2ac6957aec7cbc3990b0e40ce735c2a9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 19 Aug 2016 01:06:22 +0200 Subject: [PATCH] External.assume no longer needs to catch Unsat Following changes to the assume function in internal, it does not raise Unsat anymore, so there is no reason to try and catch it in external. --- src/core/external.ml | 5 +---- src/core/internal.mli | 5 ++--- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/src/core/external.ml b/src/core/external.ml index 20cc419a..9b16feef 100644 --- a/src/core/external.ml +++ b/src/core/external.ml @@ -68,10 +68,7 @@ module Make { unsat_conflict; get_proof; } (* Wrappers around internal functions*) - let assume ?tag l = - try - S.assume ?tag l - with S.Unsat -> () + let assume = S.assume let solve ?(assumptions=[]) () = try diff --git a/src/core/internal.mli b/src/core/internal.mli index 1f9a50ac..b9b1f81b 100644 --- a/src/core/internal.mli +++ b/src/core/internal.mli @@ -25,8 +25,7 @@ module Make val assume : ?tag:int -> St.formula list list -> unit (** Add the list of clauses to the current set of assumptions. - Modifies the sat solver state in place. - @raise Unsat if a conflict is detect when adding the clauses *) + Modifies the sat solver state in place. *) val push : unit -> unit (** Create a decision level for local assumptions. @@ -36,7 +35,7 @@ module Make (** Pop a decision level for local assumptions. *) val local : St.formula list -> unit - (** Add local assumptions + (** Add local assumptions @param assumptions list of additional local assumptions to make, removed after the callback returns a value *)