From d2642261cdfcc6d08087764bbccf7ecdc25f262f Mon Sep 17 00:00:00 2001
From: Dejan Jovanovic <dejan.jovanovic@gmail.com>
Date: Tue, 1 Sep 2015 23:08:25 -0700
Subject: theoryOf() -> uninterpreted sort owner example

---
 src/prop/cnf_stream.cpp                | 40 +++++++++++++++++++++-------------
 src/prop/cnf_stream.h                  |  2 +-
 src/theory/theory.h                    |  3 ++-
 test/regress/regress0/bool/test02.smt2 | 18 +++++++++++++++
 4 files changed, 46 insertions(+), 17 deletions(-)
 create mode 100644 test/regress/regress0/bool/test02.smt2

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 2f7f2a30a..c1c7fc518 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -227,7 +227,8 @@ SatLiteral CnfStream::convertAtom(TNode node) {
   bool preRegister = false;
 
   // Is this a variable add it to the list
-  if (node.isVar()) {
+  // TODO(bool): if Skolem, it's a theory literal
+  if (node.isVar() && true) {
     d_booleanVariables.push_back(node);
   } else {
     theoryLiteral = true;
@@ -368,35 +369,44 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 }
 
 
-SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
-  Assert(!hasLiteral(iffNode), "Atom already mapped!");
-  Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
-  Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+SatLiteral TseitinCnfStream::handleEq(TNode eqNode) {
+  Assert(!hasLiteral(eqNode), "Atom already mapped!");
+  Assert(eqNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
+  Assert(eqNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
-  Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
+  Debug("cnf") << "handleEq(" << eqNode << ")" << endl;
 
   // Convert the children to CNF
-  SatLiteral a = toCNF(iffNode[0]);
-  SatLiteral b = toCNF(iffNode[1]);
+  SatLiteral a = toCNF(eqNode[0]);
+  SatLiteral b = toCNF(eqNode[1]);
+
+  // TODO(bool): See if this is an equality between Skolem or predicates
+  bool lhsIsTheory = false;
+  bool rhsIsTheory = false;
 
   // Get the now literal
-  SatLiteral iffLit = newLiteral(iffNode);
+  SatLiteral eqLit;
+  if (lhsIsTheory && rhsIsTheory) {
+    eqLit = newLiteral(eqNode, true, true, false);
+  } else {
+    eqLit = newLiteral(eqNode);
+  }
 
   // lit -> ((a-> b) & (b->a))
   // ~lit | ((~a | b) & (~b | a))
   // (~a | b | ~lit) & (~b | a | ~lit)
-  assertClause(iffNode, ~a, b, ~iffLit);
-  assertClause(iffNode, a, ~b, ~iffLit);
+  assertClause(eqNode, ~a, b, ~eqLit);
+  assertClause(eqNode, a, ~b, ~eqLit);
 
   // (a<->b) -> lit
   // ~((a & b) | (~a & ~b)) | lit
   // (~(a & b)) & (~(~a & ~b)) | lit
   // ((~a | ~b) & (a | b)) | lit
   // (~a | ~b | lit) & (a | b | lit)
-  assertClause(iffNode, ~a, ~b, iffLit);
-  assertClause(iffNode, a, b, iffLit);
+  assertClause(eqNode, ~a, ~b, eqLit);
+  assertClause(eqNode, a, b, eqLit);
 
-  return iffLit;
+  return eqLit;
 }
 
 
@@ -481,7 +491,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case EQUAL:
       if(node[0].getType().isBoolean()) {
         // normally this is an IFF, but EQUAL is possible with pseudobooleans
-        nodeLit = handleIff(node);
+        nodeLit = handleEq(node);
       } else {
         nodeLit = convertAtom(node);
       }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b22290ae4..b0df99693 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -313,7 +313,7 @@ private:
   SatLiteral handleNot(TNode node);
   SatLiteral handleXor(TNode node);
   SatLiteral handleImplies(TNode node);
-  SatLiteral handleIff(TNode node);
+  SatLiteral handleEq(TNode node);
   SatLiteral handleIte(TNode node);
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2dab434d1..64e268358 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -331,7 +331,8 @@ public:
     } else {
       id = kindToTheoryId(typeNode.getKind());
     }
-    if (id == THEORY_BUILTIN) {
+    // TODO(bool): Check if this is OK?
+    if (id == THEORY_BUILTIN || id == THEORY_BOOL) {
       Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
       return s_uninterpretedSortOwner;
     }
diff --git a/test/regress/regress0/bool/test02.smt2 b/test/regress/regress0/bool/test02.smt2
new file mode 100644
index 000000000..051778d9b
--- /dev/null
+++ b/test/regress/regress0/bool/test02.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_UF)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun f (Bool) Bool)
+
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+
+(assert (not (= (f (f x)) (f (f y))))) ;; => f(x) != f(y) => x != y
+(assert (not (= (f y) (f z))))         ;; => y != z
+(assert (not (= x z)))
+
+(check-sat)
+
+(exit)
-- 
cgit v1.2.3