tim's fixes for context-dependent pre-registration

diff --git a/src/theory/arith/atom_database.h b/src/theory/arith/atom_database.h
index af7068ada07bf617e2227e6ab56672cb978027c7..4da8d79751fd1b9a5466aa7281937abb8e6773ad 100644 (file)
--- a/src/theory/arith/atom_database.h
+++ b/src/theory/arith/atom_database.h
@@ -96,9 +96,11 @@ public:
   bool containsLeq(TNode atom) const;
   bool containsGeq(TNode atom) const;
 
-
+  /** Check to make sure an lhs has been properly set-up. */
+  bool leftIsSetup(TNode left) const;
 
 private:
+
   VariablesSets& getVariablesSets(TNode left);
   BoundValueSet& getBoundValueSet(TNode left);
   EqualValueSet& getEqualValueSet(TNode left);
@@ -110,9 +112,6 @@ private:
   /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
   void addImplication(TNode a, TNode b);
 
-  /** Check to make sure an lhs has been properly set-up. */
-  bool leftIsSetup(TNode left) const;
-
   /** Initializes the lists associated with a unique lhs. */
   void setupLefthand(TNode left);
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1b13b9ee6476583f53bc702e5755075dd0e1666f..be8feb24567037a481b2265dd1326e17b1787d2f 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -286,13 +286,13 @@ void TheoryArith::preRegisterTerm(TNode n) {
     d_out->setIncomplete();
   }
 
-  if(Variable::isMember(n) || isStrictlyVarList){
+  if((Variable::isMember(n) || isStrictlyVarList) && !d_arithvarNodeMap.hasArithVar(n)){
     ++(d_statistics.d_statUserVariables);
     ArithVar varN = requestArithVar(n,false);
     setupInitialValue(varN);
   }
 
-  if(isRelationOperator(k)){
+  if(isRelationOperator(k) && (!d_atomDatabase.leftIsSetup(n[0]) || !d_atomDatabase.containsAtom(n))) {
     Assert(Comparison::isNormalAtom(n));
 
     d_atomDatabase.addAtom(n);