Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

1 files changed, 18 insertions, 1 deletions

diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 0ed9cbe85..c58778215 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -25,6 +25,7 @@
 
 #include "util/stats.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/substitutions.h"
 #include <set>
 #include <list>
 
@@ -45,6 +46,19 @@ private:
   std::list<TNode> d_miplibTrickKeys;
 
   /**
+   * Some integer variables are eligible to be replaced by
+   * pseudoboolean variables.  This map collects those eligible
+   * substitutions.
+   *
+   * This is a reference to the substitution map in TheoryArith; as
+   * it's not "owned" by this static learner, it isn't cleared on
+   * clear().  This makes sense, as the static learner only
+   * accumulates information in the substitution map, it never uses it
+   * (i.e., it's write-only).
+   */
+  SubstitutionMap& d_pbSubstitutions;
+
+  /**
    * Map from a node to it's minimum and maximum.
    */
   typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
@@ -52,7 +66,7 @@ private:
   NodeToMinMaxMap d_maxMap;
 
 public:
-  ArithStaticLearner();
+  ArithStaticLearner(SubstitutionMap& pbSubstitutions);
   void staticLearning(TNode n, NodeBuilder<>& learned);
 
   void addBound(TNode n);
@@ -64,11 +78,14 @@ private:
 
   void postProcess(NodeBuilder<>& learned);
 
+  void replaceWithPseudoboolean(TNode var);
   void iteMinMax(TNode n, NodeBuilder<>& learned);
   void iteConstant(TNode n, NodeBuilder<>& learned);
 
   void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned);
 
+  void checkBoundsForPseudobooleanReplacement(TNode n);
+
   /** These fields are designed to be accessable to ArithStaticLearner methods. */
   class Statistics {
   public: