diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/type.h | 3 | ||||
-rw-r--r-- | src/prop/Makefile.am | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 135 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 3 | ||||
-rw-r--r-- | src/util/Makefile.am | 12 | ||||
-rw-r--r-- | src/util/configuration.cpp | 4 | ||||
-rw-r--r-- | src/util/configuration.h | 2 | ||||
-rw-r--r-- | src/util/configuration_private.h | 8 | ||||
-rw-r--r-- | src/util/options.cpp | 5 | ||||
-rw-r--r-- | src/util/propositional_query.cpp | 228 | ||||
-rw-r--r-- | src/util/propositional_query.h | 66 | ||||
-rw-r--r-- | src/util/result.h | 1 | ||||
-rw-r--r-- | src/util/stats.h | 2 |
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. |