In order for splitting on demand to be able to retract clauses every translation...

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 350b6f5cfcba3a22f14f00594abf6fae2f89d2ca..225f95d545788ed2938c7aa5ba7df8b02ea300e7 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -326,66 +326,233 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
 }
 
 
-SatLiteral TseitinCnfStream::toCNF(TNode node) {
-  Debug("cnf") << "toCNF(" << node << ")" << endl;
+SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
+  Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
-  // If the node has already been translated, return the previous translation
-  if(isCached(node)) {
-    return lookupInCache(node);
-  }
+  SatLiteral nodeLit;
+  Node negatedNode = node.notNode();
 
-  // Handle each Boolean operator case
-  switch(node.getKind()) {
-  case NOT:
-    return handleNot(node);
-  case XOR:
-    return handleXor(node);
-  case ITE:
-    return handleIte(node);
-  case IFF:
-    return handleIff(node);
-  case IMPLIES:
-    return handleImplies(node);
-  case OR:
-    return handleOr(node);
-  case AND:
-    return handleAnd(node);
-  default:
-    {
-      //TODO make sure this does not contain any boolean substructure
-      return handleAtom(node);
-      //Unreachable();
-      //Node atomic = handleNonAtomicNode(node);
-      //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+  // If the non-negated node has already been translated, get the translation
+  if(isCached(node)) {
+    nodeLit = lookupInCache(node);
+  } else {
+    // Handle each Boolean operator case
+    switch(node.getKind()) {
+    case NOT:
+      nodeLit = handleNot(node);
+      break;
+    case XOR:
+      nodeLit = handleXor(node);
+      break;
+    case ITE:
+      nodeLit = handleIte(node);
+      break;
+    case IFF:
+      nodeLit = handleIff(node);
+      break;
+    case IMPLIES:
+      nodeLit = handleImplies(node);
+      break;
+    case OR:
+      nodeLit = handleOr(node);
+      break;
+    case AND:
+      nodeLit = handleAnd(node);
+      break;
+    default:
+      {
+        //TODO make sure this does not contain any boolean substructure
+        nodeLit = handleAtom(node);
+        //Unreachable();
+        //Node atomic = handleNonAtomicNode(node);
+        //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+      }
     }
   }
+
+  // Return the appropriate (negated) literal
+  if (!negated) return nodeLit;
+  else return ~nodeLit;
 }
 
-void TseitinCnfStream::convertAndAssert(TNode node, bool lemma) {
-  Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
-  d_assertingLemma = lemma;
-  if(node.getKind() == AND) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) {
+  Assert(node.getKind() == AND);
+  if (!negated) {
     // If the node is a conjunction, we handle each conjunct separately
-    for( TNode::const_iterator conjunct = node.begin(),
-         node_end = node.end();
-         conjunct != node_end;
-         ++conjunct ) {
-      convertAndAssert(*conjunct, lemma);
+    for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
+        conjunct != node_end; ++conjunct ) {
+      convertAndAssert(*conjunct, lemma, false);
+    }
+  } else {
+    // If the node is a disjunction, we construct a clause and assert it
+    int nChildren = node.getNumChildren();
+    SatClause clause(nChildren);
+    TNode::const_iterator disjunct = node.begin();
+    for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
+      Assert( disjunct != node.end() );
+      clause[i] = toCNF(*disjunct, true);
     }
-  } else if(node.getKind() == OR) {
+    Assert(disjunct == node.end());
+    assertClause(node, clause);
+  }
+}
+
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) {
+  Assert(node.getKind() == OR);
+  if (!negated) {
     // If the node is a disjunction, we construct a clause and assert it
     int nChildren = node.getNumChildren();
     SatClause clause(nChildren);
     TNode::const_iterator disjunct = node.begin();
     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
       Assert( disjunct != node.end() );
-      clause[i] = toCNF(*disjunct);
+      clause[i] = toCNF(*disjunct, false);
     }
-    Assert( disjunct == node.end() );
+    Assert(disjunct == node.end());
     assertClause(node, clause);
   } else {
-    // Otherwise, we just convert using the definitional transformation
-    assertClause(node, toCNF(node));
+    // If the node is a conjunction, we handle each conjunct separately
+    for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
+        conjunct != node_end; ++conjunct ) {
+      convertAndAssert(*conjunct, lemma, true);
+    }
+  }
+}
+
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) {
+  if (!negated) {
+    // p XOR q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    // Construct the clauses (p => !q) and (!q => p)
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = ~q;
+    assertClause(node, clause1);
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = q;
+    assertClause(node, clause2);
+  } else {
+    // !(p XOR q) is the same as p <=> q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    // Construct the clauses (p => q) and (q => p)
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = q;
+    assertClause(node, clause1);
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = ~q;
+    assertClause(node, clause2);
+  }
+}
+
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
+  if (!negated) {
+    // p <=> q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    // Construct the clauses (p => q) and (q => p)
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = q;
+    assertClause(node, clause1);
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = ~q;
+    assertClause(node, clause2);
+  } else {
+    // !(p <=> q) is the same as p XOR q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    // Construct the clauses (p => !q) and (!q => p)
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = ~q;
+    assertClause(node, clause1);
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = q;
+    assertClause(node, clause2);
+  }
+}
+
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
+  if (!negated) {
+    // p => q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    // Construct the clause ~p || q
+    SatClause clause(2);
+    clause[0] = ~p;
+    clause[1] = q;
+    assertClause(node, clause);
+  } else {// Construct the
+    // !(p => q) is the same as (p && ~q)
+    convertAndAssert(node[0], lemma, false);
+    convertAndAssert(node[1], lemma, true);
+  }
+}
+
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) {
+  // ITE(p, q, r)
+  SatLiteral p = toCNF(node[0], false);
+  SatLiteral q = toCNF(node[1], negated);
+  SatLiteral r = toCNF(node[2], negated);
+  // Construct the clauses:
+  // (p => q) and (!p => r) and (!q => !p) and (!r => p)
+  SatClause clause1(2);
+  clause1[0] = ~p;
+  clause1[1] = q;
+  assertClause(node, clause1);
+  SatClause clause2(2);
+  clause2[0] = p;
+  clause2[1] = r;
+  assertClause(node, clause2);
+  SatClause clause3(2);
+  clause3[0] = q;
+  clause3[1] = ~p;
+  assertClause(node, clause3);
+  SatClause clause4(2);
+  clause4[0] = r;
+  clause4[1] = p;
+  assertClause(node, clause4);
+}
+
+// At the top level we must ensure that all clauses that are asserted are
+// not unit, except for the direct assertions. This allows us to remove the
+// clauses later when they are not needed anymore (lemmas for example).
+void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) {
+  Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+  d_assertingLemma = lemma;
+  switch(node.getKind()) {
+  case AND:
+    convertAndAssertAnd(node, lemma, negated);
+    break;
+  case OR:
+    convertAndAssertOr(node, lemma, negated);
+    break;
+  case IFF:
+    convertAndAssertIff(node, lemma, negated);
+    break;
+  case XOR:
+    convertAndAssertXor(node, lemma, negated);
+    break;
+  case IMPLIES:
+    convertAndAssertImplies(node, lemma, negated);
+    break;
+  case ITE:
+    convertAndAssertIte(node, lemma, negated);
+    break;
+  case NOT:
+    convertAndAssert(node[0], lemma, !negated);
+    break;
+  default:
+    // Atoms
+    assertClause(node, toCNF(node, negated));
+    break;
   }
 }
 

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index a574adf234f6718efcb720ab4b2765bd5a198640..ce6c7eb1edd2a6b7a4bab32bcd9423b3b49a098c 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -144,9 +144,10 @@ public:
   /**
    * Converts and asserts a formula.
    * @param node node to convert and assert
-   * @param whether the sat solver can choose to remove this clause
+   * @param whether the sat solver can choose to remove the clauses
+   * @param negated wheather we are asserting the node negated
    */
-  virtual void convertAndAssert(TNode node, bool lemma = false) = 0;
+  virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -185,8 +186,9 @@ public:
    * Convert a given formula to CNF and assert it to the SAT solver.
    * @param node the formula to assert
    * @param lemma is this a lemma that is erasable
+   * @param negated true if negated
    */
-  void convertAndAssert(TNode node, bool lemma);
+  void convertAndAssert(TNode node, bool lemma, bool negated = false);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -215,13 +217,20 @@ private:
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
+  void convertAndAssertAnd(TNode node, bool lemma, bool negated);
+  void convertAndAssertOr(TNode node, bool lemma, bool negated);
+  void convertAndAssertXor(TNode node, bool lemma, bool negated);
+  void convertAndAssertIff(TNode node, bool lemma, bool negated);
+  void convertAndAssertImplies(TNode node, bool lemma, bool negated);
+  void convertAndAssertIte(TNode node, bool lemma, bool negated);
 
   /**
    * Transforms the node into CNF recursively.
    * @param node the formula to transform
+   * @param negated wheather the literal is negated
    * @return the literal representing the root of the formula
    */
-  SatLiteral toCNF(TNode node);
+  SatLiteral toCNF(TNode node, bool negated = false);
 
 }; /* class TseitinCnfStream */
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b9fbd3ce61f5b4ebce4dffb1c57c10e5816a2328..16881f9e4fdde3921451d98103d4cb645e9883a7 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -77,14 +77,14 @@ void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(node);
+  d_cnfStream->convertAndAssert(node, false, false);
 }
 
 void PropEngine::assertLemma(TNode node) {
   Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as removable
-  d_cnfStream->convertAndAssert(node);
+  d_cnfStream->convertAndAssert(node, false, false);
 }
 
 

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 9c8560783a1bb80c8938e1db8ccbd52badb7b523..bbae46df7d7cf8ccef72113245d9fb7b313cb9ef 100644 (file)
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -104,7 +104,7 @@ void testAnd() {
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::AND, a, b, c) );
+      d_nodeManager->mkNode(kind::AND, a, b, c), false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -125,13 +125,13 @@ void testComplexExpr() {
               d_nodeManager->mkNode(kind::OR, c, d),
               d_nodeManager->mkNode(
                   kind::NOT,
-                  d_nodeManager->mkNode(kind::XOR, e, f)))) );
+                  d_nodeManager->mkNode(kind::XOR, e, f)))), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
 void testFalse() {
   NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false) );
+  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -140,7 +140,7 @@ void testIff() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::IFF, a, b) );
+      d_nodeManager->mkNode(kind::IFF, a, b), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -149,7 +149,7 @@ void testImplies() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::IMPLIES, a, b) );
+      d_nodeManager->mkNode(kind::IMPLIES, a, b), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -165,7 +165,7 @@ void testIte() {
               d_nodeManager->mkVar(d_nodeManager->integerType())
           ),
           d_nodeManager->mkVar(d_nodeManager->integerType())
-                            ));
+                            ), false);
 
 }
 
@@ -173,7 +173,7 @@ void testNot() {
   NodeManagerScope nms(d_nodeManager);
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::NOT, a) );
+      d_nodeManager->mkNode(kind::NOT, a), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -183,13 +183,13 @@ void testOr() {
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::OR, a, b, c) );
+      d_nodeManager->mkNode(kind::OR, a, b, c), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
 void testTrue() {
   NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) );
+  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -197,10 +197,10 @@ void testVar() {
   NodeManagerScope nms(d_nodeManager);
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-  d_cnfStream->convertAndAssert(a);
+  d_cnfStream->convertAndAssert(a, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
   d_satSolver->reset();
-  d_cnfStream->convertAndAssert(b);
+  d_cnfStream->convertAndAssert(b, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -209,7 +209,7 @@ void testXor() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::XOR, a, b) );
+      d_nodeManager->mkNode(kind::XOR, a, b), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 };