Remove PropositionalQuery class and all CUDD-related build stuff (and references)

5 files changed, 2 insertions, 306 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index dffb22ea8..1952108f6 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -3,12 +3,7 @@ AM_CPPFLAGS = \
 	-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/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 */