diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 21:48:42 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 21:48:42 +0000 |
commit | 1f8c6509afb1d7d99f2e4c0ef2df91b25be31bec (patch) | |
tree | dd2f81ff963ed8ccdf70d27ba68aaf8e1a939444 /src | |
parent | dcb2ad496607e2f3821ee84a175a1b412f2f9a20 (diff) |
tim's fixes for context-dependent pre-registration
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/atom_database.h | 7 | ||||
-rw-r--r-- | 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); |