more progress:

* equalities are atoms, cnf doesn't dig into equalities
* kinds file: add check and propagate
* split on non-constant terms in full-check

6 files changed, 12 insertions, 47 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 2f7f2a30a..e57494ba8 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -478,14 +478,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case AND:
       nodeLit = handleAnd(node);
       break;
-    case EQUAL:
-      if(node[0].getType().isBoolean()) {
-        // normally this is an IFF, but EQUAL is possible with pseudobooleans
-        nodeLit = handleIff(node);
-      } else {
-        nodeLit = convertAtom(node);
-      }
-      break;
     default:
       {
         //TODO make sure this does not contain any boolean substructure
@@ -577,36 +569,6 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
   }
 }
 
-void TseitinCnfStream::convertAndAssertIff(TNode node, 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 negated) {
   if (!negated) {
     // p => q
@@ -689,11 +651,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   case NOT:
     convertAndAssert(node[0], !negated);
     break;
-  case EQUAL:
-    if( node[0].getType().isBoolean() ){
-      convertAndAssertIff(node, negated);
-      break;
-    }
   default:
     // Atoms
     assertClause(node, toCNF(node, negated));
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b22290ae4..634ddd93c 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -321,7 +321,6 @@ private:
   void convertAndAssertAnd(TNode node, bool negated);
   void convertAndAssertOr(TNode node, bool negated);
   void convertAndAssertXor(TNode node, bool negated);
-  void convertAndAssertIff(TNode node, bool negated);
   void convertAndAssertImplies(TNode node, bool negated);
   void convertAndAssertIte(TNode node, bool negated);
 
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index eea3a9fa6..1e906c386 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -8,6 +8,7 @@ theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_
 typechecker "theory/booleans/theory_bool_type_rules.h"
 
 properties finite
+properties check propagate
 
 rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
 
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index ac9bc9ae1..2f9bcfd9e 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -167,7 +167,7 @@ void TheoryBool::check(Effort effort) {
     Assertion assertion = get();
     TNode fact = assertion.assertion;
 
-    Debug("theroy::bool") << "TheoryBool::check(): processing " << fact << std::endl;
+    Debug("theory::bool") << "TheoryBool::check(): processing " << fact << std::endl;
 
     // Do the work
     bool polarity = fact.getKind() != kind::NOT;
@@ -181,6 +181,16 @@ void TheoryBool::check(Effort effort) {
 
   // If in full effort, check the number of classes (max 2)
   if (!d_conflict && fullEffort(effort)) {
+    // Each class should be either true or false
+    eq::EqClassesIterator class_iterator(&d_equalityEngine);
+    while (!class_iterator.isFinished()) {
+      TNode class_rep = *class_iterator;
+      if (!class_rep.isConst()) {
+        Debug("theory::bool") << "TheoryBool::check(): splitting on " << class_rep << std::endl;
+        d_out->split(class_rep);
+      }
+      ++ class_iterator;
+    }
   }
 }
 
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index f4527648a..a373a5775 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -63,7 +63,6 @@ class CVC4_PUBLIC LogicInfo {
   static inline bool isTrueTheory(theory::TheoryId theory) {
     switch(theory) {
     case theory::THEORY_BUILTIN:
-    case theory::THEORY_BOOL:
     case theory::THEORY_QUANTIFIERS:
       return false;
     default:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5dc4d9408..e570f2cf9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -224,7 +224,6 @@ void TheoryEngine::preRegister(TNode preprocessed) {
 
       // Pre-register the terms in the atom
       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
-      theories = Theory::setRemove(THEORY_BOOL, theories);
       // Remove the top theory, if any more that means multiple theories were involved
       bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
       TheoryId i;