summaryrefslogtreecommitdiff
path: root/src/theory/theory.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r--src/theory/theory.cpp26
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback