From 1f8c6509afb1d7d99f2e4c0ef2df91b25be31bec Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 15 Sep 2011 21:48:42 +0000 Subject: [PATCH] tim's fixes for context-dependent pre-registration --- src/theory/arith/atom_database.h | 7 +++---- src/theory/arith/theory_arith.cpp | 4 ++-- 2 files changed, 5 insertions(+), 6 deletions(-) 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); -- 2.30.2