merged master with dejan's constant evaluating equality engine

7 files changed, 43 insertions, 314 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 804bcde11..1952108f6 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,14 +1,9 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
+	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-noinst_LTLIBRARIES = libutil.la libutilcudd.la libstatistics.la
-
-# libutilcudd.la is a separate library so that we can pass separate
-# compiler flags
-libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@
-libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ @CUDD_LIBS@
+noinst_LTLIBRARIES = libutil.la libstatistics.la
 
 libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT
 
@@ -91,17 +86,10 @@ libutil_la_SOURCES = \
 	sort_inference.h \
 	sort_inference.cpp
 
-libutil_la_LIBADD = \
-	@builddir@/libutilcudd.la
-
 libstatistics_la_SOURCES = \
 	statistics_registry.h \
 	statistics_registry.cpp
 
-libutilcudd_la_SOURCES = \
-	propositional_query.h \
-	propositional_query.cpp
-
 BUILT_SOURCES = \
 	rational.h \
 	integer.h \
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index c6e951049..9be4e4104 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -122,7 +122,7 @@ bool Configuration::isBuiltWithCln() {
 }
 
 bool Configuration::isBuiltWithCudd() {
-  return IS_CUDD_BUILD;
+  return false;
 }
 
 bool Configuration::isBuiltWithTlsSupport() {
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 4378badc8..7c94f4c18 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -89,12 +89,6 @@ namespace CVC4 {
 #  define IS_COMPETITION_BUILD false
 #endif /* CVC4_COMPETITION_MODE */
 
-#ifdef CVC4_CUDD
-#  define IS_CUDD_BUILD true
-#else /* CVC4_CUDD */
-#  define IS_CUDD_BUILD false
-#endif /* CVC4_CUDD */
-
 #ifdef CVC4_GMP_IMP
 #  define IS_GMP_BUILD true
 #else /* CVC4_GMP_IMP */
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 240e5a0cf..de7ae2e97 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -19,6 +19,7 @@
 #include "util/ite_removal.h"
 #include "theory/rewriter.h"
 #include "expr/command.h"
+#include "theory/quantifiers/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -28,12 +29,13 @@ namespace CVC4 {
 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
-    output[i] = run(output[i], output, iteSkolemMap);
+    std::vector<Node> quantVar;
+    output[i] = run(output[i], output, iteSkolemMap, quantVar);
   }
 }
 
 Node RemoveITE::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap) {
+                    IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
@@ -50,8 +52,23 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   if(node.getKind() == kind::ITE) {
     TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean()) {
+      Node skolem;
       // Make the skolem to represent the ITE
-      Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+      if( quantVar.empty() ){
+        skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+      }else{
+        //if in the scope of free variables, make a skolem operator
+        vector< TypeNode > argTypes;
+        for( size_t i=0; i<quantVar.size(); i++ ){
+          argTypes.push_back( quantVar[i].getType() );
+        }
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
+        Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
+        vector< Node > funcArgs;
+        funcArgs.push_back( op );
+        funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
+        skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+      }
 
       // The new assertion
       Node newAssertion =
@@ -63,7 +80,16 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       d_iteCache[node] = skolem;
 
       // Remove ITEs from the new assertion, rewrite it and push it to the output
-      newAssertion = run(newAssertion, output, iteSkolemMap);
+      newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
+
+      if( !quantVar.empty() ){
+        //if in the scope of free variables, it is a quantified assertion
+        vector< Node > children;
+        children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
+        children.push_back( newAssertion );
+        newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
+      }
+
       iteSkolemMap[skolem] = output.size();
       output.push_back(newAssertion);
 
@@ -73,9 +99,16 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
 
   // If not an ITE, go deep
-  if( node.getKind() != kind::FORALL &&
+  if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
       node.getKind() != kind::EXISTS &&
       node.getKind() != kind::REWRITE_RULE ) {
+    std::vector< Node > newQuantVar;
+    newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
+    if( node.getKind()==kind::FORALL ){
+      for( size_t i=0; i<node[0].getNumChildren(); i++ ){
+        newQuantVar.push_back( node[0][i] );
+      }
+    }
     vector<Node> newChildren;
     bool somethingChanged = false;
     if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -83,7 +116,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
     }
     // Remove the ITEs from the children
     for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-      Node newChild = run(*it, output, iteSkolemMap);
+      Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
       somethingChanged |= (newChild != *it);
       newChildren.push_back(newChild);
     }
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 77e9c39db..6c0c74cd4 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -55,7 +55,7 @@ public:
    * ite created in conjunction with that skolem variable.
    */
   Node run(TNode node, std::vector<Node>& additionalAssertions,
-           IteSkolemMap& iteSkolemMap);
+           IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
 
 };/* class RemoveTTE */
 
diff --git a/src/util/propositional_query.cpp b/src/util/propositional_query.cpp
deleted file mode 100644
index f4ee3840b..000000000
--- a/src/util/propositional_query.cpp
+++ /dev/null
@@ -1,226 +0,0 @@
-/*********************                                                        */
-/*! \file propositional_query.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A class for simple, quick, propositional
- ** satisfiability/validity checking
- **
- ** PropositionalQuery is a way for parts of CVC4 to do quick purely
- ** propositional satisfiability or validity checks on a Node.  These
- ** checks do no theory reasoning, and handle atoms as propositional
- ** variables, but can sometimes be useful for subqueries.
- **/
-
-#include "util/propositional_query.h"
-
-#include <map>
-#include <algorithm>
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-
-#ifdef CVC4_CUDD
-
-#include <util.h>
-#include <cudd.h>
-#include <cuddObj.hh>
-
-namespace CVC4 {
-
-class BddInstance {
-private:
-  Cudd d_mgr;
-  typedef std::map<Node, BDD> AtomToIDMap;
-  AtomToIDMap d_atomToBddMap;
-
-  unsigned d_atomId;
-
-  BDD encodeNode(TNode t);
-  BDD encodeAtom(TNode t);
-  BDD encodeCombinator(TNode t);
-
-  bool isAnAtom(TNode t) {
-    switch(t.getKind()) {
-    case NOT:
-    case XOR:
-    case IFF:
-    case IMPLIES:
-    case OR:
-    case AND:
-      return false;
-    case ITE:
-      return t.getType().isBoolean();
-    default:
-      return true;
-    }
-  }
-
-  void setupAtoms(TNode t);
-
-  void clear() {
-    d_atomId = 0;
-    d_atomToBddMap.clear();
-  }
-
-  Result d_result;
-
-public:
-  static const unsigned MAX_VARIABLES = 20;
-
-  BddInstance(TNode t) : d_atomToBddMap(), d_atomId(0) {
-    setupAtoms(t);
-
-    Debug("bdd::sat") << t << endl;
-    Debug("bdd::sat") << d_atomToBddMap.size() << endl;
-
-
-    if(d_atomToBddMap.size() > MAX_VARIABLES) {
-      d_result = Result(Result::SAT_UNKNOWN, Result::TIMEOUT);
-    } else {
-      BDD res = encodeNode(t);
-      BDD falseBdd = d_mgr.bddZero();
-      bool isUnsat = (res == falseBdd);
-
-      clear();
-
-      if(isUnsat) {
-        d_result = Result::UNSAT;
-      } else {
-        d_result = Result::SAT;
-      }
-    }
-  }
-
-  Result getResult() const { return d_result; }
-
-};/* class BddInstance */
-
-}/* CVC4 namespace */
-
-BDD BddInstance::encodeNode(TNode t) {
-  if(isAnAtom(t)) {
-    return encodeAtom(t);
-  } else {
-    return encodeCombinator(t);
-  }
-}
-
-BDD BddInstance::encodeCombinator(TNode t) {
-  switch(t.getKind()) {
-  case XOR: {
-    Assert(t.getNumChildren() == 2);
-    return encodeNode(t[0]).Xor(encodeNode(t[1]));
-  }
-
-  case IFF: {
-    Assert(t.getNumChildren() == 2);
-    BDD left = encodeNode(t[0]);
-    BDD right = encodeNode(t[1]);
-    return (!left | right) & (left | !right);
-  }
-
-  case IMPLIES: {
-    Assert(t.getNumChildren() == 2);
-    BDD left = encodeNode(t[0]);
-    BDD right = encodeNode(t[1]);
-    return (!left | right);
-  }
-
-  case AND:
-  case OR: {
-    Assert(t.getNumChildren() >= 2);
-    TNode::iterator i = t.begin(), end = t.end();
-    BDD tmp = encodeNode(*i);
-    ++i;
-    for(; i != end; ++i) {
-      BDD curr = encodeNode(*i);
-      if(t.getKind() == AND) {
-        tmp = tmp & curr;
-      } else {
-        tmp = tmp | curr;
-      }
-    }
-    return tmp;
-  }
-
-  case ITE: {
-    Assert(t.getType().isBoolean());
-    BDD cnd = encodeNode(t[0]);
-    BDD thenBranch = encodeNode(t[1]);
-    BDD elseBranch = encodeNode(t[2]);
-    return cnd.Ite(thenBranch, elseBranch);
-  }
-
-  case NOT:
-    return ! encodeNode(t[0]);
-
-  default:
-    Unhandled(t.getKind());
-  }
-}
-
-BDD BddInstance::encodeAtom(TNode t) {
-  if(t.getKind() == kind::CONST_BOOLEAN) {
-    if(t.getConst<bool>()) {
-      return d_mgr.bddOne();
-    } else {
-      return d_mgr.bddZero();
-    }
-  }
-  Assert(t.getKind() != kind::CONST_BOOLEAN);
-
-  AtomToIDMap::iterator findT = d_atomToBddMap.find(t);
-
-  Assert(d_atomToBddMap.find(t) != d_atomToBddMap.end());
-  return findT->second;
-}
-
-void BddInstance::setupAtoms(TNode t) {
-  if(t.getKind() == kind::CONST_BOOLEAN) {
-    // do nothing
-  } else if(isAnAtom(t)) {
-    AtomToIDMap::iterator findT = d_atomToBddMap.find(t);
-    if(findT == d_atomToBddMap.end()) {
-      BDD var = d_mgr.bddVar();
-      d_atomToBddMap.insert(make_pair(t, var));
-      d_atomId++;
-    }
-  } else {
-    for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i) {
-      setupAtoms(*i);
-    }
-  }
-}
-
-Result PropositionalQuery::isSatisfiable(TNode q) {
-  BddInstance instance(q);
-  return instance.getResult();
-}
-
-Result PropositionalQuery::isTautology(TNode q) {
-  Node negQ = q.notNode();
-  Result satResult = isSatisfiable(negQ);
-  return satResult.asValidityResult();
-}
-
-#else /* CVC4_CUDD */
-
-// if CUDD wasn't available at build time, just return UNKNOWN everywhere.
-
-Result PropositionalQuery::isSatisfiable(TNode q) {
-  return Result(Result::SAT_UNKNOWN, Result::UNSUPPORTED);
-}
-
-Result PropositionalQuery::isTautology(TNode q) {
-  return Result(Result::VALIDITY_UNKNOWN, Result::UNSUPPORTED);
-}
-
-#endif /* CVC4_CUDD */
diff --git a/src/util/propositional_query.h b/src/util/propositional_query.h
deleted file mode 100644
index b1dc58cee..000000000
--- a/src/util/propositional_query.h
+++ /dev/null
@@ -1,60 +0,0 @@
-/*********************                                                        */
-/*! \file propositional_query.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A class for simple, quick, propositional
- ** satisfiability/validity checking
- **
- ** PropositionalQuery is a way for parts of CVC4 to do quick purely
- ** propositional satisfiability or validity checks on a Node.  These
- ** checks do no theory reasoning, and handle atoms as propositional
- ** variables, but can sometimes be useful for subqueries.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PROPOSITIONAL_QUERY_H
-#define __CVC4__PROPOSITIONAL_QUERY_H
-
-#include "expr/node.h"
-#include "util/result.h"
-
-namespace CVC4 {
-
-/**
- * PropositionalQuery is a way for parts of CVC4 to do quick purely
- * propositional satisfiability or validity checks on a Node.
- */
-class PropositionalQuery {
-public:
-
-  /**
-   * Returns whether a node q is propositionally satisfiable.
-   *
-   * @param q Node to be checked for satisfiability.
-   * @pre q is a ground formula.
-   * @pre effort is between 0 and 1.
-   */
-  static Result isSatisfiable(TNode q);
-
-  /**
-   * Returns whether a node q is a propositional tautology.
-   *
-   * @param q Node to be checked for satisfiability.
-   * @pre q is a ground formula.
-   * @pre effort is between 0 and 1.
-   */
-  static Result isTautology(TNode q);
-
-};/* class PropositionalQuery */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PROPOSITIONAL_QUERY_H */