From b4e3e33e41904969a5bfc836e2af45361e011b82 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 16:11:07 -0600 Subject: [PATCH] Remove old decision justification heurstic (#8275) Fixes cvc5/cvc5-projects#374. --- src/CMakeLists.txt | 7 - src/decision/decision_attributes.h | 35 - src/decision/decision_engine.cpp | 9 +- src/decision/decision_engine_old.cpp | 97 --- src/decision/decision_engine_old.h | 131 --- src/decision/decision_strategy.h | 71 -- src/decision/justification_heuristic.cpp | 743 ------------------ src/decision/justification_heuristic.h | 194 ----- src/options/decision_options.toml | 49 -- src/options/decision_weight.h | 29 - src/prop/prop_engine.cpp | 6 - .../ho/bug_freevar_PHI004^4-delta.smt2 | 2 +- 12 files changed, 4 insertions(+), 1369 deletions(-) delete mode 100644 src/decision/decision_attributes.h delete mode 100644 src/decision/decision_engine_old.cpp delete mode 100644 src/decision/decision_engine_old.h delete mode 100644 src/decision/decision_strategy.h delete mode 100644 src/decision/justification_heuristic.cpp delete mode 100644 src/decision/justification_heuristic.h delete mode 100644 src/options/decision_weight.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7becedad4..e1822991b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -21,14 +21,8 @@ libcvc5_add_sources( api/cpp/cvc5_kind.h decision/assertion_list.cpp decision/assertion_list.h - decision/decision_attributes.h decision/decision_engine.cpp decision/decision_engine.h - decision/decision_engine_old.cpp - decision/decision_engine_old.h - decision/decision_strategy.h - decision/justification_heuristic.cpp - decision/justification_heuristic.h decision/justification_strategy.cpp decision/justification_strategy.h decision/justify_info.cpp @@ -50,7 +44,6 @@ libcvc5_add_sources( omt/integer_optimizer.h omt/omt_optimizer.cpp omt/omt_optimizer.h - options/decision_weight.h options/io_utils.cpp options/io_utils.h options/language.cpp diff --git a/src/decision/decision_attributes.h b/src/decision/decision_attributes.h deleted file mode 100644 index 2654019ba..000000000 --- a/src/decision/decision_attributes.h +++ /dev/null @@ -1,35 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner, Tim King, Kshitij Bansal - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Rewriter attributes. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__DECISION__DECISION_ATTRIBUTES_H -#define CVC5__DECISION__DECISION_ATTRIBUTES_H - -#include "options/decision_weight.h" -#include "expr/attribute.h" - -namespace cvc5 { -namespace decision { -namespace attr { - struct DecisionWeightTag {}; - } // namespace attr - -typedef expr::Attribute DecisionWeightAttr; - -} // namespace decision -} // namespace cvc5 - -#endif /* CVC5__DECISION__DECISION_ATTRIBUTES_H */ diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 88f8c6c50..9fed955cf 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -14,10 +14,6 @@ */ #include "decision/decision_engine.h" -#include "decision/decision_engine_old.h" -#include "options/decision_options.h" -#include "prop/sat_solver.h" -#include "smt/env.h" #include "util/resource_manager.h" namespace cvc5 { @@ -28,7 +24,8 @@ DecisionEngine::DecisionEngine(Env& env) { } -void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs) +void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss, + prop::CnfStream* cs) { d_satSolver = ss; d_cnfStream = cs; @@ -50,7 +47,7 @@ void DecisionEngineEmpty::addSkolemDefinition(TNode lem, } prop::SatLiteral DecisionEngineEmpty::getNextInternal(bool& stopSearch) { - return undefSatLiteral; + return prop::undefSatLiteral; } } // namespace decision diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp deleted file mode 100644 index 261d78fdf..000000000 --- a/src/decision/decision_engine_old.cpp +++ /dev/null @@ -1,97 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Aina Niemetz, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Old implementation of the decision engine - */ -#include "decision/decision_engine_old.h" - -#include "decision/decision_attributes.h" -#include "decision/justification_heuristic.h" -#include "expr/node.h" -#include "options/decision_options.h" -#include "options/smt_options.h" -#include "util/resource_manager.h" - -using namespace std; - -namespace cvc5 { - -DecisionEngineOld::DecisionEngineOld(Env& env) - : DecisionEngine(env), - d_result(context(), SAT_VALUE_UNKNOWN), - d_engineState(0), - d_enabledITEStrategy(nullptr), - d_decisionStopOnly(options().decision.decisionMode - == options::DecisionMode::STOPONLY_OLD) -{ - Trace("decision") << "Creating decision engine" << std::endl; - Assert(d_engineState == 0); - d_engineState = 1; - - Trace("decision-init") << "DecisionEngineOld::init()" << std::endl; - Trace("decision-init") << " * options->decisionMode: " - << options().decision.decisionMode << std::endl; - Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly - << std::endl; - - if (options().decision.decisionMode == options::DecisionMode::JUSTIFICATION) - { - d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this)); - } -} - -void DecisionEngineOld::shutdown() -{ - Trace("decision") << "Shutting down decision engine" << std::endl; - - Assert(d_engineState == 1); - d_engineState = 2; - d_enabledITEStrategy.reset(nullptr); -} - -SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch) -{ - Assert(d_cnfStream != nullptr) - << "Forgot to set cnfStream for decision engine?"; - Assert(d_satSolver != nullptr) - << "Forgot to set satSolver for decision engine?"; - - SatLiteral ret = d_enabledITEStrategy == nullptr - ? undefSatLiteral - : d_enabledITEStrategy->getNext(stopSearch); - // if we are doing stop only, we don't return the literal - return d_decisionStopOnly ? undefSatLiteral : ret; -} - -void DecisionEngineOld::addAssertion(TNode assertion, bool isLemma) -{ - // new assertions, reset whatever result we knew - d_result = SAT_VALUE_UNKNOWN; - if (d_enabledITEStrategy != nullptr) - { - d_enabledITEStrategy->addAssertion(assertion); - } -} - -void DecisionEngineOld::addSkolemDefinition(TNode lem, - TNode skolem, - bool isLemma) -{ - // new assertions, reset whatever result we knew - d_result = SAT_VALUE_UNKNOWN; - if (d_enabledITEStrategy != nullptr) - { - d_enabledITEStrategy->addSkolemDefinition(lem, skolem); - } -} - -} // namespace cvc5 diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h deleted file mode 100644 index 5f33a5ecc..000000000 --- a/src/decision/decision_engine_old.h +++ /dev/null @@ -1,131 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Andrew Reynolds, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Old implementation of the decision engine - */ - -#include "cvc5_private.h" - -#ifndef CVC5__DECISION__DECISION_ENGINE_OLD_H -#define CVC5__DECISION__DECISION_ENGINE_OLD_H - -#include "base/output.h" -#include "context/cdo.h" -#include "decision/decision_engine.h" -#include "decision/decision_strategy.h" -#include "expr/node.h" -#include "prop/cnf_stream.h" -#include "prop/sat_solver.h" -#include "prop/sat_solver_types.h" -#include "util/result.h" - -using namespace cvc5::prop; -using namespace cvc5::decision; - -namespace cvc5 { - -class DecisionEngineOld : public decision::DecisionEngine -{ - public: - // Necessary functions - - /** Constructor */ - DecisionEngineOld(Env& env); - - /** Destructor, currently does nothing */ - ~DecisionEngineOld() - { - Trace("decision") << "Destroying decision engine" << std::endl; - } - - /** - * This is called by SolverEngine, at shutdown time, just before - * destruction. It is important because there are destruction - * ordering issues between some parts of the system. - */ - void shutdown(); - - // Interface for External World to use our services - - /** Gets the next decision based on strategies that are enabled */ - SatLiteral getNextInternal(bool& stopSearch) override; - - /** Is the DecisionEngineOld in a state where it has solved everything? */ - bool isDone() override - { - Trace("decision") << "DecisionEngineOld::isDone() returning " - << (d_result != SAT_VALUE_UNKNOWN) - << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") - << std::endl; - return (d_result != SAT_VALUE_UNKNOWN); - } - - /** */ - Result getResult() - { - switch (d_result.get()) - { - case SAT_VALUE_TRUE: return Result(Result::SAT); - case SAT_VALUE_FALSE: return Result(Result::UNSAT); - case SAT_VALUE_UNKNOWN: - return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - default: Assert(false) << "d_result is garbage"; - } - return Result(); - } - - /** */ - void setResult(SatValue val) { d_result = val; } - - // External World helping us help the Strategies - - /** - * Notify this class that assertion is an (input) assertion, not corresponding - * to a skolem definition. - */ - void addAssertion(TNode assertion, bool isLemma) override; - /** - * Notify this class that lem is the skolem definition for skolem, which is - * a part of the current assertions. - */ - void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override; - - // Interface for Strategies to use stuff stored in Decision Engine - // (which was possibly requested by them on initialization) - - // Interface for Strategies to get information about External World - - bool hasSatLiteral(TNode n) { return d_cnfStream->hasLiteral(n); } - SatLiteral getSatLiteral(TNode n) { return d_cnfStream->getLiteral(n); } - SatValue getSatValue(SatLiteral l) { return d_satSolver->value(l); } - SatValue getSatValue(TNode n) { return getSatValue(getSatLiteral(n)); } - Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } - - private: - // Disable creating decision engine without required parameters - DecisionEngineOld(); - - // Does decision engine know the answer? - context::CDO d_result; - - // init/shutdown state - unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown - /** The ITE decision strategy we have allocated */ - std::unique_ptr d_enabledITEStrategy; - /** Whether we are using stop only */ - bool d_decisionStopOnly; - -}; /* DecisionEngineOld class */ - -} // namespace cvc5 - -#endif /* CVC5__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h deleted file mode 100644 index e8f7683fd..000000000 --- a/src/decision/decision_strategy.h +++ /dev/null @@ -1,71 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Andrew Reynolds, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Decision strategy. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__DECISION__DECISION_STRATEGY_H -#define CVC5__DECISION__DECISION_STRATEGY_H - -#include - -#include "expr/node.h" -#include "prop/sat_solver_types.h" -#include "smt/env_obj.h" -#include "smt/term_formula_removal.h" - -namespace cvc5 { - -class DecisionEngineOld; - -namespace decision { - -class DecisionStrategy : protected EnvObj -{ - public: - DecisionStrategy(Env& env, DecisionEngineOld* de) - : EnvObj(env), d_decisionEngine(de) - { - } - - virtual ~DecisionStrategy() { } - - virtual prop::SatLiteral getNext(bool&) = 0; - - protected: - DecisionEngineOld* d_decisionEngine; -};/* class DecisionStrategy */ - -class ITEDecisionStrategy : public DecisionStrategy { -public: - ITEDecisionStrategy(Env& env, DecisionEngineOld* de) - : DecisionStrategy(env, de) - { - } - /** - * Add that assertion is an (input) assertion, not corresponding to a - * skolem definition. - */ - virtual void addAssertion(TNode assertion) = 0; - /** - * Add that lem is the skolem definition for skolem, which is a part of - * the current assertions. - */ - virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0; -};/* class ITEDecisionStrategy */ - -} // namespace decision -} // namespace cvc5 - -#endif /* CVC5__DECISION__DECISION_STRATEGY_H */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp deleted file mode 100644 index cadb107c3..000000000 --- a/src/decision/justification_heuristic.cpp +++ /dev/null @@ -1,743 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Andres Noetzli, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Justification heuristic for decision making - * - * A ATGP-inspired justification-based decision heuristic. This code is based - * on the CVC3 implementation of the same heuristic -- note below. - * - * It needs access to the simplified but non-clausal formula. - */ -#include "justification_heuristic.h" - -#include "decision/decision_attributes.h" -#include "decision/decision_engine_old.h" -#include "expr/kind.h" -#include "expr/node_manager.h" -#include "options/decision_options.h" -#include "smt/smt_statistics_registry.h" -#include "smt/term_formula_removal.h" -#include "theory/rewriter.h" -#include "util/random.h" - -using namespace cvc5::prop; - -namespace cvc5 { -namespace decision { - -JustificationHeuristic::JustificationHeuristic(Env& env, DecisionEngineOld* de) - : ITEDecisionStrategy(env, de), - d_justified(context()), - d_exploredThreshold(context()), - d_prvsIndex(context(), 0), - d_threshPrvsIndex(context(), 0), - d_helpfulness( - smtStatisticsRegistry().registerInt("decision::jh::helpfulness")), - d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")), - d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")), - d_assertions(userContext()), - d_skolemAssertions(userContext()), - d_skolemCache(userContext()), - d_visited(), - d_visitedComputeSkolems(), - d_curDecision(), - d_curThreshold(0), - d_childCache(userContext()), - d_weightCache(userContext()), - d_startIndexCache(context()) -{ - Trace("decision") << "Justification heuristic enabled" << std::endl; -} - -JustificationHeuristic::~JustificationHeuristic() {} - -cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) -{ - if (options().decision.decisionThreshold > 0) - { - bool stopSearchTmp = false; - prop::SatLiteral lit = - getNextThresh(stopSearchTmp, options().decision.decisionThreshold); - if (lit != prop::undefSatLiteral) - { - Assert(stopSearchTmp == false); - return lit; - } - Assert(stopSearchTmp == true); - } - return getNextThresh(stopSearch, 0); -} - -cvc5::prop::SatLiteral JustificationHeuristic::getNextThresh( - bool& stopSearch, DecisionWeight threshold) -{ - Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<hasSatLiteral(n) - ? d_decisionEngine->getSatLiteral(n) - : -1; - prop::SatValue v = tryGetSatValue(n); - Trace("justified") <<"{ "<setResult(prop::SAT_VALUE_TRUE); - return prop::undefSatLiteral; -} - -inline void computeXorIffDesiredValues(Kind k, - prop::SatValue desiredVal, - prop::SatValue& desiredVal1, - prop::SatValue& desiredVal2) -{ - Assert(k == kind::EQUAL || k == kind::XOR); - - bool shouldInvert = - (desiredVal == prop::SAT_VALUE_TRUE && k == kind::EQUAL) - || (desiredVal == prop::SAT_VALUE_FALSE && k == kind::XOR); - - if (desiredVal1 == prop::SAT_VALUE_UNKNOWN - && desiredVal2 == prop::SAT_VALUE_UNKNOWN) - { - // CHOICE: pick one of them arbitarily - desiredVal1 = prop::SAT_VALUE_FALSE; - } - - if(desiredVal2 == SAT_VALUE_UNKNOWN) { - desiredVal2 = shouldInvert ? invertValue(desiredVal1) : desiredVal1; - } else if(desiredVal1 == SAT_VALUE_UNKNOWN) { - desiredVal1 = shouldInvert ? invertValue(desiredVal2) : desiredVal2; - } -} - -void JustificationHeuristic::addAssertion(TNode assertion) -{ - // Save all assertions locally, including the assertions generated by term - // removal. We have to make sure that we assign a value to all the Boolean - // term variables. To illustrate why this is, consider the case where we have - // a single assertion - // - // (or (f a) (f b)) - // - // where `f` is a function `Bool -> Bool`. Given an assignment: - // - // (f a) -> true - // (f b) -> false - // a -> false - // - // UF will not complain and the justification heuristic considers the - // assertion to be satisifed. However, we also have to make sure that we pick - // a value for `b` that is not in conflict with the other assignments (we can - // only choose `b` to be `true` otherwise the model is incorrect). - d_assertions.push_back(assertion); -} - -void JustificationHeuristic::addSkolemDefinition(TNode lem, TNode skolem) -{ - Trace("decision::jh::ite") - << " jh-ite: " << skolem << " maps to " << lem << std::endl; - d_skolemAssertions[skolem] = lem; -} - -SatLiteral JustificationHeuristic::findSplitter(TNode node, - SatValue desiredVal) -{ - d_curDecision = undefSatLiteral; - findSplitterRec(node, desiredVal); - return d_curDecision; -} - - -void JustificationHeuristic::setJustified(TNode n) -{ - d_justified.insert(n); -} - -bool JustificationHeuristic::checkJustified(TNode n) -{ - return d_justified.find(n) != d_justified.end(); -} - -DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n) -{ - return d_exploredThreshold.find(n) == d_exploredThreshold.end() - ? std::numeric_limits::max() - : d_exploredThreshold[n]; -} - -void JustificationHeuristic::setExploredThreshold(TNode n) -{ - d_exploredThreshold[n] = d_curThreshold; -} - -int JustificationHeuristic::getPrvsIndex() -{ - if(d_curThreshold == 0) - return d_prvsIndex; - else - return d_threshPrvsIndex; -} - -void JustificationHeuristic::setPrvsIndex(int prvsIndex) -{ - if(d_curThreshold == 0) - d_prvsIndex = prvsIndex; - else - d_threshPrvsIndex = prvsIndex; -} - -DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satValue) -{ - Assert(satValue == SAT_VALUE_TRUE || satValue == SAT_VALUE_FALSE); - return getWeightPolarized(n, satValue == SAT_VALUE_TRUE); -} - -DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity) -{ - if (options().decision.decisionWeightInternal - != options::DecisionWeightInternal::USR1) - { - return getWeight(n); - } - - if(d_weightCache.find(n) == d_weightCache.end()) { - Kind k = n.getKind(); - theory::TheoryId tId = theory::kindToTheoryId(k); - DecisionWeight dW1, dW2; - if(tId != theory::THEORY_BOOL) { - dW1 = dW2 = getWeight(n); - } else { - - if(k == kind::OR) { - dW1 = std::numeric_limits::max(), dW2 = 0; - for(TNode::iterator i=n.begin(); i != n.end(); ++i) { - dW1 = std::min(dW1, getWeightPolarized(*i, true)); - dW2 = std::max(dW2, getWeightPolarized(*i, false)); - } - } else if(k == kind::AND) { - dW1 = 0, dW2 = std::numeric_limits::max(); - for(TNode::iterator i=n.begin(); i != n.end(); ++i) { - dW1 = std::max(dW1, getWeightPolarized(*i, true)); - dW2 = std::min(dW2, getWeightPolarized(*i, false)); - } - } else if(k == kind::IMPLIES) { - dW1 = std::min(getWeightPolarized(n[0], false), - getWeightPolarized(n[1], true)); - dW2 = std::max(getWeightPolarized(n[0], true), - getWeightPolarized(n[1], false)); - } else if(k == kind::NOT) { - dW1 = getWeightPolarized(n[0], false); - dW2 = getWeightPolarized(n[0], true); - } else { - dW1 = 0; - for(TNode::iterator i=n.begin(); i != n.end(); ++i) { - dW1 = std::max(dW1, getWeightPolarized(*i, true)); - dW1 = std::max(dW1, getWeightPolarized(*i, false)); - } - dW2 = dW1; - } - - } - d_weightCache[n] = std::make_pair(dW1, dW2); - } - return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second; -} - -DecisionWeight JustificationHeuristic::getWeight(TNode n) { - if(!n.hasAttribute(DecisionWeightAttr()) ) { - options::DecisionWeightInternal combiningFn = - options().decision.decisionWeightInternal; - - if (combiningFn == options::DecisionWeightInternal::OFF - || n.getNumChildren() == 0) - { - if (options().decision.decisionRandomWeight != 0) - { - n.setAttribute(DecisionWeightAttr(), - Random::getRandom().pick( - 0, options().decision.decisionRandomWeight - 1)); - } - } - else if (combiningFn == options::DecisionWeightInternal::MAX) - { - DecisionWeight dW = 0; - for (TNode::iterator i = n.begin(); i != n.end(); ++i) - dW = std::max(dW, getWeight(*i)); - n.setAttribute(DecisionWeightAttr(), dW); - } - else if (combiningFn == options::DecisionWeightInternal::SUM - || combiningFn == options::DecisionWeightInternal::USR1) - { - DecisionWeight dW = 0; - for (TNode::iterator i = n.begin(); i != n.end(); ++i) - dW = std::max(dW, getWeight(*i)); - n.setAttribute(DecisionWeightAttr(), dW); - } - else - { - Unreachable(); - } - } - return n.getAttribute(DecisionWeightAttr()); -} - -typedef std::vector ChildList; -TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) { - if (options().decision.decisionUseWeight) - { - // TODO: Optimize storing & access - if(d_childCache.find(n) == d_childCache.end()) { - ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end()); - std::sort(list0.begin(), list0.end(), JustificationHeuristic::myCompareClass(this,false)); - std::sort(list1.begin(), list1.end(), JustificationHeuristic::myCompareClass(this,true)); - d_childCache[n] = make_pair(list0, list1); - } - return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i]; - } - else - { - return n[i]; - } -} - -SatValue JustificationHeuristic::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 -} - -JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n) -{ - SkolemCache::iterator it = d_skolemCache.find(n); - if (it != d_skolemCache.end()) - { - return (*it).second; - } - else - { - // Compute the list of Skolems - // TODO: optimize by avoiding multiple lookup for d_skolemCache[n] - d_visitedComputeSkolems.clear(); - SkolemList ilist; - computeSkolems(n, ilist); - d_skolemCache.insert(n, ilist); - return ilist; - } -} - -void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l) -{ - Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n"; - d_visitedComputeSkolems.insert(n); - for(unsigned i=0; ihasSatLiteral(node); - if(Debug.isOn("decision")) { - if(!litPresent) { - Debug("decision") << "no sat literal for this node" << std::endl; - } - } -#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 */ - // See bug 374 - // 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); - bool isAtom = - (k == kind::BOOLEAN_TERM_VARIABLE ) || - ( (tId != theory::THEORY_BOOL) && - (k != kind::EQUAL || (!node[0].getType().isBoolean())) ); - - /* Some debugging stuff */ - Debug("decision::jh") << "kind = " << k << std::endl - << "theoryId = " << tId << std::endl - << "node = " << node << std::endl - << "litVal = " << litVal << std::endl; - - /** - * If not in theory of booleans, check if this is something to split-on. - */ - if(isAtom) { - // if node has embedded skolems due to term removal, resolve that first - if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER; - - if(litVal != SAT_VALUE_UNKNOWN) { - Assert(litVal == desiredVal); - setJustified(node); - return NO_SPLITTER; - } - else { - Assert(d_decisionEngine->hasSatLiteral(node)); - if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold) - return DONT_KNOW; - SatVariable v = - d_decisionEngine->getSatLiteral(node).getSatVariable(); - d_curDecision = SatLiteral(v, /* negated = */ desiredVal != SAT_VALUE_TRUE ); - Trace("decision-node") << "[decision-node] requesting split on " << d_curDecision - << ", node: " << node - << ", polarity: " << (desiredVal == SAT_VALUE_TRUE ? "true" : "false") << std::endl; - return FOUND_SPLITTER; - } - } - - SearchResult ret = NO_SPLITTER; - switch (k) { - - case kind::CONST_BOOLEAN: - Assert(node.getConst() == false || desiredVal == SAT_VALUE_TRUE); - Assert(node.getConst() == true || desiredVal == SAT_VALUE_FALSE); - break; - - case kind::AND: - if (desiredVal == SAT_VALUE_FALSE) - ret = handleAndOrEasy(node, desiredVal); - else - ret = handleAndOrHard(node, desiredVal); - break; - - case kind::OR: - if (desiredVal == SAT_VALUE_FALSE) - ret = handleAndOrHard(node, desiredVal); - else - ret = handleAndOrEasy(node, desiredVal); - break; - - case kind::IMPLIES: - if (desiredVal == SAT_VALUE_FALSE) - ret = handleBinaryHard(node[0], SAT_VALUE_TRUE, - node[1], SAT_VALUE_FALSE); - - else - ret = handleBinaryEasy(node[0], SAT_VALUE_FALSE, - node[1], SAT_VALUE_TRUE); - break; - - case kind::XOR: - case kind::EQUAL: { - SatValue desiredVal1 = tryGetSatValue(node[0]); - SatValue desiredVal2 = tryGetSatValue(node[1]); - computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2); - ret = handleBinaryHard(node[0], desiredVal1, - node[1], desiredVal2); - break; - } - - case kind::ITE: - ret = handleITE(node, desiredVal); - break; - - default: Assert(false) << "Unexpected Boolean operator"; break; - }//end of switch(k) - - if(ret == DONT_KNOW) { - setExploredThreshold(node); - } - - if(ret == NO_SPLITTER) { - Assert(litPresent == false || litVal == desiredVal) - << "Output should be justified"; - setJustified(node); - } - return ret; -}/* findRecSplit method */ - -JustificationHeuristic::SearchResult -JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) -{ - Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) - or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE)); - - int numChildren = node.getNumChildren(); - SatValue desiredValInverted = invertValue(desiredVal); - for(int i = 0; i < numChildren; ++i) { - TNode curNode = getChildByWeight(node, i, desiredVal); - if ( tryGetSatValue(curNode) != desiredValInverted ) { - SearchResult ret = findSplitterRec(curNode, desiredVal); - if(ret != DONT_KNOW) { - return ret; - } - } - } - Assert(d_curThreshold != 0) << "handleAndOrEasy: No controlling input found"; - return DONT_KNOW; -} - -int JustificationHeuristic::getStartIndex(TNode node) { - return d_startIndexCache[node]; -} -void JustificationHeuristic::saveStartIndex(TNode node, int val) { - d_startIndexCache[node] = val; -} - -JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node, - SatValue desiredVal) { - Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) - or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE)); - - int numChildren = node.getNumChildren(); - bool noSplitter = true; - int i_st = getStartIndex(node); - for(int i = i_st; i < numChildren; ++i) { - TNode curNode = getChildByWeight(node, i, desiredVal); - SearchResult ret = findSplitterRec(curNode, desiredVal); - if (ret == FOUND_SPLITTER) { - if(i != i_st) saveStartIndex(node, i); - return FOUND_SPLITTER; - } - noSplitter = noSplitter && (ret == NO_SPLITTER); - } - return noSplitter ? NO_SPLITTER : DONT_KNOW; -} - -JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TNode node1, - SatValue desiredVal1, - TNode node2, - SatValue desiredVal2) -{ - if (options().decision.decisionUseWeight - && getWeightPolarized(node1, desiredVal1) - > getWeightPolarized(node2, desiredVal2)) - { - std::swap(node1, node2); - std::swap(desiredVal1, desiredVal2); - } - - if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) { - SearchResult ret = findSplitterRec(node1, desiredVal1); - if(ret != DONT_KNOW) - return ret; - } - if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) { - SearchResult ret = findSplitterRec(node2, desiredVal2); - if(ret != DONT_KNOW) - return ret; - } - Assert(d_curThreshold != 0) << "handleBinaryEasy: No controlling input found"; - return DONT_KNOW; -} - -JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TNode node1, - SatValue desiredVal1, - TNode node2, - SatValue desiredVal2) -{ - if (options().decision.decisionUseWeight - && getWeightPolarized(node1, desiredVal1) - > getWeightPolarized(node2, desiredVal2)) - { - std::swap(node1, node2); - std::swap(desiredVal1, desiredVal2); - } - - bool noSplitter = true; - SearchResult ret; - - ret = findSplitterRec(node1, desiredVal1); - if (ret == FOUND_SPLITTER) - return FOUND_SPLITTER; - noSplitter &= (ret == NO_SPLITTER); - - ret = findSplitterRec(node2, desiredVal2); - if (ret == FOUND_SPLITTER) - return FOUND_SPLITTER; - noSplitter &= (ret == NO_SPLITTER); - - return noSplitter ? NO_SPLITTER : DONT_KNOW; -} - -JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) -{ - Debug("decision::jh") << " handleITE (" << node << ", " - << desiredVal << std::endl; - - //[0]: if, [1]: then, [2]: else - SatValue ifVal = tryGetSatValue(node[0]); - if (ifVal == SAT_VALUE_UNKNOWN) { - SatValue trueChildVal = tryGetSatValue(node[1]); - SatValue falseChildVal = tryGetSatValue(node[2]); - SatValue ifDesiredVal; - - if(trueChildVal == desiredVal || falseChildVal == invertValue(desiredVal)) { - ifDesiredVal = SAT_VALUE_TRUE; - } - else if (trueChildVal == invertValue(desiredVal) - || falseChildVal == desiredVal - || (options().decision.decisionUseWeight - && getWeightPolarized(node[1], true) - > getWeightPolarized(node[2], false))) - { - ifDesiredVal = SAT_VALUE_FALSE; - } - else - { - ifDesiredVal = SAT_VALUE_TRUE; - } - - if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER) - return FOUND_SPLITTER; - - Assert(d_curThreshold != 0) << "No controlling input found (6)"; - return DONT_KNOW; - } else { - // Try to justify 'if' - if(findSplitterRec(node[0], ifVal) == FOUND_SPLITTER) - return FOUND_SPLITTER; - - // If that was successful, we need to go into only one of 'then' - // or 'else' - int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; - - if( findSplitterRec(node[ch], desiredVal) == FOUND_SPLITTER ) { - return FOUND_SPLITTER; - } - - return NO_SPLITTER; - }// else (...ifVal...) -} - -JustificationHeuristic::SearchResult -JustificationHeuristic::handleEmbeddedSkolems(TNode node) -{ - const SkolemList l = getSkolems(node); - Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl; - - bool noSplitter = true; - for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i) - { - if(d_visited.find((*i).first) == d_visited.end()) { - d_visited.insert((*i).first); - SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE); - if (ret == FOUND_SPLITTER) - return FOUND_SPLITTER; - noSplitter = noSplitter && (ret == NO_SPLITTER); - d_visited.erase((*i).first); - } - } - return noSplitter ? NO_SPLITTER : DONT_KNOW; -} - -} /* namespace decision */ -} // namespace cvc5 diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h deleted file mode 100644 index fbba2e33a..000000000 --- a/src/decision/justification_heuristic.h +++ /dev/null @@ -1,194 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Gereon Kremer, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * 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. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__DECISION__JUSTIFICATION_HEURISTIC -#define CVC5__DECISION__JUSTIFICATION_HEURISTIC - -#include -#include - -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/cdo.h" -#include "decision/decision_strategy.h" -#include "expr/node.h" -#include "options/decision_weight.h" -#include "prop/sat_solver_types.h" -#include "util/statistics_stats.h" - -namespace cvc5 { -namespace decision { - -class JustificationHeuristic : public ITEDecisionStrategy { - // TRUE FALSE MEH - enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW}; - - typedef std::vector > SkolemList; - typedef context::CDHashMap SkolemCache; - typedef std::vector ChildList; - typedef context::CDHashMap> ChildCache; - typedef context::CDHashMap SkolemMap; - typedef context::CDHashMap> - WeightCache; - - // being 'justified' is monotonic with respect to decisions - typedef context::CDHashSet JustifiedSet; - JustifiedSet d_justified; - typedef context::CDHashMap ExploredThreshold; - ExploredThreshold d_exploredThreshold; - context::CDO d_prvsIndex; - context::CDO d_threshPrvsIndex; - - IntStat d_helpfulness; - IntStat d_giveup; - TimerStat d_timestat; - - /** - * A copy of the assertions that need to be justified - * directly. Doesn't have ones introduced during during term removal. - */ - context::CDList d_assertions; - - /** map from skolems introduced in term removal to the corresponding assertion - */ - SkolemMap d_skolemAssertions; - - /** Cache for skolems present in a atomic formula */ - SkolemCache d_skolemCache; - - /** - * This is used to prevent infinite loop when trying to find a - * splitter. Can happen when exploring assertion corresponding to a - * term-ITE. - */ - std::unordered_set d_visited; - - /** - * Set to track visited nodes in a dfs search done in computeSkolems - * function - */ - std::unordered_set d_visitedComputeSkolems; - - /** current decision for the recursive call */ - prop::SatLiteral d_curDecision; - /** current threshold for the recursive call */ - DecisionWeight d_curThreshold; - - /** child cache */ - ChildCache d_childCache; - - /** computed polarized weight cache */ - WeightCache d_weightCache; - - - class myCompareClass { - JustificationHeuristic* d_jh; - bool d_b; - public: - myCompareClass(JustificationHeuristic* jh, bool b):d_jh(jh),d_b(b) {}; - bool operator() (TNode n1, TNode n2) { - return d_jh->getWeightPolarized(n1, d_b) < d_jh->getWeightPolarized(n2, d_b); - } - }; - -public: - JustificationHeuristic(Env& env, DecisionEngineOld* de); - - ~JustificationHeuristic(); - - prop::SatLiteral getNext(bool& stopSearch) override; - - /** - * Notify this class that assertion is an (input) assertion, not corresponding - * to a skolem definition. - */ - void addAssertion(TNode assertion) override; - /** - * Notify this class that lem is the skolem definition for skolem, which is - * a part of the current assertions. - */ - void addSkolemDefinition(TNode lem, TNode skolem) override; - -private: - /* getNext with an option to specify threshold */ - prop::SatLiteral getNextThresh(bool& stopSearch, DecisionWeight threshold); - - prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal); - - /** - * Do all the hard work. - */ - SearchResult findSplitterRec(TNode node, prop::SatValue value); - - /* Helper functions */ - void setJustified(TNode); - bool checkJustified(TNode); - DecisionWeight getExploredThreshold(TNode); - void setExploredThreshold(TNode); - void setPrvsIndex(int); - int getPrvsIndex(); - DecisionWeight getWeightPolarized(TNode n, bool polarity); - DecisionWeight getWeightPolarized(TNode n, prop::SatValue); - DecisionWeight getWeight(TNode); - bool compareByWeightFalse(TNode, TNode); - bool compareByWeightTrue(TNode, TNode); - TNode getChildByWeight(TNode n, int i, bool polarity); - - /* If literal exists corresponding to the node return - that. Otherwise an UNKNOWN */ - prop::SatValue tryGetSatValue(Node n); - - /* Get list of all term-ITEs for the atomic formula v */ - JustificationHeuristic::SkolemList getSkolems(TNode n); - - /** - * For big and/or nodes, a cache to save starting index into children - * for efficiently. - */ - typedef context::CDHashMap StartIndexCache; - StartIndexCache d_startIndexCache; - int getStartIndex(TNode node); - void saveStartIndex(TNode node, int val); - - /* Compute all term-removal skolems in a node recursively */ - void computeSkolems(TNode n, SkolemList& l); - - SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal); - SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal); - SearchResult handleBinaryEasy(TNode node1, - prop::SatValue desiredVal1, - TNode node2, - prop::SatValue desiredVal2); - SearchResult handleBinaryHard(TNode node1, - prop::SatValue desiredVal1, - TNode node2, - prop::SatValue desiredVal2); - SearchResult handleITE(TNode node, prop::SatValue desiredVal); - SearchResult handleEmbeddedSkolems(TNode node); -};/* class JustificationHeuristic */ - -}/* namespace decision */ -} // namespace cvc5 - -#endif /* CVC5__DECISION__JUSTIFICATION_HEURISTIC */ diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index 552225755..7a86b03c5 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -19,55 +19,6 @@ name = "Decision Heuristics" [[option.mode.STOPONLY]] name = "stoponly" help = "Use the justification heuristic only to stop early, not for decisions." -[[option.mode.JUSTIFICATION_OLD]] - name = "justification-old" - help = "Older implementation of an ATGP-inspired justification heuristic." -[[option.mode.STOPONLY_OLD]] - name = "stoponly-old" - help = "Use the old implementation of justification heuristic only to stop early, not for decisions." - -[[option]] - name = "decisionThreshold" - category = "expert" - long = "decision-threshold=N" - type = "cvc5::decision::DecisionWeight" - default = "0" - includes = ["options/decision_weight.h"] - help = "ignore all nodes greater than threshold in first attempt to pick decision" - -[[option]] - name = "decisionUseWeight" - category = "expert" - long = "decision-use-weight" - type = "bool" - default = "false" - help = "use the weight nodes (locally, by looking at children) to direct recursive search" - - -[[option]] - name = "decisionRandomWeight" - category = "expert" - long = "decision-random-weight=N" - type = "int64_t" - default = "0" - help = "assign random weights to nodes between 0 and N-1 (0: disable)" - -[[option]] - name = "decisionWeightInternal" - category = "expert" - long = "decision-weight-internal=HOW" - type = "DecisionWeightInternal" - default = "OFF" - help = "compute weights of internal nodes using children: off, max, sum, usr1" - help_mode = "Decision weight internal mode." -[[option.mode.OFF]] - name = "off" -[[option.mode.MAX]] - name = "max" -[[option.mode.SUM]] - name = "sum" -[[option.mode.USR1]] - name = "usr1" [[option]] name = "jhSkolemMode" diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h deleted file mode 100644 index 2e2f8db0c..000000000 --- a/src/options/decision_weight.h +++ /dev/null @@ -1,29 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner, Kshitij Bansal - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Rewriter attributes. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__OPTIONS__DECISION_WEIGHT_H -#define CVC5__OPTIONS__DECISION_WEIGHT_H - -namespace cvc5 { -namespace decision { - -typedef uint64_t DecisionWeight; - -} // namespace decision -} // namespace cvc5 - -#endif /* CVC5__OPTIONS__DECISION_WEIGHT_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 734da0b76..4fe7da695 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -21,7 +21,6 @@ #include "base/check.h" #include "base/output.h" -#include "decision/decision_engine_old.h" #include "decision/justification_strategy.h" #include "options/base_options.h" #include "options/decision_options.h" @@ -88,11 +87,6 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te) { d_decisionEngine.reset(new decision::JustificationStrategy(env)); } - else if (dmode == options::DecisionMode::JUSTIFICATION_OLD - || dmode == options::DecisionMode::STOPONLY_OLD) - { - d_decisionEngine.reset(new DecisionEngineOld(env)); - } else { d_decisionEngine.reset(new decision::DecisionEngineEmpty(env)); diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 0155eecb2..6295f7e5e 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --decision=justification-old --uf-lazy-ll -q +; COMMAND-LINE: --finite-model-find --decision=justification --uf-lazy-ll -q ; EXPECT: sat (set-logic HO_ALL) -- 2.30.2