diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-05 14:10:10 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-05 14:31:12 -0400 |
commit | dfb807946da87254f927bf5550ff0f35fc780631 (patch) | |
tree | d51f32579b693b7171fdcfad4d16a391a702428b /src/theory/valuation.cpp | |
parent | 9b59e12cf7eb284d4d99bf19036ba28fc5fb32cf (diff) |
Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and contract is the same as for TheoryEngine version.
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r-- | src/theory/valuation.cpp | 63 |
1 files changed, 33 insertions, 30 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index d4aef4fff..72d878782 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -23,34 +23,34 @@ namespace CVC4 { namespace theory { bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) { - switch (s1) { - case EQUALITY_TRUE: - case EQUALITY_TRUE_IN_MODEL: - case EQUALITY_TRUE_AND_PROPAGATED: - switch (s2) { - case EQUALITY_TRUE: - case EQUALITY_TRUE_IN_MODEL: - case EQUALITY_TRUE_AND_PROPAGATED: - return true; - default: - return false; - } - break; - case EQUALITY_FALSE: - case EQUALITY_FALSE_IN_MODEL: - case EQUALITY_FALSE_AND_PROPAGATED: - switch (s2) { - case EQUALITY_FALSE: - case EQUALITY_FALSE_IN_MODEL: - case EQUALITY_FALSE_AND_PROPAGATED: - return true; - default: - return false; - } - break; - default: - return false; - } + switch (s1) { + case EQUALITY_TRUE: + case EQUALITY_TRUE_IN_MODEL: + case EQUALITY_TRUE_AND_PROPAGATED: + switch (s2) { + case EQUALITY_TRUE: + case EQUALITY_TRUE_IN_MODEL: + case EQUALITY_TRUE_AND_PROPAGATED: + return true; + default: + return false; + } + break; + case EQUALITY_FALSE: + case EQUALITY_FALSE_IN_MODEL: + case EQUALITY_FALSE_AND_PROPAGATED: + switch (s2) { + case EQUALITY_FALSE: + case EQUALITY_FALSE_IN_MODEL: + case EQUALITY_FALSE_AND_PROPAGATED: + return true; + default: + return false; + } + break; + default: + return false; + } } bool Valuation::isSatLiteral(TNode n) const { @@ -87,7 +87,6 @@ Node Valuation::getModelValue(TNode var) { return d_engine->getModelValue(var); } - Node Valuation::ensureLiteral(TNode n) { Debug("ensureLiteral") << "rewriting: " << n << std::endl; Node rewritten = Rewriter::rewrite(n); @@ -106,5 +105,9 @@ unsigned Valuation::getAssertionLevel() const{ return d_engine->getPropEngine()->getAssertionLevel(); } +std::pair<bool, Node> Valuation::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params, theory::EntailmentCheckSideEffects* out) { + return d_engine->entailmentCheck(mode, lit, params, out); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |