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/theory_engine.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/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8bc67616f..0495a866b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -73,8 +73,7 @@ struct NodeTheoryPairHashFunction { };/* struct NodeTheoryPairHashFunction */ - -/* Forward Declarations Block */ +/* Forward declarations */ namespace theory { class TheoryModel; class TheoryEngineModelBuilder; @@ -82,11 +81,12 @@ namespace theory { namespace eq { class EqualityEngine; - } + }/* CVC4::theory::eq namespace */ class EntailmentCheckParameters; class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ + class DecisionEngine; class RemoveITE; class UnconstrainedSimplifier; @@ -759,7 +759,7 @@ public: Node getModelValue(TNode var); /** - * Forwards an entailmentCheck according to the given theoryOfMode mode. + * Forwards 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); |