summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am4
-rw-r--r--src/decision/Makefile4
-rw-r--r--src/decision/Makefile.am13
-rw-r--r--src/decision/decision_engine.cpp55
-rw-r--r--src/decision/decision_engine.h150
-rw-r--r--src/decision/decision_strategy.h50
-rw-r--r--src/decision/justification_heuristic.cpp393
-rw-r--r--src/decision/justification_heuristic.h96
-rw-r--r--src/prop/prop_engine.cpp11
-rw-r--r--src/prop/prop_engine.h8
-rw-r--r--src/prop/sat_solver_types.h3
-rw-r--r--src/prop/theory_proxy.cpp13
-rw-r--r--src/prop/theory_proxy.h9
-rw-r--r--src/smt/smt_engine.cpp21
-rw-r--r--src/smt/smt_engine.h5
-rw-r--r--src/theory/arith/arith_priority_queue.h2
-rw-r--r--src/theory/arith/simplex.cpp6
-rw-r--r--src/theory/arith/simplex.h8
-rw-r--r--src/util/options.cpp2
-rw-r--r--src/util/options.h17
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback