summaryrefslogtreecommitdiff
path: root/src/decision/relevancy.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision/relevancy.cpp')
-rw-r--r--src/decision/relevancy.cpp379
1 files changed, 0 insertions, 379 deletions
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
deleted file mode 100644
index f83e238d4..000000000
--- a/src/decision/relevancy.cpp
+++ /dev/null
@@ -1,379 +0,0 @@
-/********************* */
-/*! \file relevancy.cpp
- ** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** 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.
- **/
-/*****************************************************************************/
-
-#include "relevancy.h"
-
-#include "expr/node_manager.h"
-#include "expr/kind.h"
-#include "theory/rewriter.h"
-#include "util/ite_removal.h"
-
-// Relevancy stuff
-
-const double Relevancy::secondsPerDecision = 0.001;
-const double Relevancy::secondsPerExpense = 1e-7;
-const double Relevancy::EPS = 1e-9;
-
-
-void Relevancy::setJustified(TNode n)
-{
- Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;
- d_justified.insert(n);
- if(options::decisionComputeRelevancy()) {
- d_relevancy[n] = d_maxRelevancy[n];
- updateRelevancy(n);
- }
-}
-
-bool Relevancy::checkJustified(TNode n)
-{
- return d_justified.find(n) != d_justified.end();
-}
-
-SatValue Relevancy::tryGetSatValue(Node n)
-{
- Debug("decision") << " " << n << " has sat value " << " ";
- if(d_decisionEngine->hasSatLiteral(n) ) {
- Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl;
- return d_decisionEngine->getSatValue(n);
- } else {
- Debug("decision") << "NO SAT LITERAL" << std::endl;
- return SAT_VALUE_UNKNOWN;
- }//end of else
-}
-
-void Relevancy::computeITEs(TNode n, IteList &l)
-{
- Debug("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);
- computeITEs(n[i], l);
- }
-}
-
-const Relevancy::IteList& Relevancy::getITEs(TNode n)
-{
- IteCache::iterator it = d_iteCache.find(n);
- if(it != d_iteCache.end()) {
- return it->second;
- } else {
- // Compute the list of ITEs
- // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
- d_iteCache[n] = vector<TNode>();
- computeITEs(n, d_iteCache[n]);
- return d_iteCache[n];
- }
-}
-
-bool Relevancy::findSplitterRec(TNode node,
- SatValue desiredVal)
-{
- Trace("decision")
- << "findSplitterRec([" << node.getId() << "]" << node << ", "
- << desiredVal << ", .. )" << std::endl;
-
- ++d_expense;
-
- /* Handle NOT as a special case */
- while (node.getKind() == kind::NOT) {
- desiredVal = invertValue(desiredVal);
- node = node[0];
- }
-
- /* Avoid infinite loops */
- if(d_visited.find(node) != d_visited.end()) {
- Debug("decision") << " node repeated. kind was " << node.getKind() << std::endl;
- Assert(false);
- Assert(node.getKind() == kind::ITE);
- return false;
- }
-
- /* Base case */
- if(checkJustified(node)) {
- return false;
- }
-
- /**
- * If we have already explored the subtree for some desiredVal, we
- * skip this and continue exploring the rest
- */
- if(d_polarityCache.find(node) == d_polarityCache.end()) {
- d_polarityCache[node] = desiredVal;
- } else {
- Assert(d_multipleBacktrace || options::decisionComputeRelevancy());
- return true;
- }
-
- d_visited.insert(node);
-
-#if defined CVC4_ASSERTIONS || defined CVC4_TRACING
- // 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(!litPresent) {
- Trace("decision") << "no sat literal for this node" << std::endl;
- }
- }
- //Assert(litPresent); -- fails
-#endif
-
- // Get value of sat literal for the node, if there is one
- SatValue litVal = tryGetSatValue(node);
-
- /* You'd better know what you want */
- Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
-
- /* Good luck, hope you can get what you want */
- Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
- "invariant violated");
-
- /* What type of node is this */
- Kind k = node.getKind();
- 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;
-
- /**
- * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
- * then check if this is something to split-on.
- */
- if(tId != theory::THEORY_BOOL
- // && !(k == kind::EQUAL && node[0].getType().isBoolean())
- ) {
-
- // 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;
- for(unsigned i = 0; i < l.size(); ++i) {
- Assert(l[i].getKind() == kind::ITE, "Expected ITE");
- Debug("jh-ite") << " i = " << i
- << " l[i] = " << l[i] << std::endl;
- if(d_visited.find(node) != d_visited.end() ) continue;
- if(findSplitterRec(l[i], SAT_VALUE_TRUE)) {
- d_visited.erase(node);
- return true;
- }
- }
- Debug("jh-ite") << " ite done " << l.size() << std::endl;
-
- if(litVal != SAT_VALUE_UNKNOWN) {
- d_visited.erase(node);
- setJustified(node);
- return false;
- } else {
- /* if(not d_decisionEngine->hasSatLiteral(node))
- throw GiveUpException(); */
- Assert(d_decisionEngine->hasSatLiteral(node));
- SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
- *d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
- Trace("decision") << "decision " << *d_curDecision << std::endl;
- Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
- d_visited.erase(node);
- return true;
- }
- }
-
- bool ret = false;
- SatValue flipCaseVal = SAT_VALUE_FALSE;
- switch (k) {
-
- case kind::CONST_BOOLEAN:
- Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE);
- Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE);
- break;
-
- case kind::AND:
- if (desiredVal == SAT_VALUE_FALSE) ret = handleOrTrue(node, SAT_VALUE_FALSE);
- else ret = handleOrFalse(node, SAT_VALUE_TRUE);
- break;
-
- case kind::OR:
- if (desiredVal == SAT_VALUE_FALSE) ret = handleOrFalse(node, SAT_VALUE_FALSE);
- else ret = handleOrTrue(node, SAT_VALUE_TRUE);
- break;
-
- case kind::IMPLIES:
- Assert(node.getNumChildren() == 2, "Expected 2 fanins");
- if (desiredVal == SAT_VALUE_FALSE) {
- ret = findSplitterRec(node[0], SAT_VALUE_TRUE);
- if(ret) break;
- ret = findSplitterRec(node[1], SAT_VALUE_FALSE);
- break;
- }
- else {
- if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
- ret = findSplitterRec(node[0], SAT_VALUE_FALSE);
- //if(!ret || !d_multipleBacktrace)
- break;
- }
- if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
- ret = findSplitterRec(node[1], SAT_VALUE_TRUE);
- break;
- }
- Assert(d_multipleBacktrace, "No controlling input found (3)");
- }
- break;
-
- case kind::XOR:
- flipCaseVal = SAT_VALUE_TRUE;
- case kind::IFF: {
- SatValue val = tryGetSatValue(node[0]);
- if (val != SAT_VALUE_UNKNOWN) {
- ret = findSplitterRec(node[0], val);
- if (ret) break;
- if (desiredVal == flipCaseVal) val = invertValue(val);
- ret = findSplitterRec(node[1], val);
- }
- else {
- val = tryGetSatValue(node[1]);
- if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
- if (desiredVal == flipCaseVal) val = invertValue(val);
- ret = findSplitterRec(node[0], val);
- if(ret) break;
- Assert(false, "Unable to find controlling input (4)");
- }
- break;
- }
-
- case kind::ITE:
- ret = handleITE(node, desiredVal);
- break;
-
- default:
- Assert(false, "Unexpected Boolean operator");
- break;
- }//end of switch(k)
-
- d_visited.erase(node);
- if(ret == false) {
- Assert(litPresent == false || litVal == desiredVal,
- "Output should be justified");
- setJustified(node);
- }
- return ret;
-
- Unreachable();
-}/* findRecSplit method */
-
-bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) {
- Debug("jh-findSplitterRec") << " handleOrFalse (" << node << ", "
- << desiredVal << std::endl;
-
- Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or
- (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) );
-
- int n = node.getNumChildren();
- bool ret = false;
- for(int i = 0; i < n; ++i) {
- if (findSplitterRec(node[i], desiredVal)) {
- if(!options::decisionComputeRelevancy())
- return true;
- else
- ret = true;
- }
- }
- return ret;
-}
-
-bool Relevancy::handleOrTrue(TNode node, SatValue desiredVal) {
- Debug("jh-findSplitterRec") << " handleOrTrue (" << node << ", "
- << desiredVal << std::endl;
-
- Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or
- (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) );
-
- int n = node.getNumChildren();
- SatValue desiredValInverted = invertValue(desiredVal);
- for(int i = 0; i < n; ++i) {
- if ( tryGetSatValue(node[i]) != desiredValInverted ) {
- // PRE RELEVANCY return findSplitterRec(node[i], desiredVal);
- bool ret = findSplitterRec(node[i], desiredVal);
- if(ret) {
- // Splitter could be found... so can't justify this node
- if(!d_multipleBacktrace)
- return true;
- }
- else {
- // Splitter couldn't be found... should be justified
- return false;
- }
- }
- }
- // Multiple backtrace is on, so must have reached here because
- // everything had splitter
- if(d_multipleBacktrace) return true;
-
- if(Debug.isOn("jh-findSplitterRec")) {
- Debug("jh-findSplitterRec") << " * ** " << std::endl;
- Debug("jh-findSplitterRec") << node.getKind() << " "
- << node << std::endl;
- for(unsigned i = 0; i < node.getNumChildren(); ++i)
- Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i])
- << std::endl;
- Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node)
- << std::endl;
- }
- Assert(false, "No controlling input found");
- return false;
-}
-
-bool Relevancy::handleITE(TNode node, SatValue desiredVal)
-{
- Debug("jh-findSplitterRec") << " handleITE (" << node << ", "
- << desiredVal << std::endl;
-
- //[0]: if, [1]: then, [2]: else
- SatValue ifVal = tryGetSatValue(node[0]);
- if (ifVal == SAT_VALUE_UNKNOWN) {
-
- // are we better off trying false? if not, try true
- SatValue ifDesiredVal =
- (tryGetSatValue(node[2]) == desiredVal ||
- tryGetSatValue(node[1]) == invertValue(desiredVal))
- ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
-
- if(findSplitterRec(node[0], ifDesiredVal)) return true;
-
- Assert(false, "No controlling input found (6)");
- } else {
-
- // Try to justify 'if'
- if(findSplitterRec(node[0], ifVal)) 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(node[ch]);
- if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) &&
- findSplitterRec(node[ch], desiredVal) ) {
- return true;
- }
- }// else (...ifVal...)
- return false;
-}//handleITE
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback