summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r--src/theory/arith/theory_arith.cpp11
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 395d51d3e..239385bfc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -25,9 +25,9 @@ namespace CVC4 {
namespace theory {
namespace arith {
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
- : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
- , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, qe))
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+ : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
+ , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
{}
TheoryArith::~TheoryArith(){
@@ -42,6 +42,11 @@ void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_internal->setMasterEqualityEngine(eq);
}
+void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) {
+ this->Theory::setQuantifiersEngine(qe);
+ d_internal->setQuantifiersEngine(qe);
+}
+
void TheoryArith::addSharedTerm(TNode n){
d_internal->addSharedTerm(n);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback