Preregistration has been turned on. Highly experimental eager splitting support has...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 51ae695cf31c73359d23d11111028c7d44da6799..a245eb469da027ace0c2b64fc28c8672edb53290 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -359,6 +359,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
     }
 
     if(somethingChanged) {
+
       rewrite = nodeManager->mkNode(node.getKind(), newChildren);
       nodeManager->setAttribute(node, IteRewriteAttr(), rewrite);
       return rewrite;
@@ -399,7 +400,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
   case AND:
     return handleAnd(node);
   default:
-    return handleAtom(handleNonAtomicNode(node));
+    {
+      Node atomic = handleNonAtomicNode(node);
+      AlwaysAssert(isCached(atomic) || atomic.isAtomic());
+      return toCNF(atomic);
+    }
   }
 }
 

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 7237c3a5476f8f9a32806060ed2d955255c881c4..fa0712e7e8906eac1e9a370e1e1e9113f79d6359 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -36,6 +36,7 @@ public:
 
     //TODO Assert(d_x_i.getType() == REAL);
     Assert(sum.getKind() == PLUS);
+    Rational zero(0,1);
 
     for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){
       TNode pair = *iter;
@@ -48,7 +49,10 @@ public:
       //TODO Assert(var_i.getKind() == REAL);
       Assert(!has(var_i));
       d_nonbasic.insert(var_i);
-      d_coeffs[var_i] = coeff.getConst<Rational>();
+      Rational q = coeff.getConst<Rational>();
+      d_coeffs[var_i] = q;
+      Assert(q != zero);
+      Assert(d_coeffs[var_i] != zero);
     }
   }
 
@@ -66,12 +70,13 @@ public:
 
   bool has(TNode x_j){
     CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-
     return x_jPos != d_coeffs.end();
   }
 
   Rational& lookup(TNode x_j){
-    return d_coeffs[x_j];
+    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
+    Assert(x_jPos !=  d_coeffs.end());
+    return (*x_jPos).second;
   }
 
   void pivot(TNode x_j){
@@ -89,17 +94,22 @@ public:
       TNode nb = *nonbasicIter;
       d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs;
     }
+
   }
 
   void subsitute(Row& row_s){
     TNode x_s = row_s.basicVar();
 
     Assert(has(x_s));
+    Assert(d_nonbasic.find(x_s) != d_nonbasic.end());
     Assert(x_s != d_x_i);
 
+    Rational zero(0,1);
 
     Rational a_rs = lookup(x_s);
+    Assert(a_rs != zero);
     d_coeffs.erase(x_s);
+    d_nonbasic.erase(x_s);
 
     for(std::set<TNode>::iterator iter = row_s.d_nonbasic.begin();
         iter != row_s.d_nonbasic.end();
@@ -108,6 +118,10 @@ public:
       Rational a_sj = a_rs * row_s.lookup(x_j);
       if(has(x_j)){
         d_coeffs[x_j] = d_coeffs[x_j] + a_sj;
+        if(d_coeffs[x_j] == zero){
+          d_coeffs.erase(x_j);
+          d_nonbasic.erase(x_j);
+        }
       }else{
         d_nonbasic.insert(x_j);
         d_coeffs[x_j] = a_sj;

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ff74f0f915be9ad9b8622a7c52633c052dc27d0..08b609ba44fe817ee2c31c8057e48b64a0fd42ef 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -29,6 +29,10 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+struct EagerSplittingTag {};
+typedef expr::Attribute<EagerSplittingTag, bool> EagerlySplitUpon;
+
+
 TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   Theory(c, out),
   d_preprocessed(c),
@@ -47,6 +51,29 @@ TheoryArith::~TheoryArith(){
   }
 }
 
+void TheoryArith::preRegisterTerm(TNode n) {
+  Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
+                             << n << ")" << endl;
+
+  if(n.getKind() == EQUAL){
+    if(!n.getAttribute(EagerlySplitUpon())){
+      TNode left = n[0];
+      TNode right = n[1];
+
+      Node lt = NodeManager::currentNM()->mkNode(LT, left,right);
+      Node gt = NodeManager::currentNM()->mkNode(GT, left,right);
+      Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt);
+
+      d_splits.push_back(eagerSplit);
+
+      n.setAttribute(EagerlySplitUpon(), true);
+      d_out->augmentingLemma(eagerSplit);
+    }
+  }
+
+  Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
+                             << n << ")" << endl;
+}
 
 bool isBasicSum(TNode n){
   if(n.getKind() != kind::PLUS) return false;
@@ -220,11 +247,13 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
     TNode x_j = *basicIter;
     Row* row_j = d_tableau.lookup(x_j);
 
-    Rational& a_ji = row_j->lookup(x_i);
+    if(row_j->has(x_i)){
+      Rational& a_ji = row_j->lookup(x_i);
 
-    DeltaRational assignment = d_partialModel.getAssignment(x_j);
-    DeltaRational  nAssignment = assignment+(diff * a_ji);
-    d_partialModel.setAssignment(x_j, nAssignment);
+      DeltaRational assignment = d_partialModel.getAssignment(x_j);
+      DeltaRational  nAssignment = assignment+(diff * a_ji);
+      d_partialModel.setAssignment(x_j, nAssignment);
+    }
   }
 
   d_partialModel.setAssignment(x_i, v);
@@ -252,7 +281,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
     TNode x_k = *basicIter;
     Row* row_k = d_tableau.lookup(x_k);
 
-    if(x_k != x_i){
+    if(x_k != x_i && row_k->has(x_j)){
       DeltaRational a_kj = row_k->lookup(x_j);
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + theta;
       d_partialModel.setAssignment(x_k, nextAssignment);
@@ -321,7 +350,9 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   d_partialModel.beginRecordingAssignments();
   while(true){
     TNode x_i = selectSmallestInconsistentVar();
+    Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == Node::null()){
+      Debug("arith_update") << "No inconsistent variables" << endl;
       d_partialModel.stopRecordingAssignments(false);
       return Node::null(); //sat
     }
@@ -509,6 +540,8 @@ void TheoryArith::check(Effort level){
     if(possibleConflict != Node::null()){
       Debug("arith") << "Found a conflict " << possibleConflict << endl;
       d_out->conflict(possibleConflict);
+    }else{
+      Debug("arith") << "No conflict found" << endl;
     }
   }
 
@@ -516,22 +549,33 @@ void TheoryArith::check(Effort level){
     bool enqueuedCaseSplit = false;
     typedef context::CDList<Node>::const_iterator diseq_iterator;
     for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
+
       Node assertion = *i;
+      Debug("arith") << "splitting"  << assertion << endl;
       TNode eq = assertion[0];
       TNode x_i = eq[0];
       TNode c_i = eq[1];
       DeltaRational constant =  c_i.getConst<Rational>();
+      Debug("arith") << "broken apart" << endl;
       if(d_partialModel.getAssignment(x_i) == constant){
+        Debug("arith") << "here" << endl;
         enqueuedCaseSplit = true;
         Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
         Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
         Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
         //d_out->enqueueCaseSplits(caseSplit);
+        Debug("arith") << "finished" << caseSplit << endl;
       }
+      Debug("arith") << "end of for loop" << endl;
+
     }
+    Debug("arith") << "finished" << endl;
+
     if(enqueuedCaseSplit){
       //d_out->caseSplit();
-      Warning() << "Outstanding case split in theory arith" << endl;
+      //Warning() << "Outstanding case split in theory arith" << endl;
     }
   }
+  Debug("arith") << "TheoryArith::check end" << std::endl;
+
 }

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7bfa535a84121c8b8ce152a6ee18e6944b956fd7..1d6cca5cce899ec4b8b5cf755bb54ddbc6edf2bf 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -38,6 +38,10 @@ class TheoryArith : public Theory {
 private:
   /* Chopping block begins */
 
+  std::vector<Node> d_splits;
+  //This stores the eager splits sent out of the theory.
+  //TODO get rid of this.
+
   context::CDList<Node> d_preprocessed;
   //TODO This is currently needed to save preprocessed nodes that may not
   //currently have an outisde reference. Get rid of when preprocessing is occuring
@@ -65,7 +69,7 @@ public:
 
   Node rewrite(TNode n);
 
-  void preRegisterTerm(TNode n) { Unimplemented(); }
+  void preRegisterTerm(TNode n);
   void registerTerm(TNode n);
   void check(Effort e);
   void propagate(Effort e) { Unimplemented(); }

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index eb6e84c390f7bae07e7bf904f7d06a8b26b4756a..b39663449e6b70ac4c341ca36489b6380987dff7 100644 (file)
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -31,11 +31,18 @@ public:
     Theory(c, out) {
   }
 
-  void preRegisterTerm(TNode n) { Unimplemented(); }
-  void registerTerm(TNode n) { Unimplemented(); }
+  void preRegisterTerm(TNode n) {
+    Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
+    Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
+  }
+  void registerTerm(TNode n) {
+    Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
+    Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
+  }
   void check(Effort e) { Unimplemented(); }
   void propagate(Effort e) { Unimplemented(); }
   void explain(TNode n, Effort e) { Unimplemented(); }
+
 };
 
 }/* CVC4::theory::booleans namespace */

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 54fa7180811401cd677ad67855bb63d8e86f0047..08a3353e6afd9ac0f3c17c99a6a746fbdd724243 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -18,6 +18,7 @@
 #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
 #define __CVC4__THEORY__OUTPUT_CHANNEL_H
 
+#include "util/Assert.h"
 #include "theory/interrupted.h"
 
 namespace CVC4 {
@@ -53,7 +54,7 @@ public:
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
-  virtual void safePoint() throw(Interrupted) {
+  virtual void safePoint() throw(Interrupted, AssertionException) {
   }
 
   /**
@@ -66,7 +67,7 @@ public:
    *
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0;
+  virtual void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
 
   /**
    * Propagate a theory literal.
@@ -75,7 +76,7 @@ public:
    *
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0;
+  virtual void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
@@ -84,7 +85,16 @@ public:
    * @param n - a theory lemma valid at decision level 0
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0;
+  virtual void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
+
+  /**
+   * Tell the core to add the following valid lemma as if it were a user assertion.
+   * This should NOT be called during solving, only preprocessing.
+   *
+   * @param n - a theory lemma valid to be asserted
+   * @param safe - whether it is safe to be interrupted
+   */
+  virtual void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
 
   /**
    * Provide an explanation in response to an explanation request.
@@ -92,7 +102,7 @@ public:
    * @param n - an explanation
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0;
+  virtual void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0;
 
 };/* class OutputChannel */
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d2919501160405bc2635622cf929b0be5b8feb5d..5af64c5ddc0f73567466423c6a919f929eb765f3 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -32,8 +32,7 @@ typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
 
 Node TheoryEngine::preprocess(TNode t) {
   Node top = rewrite(t);
-  Debug("rewrite") << "rewrote: " << t << "\nto     : " << top << "\n";
-  return top;
+  Debug("rewrite") << "rewrote: " << t << endl << "to     : " << top << endl;
 
   list<TNode> toReg;
   toReg.push_back(top);

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e85e66e99671bcb4c37c1abbb1a36cb55ae4ee34..00336a1e33557188c86b867402024587a4571444 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -68,7 +68,7 @@ class TheoryEngine {
       d_conflictNode(context) {
     }
 
-    void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted) {
+    void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) {
       Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
       d_conflictNode = conflictNode;
       if(safe) {
@@ -76,14 +76,16 @@ class TheoryEngine {
       }
     }
 
-    void propagate(TNode, bool) throw(theory::Interrupted) {
+    void propagate(TNode, bool) throw(theory::Interrupted, AssertionException) {
     }
 
-    void lemma(TNode node, bool) throw(theory::Interrupted) {
+    void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
       d_engine->newLemma(node);
     }
-
-    void explanation(TNode, bool) throw(theory::Interrupted) {
+    void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
+      d_engine->newAugmentingLemma(node);
+    }
+    void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) {
     }
   };
 
@@ -289,7 +291,10 @@ public:
   inline void newLemma(TNode node) {
     d_propEngine->assertLemma(node);
   }
-
+  inline void newAugmentingLemma(TNode node) {
+    Node preprocessed = preprocess(node);
+    d_propEngine->assertFormula(preprocessed);
+  }
   /**
    * Returns the last conflict (if any).
    */

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index e0061dcd9452dce688ad91558b2508bd7918d435..515d496f527e8b7cadc837796eb3ccee0b652ced 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -11,6 +11,7 @@ TESTS =       \
        flet.smt \
        flet2.smt \
        ite_real_int_type.smt \
+       ite_real_valid.smt \
        let.smt \
        let2.smt \
        simple2.smt \

diff --git a/test/regress/regress0/ite_real_valid.smt b/test/regress/regress0/ite_real_valid.smt
new file mode 100644 (file)
index 0000000..eeaaa17
--- /dev/null
+++ b/test/regress/regress0/ite_real_valid.smt
@@ -0,0 +1,8 @@
+(benchmark ite_real_valid
+:logic QF_LRA
+:status unsat
+:extrafuns ((x Real))
+:extrapreds ((b))
+:formula
+  (not (implies (= x (ite b 0 1)) (>= x 0)))
+)

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index e0dfd7aa830866db07c013ce15cc5375da329be4..0443b7b8e885b6800afd938763e85a535815a430 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -47,20 +47,24 @@ public:
 
   ~TestOutputChannel() {}
 
-  void safePoint() throw(Interrupted) {}
+  void safePoint() throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n, bool safe = false) throw(Interrupted) {
+  void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false) throw(Interrupted) {
+  void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
     push(PROPAGATE, n);
   }
 
-  void lemma(TNode n, bool safe = false) throw(Interrupted) {
+  void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
     push(LEMMA, n);
   }
-  void explanation(TNode n, bool safe = false) throw(Interrupted) {
+  void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+    Unreachable();
+  }
+
+  void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
     push(EXPLANATION, n);
   }
 

diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index 6b14a38d56530ab8a716d86cb645843b2c820fc1..8be56bc79d3fae9f947b03958b17765763eeecc0 100644 (file)
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -48,20 +48,23 @@ public:
 
   ~TestOutputChannel() {}
 
-  void safePoint() throw(Interrupted) {}
+  void safePoint()  throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n, bool safe = false) throw(Interrupted) {
+  void conflict(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false) throw(Interrupted) {
+  void propagate(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
     push(PROPOGATE, n);
   }
 
-  void lemma(TNode n, bool safe = false) throw(Interrupted) {
+  void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
     push(LEMMA, n);
   }
-  void explanation(TNode n, bool safe = false) throw(Interrupted) {
+  void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+    Unreachable();
+  }
+  void explanation(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
     push(EXPLANATION, n);
   }