Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its...

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7c8fb229acdd7f85aa43fa57b0b2ac1fb21b5920..a1b5b771fab70898a8d190bc6db047316d204862 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -229,6 +229,9 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
     case kind::UMINUS:
       typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
       break;
+    case kind::DIVISION:
+      typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
+      break;
     case kind::CONST_RATIONAL:
       typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n);
       break;

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 219c25399ee2786bb60eafa0e70dd6b931e6a731..350b6f5cfcba3a22f14f00594abf6fae2f89d2ca 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -325,49 +325,6 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   return iteLit;
 }
 
-Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
-  Debug("cnf") << "handleNonAtomicNode(" << node << ")" << endl;
-
-  /* Our main goal here is to tease out any ITE's sitting under a theory operator. */
-  Node rewrite;
-  NodeManager *nodeManager = NodeManager::currentNM();
-  if(nodeManager->getAttribute(node, IteRewriteAttr(), rewrite)) {
-    return rewrite.isNull() ? Node(node) : rewrite;
-  }
-
-  if(node.getKind() == ITE) {
-    Assert( node.getNumChildren() == 3 );
-    //TODO should this be a skolem?
-    Node skolem = nodeManager->mkVar(node.getType());
-    Node newAssertion =
-        nodeManager->mkNode(
-            ITE,
-            node[0],
-            nodeManager->mkNode(EQUAL, skolem, node[1]),
-            nodeManager->mkNode(EQUAL, skolem, node[2]));
-    nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
-    convertAndAssert(newAssertion, d_assertingLemma);
-    return skolem;
-  } else {
-    std::vector<Node> newChildren;
-    bool somethingChanged = false;
-    for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-      Node newChild = handleNonAtomicNode(*it);
-      somethingChanged |= (newChild != *it);
-      newChildren.push_back(newChild);
-    }
-
-    if(somethingChanged) {
-
-      rewrite = nodeManager->mkNode(node.getKind(), newChildren);
-      nodeManager->setAttribute(node, IteRewriteAttr(), rewrite);
-      return rewrite;
-    } else {
-      nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
-      return node;
-    }
-  }
-}
 
 SatLiteral TseitinCnfStream::toCNF(TNode node) {
   Debug("cnf") << "toCNF(" << node << ")" << endl;
@@ -395,8 +352,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
     return handleAnd(node);
   default:
     {
-      Node atomic = handleNonAtomicNode(node);
-      return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+      //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);
     }
   }
 }

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 1ea600322afc7c098b48c63486b9b8dc27cd3520..a574adf234f6718efcb720ab4b2765bd5a198640 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -215,9 +215,6 @@ private:
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
-  struct IteRewriteTag {};
-  typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
-  Node handleNonAtomicNode(TNode node);
 
   /**
    * Transforms the node into CNF recursively.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5af64c5ddc0f73567466423c6a919f929eb765f3..22b2b2b22365cc0c416a464a3f18e4ed30f3cea7 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -28,6 +28,9 @@ namespace theory {
 struct PreRegisteredTag {};
 typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
 
+struct IteRewriteTag {};
+typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
+
 }/* CVC4::theory namespace */
 
 Node TheoryEngine::preprocess(TNode t) {
@@ -82,6 +85,57 @@ Node TheoryEngine::preprocess(TNode t) {
   }
 
   return top;
+}
+  /* Our goal is to tease out any ITE's sitting under a theory operator. */
+Node TheoryEngine::removeITEs(TNode node) {
+  Debug("ite") << "handleNonAtomicNode(" << node << ")" << endl;
+
+  /* The result may be cached already */
+  Node rewrite;
+  NodeManager *nodeManager = NodeManager::currentNM();
+  if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), rewrite)) {
+    return rewrite.isNull() ? Node(node) : rewrite;
+  }
+
+  if(node.getKind() == kind::ITE){
+    if(theoryOf(node[1]) != &d_bool && node[1].getKind() != kind::EQUAL) {
+      Assert( node.getNumChildren() == 3 );
+
+      Debug("ite") << theoryOf(node[1]) << " " << &d_bool <<endl;
+
+      Node skolem = nodeManager->mkVar(node.getType());
+      Node newAssertion =
+        nodeManager->mkNode(
+                            kind::ITE,
+                            node[0],
+                            nodeManager->mkNode(kind::EQUAL, skolem, node[1]),
+                            nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
+      nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
+
+      Node preprocessed = preprocess(newAssertion);
+      d_propEngine->assertFormula(preprocessed);
+
+      return skolem;
+    }
+  }
+  std::vector<Node> newChildren;
+  bool somethingChanged = false;
+  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+    Node newChild = removeITEs(*it);
+    somethingChanged |= (newChild != *it);
+    newChildren.push_back(newChild);
+  }
+
+  if(somethingChanged) {
+
+    rewrite = nodeManager->mkNode(node.getKind(), newChildren);
+    nodeManager->setAttribute(node, theory::IteRewriteAttr(), rewrite);
+    return rewrite;
+  } else {
+    nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null());
+    return node;
+  }
+
 }
 
 Node TheoryEngine::rewrite(TNode in) {
@@ -93,28 +147,10 @@ Node TheoryEngine::rewrite(TNode in) {
     return in;
   }
 
-  /*
-    theory::Theory* thy = theoryOf(in);
-    if(thy == NULL) {
-    Node out = rewriteBuiltins(in);
-    setRewriteCache(in, out);
-    return in;
-    } else {
-    Node out = thy->rewrite(in);
-    setRewriteCache(in, out);
-    return out;
-    }
-  */
+  in = removeITEs(in);
 
   // these special cases should go away when theory rewriting comes online
-  if(in.getKind() == kind::EQUAL) {
-    Assert(in.getNumChildren() == 2);
-    if(in[0] == in[1]) {
-      Node out = NodeManager::currentNM()->mkConst(true);
-      //setRewriteCache(in, out);
-      return out;
-    }
-  } else if(in.getKind() == kind::DISTINCT) {
+  if(in.getKind() == kind::DISTINCT) {
     vector<Node> diseqs;
     for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
       TNode::iterator j = i;
@@ -130,14 +166,24 @@ Node TheoryEngine::rewrite(TNode in) {
       : NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
     //setRewriteCache(in, out);
     return out;
-  } else {
-    Node out = rewriteChildren(in);
+  }
+
+  theory::Theory* thy = theoryOf(in);
+  if(thy == NULL) {
+    Node out = rewriteBuiltins(in);
+    //setRewriteCache(in, out);
+    return in;
+  } else if(thy != &d_bool){
+    Node out = thy->rewrite(in);
     //setRewriteCache(in, out);
     return out;
+  }else{
+    Node out = rewriteChildren(in);
+    setRewriteCache(in, out);
+    return out;
   }
 
-  //setRewriteCache(in, in);
-  return in;
+  Unreachable();
 }
 
 }/* CVC4 namespace */

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 00336a1e33557188c86b867402024587a4571444..e9cb56b88396663ae8585d116f0d5e60199bd463 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -136,6 +136,10 @@ class TheoryEngine {
     }
 
     NodeBuilder<> b(in.getKind());
+    if(in.getMetaKind() == kind::metakind::PARAMETERIZED){
+      Assert(in.hasOperator());
+      b << in.getOperator();
+    }
     for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
       b << rewrite(*c);
     }
@@ -168,6 +172,8 @@ class TheoryEngine {
     }
   }
 
+  Node removeITEs(TNode t);
+
 public:
 
   /**
@@ -220,7 +226,14 @@ public:
     Assert(k >= 0 && k < kind::LAST_KIND);
 
     if(k == kind::VARIABLE) {
-      return &d_uf;
+      TypeNode t = n.getType();
+      if(t.isBoolean()){
+        return &d_bool;
+      }else if(t.isReal()){
+        return &d_arith;
+      }else{
+        return &d_uf;
+      }
       //Unimplemented();
     } else if(k == kind::EQUAL) {
       // if LHS is a VARIABLE, use theoryOf(LHS.getType())

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2d7d4e91fd5806034c253dd47d4a8a4d218ce585..1f09ce81d45866dca33ce851236246abb0450575 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -35,6 +35,18 @@ TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
 TheoryUF::~TheoryUF() {
 }
 
+Node TheoryUF::rewrite(TNode n){
+  Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+  Node ret(n);
+  if(n.getKind() == EQUAL){
+    Assert(n.getNumChildren() == 2);
+    if(n[0] == n[1]) {
+      ret = NodeManager::currentNM()->mkConst(true);
+    }
+  }
+  Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+  return ret;
+}
 void TheoryUF::preRegisterTerm(TNode n) {
   Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
   Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 5863a31fcd4cddd0cf8e822b48dcd0299206f4e9..be08cfee796c7024f6dc00e352332b2a06ebe288 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -119,6 +119,14 @@ public:
    */
   void check(Effort level);
 
+
+  /**
+   * Rewrites a node in the theory of uninterpreted functions.
+   * This is fairly basic and only ensures that atoms that are
+   * unsatisfiable or a valid are rewritten to false or true respectively.
+   */
+  Node rewrite(TNode n);
+
   /**
    * Propagates theory literals. Currently does nothing.
    *