Added Theory::presolve().

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ab1afceba6293e3ba1716e63b0cb05c1543b1c01..4939ecb436a429da0fabf4971753f4a18cba4409 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -118,6 +118,9 @@ Result PropEngine::checkSat() {
   ScopedBool scopedBool(d_inCheckSat);
   d_inCheckSat = true;
 
+  // TODO This currently ignores conflicts (a dangerous practice).
+  d_theoryEngine->presolve();
+
   // Check the problem
   bool result = d_satSolver->solve();
 

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 81711a10143fa8518dbe8708a952734992cd97a0..e9ff06adba10f2fc6f7cd31f8e1202716d1aece6 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -134,6 +134,12 @@ public:
 
   void shutdown(){ }
 
+  void presolve(){
+    static int callCount = 0;
+    Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
+    check(FULL_EFFORT);
+  }
+
   std::string identify() const { return std::string("TheoryArith"); }
 
 private:

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 89631d59fe4ff00a584a277354012b053748b9d7..22a0148e1db1a2260f8cc23577d85312b3944638 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -48,6 +48,10 @@ public:
     return RewriteComplete(in);
   }
 
+  void presolve() {
+    Unimplemented();
+  }
+
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void check(Effort e);

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 2c77c09b3208338daf0dd64afc2d2e712b4e83a8..fa826539c2d1fa1b372fe3a98d09ec1d9934b476 100644 (file)
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -46,6 +46,8 @@ public:
   void propagate(Effort e) { Unimplemented(); }
   void explain(TNode n, Effort e) { Unimplemented(); }
 
+  void presolve(){ Unimplemented(); }
+
   Node getValue(TNode n, TheoryEngine* engine);
 
   RewriteResponse preRewrite(TNode n, bool topLevel);

diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 57c5d1558973df615629091b22b7e19f817df31b..f373d16c27839c161a4548596d9d8b4cea046710 100644 (file)
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -39,6 +39,7 @@ public:
   void check(Effort e) { Unreachable(); }
   void propagate(Effort e) { Unreachable(); }
   void explain(TNode n, Effort e) { Unreachable(); }
+  void presolve() { Unreachable(); }
   Node getValue(TNode n, TheoryEngine* engine);
   void shutdown() { }
   RewriteResponse preRewrite(TNode n, bool topLevel);

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c673a56b41b8e4f953424d4344f4ec39ca76ff21..f6073eff9b1faf8574327e574ff38f6947cc8520 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -71,6 +71,10 @@ public:
 
   void check(Effort e);
 
+  void presolve(){
+    Unimplemented();
+  }
+
   void propagate(Effort e) {}
 
   void explain(TNode n, Effort e) { }

diff --git a/src/theory/theory.h b/src/theory/theory.h
index df9dcafef328ffdaa9abae396866998d75f6397a..de260dd991e275dcf789eb97226c2a6e8581242c 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -443,6 +443,16 @@ public:
    */
   virtual Node getValue(TNode n, TheoryEngine* engine) = 0;
 
+  /**
+   * A Theory is called with presolve exactly one time per user check-sat.
+   * presolve() is called after preregistration, rewriting, and Boolean propagation,
+   * (other theories' propagation?), but the notified Theory has not yet had its check()
+   * or propagate() method called yet.
+   * A Theory may empty its assertFact() queue using get().
+   * A Theory can raise conflicts, add lemmas, and propagate literals during presolve.
+   */
+  virtual void presolve() = 0;
+
   /**
    * Identify this theory (for debugging, dynamic configuration,
    * etc..)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index eb4c1816178fff14023b6af4fed69295cd757701..f27e615443c0430eba648ca5dff5f25a830dff06 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -617,4 +617,20 @@ Node TheoryEngine::getValue(TNode node) {
   return theoryOf(node)->getValue(node, this);
 }/* TheoryEngine::getValue(TNode node) */
 
+
+bool TheoryEngine::presolve(){
+  d_theoryOut.d_conflictNode = Node::null();
+  d_theoryOut.d_propagatedLiterals.clear();
+  try {
+    //d_uf->presolve();
+    d_arith->presolve();
+    //d_arrays->presolve();
+    //d_bv->presolve();
+  } catch(const theory::Interrupted&) {
+    Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl;
+  }
+  // Return wheather we have a conflict
+  return d_theoryOut.d_conflictNode.get().isNull();
+}
+
 }/* CVC4 namespace */

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7958d977ee67e8a1933cca3a11bf28342a1fbd1f..8ee5c91d7b4ebf7d7676a4ba4250c41c2e434721 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -305,10 +305,16 @@ public:
     } catch(const theory::Interrupted&) {
       Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
     }
-    // Return wheather we have a conflict
+    // Return whether we have a conflict
     return d_theoryOut.d_conflictNode.get().isNull();
   }
 
+  /**
+   * Calls presolve() on all active theories and returns true
+   * if one of the theories discovers a conflict.
+   */
+  bool presolve();
+
   inline const std::vector<TNode>& getPropagatedLiterals() const {
     return d_theoryOut.d_propagatedLiterals;
   }

diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 023e100a9817402289793172aa92354bc29985ff..569f9bb4958b84cd77b37d5230e96e14d369bda3 100644 (file)
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -130,6 +130,10 @@ public:
    */
   void check(Effort level);
 
+  void presolve(){
+    Unimplemented();
+  }
+
   /**
    * Rewrites a node in the theory of uninterpreted functions.
    * This is fairly basic and only ensures that atoms that are

diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index 4c8a1a71a7c2dd17667e17d83355d9e7eb9bc5e7..44f061c1210fc48083e428732508cf885b09ec46 100644 (file)
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -126,6 +126,10 @@ public:
   void check(Effort level);
 
 
+  void presolve() {
+    Unimplemented();
+  }
+
   /**
    * Rewrites a node in the theory of uninterpreted functions.
    * This is fairly basic and only ensures that atoms that are

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index f0da885c7b8b8b5c6fd21425ae02f8758cda2bba..7387551e3302c73913a7d162a5a6c3a15f4cc624 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -136,6 +136,9 @@ public:
     }
   }
 
+  void presolve() {
+    Unimplemented();
+  }
   void preRegisterTerm(TNode n) {}
   void propagate(Effort level) {}
   void explain(TNode n, Effort level) {}

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index bd6ec515b009f3fcfdd4556adbbef88defdf7057..594b5646dc7796632adc7cdcb271cbbdebe3a727 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -203,6 +203,8 @@ public:
     return "Fake" + d_id;
   }
 
+  void presolve() { Unimplemented(); }
+
   void preRegisterTerm(TNode) { Unimplemented(); }
   void registerTerm(TNode) { Unimplemented(); }
   void check(Theory::Effort) { Unimplemented(); }