summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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
14 files changed, 471 insertions, 8 deletions
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback