diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 93c02942d..3831536e9 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -281,6 +281,13 @@ void TheoryArith::preRegisterTerm(TNode n) { if(!left.getAttribute(Slack())){ setupSlack(left); } + } else { + if (theoryOf(left) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(left)) { + // The only way not to get it through pre-register is if it's a foreign term + ++(d_statistics.d_statUserVariables); + ArithVar av = requestArithVar(left, false); + setupInitialValue(av); + } } } Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl; @@ -306,7 +313,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ return varX; } -void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) const{ +void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) { for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){ const Monomial& mono = *i; const Constant& constant = mono.getConstant(); @@ -317,10 +324,19 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v Debug("rewriter") << "should be var: " << n << endl; Assert(isLeaf(n)); - Assert(d_arithvarNodeMap.hasArithVar(n)); - - ArithVar av = d_arithvarNodeMap.asArithVar(n); + Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n)); + ArithVar av; + if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) { + // The only way not to get it through pre-register is if it's a foreign term + ++(d_statistics.d_statUserVariables); + av = requestArithVar(n,false); + setupInitialValue(av); + } else { + // Otherwise, we already have it's variable + av = d_arithvarNodeMap.asArithVar(n); + } + coeffs.push_back(constant.getValue()); variables.push_back(av); } @@ -334,8 +350,6 @@ void TheoryArith::setupSlack(TNode left){ d_rowHasBeenAdded = true; - ArithVar varSlack = requestArithVar(left, true); - Polynomial polyLeft = Polynomial::parsePolynomial(left); vector<ArithVar> variables; @@ -343,8 +357,8 @@ void TheoryArith::setupSlack(TNode left){ asVectors(polyLeft, coefficients, variables); + ArithVar varSlack = requestArithVar(left, true); d_tableau.addRow(varSlack, coefficients, variables); - setupInitialValue(varSlack); } |