diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-31 14:29:58 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-19 19:09:27 -0400 |
commit | 7dd316a13b796d02985be63b1b03975a756fb624 (patch) | |
tree | ab348129940e25c4dde47c19568aea40d31a51ea /src/util | |
parent | 89a1304db9208a366c10136e8dee722f634015e9 (diff) |
Remove PropositionalQuery class and all CUDD-related build stuff (and references)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 14 | ||||
-rw-r--r-- | src/util/configuration.cpp | 2 | ||||
-rw-r--r-- | src/util/configuration_private.h | 6 | ||||
-rw-r--r-- | src/util/propositional_query.cpp | 226 | ||||
-rw-r--r-- | src/util/propositional_query.h | 60 |
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 */ |