diff options
author | Tim King <taking@cs.nyu.edu> | 2014-04-30 17:28:00 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-30 19:07:28 -0400 |
commit | c5e4a56d4895ce29cd37bac027bb3d486d687f9d (patch) | |
tree | 6712748188bcfa6dc4e6074e091ee9106729f058 /src/theory/theory.cpp | |
parent | 221e509c0eb230aa549fe0107ba88514b6944ca2 (diff) |
T-entailment work, and QCF (quant conflict find) work that uses it.
This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index c52ee936a..f65e48ec2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -228,6 +228,32 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti return PP_ASSERT_STATUS_UNSOLVED; } +std::pair<bool, Node> Theory::entailmentCheck(TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out){ + return make_pair(false, Node::null()); +} + +EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) + : d_tid(tid) { +} + +EntailmentCheckParameters::~EntailmentCheckParameters(){} + +TheoryId EntailmentCheckParameters::getTheoryId() const { + return d_tid; +} + +EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid) + : d_tid(tid) +{} + +TheoryId EntailmentCheckSideEffects::getTheoryId() const { + return d_tid; +} + +EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { +} }/* CVC4::theory namespace */ }/* CVC4 namespace */ |