diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 1 | ||||
-rw-r--r-- | src/theory/arith/tableau.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 20 |
4 files changed, 22 insertions, 4 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 13ee9183f..6f1df5958 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -417,6 +417,9 @@ Node ArithRewriter::rewriteTerm(TNode t){ return rewritePlus(t); }else if(t.getKind() == kind::DIVISION){ return rewriteConstantDiv(t); + }else if(t.getKind() == kind::MINUS){ + Node sub = makeSubtractionNode(t[0],t[1]); + return rewrite(sub); }else{ Unreachable(); return Node::null(); diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 5d94d20a9..184844dbc 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -75,6 +75,7 @@ private: Node rewriteTerm(TNode t); Node rewriteMult(TNode t); Node rewritePlus(TNode t); + Node rewriteMinus(TNode t); Node makeSubtractionNode(TNode l, TNode r); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 2ab94c195..7237c3a54 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -94,7 +94,7 @@ public: void subsitute(Row& row_s){ TNode x_s = row_s.basicVar(); - Assert(!has(x_s)); + Assert(has(x_s)); Assert(x_s != d_x_i); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 66883161e..6ca447ea5 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -99,6 +99,7 @@ void TheoryArith::registerTerm(TNode tn){ if(tn.getKind() == kind::BUILTIN) return; if(tn.getMetaKind() == metakind::VARIABLE){ + setupVariable(tn); } @@ -419,12 +420,25 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ Node TheoryArith::simulatePreprocessing(TNode n){ if(n.getKind() == NOT){ Node sub = simulatePreprocessing(n[0]); - return NodeManager::currentNM()->mkNode(NOT,sub); + if(sub.getKind() == NOT){ + return sub[0]; + }else{ + return NodeManager::currentNM()->mkNode(NOT,sub); + } }else{ Node rewritten = rewrite(n); Kind k = rewritten.getKind(); - if(!isRelationOperator(k)){ - return rewritten; + bool negate = false; + + if(rewritten.getKind() == NOT){ + Node sub = simulatePreprocessing(rewritten[0]); + if(sub.getKind() == NOT){ + return sub[0]; + }else{ + return NodeManager::currentNM()->mkNode(NOT,sub); + } + } else if(!isRelationOperator(k)){ + Unreachable("Slack must be have been created!"); }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){ return rewritten; }else { |