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.h | |
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.h')
-rw-r--r-- | src/theory/valuation.h | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/valuation.h b/src/theory/valuation.h index d175e5e3d..2462896c7 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic ** Minor contributors (to current version): Tim King, Andrew Reynolds, Clark Barrett ** 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 ** @@ -22,6 +22,7 @@ #define __CVC4__THEORY__VALUATION_H #include "expr/node.h" +#include "theory/theoryof_mode.h" namespace CVC4 { @@ -29,6 +30,9 @@ class TheoryEngine; namespace theory { +class EntailmentCheckParameters; +class EntailmentCheckSideEffects; + /** * The status of an equality in the current context. */ @@ -47,11 +51,11 @@ enum EqualityStatus { EQUALITY_FALSE_IN_MODEL, /** The equality is completely unknown */ EQUALITY_UNKNOWN -}; +};/* enum EqualityStatus */ /** - * Returns true if the two statuses are compatible, i.e. bot TRUE - * or both FALSE (regardles of inmodel/propagation). + * Returns true if the two statuses are compatible, i.e. both TRUE + * or both FALSE (regardless of inmodel/propagation). */ bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2); @@ -125,6 +129,12 @@ public: */ unsigned getAssertionLevel() const; + /** + * Request an entailment check according to the given theoryOfMode. + * See theory.h for documentation on entailmentCheck(). + */ + std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL); + };/* class Valuation */ }/* CVC4::theory namespace */ |