From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 15 Sep 2011 21:48:42 +0000 (+0000)
Subject: tim's fixes for context-dependent pre-registration
X-Git-Tag: cvc5-1.0.0~8477
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f8c6509afb1d7d99f2e4c0ef2df91b25be31bec;p=cvc5.git

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 af7068ada..4da8d7975 100644
--- 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 1b13b9ee6..be8feb245 100644
--- 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);