summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/justification_heuristic.cpp119
-rw-r--r--src/decision/justification_heuristic.h25
-rw-r--r--src/decision/relevancy.cpp2
-rw-r--r--src/decision/relevancy.h9
-rw-r--r--src/smt/smt_engine.cpp12
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h3
7 files changed, 61 insertions, 111 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 93ff65e6d..065d40a9a 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -96,16 +96,18 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
void JustificationHeuristic::computeITEs(TNode n, IteList &l)
{
- Debug("jh-ite") << " computeITEs( " << n << ", &l)\n";
+ Trace("jh-ite") << " computeITEs( " << n << ", &l)\n";
for(unsigned i=0; i<n.getNumChildren(); ++i) {
SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
- if(it2 != d_iteAssertions.end())
- l.push_back(it2->second);
+ if(it2 != d_iteAssertions.end()) {
+ l.push_back(make_pair(n[i], it2->second));
+ Assert(n[i].getNumChildren() == 0);
+ }
computeITEs(n[i], l);
}
}
-const IteList& JustificationHeuristic::getITEs(TNode n)
+const JustificationHeuristic::IteList& JustificationHeuristic::getITEs(TNode n)
{
IteCache::iterator it = d_iteCache.find(n);
if(it != d_iteCache.end()) {
@@ -113,7 +115,7 @@ const IteList& JustificationHeuristic::getITEs(TNode n)
} else {
// Compute the list of ITEs
// TODO: optimize by avoiding multiple lookup for d_iteCache[n]
- d_iteCache[n] = vector<TNode>();
+ d_iteCache[n] = IteList();
computeITEs(n, d_iteCache[n]);
return d_iteCache[n];
}
@@ -123,7 +125,7 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
SatValue desiredVal,
SatLiteral* litDecision)
{
- Trace("decision")
+ Trace("jh-findSplitterRec")
<< "findSplitterRec(" << node << ", "
<< desiredVal << ", .. )" << std::endl;
@@ -136,36 +138,20 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
if(Debug.isOn("decision")) {
if(checkJustified(node))
Debug("decision") << " justified, returning" << std::endl;
- if(d_visited.find(node) != d_visited.end())
- Debug("decision") << " visited, returning" << std::endl;
}
/* Base case */
- if (checkJustified(node))
+ if (checkJustified(node)) {
return false;
- if(d_visited.find(node) != d_visited.end()) {
-
- if(tryGetSatValue(node) != SAT_VALUE_UNKNOWN) {
- setJustified(node);
- return false;
- } else {
- Assert(d_decisionEngine->hasSatLiteral(node));
- SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
- *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
- Trace("decision") << "decision " << *litDecision << std::endl;
- Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
- return true;
- }
-
}
-#if defined CVC4_ASSERTIONS || defined CVC4_TRACING
+#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
// We don't always have a sat literal, so remember that. Will need
// it for some assertions we make.
bool litPresent = d_decisionEngine->hasSatLiteral(node);
- if(Trace.isOn("decision")) {
+ if(Debug.isOn("decision")) {
if(!litPresent) {
- Trace("decision") << "no sat literal for this node" << std::endl;
+ Debug("decision") << "no sat literal for this node" << std::endl;
}
}
//Assert(litPresent); -- fails
@@ -186,10 +172,10 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
theory::TheoryId tId = theory::kindToTheoryId(k);
/* Some debugging stuff */
- Trace("jh-findSplitterRec") << "kind = " << k << std::endl;
- Trace("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
- Trace("jh-findSplitterRec") << "node = " << node << std::endl;
- Trace("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
+ Debug("jh-findSplitterRec") << "kind = " << k << std::endl;
+ Debug("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
+ Debug("jh-findSplitterRec") << "node = " << node << std::endl;
+ Debug("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
/**
* If not in theory of booleans, and not a "boolean" EQUAL (IFF),
@@ -202,73 +188,20 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
// if node has embedded ites -- which currently happens iff it got
// replaced during ite removal -- then try to resolve that first
const IteList& l = getITEs(node);
- Debug("jh-ite") << " ite size = " << l.size() << std::endl;
- d_visited.insert(node);
- for(unsigned i = 0; i < l.size(); ++i) {
- Debug("jh-ite") << " i = " << i
- << " l[i] = " << l[i] << std::endl;
- if (checkJustified(l[i])) continue;
-
- // Assert(l[i].getKind() == kind::ITE, "Expected ITE");
- if(l[i].getKind() != kind::ITE) {
- //this might happen because of repeatSimp
- Debug("jh-ite") << " not an ite, must have got repeatSimp-ed"
- << std::endl;
- findSplitterRec(l[i], SAT_VALUE_TRUE, litDecision);
- continue;
- }
-
- SatValue desiredVal = SAT_VALUE_TRUE; //NOTE: Reusing variable
-#ifdef CVC4_ASSERTIONS
- bool litPresent = d_decisionEngine->hasSatLiteral(l[i]);
-#endif
-
- // Handle the ITE to catch the case when a variable is its own
- // fanin
- SatValue ifVal = tryGetSatValue(l[i][0]);
- if (ifVal == SAT_VALUE_UNKNOWN) {
- // are we better off trying false? if not, try true
- SatValue ifDesiredVal =
- (tryGetSatValue(l[i][2]) == desiredVal ||
- tryGetSatValue(l[i][1]) == invertValue(desiredVal))
- ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
-
- if(findSplitterRec(l[i][0], ifDesiredVal, litDecision)) {
- return true;
- }
-
- // Handle special case when if node itself is visited. Decide
- // on it.
- if(d_visited.find(l[i][0]) != d_visited.end()) {
- Assert(d_decisionEngine->hasSatLiteral(l[i][0]));
- SatVariable v = d_decisionEngine->getSatLiteral(l[i][0]).getSatVariable();
- *litDecision = SatLiteral(v, ifDesiredVal != SAT_VALUE_TRUE );
+ Trace("jh-ite") << " ite size = " << l.size() << std::endl;
+ /*d_visited.insert(node);*/
+ for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
+ if(d_visited.find(i->first) == d_visited.end()) {
+ d_visited.insert(i->first);
+ Debug("jh-ite") << "jh-ite: adding visited " << i->first << std::endl;
+ if(findSplitterRec(i->second, SAT_VALUE_TRUE, litDecision))
return true;
- }
-
- Assert(false, "No controlling input found (1)");
+ Debug("jh-ite") << "jh-ite: removing visited " << i->first << std::endl;
+ d_visited.erase(i->first);
} else {
-
- // Try to justify 'if'
- if (findSplitterRec(l[i][0], ifVal, litDecision)) {
- return true;
- }
-
- // If that was successful, we need to go into only one of 'then'
- // or 'else'
- int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
- int chVal = tryGetSatValue(l[i][ch]);
- if( d_visited.find(l[i]) == d_visited.end()
- && (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal)
- && findSplitterRec(l[i][ch], desiredVal, litDecision) ) {
- return true;
- }
+ Debug("jh-ite") << "jh-ite: already visited " << i->first << std::endl;
}
- Assert(litPresent == false || litVal == desiredVal,
- "Output should be justified");
- setJustified(l[i]);
}
- d_visited.erase(node);
if(litVal != SAT_VALUE_UNKNOWN) {
setJustified(node);
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 6c470e6df..1dc7a85d7 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -34,8 +34,6 @@ namespace CVC4 {
namespace decision {
-typedef std::vector<TNode> IteList;
-
class GiveUpException : public Exception {
public:
GiveUpException() :
@@ -44,11 +42,13 @@ public:
};/* class GiveUpException */
class JustificationHeuristic : public ITEDecisionStrategy {
+ typedef std::vector<pair<TNode,TNode> > IteList;
typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
// being 'justified' is monotonic with respect to decisions
- context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+ typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
+ JustifiedSet d_justified;
context::CDO<unsigned> d_prvsIndex;
IntStat d_helfulness;
@@ -99,8 +99,19 @@ public:
d_visited.clear();
+ if(Trace.isOn("justified")) {
+ for(JustifiedSet::iterator i = d_justified.begin();
+ i != d_justified.end(); ++i) {
+ TNode n = *i;
+ SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
+ d_decisionEngine->getSatLiteral(n) : -1;
+ SatValue v = tryGetSatValue(n);
+ Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
+ }
+ }
+
for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
- Trace("decision") << d_assertions[i] << std::endl;
+ Debug("decision") << d_assertions[i] << std::endl;
// Sanity check: if it was false, aren't we inconsistent?
Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
@@ -153,7 +164,7 @@ public:
// Save mapping between ite skolems and ite assertions
for(IteSkolemMap::iterator i = iteSkolemMap.begin();
i != iteSkolemMap.end(); ++i) {
- Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to "
+ Trace("jh-ite") << " jh-ite: " << (i->first) << " maps to "
<< assertions[(i->second)] << std::endl;
Assert(i->second >= assertionsEnd && i->second < assertions.size());
d_iteAssertions[i->first] = assertions[i->second];
@@ -175,7 +186,7 @@ private:
return prop::undefSatLiteral;
}
if(ret == true) {
- Trace("decision") << "Yippee!!" << std::endl;
+ Debug("decision") << "Yippee!!" << std::endl;
//d_prvsIndex = i;
++d_helfulness;
return litDecision;
@@ -199,7 +210,7 @@ private:
SatValue tryGetSatValue(Node n);
/* Get list of all term-ITEs for the atomic formula v */
- const IteList& getITEs(TNode n);
+ const JustificationHeuristic::IteList& getITEs(TNode n);
/* Compute all term-ITEs in a node recursively */
void computeITEs(TNode n, IteList &l);
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
index c5e1f7fbc..f73337c8f 100644
--- a/src/decision/relevancy.cpp
+++ b/src/decision/relevancy.cpp
@@ -68,7 +68,7 @@ void Relevancy::computeITEs(TNode n, IteList &l)
}
}
-const IteList& Relevancy::getITEs(TNode n)
+const Relevancy::IteList& Relevancy::getITEs(TNode n)
{
IteCache::iterator it = d_iteCache.find(n);
if(it != d_iteCache.end()) {
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index 3a33a5cb8..f45ce2e8f 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -46,8 +46,6 @@ namespace CVC4 {
namespace decision {
-typedef std::vector<TNode> IteList;
-
class RelGiveUpException : public Exception {
public:
RelGiveUpException() :
@@ -56,6 +54,7 @@ public:
};/* class GiveUpException */
class Relevancy : public RelevancyStrategy {
+ typedef std::vector<TNode> IteList;
typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
@@ -139,6 +138,10 @@ public:
d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0),
d_curDecision(NULL)
{
+ Warning() << "There are known bugs in this Relevancy code which we know"
+ << "how to fix (but haven't yet)." << std::endl
+ << "Please bug kshitij if you wish to use." << std::endl;
+
StatisticsRegistry::registerStat(&d_helfulness);
StatisticsRegistry::registerStat(&d_polqueries);
StatisticsRegistry::registerStat(&d_polhelp);
@@ -350,7 +353,7 @@ private:
SatValue tryGetSatValue(Node n);
/* Get list of all term-ITEs for the atomic formula v */
- const IteList& getITEs(TNode n);
+ const Relevancy::IteList& getITEs(TNode n);
/* Compute all term-ITEs in a node recursively */
void computeITEs(TNode n, IteList &l);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2bdf7b71f..5e8d71198 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1267,7 +1267,7 @@ bool SmtEnginePrivate::simplifyAssertions()
d_assertionsToCheck.swap(d_assertionsToPreprocess);
}
- Debug("smt") << "POST nonClasualSimplify" << std::endl;
+ Trace("smt") << "POST nonClasualSimplify" << std::endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
@@ -1283,7 +1283,7 @@ bool SmtEnginePrivate::simplifyAssertions()
}
}
- Debug("smt") << "POST theoryPP" << std::endl;
+ Trace("smt") << "POST theoryPP" << std::endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
@@ -1292,7 +1292,7 @@ bool SmtEnginePrivate::simplifyAssertions()
simpITE();
}
- Debug("smt") << "POST iteSimp" << std::endl;
+ Trace("smt") << "POST iteSimp" << std::endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
@@ -1301,7 +1301,7 @@ bool SmtEnginePrivate::simplifyAssertions()
unconstrainedSimp();
}
- Debug("smt") << "POST unconstraintedSimp" << std::endl;
+ Trace("smt") << "POST unconstraintedSimp" << std::endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
@@ -1313,7 +1313,7 @@ bool SmtEnginePrivate::simplifyAssertions()
if(!noConflict) return false;
}
- Debug("smt") << "POST repeatSimp" << std::endl;
+ Trace("smt") << "POST repeatSimp" << std::endl;
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
@@ -1480,7 +1480,7 @@ void SmtEnginePrivate::processAssertions() {
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
- Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
+ Debug("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/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0c0d65d74..92e4b17df 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -19,6 +19,8 @@
#include <vector>
#include <list>
+#include "decision/decision_engine.h"
+
#include "expr/attribute.h"
#include "expr/node.h"
#include "expr/node_builder.h"
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2440a2e53..0452d13aa 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -25,7 +25,6 @@
#include <vector>
#include <utility>
-#include "decision/decision_engine.h"
#include "expr/node.h"
#include "expr/command.h"
#include "prop/prop_engine.h"
@@ -76,6 +75,8 @@ namespace theory {
class Instantiator;
}/* CVC4::theory namespace */
+class DecisionEngine;
+
/**
* This is essentially an abstraction for a collection of theories. A
* TheoryEngine provides services to a PropEngine, making various
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback