diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 4 | ||||
-rw-r--r-- | src/decision/Makefile | 4 | ||||
-rw-r--r-- | src/decision/Makefile.am | 13 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 55 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 150 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 50 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 393 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 96 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 11 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 8 | ||||
-rw-r--r-- | src/prop/sat_solver_types.h | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 13 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 9 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 21 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 | ||||
-rw-r--r-- | src/theory/arith/arith_priority_queue.h | 2 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 8 | ||||
-rw-r--r-- | src/util/options.cpp | 2 | ||||
-rw-r--r-- | src/util/options.h | 17 |
20 files changed, 847 insertions, 23 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 4f00b061b..818acfa29 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = \ -I@srcdir@/include -I@srcdir@ -I@builddir@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib expr util context theory prop smt printer proof . parser compat bindings main +SUBDIRS = lib expr util context theory prop decision smt printer proof . parser compat bindings main lib_LTLIBRARIES = libcvc4.la if HAVE_CXXTESTGEN @@ -43,6 +43,7 @@ libcvc4_la_LIBADD = \ @builddir@/printer/libprinter.la \ @builddir@/smt/libsmt.la \ @builddir@/theory/libtheory.la \ + @builddir@/decision/libdecision.la \ @builddir@/lib/libreplacements.la libcvc4_noinst_la_LIBADD = \ @builddir@/util/libutil.la \ @@ -55,6 +56,7 @@ libcvc4_noinst_la_LIBADD = \ @builddir@/printer/libprinter.la \ @builddir@/smt/libsmt.la \ @builddir@/theory/libtheory.la \ + @builddir@/decision/libdecision.la \ @builddir@/lib/libreplacements.la CLEANFILES = \ diff --git a/src/decision/Makefile b/src/decision/Makefile new file mode 100644 index 000000000..27978f85f --- /dev/null +++ b/src/decision/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = src/decision + +include $(topdir)/Makefile.subdir diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am new file mode 100644 index 000000000..c399cbf71 --- /dev/null +++ b/src/decision/Makefile.am @@ -0,0 +1,13 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libdecision.la + +libdecision_la_SOURCES = \ + decision_engine.h \ + decision_engine.cpp \ + decision_strategy.h \ + justification_heuristic.h \ + justification_heuristic.cpp diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp new file mode 100644 index 000000000..936ac8e73 --- /dev/null +++ b/src/decision/decision_engine.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file decision_engine.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 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 Decision engine + ** + ** Decision engine + **/ + +#include "decision/decision_engine.h" +#include "decision/justification_heuristic.h" + +#include "expr/node.h" +#include "util/options.h" + +using namespace std; + +namespace CVC4 { + +DecisionEngine::DecisionEngine() : d_needSimplifiedPreITEAssertions() { + const Options* options = Options::current(); + Trace("decision") << "Creating decision engine" << std::endl; + if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { } + if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) { + DecisionStrategy* ds = new decision::JustificationHeuristic(this); + enableStrategy(ds); + } +} + +void DecisionEngine::enableStrategy(DecisionStrategy* ds) +{ + d_enabledStrategies.push_back(ds); + if( ds->needSimplifiedPreITEAssertions() ) + d_needSimplifiedPreITEAssertions.push_back(ds); +} + +void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions) +{ + d_assertions.reserve(assertions.size()); + for(unsigned i = 0; i < assertions.size(); ++i) + d_assertions.push_back(assertions[i]); + for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i) + d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); +} + +}/* CVC4 namespace */ diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h new file mode 100644 index 000000000..d4037acff --- /dev/null +++ b/src/decision/decision_engine.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file decision_engine.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 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 Decision engine + ** + ** Decision engine + **/ + +#ifndef __CVC4__DECISION__DECISION_ENGINE_H +#define __CVC4__DECISION__DECISION_ENGINE_H + +#include <vector> + +#include "decision/decision_strategy.h" + +#include "expr/node.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/sat_solver_types.h" +#include "util/output.h" + +using namespace std; +using namespace CVC4::prop; +using namespace CVC4::decision; + +namespace CVC4 { + +class DecisionEngine { + + vector <DecisionStrategy* > d_enabledStrategies; + vector <DecisionStrategy* > d_needSimplifiedPreITEAssertions; + + vector <Node> d_assertions; + + // PropEngine* d_propEngine; + CnfStream* d_cnfStream; + DPLLSatSolverInterface* d_satSolver; +public: + // Necessary functions + + /** Constructor, enables decision stragies based on options */ + DecisionEngine(); + + /** Destructor, currently does nothing */ + ~DecisionEngine() { + Trace("decision") << "Destroying decision engine" << std::endl; + } + + // void setPropEngine(PropEngine* pe) { + // // setPropEngine should not be called more than once + // Assert(d_propEngine == NULL); + // Assert(pe != NULL); + // d_propEngine = pe; + // } + + void setSatSolver(DPLLSatSolverInterface* ss) { + // setPropEngine should not be called more than once + Assert(d_satSolver == NULL); + Assert(ss != NULL); + d_satSolver = ss; + } + + void setCnfStream(CnfStream* cs) { + // setPropEngine should not be called more than once + Assert(d_cnfStream == NULL); + Assert(cs != NULL); + d_cnfStream = cs; + } + + + // Interface for External World to use our services + + /** Gets the next decision based on strategies that are enabled */ + SatLiteral getNext() { + SatLiteral ret = undefSatLiteral; + for(unsigned i = 0; i < d_enabledStrategies.size() + and ret == undefSatLiteral; ++i) { + ret = d_enabledStrategies[i]->getNext(); + } + return ret; + } + + /** + * This is called by SmtEngine, at shutdown time, just before + * destruction. It is important because there are destruction + * ordering issues between some parts of the system. For now, + * there's nothing to do here in the DecisionEngine. + */ + void shutdown() { + Trace("decision") << "Shutting down decision engine" << std::endl; + } + + + // External World helping us help the Strategies + + /** If one of the enabled strategies needs them */ + bool needSimplifiedPreITEAssertions() { + return d_needSimplifiedPreITEAssertions.size() > 0; + } + void informSimplifiedPreITEAssertions(const vector<Node> &assertions); + + + // Interface for Strategies to use stuff stored in Decision Engine + // (which was possibly requested by them on initialization) + + /** + * Get the assertions. Strategies are notified when these are available. + */ + const vector<Node>& getAssertions() { + return d_assertions; + } + + + // Interface for Strategies to get information about External World + + bool hasSatLiteral(Node n) { + return d_cnfStream->hasLiteral(n); + } + SatLiteral getSatLiteral(Node n) { + return d_cnfStream->getLiteral(n); + } + SatValue getSatValue(SatLiteral l) { + return d_satSolver->value(l); + } + Node getNode(SatLiteral l) { + return d_cnfStream->getNode(l); + } + +private: + /** + * Enable a particular decision strategy, also updating + * corresponding vector<DecisionStrategy*>-s is the engine + */ + void enableStrategy(DecisionStrategy* ds); + +};/* DecisionEngine class */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h new file mode 100644 index 000000000..abcbbaace --- /dev/null +++ b/src/decision/decision_strategy.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file decision_strategy.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 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 Decision stategy + ** + ** Decision strategy + **/ + +#ifndef __CVC4__DECISION__DECISION_STRATEGY_H +#define __CVC4__DECISION__DECISION_STRATEGY_H + +#include "prop/sat_solver_types.h" + +namespace CVC4 { + +class DecisionEngine; + +namespace decision { + +class DecisionStrategy { +protected: + DecisionEngine* d_decisionEngine; +public: + DecisionStrategy(DecisionEngine* de) : + d_decisionEngine(de) { + } + + virtual ~DecisionStrategy() { } + + virtual prop::SatLiteral getNext() = 0; + + virtual bool needSimplifiedPreITEAssertions() { return false; } + + virtual void notifyAssertionsAvailable() { return; } +}; + +}/* decision namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__DECISION__DECISION_STRATEGY_H */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp new file mode 100644 index 000000000..4b017ef45 --- /dev/null +++ b/src/decision/justification_heuristic.cpp @@ -0,0 +1,393 @@ +/********************* */ +/*! \file justification_heuristic.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 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 Justification heuristic for decision making + ** + ** A ATGP-inspired justification-based decision heuristic. See + ** [insert reference] for more details. This code is, or not, based + ** on the CVC3 implementation of the same heuristic -- note below. + ** + ** It needs access to the simplified but non-clausal formula. + **/ +/*****************************************************************************/ +/*! + *\file search_sat.cpp + *\brief Implementation of Search engine with generic external sat solver + * + * Author: Clark Barrett + * + * Created: Wed Dec 7 21:00:24 2005 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + */ +/*****************************************************************************/ + +#include "justification_heuristic.h" + + +/*** + +Summary of the algorithm: + + + +***/ + +/* + +CVC3 code <----> this code + + value desiredVal + getValue(lit) litVal + +***/ + +void JustificationHeuristic::setJustified(SatVariable v) +{ + d_justified.insert(v); +} + +bool JustificationHeuristic::checkJustified(SatVariable v) +{ + return d_justified.find(v) != d_justified.end(); +} + +SatValue invertValue(SatValue v) +{ + if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN; + else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE; + else return SAT_VALUE_TRUE; +} + +bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal, SatLiteral* litDecision) +//bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision) +{ + // if(not ) { + // // Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl; + // return false; + // // Assert(not lit.isNull()); + // } + + /** + * TODO -- Base case. Way CVC3 seems to handle is that it has + * literals correpsonding to true and false. We'll have to take care + * somewhere else. + */ + + // Var v = lit.getVar(); + SatVariable v = lit.getSatVariable(); + SatValue litVal = d_decisionEngine->getSatValue(lit); + + // if (lit.isFalse() || lit.isTrue()) return false; + if (v == 0) return false; + + + /* You'd better know what you want */ + // DebugAssert(value != Var::UNKNOWN, "expected known value"); + Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); + + /* Good luck, hope you can get what you want */ + // DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN, + // "invariant violated"); + Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, + "invariant voilated"); + + + if (checkJustified(v)) return false; + + if (lit.isNegated()) { + desiredVal = invertValue(desiredVal); + } + + Node node = d_decisionEngine->getNode(lit); + Trace("decision") << "lit = " << lit << std::endl; + Trace("decision") << node.getKind() << std::endl; + Trace("decision") << node << std::endl; + + /* + if (d_cnfManager->numFanins(v) == 0) { + if (getValue(v) != Var::UNKNOWN) { + setJustified(v); + return false; + } + else { + *litDecision = Lit(v, value == Var::TRUE_VAL); + return true; + } + } + */ + if(node.getNumChildren() == 0) { + if(litVal != SAT_VALUE_UNKNOWN) { + setJustified(v); + return false; + } else { + *litDecision = SatLiteral(v, desiredVal == SAT_VALUE_TRUE ); + return true; + } + } + + + /* + else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) { + // This node represents a predicate with embedded ITE's + // We handle this case specially in order to catch the + // corner case when a variable is in its own fanin. + n = d_cnfManager->numFanins(v); + for (i=0; i < n; ++i) { + litTmp = d_cnfManager->getFanin(v, i); + varTmp = litTmp.getVar(); + DebugAssert(!litTmp.isInverted(),"Expected positive fanin"); + if (checkJustified(varTmp)) continue; + DebugAssert(d_cnfManager->concreteVar(varTmp).getKind() == ITE, + "Expected ITE"); + DebugAssert(getValue(varTmp) == Var::TRUE_VAL,"Expected TRUE"); + Lit cIf = d_cnfManager->getFanin(varTmp,0); + Lit cThen = d_cnfManager->getFanin(varTmp,1); + Lit cElse = d_cnfManager->getFanin(varTmp,2); + if (getValue(cIf) == Var::UNKNOWN) { + if (getValue(cElse) == Var::TRUE_VAL || + getValue(cThen) == Var::FALSE_VAL) { + ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision); + } + else { + ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision); + } + if (!ret) { + cout << d_cnfManager->concreteVar(cIf.getVar()) << endl; + DebugAssert(false,"No controlling input found (1)"); + } + return true; + } + else if (getValue(cIf) == Var::TRUE_VAL) { + if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) { + return true; + } + if (cThen.getVar() != v && + (getValue(cThen) == Var::UNKNOWN || + getValue(cThen) == Var::TRUE_VAL) && + findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) { + return true; + } + } + else { + if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) { + return true; + } + if (cElse.getVar() != v && + (getValue(cElse) == Var::UNKNOWN || + getValue(cElse) == Var::TRUE_VAL) && + findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) { + return true; + } + } + setJustified(varTmp); + } + if (getValue(v) != Var::UNKNOWN) { + setJustified(v); + return false; + } + else { + *litDecision = Lit(v, value == Var::TRUE_VAL); + return true; + } + } + + int kind = d_cnfManager->concreteVar(v).getKind(); + Var::Val valHard = Var::FALSE_VAL; + switch (kind) { + case AND: + valHard = Var::TRUE_VAL; + case OR: + if (value == valHard) { + n = d_cnfManager->numFanins(v); + for (i=0; i < n; ++i) { + litTmp = d_cnfManager->getFanin(v, i); + if (findSplitterRec(litTmp, valHard, litDecision)) { + return true; + } + } + DebugAssert(getValue(v) == valHard, "Output should be justified"); + setJustified(v); + return false; + } + else { + Var::Val valEasy = Var::invertValue(valHard); + n = d_cnfManager->numFanins(v); + for (i=0; i < n; ++i) { + litTmp = d_cnfManager->getFanin(v, i); + if (getValue(litTmp) != valHard) { + if (findSplitterRec(litTmp, valEasy, litDecision)) { + return true; + } + DebugAssert(getValue(v) == valEasy, "Output should be justified"); + setJustified(v); + return false; + } + } + DebugAssert(false, "No controlling input found (2)"); + } + break; + case IMPLIES: + DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins"); + if (value == Var::FALSE_VAL) { + litTmp = d_cnfManager->getFanin(v, 0); + if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) { + return true; + } + litTmp = d_cnfManager->getFanin(v, 1); + if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) { + return true; + } + DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified"); + setJustified(v); + return false; + } + else { + litTmp = d_cnfManager->getFanin(v, 0); + if (getValue(litTmp) != Var::TRUE_VAL) { + if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) { + return true; + } + DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified"); + setJustified(v); + return false; + } + litTmp = d_cnfManager->getFanin(v, 1); + if (getValue(litTmp) != Var::FALSE_VAL) { + if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) { + return true; + } + DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified"); + setJustified(v); + return false; + } + DebugAssert(false, "No controlling input found (3)"); + } + break; + case IFF: { + litTmp = d_cnfManager->getFanin(v, 0); + Var::Val val = getValue(litTmp); + if (val != Var::UNKNOWN) { + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + if (value == Var::FALSE_VAL) val = Var::invertValue(val); + litTmp = d_cnfManager->getFanin(v, 1); + + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(getValue(v) == value, "Output should be justified"); + setJustified(v); + return false; + } + else { + val = getValue(d_cnfManager->getFanin(v, 1)); + if (val == Var::UNKNOWN) val = Var::FALSE_VAL; + if (value == Var::FALSE_VAL) val = Var::invertValue(val); + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(false, "Unable to find controlling input (4)"); + } + break; + } + case XOR: { + litTmp = d_cnfManager->getFanin(v, 0); + Var::Val val = getValue(litTmp); + if (val != Var::UNKNOWN) { + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + if (value == Var::TRUE_VAL) val = Var::invertValue(val); + litTmp = d_cnfManager->getFanin(v, 1); + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(getValue(v) == value, "Output should be justified"); + setJustified(v); + return false; + } + else { + val = getValue(d_cnfManager->getFanin(v, 1)); + if (val == Var::UNKNOWN) val = Var::FALSE_VAL; + if (value == Var::TRUE_VAL) val = Var::invertValue(val); + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(false, "Unable to find controlling input (5)"); + } + break; + } + case ITE: { + Lit cIf = d_cnfManager->getFanin(v, 0); + Lit cThen = d_cnfManager->getFanin(v, 1); + Lit cElse = d_cnfManager->getFanin(v, 2); + if (getValue(cIf) == Var::UNKNOWN) { + if (getValue(cElse) == value || + getValue(cThen) == Var::invertValue(value)) { + ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision); + } + else { + ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision); + } + if (!ret) { + cout << d_cnfManager->concreteVar(cIf.getVar()) << endl; + DebugAssert(false,"No controlling input found (6)"); + } + return true; + } + else if (getValue(cIf) == Var::TRUE_VAL) { + if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) { + return true; + } + if (cThen.isVar() && cThen.getVar() != v && + (getValue(cThen) == Var::UNKNOWN || + getValue(cThen) == value) && + findSplitterRec(cThen, value, litDecision)) { + return true; + } + } + else { + if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) { + return true; + } + if (cElse.isVar() && cElse.getVar() != v && + (getValue(cElse) == Var::UNKNOWN || + getValue(cElse) == value) && + findSplitterRec(cElse, value, litDecision)) { + return true; + } + } + DebugAssert(getValue(v) == value, "Output should be justified"); + setJustified(v); + return false; + } + default: + DebugAssert(false, "Unexpected Boolean operator"); + break; + } + FatalAssert(false, "Should be unreachable"); + ------------------------------------------------ */ + return false; + + Unreachable(); + +}/* findRecSplit method */ diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h new file mode 100644 index 000000000..cb2216d6d --- /dev/null +++ b/src/decision/justification_heuristic.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file justification_heuristic.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 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 Justification heuristic for decision making + ** + ** A ATGP-inspired justification-based decision heuristic. See + ** [insert reference] for more details. This code is, or not, based + ** on the CVC3 implementation of the same heuristic. + ** + ** It needs access to the simplified but non-clausal formula. + **/ + +#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC +#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC + +#include "decision_engine.h" +#include "decision_strategy.h" + +#include "prop/sat_solver_types.h" +#include "expr/node.h" + +using namespace CVC4::prop; + +namespace CVC4 { + +namespace decision { + +class JustificationHeuristic : public DecisionStrategy { + set<SatVariable> d_justified; + unsigned d_prvsIndex; +public: + JustificationHeuristic(CVC4::DecisionEngine* de) : + DecisionStrategy(de) { + Trace("decision") << "Justification heuristic enabled" << std::endl; + } + prop::SatLiteral getNext() { + Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; + + const vector<Node>& assertions = d_decisionEngine->getAssertions(); + + for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) { + SatLiteral litDecision; + + /* Make sure there is a literal corresponding to the node */ + if( not d_decisionEngine->hasSatLiteral(assertions[i]) ) { + // Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl; + continue; + // Assert(not lit.isNull()); + } + + SatLiteral lit = d_decisionEngine->getSatLiteral(assertions[i]); + SatValue desiredVal = d_decisionEngine->getSatValue(lit); + if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE; + bool ret = findSplitterRec(lit, desiredVal, &litDecision); + if(ret == true) { + d_prvsIndex = i; + return litDecision; + } + } + + return prop::undefSatLiteral; + } + bool needSimplifiedPreITEAssertions() { return true; } + void notifyAssertionsAvailable() { + Trace("decision") << "JustificationHeuristic::notifyAssertionsAvailable()" + << " size = " << d_decisionEngine->getAssertions().size() + << std::endl; + /* clear the justifcation labels -- reconsider if/when to do + this */ + d_justified.clear(); + d_prvsIndex = 0; + } +private: + /* Do all the hardwork. */ + bool findSplitterRec(SatLiteral lit, SatValue value, SatLiteral* litDecision); + + /* Helper functions */ + void setJustified(SatVariable v); + bool checkJustified(SatVariable v); +};/* class JustificationHeuristic */ + +}/* namespace decision */ + +}/* namespace CVC4 */ + +#endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index abe22cb48..848c63a18 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): barrett, taking, cconway + ** Minor contributors (to current version): barrett, taking, cconway, kshitij ** 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 @@ -22,6 +22,7 @@ #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "decision/decision_engine.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" #include "util/Assert.h" @@ -61,9 +62,10 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, Context* context) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : d_inCheckSat(false), d_theoryEngine(te), + d_decisionEngine(de), d_context(context), d_satSolver(NULL), d_cnfStream(NULL), @@ -77,7 +79,10 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) : theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1); - d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_context, d_cnfStream)); + d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); + + d_decisionEngine->setSatSolver(d_satSolver); + d_decisionEngine->setCnfStream(d_cnfStream); } PropEngine::~PropEngine() { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 93c35bbf3..3d114db3a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking, dejan - ** Minor contributors (to current version): cconway, barrett + ** Minor contributors (to current version): cconway, barrett, kshitij ** 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 @@ -31,6 +31,7 @@ namespace CVC4 { +class DecisionEngine; class TheoryEngine; namespace prop { @@ -127,6 +128,9 @@ class PropEngine { /** The theory engine we will be using */ TheoryEngine *d_theoryEngine; + /** The decision engine we will be using */ + DecisionEngine *d_decisionEngine; + /** The context */ context::Context* d_context; @@ -153,7 +157,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, context::Context*); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context*); /** * Destructor. diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 406782468..0da4d7a6a 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -26,6 +26,9 @@ #include "cvc4_private.h" +#include <string> +#include <sstream> + namespace CVC4 { namespace prop { diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 43f7f75af..f024dccf3 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: dejan, taking, mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): kshitij ** 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 @@ -24,6 +24,8 @@ #include "theory/theory_engine.h" #include "theory/rewriter.h" #include "expr/expr_stream.h" +#include "decision/decision_engine.h" + namespace CVC4 { namespace prop { @@ -73,7 +75,14 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { SatLiteral TheoryProxy::getNextDecisionRequest() { TNode n = d_theoryEngine->getNextDecisionRequest(); - return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n); + if(not n.isNull()) + return d_cnfStream->getLiteral(n); + + // If theory doesn't give us a deicsion ask the decision engine. It + // may return in undefSatLiteral in which case the sat solver figure + // it out something + Assert(d_decisionEngine != NULL); + return d_decisionEngine->getNext(); } bool TheoryProxy::theoryNeedCheck() const { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 8b585710f..ceb328d90 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking, cconway, dejan - ** Minor contributors (to current version): barrett + ** Minor contributors (to current version): barrett, kshitij ** 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 @@ -33,6 +33,7 @@ namespace CVC4 { +class DecisionEngine; class TheoryEngine; namespace prop { @@ -51,6 +52,9 @@ class TheoryProxy { /** The CNF engine we are using */ CnfStream* d_cnfStream; + /** The decision engine we are using */ + DecisionEngine* d_decisionEngine; + /** The theory engine we are using */ TheoryEngine* d_theoryEngine; @@ -66,6 +70,7 @@ class TheoryProxy { public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream); @@ -113,10 +118,12 @@ public: inline TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream) : d_propEngine(propEngine), d_cnfStream(cnfStream), + d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), d_context(context) {} diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 97407a425..a41def821 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): cconway, kshitij ** 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 @@ -27,6 +27,7 @@ #include "context/cdlist.h" #include "context/cdhashset.h" #include "context/context.h" +#include "decision/decision_engine.h" #include "expr/command.h" #include "expr/expr.h" #include "expr/kind.h" @@ -223,6 +224,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_userContext(new UserContext()), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), + d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), d_definedFunctions(NULL), @@ -262,8 +264,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY); CVC4_FOR_EACH_THEORY; - d_propEngine = new PropEngine(d_theoryEngine, d_context); + d_decisionEngine = new DecisionEngine(); + d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + // d_decisionEngine->setPropEngine(d_propEngine); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); @@ -309,6 +313,7 @@ void SmtEngine::shutdown() { d_propEngine->shutdown(); d_theoryEngine->shutdown(); + d_decisionEngine->shutdown(); } SmtEngine::~SmtEngine() throw() { @@ -917,9 +922,6 @@ void SmtEnginePrivate::simplifyAssertions() staticLearning(); } - // Remove ITEs - removeITEs(); - } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any // typechecking exceptions via (e.g.) ensureBoolean(). But a @@ -1004,6 +1006,15 @@ void SmtEnginePrivate::processAssertions() { // Simplify the assertions simplifyAssertions(); + if(d_smt.d_decisionEngine->needSimplifiedPreITEAssertions()) { + d_smt.d_decisionEngine->informSimplifiedPreITEAssertions(d_assertionsToCheck); + } + + // Remove ITEs + removeITEs(); // This may need to be in a try-catch + // block. make regress is passing, so + // skipping for now --K + Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5149ed2e9..abd07538b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): cconway, kshitij ** 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 @@ -50,6 +50,7 @@ typedef NodeTemplate<true> Node; typedef NodeTemplate<false> TNode; class NodeHashFunction; +class DecisionEngine; class TheoryEngine; class StatisticsRegistry; @@ -109,6 +110,8 @@ class CVC4_PUBLIC SmtEngine { /** Our internal expression/node manager */ NodeManager* d_nodeManager; /** The decision engine */ + DecisionEngine* d_decisionEngine; + /** The theory engine */ TheoryEngine* d_theoryEngine; /** The propositional engine */ prop::PropEngine* d_propEngine; diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 8c7069975..9dd8e588a 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -119,7 +119,7 @@ private: /** * Priority Queue of the basic variables that may be inconsistent. * Variables are ordered according to which violates its bound the most. - * This is a hueristic and makes no guarentees to terminate! + * This is a heuristic and makes no guarentees to terminate! * This heuristic comes from Alberto Griggio's thesis. */ DifferenceArray d_diffQueue; diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 5837d4793..9f48dad77 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -254,9 +254,9 @@ bool SimplexDecisionProcedure::findModel(){ foundConflict = findConflictOnTheQueue(BeforeDiffSearch); } if(!foundConflict){ - uint32_t numHueristicPivots = d_numVariables + 1; - uint32_t pivotsRemaining = numHueristicPivots; - uint32_t pivotsPerCheck = (numHueristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); + uint32_t numHeuristicPivots = d_numVariables + 1; + uint32_t pivotsRemaining = numHeuristicPivots; + uint32_t pivotsPerCheck = (numHeuristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); while(!d_queue.empty() && !foundConflict && pivotsRemaining > 0){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 4e5ba3d9e..7ad7734c7 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -27,13 +27,13 @@ ** we do not maintain that the queue of variables needs to be only basic variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a hueristic pivoting rule. (See PreferenceFunction Documentation for the available options.) + ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction Documentation for the available options.) ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue hueristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue heuristics, and ** 3) detect multiple conflicts. ** ** Conflicts are greedily slackened to use the weakest bounds that still produce the conflict. @@ -152,7 +152,7 @@ private: * minRowCount is a PreferenceFunction for selecting the variable with the smaller * row count in the tableau. * - * This is a hueristic rule and should not be used + * This is a heuristic rule and should not be used * during the VarOrder stage of findModel. */ static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); @@ -163,7 +163,7 @@ private: * If both have bounds or both do not have bounds, * the rule falls back to minRowCount(...). * - * This is a hueristic rule and should not be used + * This is a heuristic rule and should not be used * during the VarOrder stage of findModel. */ static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); diff --git a/src/util/options.cpp b/src/util/options.cpp index b6a306ee0..0bd02f308 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -80,6 +80,8 @@ Options::Options() : printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), simplificationModeSetByUser(false), + decisionMode(DECISION_STRATEGY_INTERNAL), + decisionModeSetByUser(false), doStaticLearning(true), interactive(false), interactiveSetByUser(false), diff --git a/src/util/options.h b/src/util/options.h index c7fbcd896..6205c7543 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -126,6 +126,23 @@ struct CVC4_PUBLIC Options { /** Whether the user set the nonclausal simplification mode. */ bool simplificationModeSetByUser; + /** Enumeration of decision strategies */ + typedef enum { + /** + * Decision engine doesn't do anything. Use sat solver's internal + * heuristics + */ + DECISION_STRATEGY_INTERNAL, + /** + * Use the justification heuristic + */ + DECISION_STRATEGY_JUSTIFICATION + } DecisionMode; + /** When/whether to use any decision strategies */ + DecisionMode decisionMode; + /** Whether the user set the decision strategy */ + bool decisionModeSetByUser; + /** Whether to perform the static learning pass. */ bool doStaticLearning; |