new miplib pass, works for 1 or 2 vars

3 files changed, 18 insertions, 4 deletions

diff --git a/src/theory/arith/options b/src/theory/arith/options
index 719c826ae..d21ccc0ee 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -51,7 +51,7 @@ option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-
  turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
 /turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
 
-option arithMLTrick --enable-miplib-trick/--disable-miplib-trick bool :default false :read-write
+option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default true
  turns on the preprocessing step of attempting to infer bounds on miplib problems
 /turns off the preprocessing step of attempting to infer bounds on miplib problems
 
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index aec0cff58..de4bb30d2 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -64,6 +64,8 @@ public:
     else return ASSIGNED_TO_TRUE;
   }
 
+  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+
 private:
 
   context::Context d_context;
@@ -96,7 +98,7 @@ private:
    */
   DataClearer< std::vector<TNode> > d_propagationQueueClearer;
 
-  /** Are we in conflict */
+  /** Are we in conflict? */
   context::CDO<bool> d_conflict;
 
   /** Map of substitutions */
@@ -107,8 +109,9 @@ private:
    */
   DataClearer< std::vector<Node> > d_learnedLiteralClearer;
 
-  /** Back edges from nodes to where they are used */
-  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+  /**
+   * Back edges from nodes to where they are used.
+   */
   BackEdgesMap d_backEdges;
 
   /**
@@ -157,6 +160,7 @@ private:
     }
   }
 
+public:
   /** True iff Node is assigned in circuit (either true or false). */
   bool isAssigned(TNode n) const {
     AssignmentMap::const_iterator i = d_state.find(n);
@@ -179,6 +183,7 @@ private:
     return (*i).second == ASSIGNED_TO_TRUE;
   }
 
+private:
   /** Predicate for use in STL functions. */
   class IsAssigned : public std::unary_function<TNode, bool> {
     CircuitPropagator& d_circuit;
@@ -268,6 +273,13 @@ public:
    */
   bool propagate() CVC4_WARN_UNUSED_RESULT;
 
+  /**
+   * Get the back edges of this circuit.
+   */
+  const BackEdgesMap& getBackEdges() const {
+    return d_backEdges;
+  }
+
 };/* class CircuitPropagator */
 
 }/* CVC4::theory::booleans namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 35ed63bed..efbc42ebf 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -286,7 +286,9 @@ void TheoryEngine::check(Theory::Effort effort) {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
+Debug("theory") << "check<" << THEORY << ">" << std::endl; \
        theoryOf(THEORY)->check(effort); \
+Debug("theory") << "done<" << THEORY << ">" << std::endl; \
        if (d_inConflict) { \
          break; \
        } \