From: Tim King <taking@cs.nyu.edu>
Date: Tue, 16 Nov 2010 21:11:11 +0000 (+0000)
Subject: Added Theory::presolve().
X-Git-Tag: cvc5-1.0.0~8730
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb2a0e0e12f39a1b4dea8fb0c990decba4708a1c;p=cvc5.git

Added Theory::presolve().
---

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ab1afceba..4939ecb43 100644
--- 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 81711a101..e9ff06adb 100644
--- 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 89631d59f..22a0148e1 100644
--- 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 2c77c09b3..fa826539c 100644
--- 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 57c5d1558..f373d16c2 100644
--- 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 c673a56b4..f6073eff9 100644
--- 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 df9dcafef..de260dd99 100644
--- 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 eb4c18161..f27e61544 100644
--- 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 7958d977e..8ee5c91d7 100644
--- 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 023e100a9..569f9bb49 100644
--- 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 4c8a1a71a..44f061c12 100644
--- 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 f0da885c7..7387551e3 100644
--- 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 bd6ec515b..594b5646d 100644
--- 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(); }