diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-28 22:17:04 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-28 22:17:04 +0000 |
commit | c5f652834b915641ae6cbeccf97e959470757863 (patch) | |
tree | e3fb985b65f35dbf0c070d4a0f19b9f9f86a0bdd /src/theory | |
parent | 07f9271bf426f9ed40bd0d01e4e77a17fa217e23 (diff) |
This update enables TheoryArith to accept assertions that rewrite to true or false. This is temporary and will be removed once TheoryEngine rewriting is more fully debugged.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 08b609ba4..b3c19a040 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -107,6 +107,7 @@ Kind multKind(Kind k){ void registerAtom(TNode rel){ //addBound(rel); //Anything else? + } Node TheoryArith::rewrite(TNode n){ @@ -132,6 +133,7 @@ void TheoryArith::registerTerm(TNode tn){ //TODO is an atom if(isRelationOperator(tn.getKind())){ + Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn); normalForm = (normalForm.getKind() == NOT) ? pushInNegation(normalForm):normalForm; Kind k = normalForm.getKind(); @@ -160,6 +162,8 @@ void TheoryArith::registerTerm(TNode tn){ //TODO this has to be wrong no? YES (dejan) // d_out->lemma(slackEqLeft); + Debug("slack") << "slack " << slackEqLeft << endl; + d_tableau.addRow(slackEqLeft); Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right); @@ -468,7 +472,14 @@ Node TheoryArith::simulatePreprocessing(TNode n){ return NodeManager::currentNM()->mkNode(NOT,sub); } } else if(!isRelationOperator(k)){ - Unreachable("Slack must be have been created!"); + if(rewritten.getKind() == CONST_BOOLEAN){ + Warning() << "How did I get a const boolean here" << endl; + Warning() << "offending node has id " << n.getId() << endl; + Warning() << "offending node is "<< n << endl; + return rewritten; + }else{ + Unreachable("Unexpected type!"); + } }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){ return rewritten; }else { @@ -496,6 +507,9 @@ void TheoryArith::check(Effort level){ d_preprocessed.push_back(assertion); switch(assertion.getKind()){ + case CONST_BOOLEAN: + Warning() << "No bools should be reached dagnabbit" << endl; + break; case LEQ: AssertUpper(assertion, original); break; @@ -525,6 +539,9 @@ void TheoryArith::check(Effort level){ case EQUAL: d_diseq.push_back(assertion); break; + case CONST_BOOLEAN: + Warning() << "No bools should be reached dagnabbit" << endl; + break; default: Unhandled(); } |