diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-02 20:21:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-03 01:21:04 +0000 |
| commit | 6b55bf59675fcdaab4c8dbf70a8a74ebb1f990e9 (patch) | |
| tree | 5a3b4b8dff3f72acff78988ef7dd8def6597038b /src/smt/assertions.h | |
| parent | 9547af1fb7fa26d6a3299ede363fc2faaae85908 (diff) | |
Remove "inUnsatCore" flag throughout (#6964)
The internal solver no longer cares about what assertions are named / are in the unsat core.
This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces.
This eliminates another external use of `getSmtEngine`.
Diffstat (limited to 'src/smt/assertions.h')
| -rw-r--r-- | src/smt/assertions.h | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/src/smt/assertions.h b/src/smt/assertions.h index c922cbaea..de7ba72c9 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -65,24 +65,20 @@ class Assertions * upcoming check-sat call. * * @param assumptions The assumptions of the upcoming check-sat call. - * @param inUnsatCore Whether assumptions are in the unsat core. * @param isEntailmentCheck Whether we are checking entailment of assumptions * in the upcoming check-sat call. */ void initializeCheckSat(const std::vector<Node>& assumptions, - bool inUnsatCore, bool isEntailmentCheck); /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for * literals and conjunction of literals. Returns false if - * immediately determined to be inconsistent. This version - * takes a Boolean flag to determine whether to include this asserted - * formula in an unsat core (if one is later requested). + * immediately determined to be inconsistent. * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - void assertFormula(const Node& n, bool inUnsatCore = true); + void assertFormula(const Node& n); /** * Assert that n corresponds to an assertion from a define-fun or * define-fun-rec command. @@ -145,7 +141,6 @@ class Assertions * (this is used to distinguish assertions and assumptions) */ void addFormula(TNode n, - bool inUnsatCore, bool inInput, bool isAssumption, bool isFunDef, |