From: Morgan Deters Date: Tue, 15 Mar 2011 20:32:13 +0000 (+0000) Subject: Merge from cudd branch. This mostly just adds support for linking X-Git-Tag: cvc5-1.0.0~8658 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fb7c711588cb070c1e4a1d076b47f9277bfc3fe;p=cvc5.git Merge from cudd branch. This mostly just adds support for linking against cudd libraries, the propositional_query class (in util/), which uses cudd if it's available (and otherwise answers UNKNOWN for all queries), and the arith theory support for it (currently disabled per Tim's request, so he can clean it up). Other changes include: * contrib/debug-keys - script to print all used keys under Debug(), Trace() * test/regress/run_regression - minor fix (don't export a variable) * configure.ac - replace a comment removed by dejan's google perf commit * some minor copyright/documentation updates, and minor changes to source text to make 'clang --analyze' happy. --- diff --git a/Makefile b/Makefile index 0f04a94cb..4b731cb04 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,10 @@ +# -*-makefile-*- +# +# This makefile is the _source_ directory's makefile, and is static, +# not generated. Makefile.am is the automake makefile for the build +# top-level (its corresponding Makefile.in is here, too, but the +# corresponding Makefile is under builds/$arch/$buildid. +# builddir = builds .PHONY: _default_build_ all diff --git a/Makefile.subdir b/Makefile.subdir index 293b2771b..7b7c90561 100644 --- a/Makefile.subdir +++ b/Makefile.subdir @@ -1,4 +1,10 @@ # -*-makefile-*- +# +# This makefile is included from source directories in order to +# trigger a build in the corresponding build directory. +# +# See src/Makefile for an example. +# include $(topdir)/builds/current builddir = $(topdir)/builds/$(CURRENT_BUILD)/$(srcdir) unittestdir = $(topdir)/builds/$(CURRENT_BUILD)/test/unit diff --git a/README b/README index d064c226d..aaa36ff67 100644 --- a/README +++ b/README @@ -27,9 +27,25 @@ given are minimum versions; more recent versions should be compatible. GNU C and C++ (gcc and g++), reasonably recent versions GNU Make -GMP v4.2 -libantlr3c v3.2 -Optional: CLN v1.3 +GMP v4.2 (GNU Multi-Precision arithmetic library) +libantlr3c v3.2 (ANTLR parser generator) +Optional: CLN v1.3 (Class Library for Numbers) +Optional: CUDD v2.4.2 (Colorado University Decision Diagram package) + +CUDD, if desired, must be installed in a special manner. The default +distribution from vlsi.colorado.edu doesn't build shared objects, +and names things that make it difficult to compose software +dependences (e.g. a "libutil" is distributed). So we packaged our +own version of cudd that changes only its build process, making it +play nicely with libtool and packaging all the various cudd libraries +into just a few. This version must be used for cvc4, and is available +from the CVC4 apt repository by dropping the following line into your +/etc/apt/sources.list: + + deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/ + +The debian source package "cudd", available from the same repository, +includes a diff of all changes made to cudd makefiles. *** Build dependencies diff --git a/configure.ac b/configure.ac index 66e8acd7d..05e3bac8e 100644 --- a/configure.ac +++ b/configure.ac @@ -662,6 +662,49 @@ AC_SEARCH_LIBS([clock_gettime], [rt], [Defined to 1 if clock_gettime() is supported by the platform.])], [AC_LIBOBJ([clock_gettime])]) +AC_ARG_WITH([cudd-dir], + [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])], + [CUDD_DIR="$withval"]) +if test -z "$CUDD_DIR"; then + CUDD_DIR=/usr +fi +AC_MSG_CHECKING([for cudd includes under $CUDD_DIR]) +CUDD_CPPFLAGS= +CUDD_LDFLAGS= +cvc4cudd=no +result="not found" +for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do + if test -r "$cuddinc/cudd.h"; then + dnl TODO - should do a TRY_COMPILE instead + CUDD_CPPFLAGS="\"-I$cuddinc\"" + result="$cuddinc" + cvc4cudd=yes + break + fi +done +AC_MSG_RESULT([$result]) +if test $cvc4cudd = yes; then + AC_MSG_CHECKING([for cudd libraries under $CUDD_DIR]) + cvc4cudd=no + result="not found" + for cuddlib in "$CUDD_DIR/lib" "$CUDD_DIR/lib/cudd" "$CUDD_DIR"; do + if test -r "$cuddlib/libcuddxx.la"; then + dnl TODO - should do a TRY_LINK instead, that has the extra benefit + dnl of making sure both shared & static work + CUDD_LDFLAGS="\"-L$cuddlib\" -lcuddxx" + result="$cuddlib" + cvc4cudd=yes + break + fi + done + AC_MSG_RESULT([$result]); + if test $cvc4cudd = yes; then + AC_DEFINE_UNQUOTED(CVC4_CUDD, [], [Defined if using the CU Decision Diagram package (cudd).]) + fi +fi +AC_SUBST([CUDD_CPPFLAGS]) +AC_SUBST([CUDD_LDFLAGS]) + # Check for antlr C++ runtime (defined in config/antlr.m4) AC_LIB_ANTLR diff --git a/contrib/addsourcedir b/contrib/addsourcedir index ef6aedd15..00357cadf 100755 --- a/contrib/addsourcedir +++ b/contrib/addsourcedir @@ -2,7 +2,7 @@ # # addsourcedir # Morgan Deters for the CVC4 project -# Copyright (c) 2010 The CVC4 Project +# Copyright (c) 2010, 2011 The CVC4 Project # # usage: addsourcedir paths... # diff --git a/contrib/configure-in-place b/contrib/configure-in-place index 09771676e..9da584d36 100755 --- a/contrib/configure-in-place +++ b/contrib/configure-in-place @@ -2,7 +2,7 @@ # # configure-in-place # Morgan Deters for CVC4 -# Copyright (c) 2010 The CVC4 Project +# Copyright (c) 2010, 2011 The CVC4 Project # # usage: configure-in-place [ arguments... ] # diff --git a/contrib/debug-keys b/contrib/debug-keys new file mode 100755 index 000000000..6d2804974 --- /dev/null +++ b/contrib/debug-keys @@ -0,0 +1,33 @@ +#!/bin/bash +# +# Lists the Trace() and Debug() keys used in sources. +# +# e.g. if Debug("uf") occurs in the sources, then "uf" is printed by this script. + +if [ "$1" = "-h" -o "$1" = "-help" -o "$1" = "-?" -o "$1" = "--help" ]; then + echo "usage: `basename $0` [dirs...]" >&2 + echo "This utility will print all Debug("foo") and Trace("foo") keys." + echo "With optional dirs..., use dirs instead of top-level \"src\"." >&2 + exit 1 +fi + +if [ $# -eq 0 ]; then + cd `dirname "$0"`/.. + + if ! [ -d src ]; then + echo "`basename $0`: not in CVC4 directory tree?!" >&2 + exit 1 + fi + + set src +fi + +echo "Trace and debug flags used in $*:" + +while [ $# -gt 0 ]; do + dir="$1" + shift + + test -r "$dir" && grep -r --exclude-dir=.svn '\(Debug\|Trace\)\(\.isOn\)\?("[^"]\+")' "$dir" | sed 's,.*\(Debug\|Trace\)\(\.isOn\)\?("\([^"]\+\)").*,\3,' | sort -u +done | sort -u + diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl index 6c1e0eeea..701768119 100755 --- a/contrib/dimacs_to_smt.pl +++ b/contrib/dimacs_to_smt.pl @@ -1,7 +1,7 @@ #!/usr/bin/perl -w # DIMACS to SMT # Morgan Deters -# Copyright (c) 2009, 2010 The CVC4 Project +# Copyright (c) 2009, 2010, 2011 The CVC4 Project use strict; diff --git a/contrib/get-authors b/contrib/get-authors index dbe878d6b..ef6abff8e 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -2,7 +2,7 @@ # # get-authors # Morgan Deters for CVC4 -# Copyright (c) 2009, 2010 The CVC4 Project +# Copyright (c) 2009, 2010, 2011 The CVC4 Project # # usage: get-authors [ files... ] # diff --git a/src/expr/type.h b/src/expr/type.h index 453eaf5c4..d357c869e 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -34,6 +34,8 @@ class NodeManager; class ExprManager; class TypeNode; +class SmtEngine; + template class NodeTemplate; @@ -69,7 +71,6 @@ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; class CVC4_PUBLIC Type { friend class SmtEngine; - friend class SmtEnginePrivate; friend class ExprManager; friend class TypeNode; friend class TypeHashStrategy; diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 2cdba2d27..30be07d7c 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -11,7 +11,7 @@ libprop_la_SOURCES = \ prop_engine.cpp \ prop_engine.h \ sat.h \ - sat.cpp \ + sat.cpp \ cnf_stream.h \ cnf_stream.cpp diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 273b2322a..fe5e55ae6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -530,7 +530,7 @@ Result SmtEngine::query(const BoolExpr& e) { d_queryMade = true; ensureBoolean(e);// ensure expr is type-checked at this point internalPush(); - SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); + smt::SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); internalPop(); d_status = r; @@ -547,7 +547,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { if(d_assertionList != NULL) { d_assertionList->push_back(e); } - SmtEnginePrivate::addFormula(*this, e.getNode()); + smt::SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } @@ -589,7 +589,7 @@ Expr SmtEngine::getValue(const Expr& e) NodeManagerScope nms(d_nodeManager); Node eNode = e.getNode(); - Node n = SmtEnginePrivate::preprocess(*this, eNode); + Node n = smt::SmtEnginePrivate::preprocess(*this, eNode); Debug("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); @@ -655,7 +655,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { ++i) { Assert((*i).getType() == boolType); - Node n = SmtEnginePrivate::preprocess(*this, *i); + Node n = smt::SmtEnginePrivate::preprocess(*this, *i); Debug("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 456fdb746..b75140bc7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -27,6 +27,8 @@ #include "util/rational.h" #include "util/integer.h" +#include "theory/rewriter.h" + #include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" @@ -79,6 +81,8 @@ TheoryArith::Statistics::Statistics(): d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), + d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0), + d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues"), d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0), d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"), d_tableauResets("theory::arith::tableauResets", 0), @@ -93,6 +97,9 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); StatisticsRegistry::registerStat(&d_presolveTime); + StatisticsRegistry::registerStat(&d_miplibtrickApplications); + StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues); + StatisticsRegistry::registerStat(&d_initialTableauDensity); StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart); StatisticsRegistry::registerStat(&d_tableauResets); @@ -109,19 +116,43 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); StatisticsRegistry::unregisterStat(&d_presolveTime); + StatisticsRegistry::unregisterStat(&d_miplibtrickApplications); + StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues); + StatisticsRegistry::unregisterStat(&d_initialTableauDensity); StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart); StatisticsRegistry::unregisterStat(&d_tableauResets); StatisticsRegistry::unregisterStat(&d_restartTimer); } +#include "util/propositional_query.h" void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); + /* + if(Debug.isOn("prop::static")){ + Debug("prop::static") << n << "is " + << prop::PropositionalQuery::isSatisfiable(n) + << endl; + } + */ + vector workList; workList.push_back(n); __gnu_cxx::hash_set processed; + //Contains an underapproximation of nodes that must hold. + __gnu_cxx::hash_set defTrue; + + /* Maps a variable, x, to the set of defTrue nodes of the form + * (=> _ (= x c)) + * where c is a constant. + */ + typedef __gnu_cxx::hash_map, TNodeHashFunction> VarToNodeSetMap; + VarToNodeSetMap miplibTrick; + + defTrue.insert(n); + while(!workList.empty()) { n = workList.back(); @@ -133,6 +164,11 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { unprocessedChildren = true; } } + if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){ + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { + defTrue.insert(*i); + } + } if(unprocessedChildren) { continue; @@ -202,6 +238,105 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { Debug("arith::mins") << n << " is a constant sandwich" << nGeqMin << nLeqMax << endl; learned << nGeqMin << nLeqMax; } + // == 3-FINITE VALUE SET : Collect information == + if(n.getKind() == IMPLIES && + n[1].getKind() == EQUAL && + n[1][0].getMetaKind() == metakind::VARIABLE && + defTrue.find(n) != defTrue.end()){ + Node eqTo = n[1][1]; + Node rewriteEqTo = Rewriter::rewrite(eqTo); + if(rewriteEqTo.getKind() == CONST_RATIONAL){ + + TNode var = n[1][0]; + if(miplibTrick.find(var) == miplibTrick.end()){ + //[MGD] commented out following line as per TAK's instructions + //miplibTrick.insert(make_pair(var, set())); + } + //[MGD] commented out following line as per TAK's instructions + //miplibTrick[var].insert(n); + Debug("arith::miplib") << "insert " << var << " const " << n << endl; + } + } + } + + // == 3-FINITE VALUE SET == + VarToNodeSetMap::iterator i = miplibTrick.begin(), endMipLibTrick = miplibTrick.end(); + for(; i != endMipLibTrick; ++i){ + TNode var = i->first; + const set& imps = i->second; + + Assert(!imps.empty()); + vector conditions; + vector valueCollection; + set::const_iterator j=imps.begin(), impsEnd=imps.end(); + for(; j != impsEnd; ++j){ + TNode imp = *j; + Assert(imp.getKind() == IMPLIES); + Assert(defTrue.find(imp) != defTrue.end()); + Assert(imp[1].getKind() == EQUAL); + + + Node eqTo = imp[1][1]; + Node rewriteEqTo = Rewriter::rewrite(eqTo); + Assert(rewriteEqTo.getKind() == CONST_RATIONAL); + + conditions.push_back(imp[0]); + valueCollection.push_back(rewriteEqTo.getConst()); + } + + Node possibleTaut = Node::null(); + if(conditions.size() == 1){ + possibleTaut = conditions.front(); + }else{ + NodeBuilder<> orBuilder(OR); + orBuilder.append(conditions); + possibleTaut = orBuilder; + } + + + Debug("arith::miplib") << "var: " << var << endl; + Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl; + + Result isTaut = PropositionalQuery::isTautology(possibleTaut); + if(isTaut == Result(Result::VALID)){ + Debug("arith::miplib") << var << " found a tautology!"<< endl; + + set values(valueCollection.begin(), valueCollection.end()); + const Rational& min = *(values.begin()); + const Rational& max = *(values.rbegin()); + + Debug("arith::miplib") << "min: " << min << endl; + Debug("arith::miplib") << "max: " << max << endl; + + Assert(min <= max); + + ++(d_statistics.d_miplibtrickApplications); + (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size()); + + Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min); + Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max); + Debug("arith::miplib") << nGeqMin << nLeqMax << endl; + learned << nGeqMin << nLeqMax; + set::iterator valuesIter = values.begin(); + set::iterator valuesEnd = values.end(); + set::iterator valuesPrev = valuesIter; + ++valuesIter; + for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){ + const Rational& prev = *valuesPrev; + const Rational& curr = *valuesIter; + Assert(prev < curr); + + //The interval (last,curr) can be excluded: + //(not (and (> var prev) (< var curr)) + //<=> (or (not (> var prev)) (not (< var curr))) + //<=> (or (<= var prev) (>= var curr)) + Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev); + Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr); + Node excludedMiddle = NodeBuilder<2>(OR) << leqPrev << geqCurr; + Debug("arith::miplib") << excludedMiddle << endl; + learned << excludedMiddle; + } + } } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 3ff83abdf..1dcdceab0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -237,6 +237,9 @@ private: IntStat d_permanentlyRemovedVariables; TimerStat d_presolveTime; + IntStat d_miplibtrickApplications; + AverageStat d_avgNumMiplibtrickValues; + BackedStat d_initialTableauDensity; AverageStat d_avgTableauDensityAtRestart; IntStat d_tableauResets; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 4f853b9e3..c94d208d2 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -3,7 +3,12 @@ AM_CPPFLAGS = \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -noinst_LTLIBRARIES = libutil.la +noinst_LTLIBRARIES = libutil.la libutilcudd.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@ libutil_la_SOURCES = \ Assert.h \ @@ -34,6 +39,11 @@ libutil_la_SOURCES = \ dynamic_array.h \ language.h \ triple.h +libutil_la_LIBADD = \ + @builddir@/libutilcudd.la +libutilcudd_la_SOURCES = \ + propositional_query.h \ + propositional_query.cpp BUILT_SOURCES = \ rational.h \ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 8cd824b0c..94ade5a52 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -96,6 +96,10 @@ bool Configuration::isBuiltWithCln() { return IS_CLN_BUILD; } +bool Configuration::isBuiltWithCudd() { + return IS_CUDD_BUILD; +} + bool Configuration::isBuiltWithTlsSupport() { return USING_TLS; } diff --git a/src/util/configuration.h b/src/util/configuration.h index a9d59a7fe..150354c29 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -71,6 +71,8 @@ public: static bool isBuiltWithCln(); + static bool isBuiltWithCudd(); + static bool isBuiltWithTlsSupport(); }; diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 56423e7d5..c0ce86c97 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -70,6 +70,12 @@ 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 */ @@ -90,7 +96,7 @@ namespace CVC4 { #define CVC4_ABOUT_STRING string("\ This is CVC4 version " CVC4_RELEASE_STRING "\n\n\ -Copyright (C) 2009, 2010\n\ +Copyright (C) 2009, 2010, 2011\n\ The ACSys Group\n\ Courant Institute of Mathematical Sciences\n\ New York University\n\ diff --git a/src/util/options.cpp b/src/util/options.cpp index 0c3915d1d..6fc71bae3 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -416,6 +416,11 @@ throw(OptionException) { printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); + printf("\n"); + printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); + printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); + printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); + printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); case '?': diff --git a/src/util/propositional_query.cpp b/src/util/propositional_query.cpp new file mode 100644 index 000000000..067896922 --- /dev/null +++ b/src/util/propositional_query.cpp @@ -0,0 +1,228 @@ +/********************* */ +/*! \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, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 +#include + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; + +#ifdef CVC4_CUDD + +#include +#include +#include + +namespace CVC4 { + +class BddInstance { +private: + Cudd d_mgr; + typedef std::map 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()) { + 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 new file mode 100644 index 000000000..f520f142d --- /dev/null +++ b/src/util/propositional_query.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \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, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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. + * + * @params q Node to be checked for satisfiability. + * @params e A number representing the effort to use between 0 (minimum effort), + * and 1 (maximum effort). + * @precondition q is a ground formula. + * @precondition effort is between 0 and 1. + */ + static Result isSatisfiable(TNode q); + + /** + * Returns whether a node q is a propositional tautology. + * + * @params q Node to be checked for satisfiability. + * @params e A number representing the effort to use between 0 (minimum effort), + * and 1 (maximum effort). + * @precondition q is a ground formula. + * @precondition effort is between 0 and 1. + */ + static Result isTautology(TNode q); + +};/* class PropositionalQuery */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__PROPOSITIONAL_QUERY_H */ diff --git a/src/util/result.h b/src/util/result.h index 1e0729332..7da1dc0b7 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -61,6 +61,7 @@ public: TIMEOUT, MEMOUT, NO_STATUS, + UNSUPPORTED, OTHER, UNKNOWN_REASON }; diff --git a/src/util/stats.h b/src/util/stats.h index 4dbf31120..a78070de4 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -43,6 +43,8 @@ namespace CVC4 { class CVC4_PUBLIC Stat; +inline std::ostream& operator<<(std::ostream& os, const ::timespec& t); + /** * The main statistics registry. This registry maintains the list of * currently active statistics and is able to "flush" them all. diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 91b1d41c7..aca076d9f 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -8,7 +8,8 @@ TESTS = \ arith.02.cvc \ arith.03.cvc \ delta-minimized-row-vector-bug.smt \ - leq.01.smt + leq.01.smt \ + miplibtrick.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/miplibtrick.smt b/test/regress/regress0/arith/miplibtrick.smt new file mode 100644 index 000000000..93cd6d219 --- /dev/null +++ b/test/regress/regress0/arith/miplibtrick.smt @@ -0,0 +1,11 @@ +(benchmark miplibtrick + :status sat + :logic QF_LRA + :extrafuns ((tmp1 Real)) + :extrapreds ((x177)) + + :formula( and + ( implies ( and ( not x177 ) true ) ( = tmp1 0 ) ) + ( implies ( and x177 true ) ( = tmp1 (~ 350) ) ) + ) +)