Simplification of the preregister and register throught a NodeVisitor class. The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.

2 files changed, 22 insertions, 8 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);
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 255e2a304..8213dd47a 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -240,7 +240,7 @@ private:
 
   void asVectors(Polynomial& p,
                  std::vector<Rational>& coeffs,
-                 std::vector<ArithVar>& variables) const;
+                 std::vector<ArithVar>& variables);
 
   /** Routine for debugging. Print the assertions the theory is aware of. */
   void debugPrintAssertions();