summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile7
-rw-r--r--Makefile.subdir6
-rw-r--r--README22
-rw-r--r--configure.ac43
-rwxr-xr-xcontrib/addsourcedir2
-rwxr-xr-xcontrib/configure-in-place2
-rwxr-xr-xcontrib/debug-keys33
-rwxr-xr-xcontrib/dimacs_to_smt.pl2
-rwxr-xr-xcontrib/get-authors2
-rw-r--r--src/expr/type.h3
-rw-r--r--src/prop/Makefile.am2
-rw-r--r--src/smt/smt_engine.cpp8
-rw-r--r--src/theory/arith/theory_arith.cpp135
-rw-r--r--src/theory/arith/theory_arith.h3
-rw-r--r--src/util/Makefile.am12
-rw-r--r--src/util/configuration.cpp4
-rw-r--r--src/util/configuration.h2
-rw-r--r--src/util/configuration_private.h8
-rw-r--r--src/util/options.cpp5
-rw-r--r--src/util/propositional_query.cpp228
-rw-r--r--src/util/propositional_query.h66
-rw-r--r--src/util/result.h1
-rw-r--r--src/util/stats.h2
-rw-r--r--test/regress/regress0/arith/Makefile.am3
-rw-r--r--test/regress/regress0/arith/miplibtrick.smt11
25 files changed, 596 insertions, 16 deletions
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 <mdeters@cs.nyu.edu> 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 <mdeters@cs.nyu.edu> 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 <mdeters@cs.nyu.edu> 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 <bool ref_count>
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<TNode> workList;
workList.push_back(n);
__gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+ //Contains an underapproximation of nodes that must hold.
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> 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<TNode, set<TNode>, 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<TNode>()));
+ }
+ //[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<TNode>& imps = i->second;
+
+ Assert(!imps.empty());
+ vector<Node> conditions;
+ vector<Rational> valueCollection;
+ set<TNode>::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<Rational>());
+ }
+
+ 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<Rational> 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<Rational>::iterator valuesIter = values.begin();
+ set<Rational>::iterator valuesEnd = values.end();
+ set<Rational>::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<double> 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 <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
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) ) )
+ )
+)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback