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/theory/arith/atom_database.h | |
| parent | dcb2ad496607e2f3821ee84a175a1b412f2f9a20 (diff) | |
tim's fixes for context-dependent pre-registration
Diffstat (limited to 'src/theory/arith/atom_database.h')
| -rw-r--r-- | src/theory/arith/atom_database.h | 7 |
1 files changed, 3 insertions, 4 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); |