diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-20 22:51:48 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-20 22:51:48 +0000 |
commit | 5321d62fce6c747fa9d11e9df5b2ef8c4e25de21 (patch) | |
tree | 87685c6a9f32d99f09de28a02fc80378a94b6ec9 /src/theory/arith/theory_arith.cpp | |
parent | ff70395fd3dcde9f68eda1c6a8bd70e6491f7458 (diff) |
Added the division symbol to the parser, and minimal support for it in TheoryArith. Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 390cb60aa..66883161e 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -31,15 +31,20 @@ using namespace CVC4::theory::arith; TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : Theory(c, out), + d_preprocessed(c), d_constants(NodeManager::currentNM()), d_partialModel(c), d_diseq(c), - d_preprocessed(c), d_rewriter(&d_constants) { uint64_t ass_id = partial_model::Assignment::getId(); - Debug("arithsetup") << "Assignment: " << ass_id - << std::endl; + Debug("arithsetup") << "Assignment: " << ass_id << std::endl; +} +TheoryArith::~TheoryArith(){ + for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ + Node var = *i; + Debug("arithgc") << var << endl; + } } @@ -87,13 +92,14 @@ Node TheoryArith::rewrite(TNode n){ return result; } + void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; if(tn.getKind() == kind::BUILTIN) return; if(tn.getMetaKind() == metakind::VARIABLE){ - d_partialModel.setAssignment(tn,d_constants.d_ZERO_DELTA); + setupVariable(tn); } //TODO is an atom @@ -115,7 +121,9 @@ void TheoryArith::registerTerm(TNode tn){ //TODO TypeNode real_type = NodeManager::currentNM()->realType(); slack = NodeManager::currentNM()->mkVar(real_type); - d_partialModel.setAssignment(slack,d_constants.d_ZERO_DELTA); + + setupVariable(slack); + left.setAttribute(Slack(), slack); makeBasic(slack); |