From 977730599a67d53fb4479b32714fafa7867cfa11 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 16 Feb 2011 23:23:04 +0000 Subject: Overview of the changes: - Preparing to remove row ejection from the code base! - Checks for conflicts immediately after a pivot to avoid potentially wasteful search. - Added arithvar_set.h. This replaces ArithVarSet that was previously in the Tableau, and ArithVarDenseSet. - Removes variables that have no preregistered bounds during presolve(). - Theory::isLeafOf() currently returns true for atoms. (I was unaware.) I modified Variable::isMember() to account for this exclude atoms. - Added statistics all over the place. This commit effects both boolean search and simplex search so expect running times to go all over the place. The time differences should be roughly as follows: http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1486&reference_id=1447&p=10&category=1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29 --- src/theory/arith/unate_propagator.h | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/theory/arith/unate_propagator.h') diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index 1aab795cb..ca2135cf3 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -77,6 +77,9 @@ public: */ void addAtom(TNode atom); + /** Returns true if v has been added as a left hand side in an atom */ + bool hasAnyAtoms(TNode v); + private: /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */ void addImplication(TNode a, TNode b); -- cgit v1.2.3