This PR significantly improves the quality of values in get-difficulty. It fixes several bugs related to get-difficulty, including over-pruning values in ProofManager, and not tracking explanations for certain literals. It also improves performance by tracking justifications in relevance manager in a SAT-context dependent manner.
This is to support difficulty measurements based on lemmas sent at STANDARD effort.
It also adds 2 simple regressions.
A further PR will further improve the quality by being more careful about the relationships between literals and the assertions that entail that they are relevant.
std::map<Node, Node> dmapp = dmap;
dmap.clear();
std::vector<Node> ppAsserts;
- std::vector<Node> asserts;
- getAssertions(as, asserts);
for (const std::pair<const Node, Node>& ppa : dmapp)
{
Trace("difficulty") << " preprocess difficulty: " << ppa.second << " for "
<< ppa.first << std::endl;
- // Ensure that only input assertions are marked as having a difficulty.
- // In some cases, a lemma may be marked as having a difficulty
- // internally, e.g. for lemmas that require justification, which we should
- // skip or otherwise we end up with an open proof below.
- if (std::find(asserts.begin(), asserts.end(), ppa.first) != asserts.end())
- {
- ppAsserts.push_back(ppa.first);
- }
+ // The difficulty manager should only report difficulty for preprocessed
+ // assertions, or we will get an open proof below. This is ensured
+ // internally by the difficuly manager.
+ ppAsserts.push_back(ppa.first);
}
// assume a SAT refutation from all input assertions that were marked
// as having a difficulty
bool SetDefaults::safeUnsatCores(const Options& opts) const
{
// whether we want to force safe unsat cores, i.e., if we are in the default
- // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental
- return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS
- || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY;
+ // ASSUMPTIONS mode, since other ones are experimental
+ return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
}
bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
namespace theory {
DifficultyManager::DifficultyManager(context::Context* c, Valuation val)
- : d_val(val), d_dfmap(c)
+ : d_input(c), d_val(val), d_dfmap(c)
{
}
+void DifficultyManager::notifyInputAssertions(
+ const std::vector<Node>& assertions)
+{
+ for (const Node& a : assertions)
+ {
+ d_input.insert(a);
+ }
+}
+
void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap)
{
NodeManager* nm = NodeManager::currentNM();
}
}
-void DifficultyManager::notifyLemma(const std::map<TNode, TNode>& rse, Node n)
+void DifficultyManager::notifyLemma(const context::CDHashMap<Node, Node>& rse,
+ Node n)
{
if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL)
{
{
litsToCheck.push_back(n);
}
- std::map<TNode, TNode>::const_iterator it;
+ context::CDHashMap<Node, Node>::const_iterator it;
for (TNode nc : litsToCheck)
{
bool pol = nc.getKind() != kind::NOT;
Trace("diff-man-debug")
<< "Check literal: " << atom << ", has reason = " << (it != rse.end())
<< std::endl;
- if (it != rse.end())
+ // must be an input assertion
+ if (it != rse.end() && d_input.find(it->second) != d_input.end())
{
incrementDifficulty(it->second);
}
}
}
-void DifficultyManager::notifyCandidateModel(const NodeList& input,
- TheoryModel* m)
+void DifficultyManager::notifyCandidateModel(TheoryModel* m)
{
if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK)
{
return;
}
Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input="
- << input.size() << std::endl;
- for (const Node& a : input)
+ << d_input.size() << std::endl;
+ for (const Node& a : d_input)
{
// should have miniscoped the assertions upstream
Assert(a.getKind() != kind::AND);
#define CVC5__THEORY__DIFFICULTY_MANAGER__H
#include "context/cdhashmap.h"
-#include "context/cdlist.h"
+#include "context/cdhashset.h"
#include "expr/node.h"
#include "theory/valuation.h"
*/
class DifficultyManager
{
- typedef context::CDList<Node> NodeList;
+ typedef context::CDHashSet<Node> NodeSet;
typedef context::CDHashMap<Node, uint64_t> NodeUIntMap;
public:
DifficultyManager(context::Context* c, Valuation val);
+ /** Notify input assertions */
+ void notifyInputAssertions(const std::vector<Node>& assertions);
/**
* Get difficulty map, which populates dmap mapping preprocessed assertions
* to a difficulty measure (a constant integer).
* the reason why that literal was relevant in the current context
* @param lem The lemma
*/
- void notifyLemma(const std::map<TNode, TNode>& rse, Node lem);
+ void notifyLemma(const context::CDHashMap<Node, Node>& rse, Node lem);
/**
* Notify that `m` is a (candidate) model. This increments the difficulty
* of assertions that are not satisfied by that model.
*
- * @param input The list of preprocessed assertions
* @param m The candidate model.
*/
- void notifyCandidateModel(const NodeList& input, TheoryModel* m);
+ void notifyCandidateModel(TheoryModel* m);
private:
/** Increment difficulty on assertion a */
void incrementDifficulty(TNode a, uint64_t amount = 1);
+ /**
+ * The input assertions, tracked to ensure we do not increment difficulty
+ * on lemmas.
+ */
+ NodeSet d_input;
/** The valuation object, used to query current value of theory literals */
Valuation d_val;
/**
namespace cvc5 {
namespace theory {
-RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val)
- : d_val(val),
- d_input(lemContext),
- d_computed(false),
+RelevanceManager::RelevanceManager(Env& env, Valuation val)
+ : EnvObj(env),
+ d_val(val),
+ d_input(userContext()),
+ d_rset(context()),
+ d_inFullEffortCheck(false),
d_success(false),
d_trackRSetExp(false),
- d_miniscopeTopLevel(true)
+ d_miniscopeTopLevel(true),
+ d_rsetExp(context()),
+ d_jcache(context())
{
- if (options::produceDifficulty())
+ if (options().smt.produceDifficulty)
{
- d_dman.reset(new DifficultyManager(lemContext, val));
+ d_dman.reset(new DifficultyManager(userContext(), val));
d_trackRSetExp = true;
// we cannot miniscope AND at the top level, since we need to
// preserve the exact form of preprocessed assertions so the dependencies
}
void RelevanceManager::notifyPreprocessedAssertions(
- const std::vector<Node>& assertions)
+ const std::vector<Node>& assertions, bool isInput)
{
// add to input list, which is user-context dependent
std::vector<Node> toProcess;
}
}
addAssertionsInternal(toProcess);
+ // notify the difficulty manager if these are input assertions
+ if (isInput && d_dman != nullptr)
+ {
+ d_dman->notifyInputAssertions(assertions);
+ }
}
-void RelevanceManager::notifyPreprocessedAssertion(Node n)
+void RelevanceManager::notifyPreprocessedAssertion(Node n, bool isInput)
{
std::vector<Node> toProcess;
toProcess.push_back(n);
- addAssertionsInternal(toProcess);
+ notifyPreprocessedAssertions(toProcess, isInput);
}
void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
}
}
-void RelevanceManager::beginRound()
-{
- d_computed = false;
-}
+void RelevanceManager::beginRound() { d_inFullEffortCheck = true; }
+
+void RelevanceManager::endRound() { d_inFullEffortCheck = false; }
void RelevanceManager::computeRelevance()
{
- d_computed = true;
- d_rset.clear();
- d_rsetExp.clear();
- Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
- std::unordered_map<TNode, int> cache;
- d_success = true;
+ // if not at full effort, should be tracking something else, e.g. explanation
+ // for why literals are relevant.
+ Assert(d_inFullEffortCheck || d_trackRSetExp);
+ Trace("rel-manager") << "RelevanceManager::computeRelevance, full effort = "
+ << d_inFullEffortCheck << "..." << std::endl;
for (const Node& node: d_input)
{
TNode n = node;
- int val = justify(n, cache);
+ int val = justify(n);
if (val != 1)
{
- if (Trace.isOn("rel-manager"))
+ // if we are in full effort check and fail to justify, then we should
+ // give a failure and set success to false, or otherwise calls to
+ // isRelevant cannot be trusted.
+ if (d_inFullEffortCheck)
{
std::stringstream serr;
serr
<< "RelevanceManager::computeRelevance: WARNING: failed to justify "
<< n;
Trace("rel-manager") << serr.str() << std::endl;
+ Assert(false) << serr.str();
+ d_success = false;
+ return;
}
- d_success = false;
- // If we fail to justify an assertion, we set success to false and
- // continue to try to justify the remaining assertions. This is important
- // for cases where the difficulty manager is measuring based on lemmas
- // that are being sent at STANDARD effort, before all assertions are
- // satisfied.
}
}
- if (!d_success)
+ if (Trace.isOn("rel-manager"))
{
- d_rset.clear();
- return;
+ if (d_inFullEffortCheck)
+ {
+ Trace("rel-manager") << "...success (full), size = " << d_rset.size()
+ << std::endl;
+ }
+ else
+ {
+ Trace("rel-manager") << "...success, exp size = " << d_rsetExp.size()
+ << std::endl;
+ }
}
- Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl;
+ d_success = true;
}
bool RelevanceManager::isBooleanConnective(TNode cur)
|| (k == EQUAL && cur[0].getType().isBoolean());
}
-bool RelevanceManager::updateJustifyLastChild(
- TNode cur,
- std::vector<int>& childrenJustify,
- std::unordered_map<TNode, int>& cache)
+bool RelevanceManager::updateJustifyLastChild(TNode cur,
+ std::vector<int>& childrenJustify)
{
// This method is run when we are informed that child index of cur
// has justify status lastChildJustify. We return true if we would like to
Assert(isBooleanConnective(cur));
size_t index = childrenJustify.size();
Assert(index < nchildren);
- Assert(cache.find(cur[index]) != cache.end());
+ Assert(d_jcache.find(cur[index]) != d_jcache.end());
Kind k = cur.getKind();
// Lookup the last child's value in the overall cache, we may choose to
// add this to childrenJustify if we return true.
- int lastChildJustify = cache[cur[index]];
+ int lastChildJustify = d_jcache[cur[index]];
if (k == NOT)
{
- cache[cur] = -lastChildJustify;
+ d_jcache[cur] = -lastChildJustify;
}
else if (k == IMPLIES || k == AND || k == OR)
{
if (lastChildJustify
== ((k == AND || (k == IMPLIES && index == 0)) ? -1 : 1))
{
- cache[cur] = k == AND ? -1 : 1;
+ d_jcache[cur] = k == AND ? -1 : 1;
return false;
}
}
break;
}
}
- cache[cur] = ret;
+ d_jcache[cur] = ret;
}
else
{
else if (lastChildJustify == 0)
{
// all other cases, an unknown child implies we are unknown
- cache[cur] = 0;
+ d_jcache[cur] = 0;
}
else if (k == ITE)
{
// should be in proper branch
Assert(childrenJustify[0] == (index == 1 ? 1 : -1));
// we are the value of the branch
- cache[cur] = lastChildJustify;
+ d_jcache[cur] = lastChildJustify;
}
}
else
{
// both children known, compute value
Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0);
- cache[cur] =
+ d_jcache[cur] =
((k == XOR ? -1 : 1) * lastChildJustify == childrenJustify[0]) ? 1
: -1;
}
return false;
}
-int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache)
+int RelevanceManager::justify(TNode n)
{
+ // The set of nodes that we have computed currently have no value. Those
+ // that are marked as having no value in d_jcache must be recomputed, since
+ // the values for SAT literals may have changed.
+ std::unordered_set<Node> noJustify;
// the vector of values of children
std::unordered_map<TNode, std::vector<int>> childJustify;
- std::unordered_map<TNode, int>::iterator it;
+ NodeUIntMap::iterator it;
std::unordered_map<TNode, std::vector<int>>::iterator itc;
std::vector<TNode> visit;
TNode cur;
cur = visit.back();
// should always have Boolean type
Assert(cur.getType().isBoolean());
- it = cache.find(cur);
- if (it != cache.end())
+ it = d_jcache.find(cur);
+ if (it != d_jcache.end())
{
- visit.pop_back();
- // already computed value
- continue;
+ if (it->second != 0 || noJustify.find(cur) != noJustify.end())
+ {
+ visit.pop_back();
+ // already computed value
+ continue;
+ }
}
itc = childJustify.find(cur);
// have we traversed to children yet?
if (d_trackRSetExp)
{
d_rsetExp[cur] = n;
+ Trace("rel-manager-exp")
+ << "Reason for " << cur << " is " << n << std::endl;
}
}
- cache[cur] = ret;
+ d_jcache[cur] = ret;
+ if (ret == 0)
+ {
+ noJustify.insert(cur);
+ }
}
}
else
{
// this processes the impact of the current child on the value of cur,
// and possibly requests that a new child is computed.
- if (updateJustifyLastChild(cur, itc->second, cache))
+ if (updateJustifyLastChild(cur, itc->second))
{
Assert(itc->second.size() < cur.getNumChildren());
TNode nextChild = cur[itc->second.size()];
else
{
visit.pop_back();
+ Assert(d_jcache.find(cur) != d_jcache.end());
+ if (d_jcache[cur] == 0)
+ {
+ noJustify.insert(cur);
+ }
}
}
} while (!visit.empty());
- Assert(cache.find(n) != cache.end());
- return cache[n];
+ Assert(d_jcache.find(n) != d_jcache.end());
+ return d_jcache[n];
}
bool RelevanceManager::isRelevant(Node lit)
{
- if (!d_computed)
- {
- computeRelevance();
- }
+ Assert(d_inFullEffortCheck);
+ computeRelevance();
if (!d_success)
{
// always relevant if we failed to compute
return d_rset.find(lit) != d_rset.end();
}
-const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions(
- bool& success)
+std::unordered_set<TNode> RelevanceManager::getRelevantAssertions(bool& success)
{
- if (!d_computed)
- {
- computeRelevance();
- }
+ computeRelevance();
// update success flag
success = d_success;
- return d_rset;
+ std::unordered_set<TNode> rset;
+ if (success)
+ {
+ for (const Node& a : d_rset)
+ {
+ rset.insert(a);
+ }
+ }
+ return rset;
}
void RelevanceManager::notifyLemma(Node n)
{
- // only consider lemmas that were sent at full effort, when we have a
- // complete SAT assignment.
+ // notice that we may be in FULL or STANDARD effort here.
if (d_dman != nullptr)
{
// ensure we know which literals are relevant, and why
{
if (d_dman != nullptr)
{
- d_dman->notifyCandidateModel(d_input, m);
+ d_dman->notifyCandidateModel(m);
}
}
#include <unordered_map>
#include <unordered_set>
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/difficulty_manager.h"
#include "theory/valuation.h"
* selection is computed lazily, i.e. only when someone asks if a literal is
* relevant, and only at most once per FULL effort check.
*/
-class RelevanceManager
+class RelevanceManager : protected EnvObj
{
- typedef context::CDList<Node> NodeList;
+ using NodeList = context::CDList<Node>;
+ using NodeMap = context::CDHashMap<Node, Node>;
+ using NodeSet = context::CDHashSet<Node>;
+ using NodeUIntMap = context::CDHashMap<Node, uint64_t>;
public:
/**
- * @param lemContext The context which lemmas live at
+ * @param env The environment
* @param val The valuation class, for computing what is relevant.
*/
- RelevanceManager(context::Context* lemContext, Valuation val);
+ RelevanceManager(Env& env, Valuation val);
/**
* Notify (preprocessed) assertions. This is called for input formulas or
* lemmas that need justification that have been fully processed, just before
* adding them to the PropEngine.
+ *
+ * @param assertions The assertions
+ * @param isInput Whether the assertions are preprocessed input assertions;
+ * this flag is false for lemmas.
*/
- void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
+ void notifyPreprocessedAssertions(const std::vector<Node>& assertions,
+ bool isInput);
/** Singleton version of above */
- void notifyPreprocessedAssertion(Node n);
+ void notifyPreprocessedAssertion(Node n, bool isInput);
/**
- * Begin round, called at the beginning of a check in TheoryEngine.
+ * Begin round, called at the beginning of a full effort check in
+ * TheoryEngine.
*/
void beginRound();
+ /** End round, called at the end of a full effort check in TheoryEngine. */
+ void endRound();
/**
* Is lit part of the current relevant selection? This computes the set of
* relevant assertions if not already done so. This call is valid during a
* the assertions we are notified of. This should never happen.
*
* The value of this return is only valid if success was not updated to false.
+ *
+ * Note that this returns a context-independent set to the user, which
+ * copies the assertions.
*/
- const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
+ std::unordered_set<TNode> getRelevantAssertions(bool& success);
/** Notify lemma, for difficulty measurements */
void notifyLemma(Node n);
/** Notify that m is a (candidate) model, for difficulty measurements */
* This method returns 1 if we justified n to be true, -1 means
* justified n to be false, 0 means n could not be justified.
*/
- int justify(TNode n, std::unordered_map<TNode, int>& cache);
+ int justify(TNode n);
/** Is the top symbol of cur a Boolean connective? */
bool isBooleanConnective(TNode cur);
/**
* Update justify last child. This method is a helper function for justify,
* which is called at the moment that Boolean connective formula cur
- * has a new child that has been computed in the justify cache.
+ * has a new child that has been computed in the justify cache maintained
+ * by this class.
*
* @param cur The Boolean connective formula
* @param childrenJustify The values of the previous children (not including
* the current one)
- * @param cache The justify cache
* @return True if we wish to visit the next child. If this is the case, then
* the justify value of the current child is added to childrenJustify.
*/
- bool updateJustifyLastChild(TNode cur,
- std::vector<int>& childrenJustify,
- std::unordered_map<TNode, int>& cache);
+ bool updateJustifyLastChild(TNode cur, std::vector<int>& childrenJustify);
/** The valuation object, used to query current value of theory literals */
Valuation d_val;
/** The input assertions */
NodeList d_input;
- /** The current relevant selection. */
- std::unordered_set<TNode> d_rset;
- /** Have we computed the relevant selection this round? */
- bool d_computed;
+ /**
+ * The current relevant selection, SAT-context dependent, includes
+ * literals that are definitely relevant in this context.
+ */
+ NodeSet d_rset;
/** Are we in a full effort check? */
bool d_inFullEffortCheck;
/**
* assignment since this class found that the input formula was not satisfied
* by the assignment. This should never happen, but if it does, this class
* aborts and indicates that all literals are relevant.
+ *
+ * This flag is only valid at FULL effort.
*/
bool d_success;
/** Are we tracking the sources of why a literal is relevant */
* Map from the domain of d_rset to the assertion in d_input that is the
* reason why that literal is currently relevant.
*/
- std::map<TNode, TNode> d_rsetExp;
+ NodeMap d_rsetExp;
+ /**
+ * Set of nodes that we have justified (SAT context dependent). This is SAT
+ * context dependent to avoid repeated calls to justify for uses of
+ * the relevance manager at standard effort.
+ */
+ NodeUIntMap d_jcache;
/** Difficulty module */
std::unique_ptr<DifficultyManager> d_dman;
};
// create the relevance filter if any option requires it
if (options().theory.relevanceFilter || options().smt.produceDifficulty)
{
- d_relManager.reset(new RelevanceManager(userContext(), Valuation(this)));
+ d_relManager.reset(new RelevanceManager(d_env, Valuation(this)));
}
// initialize the quantifiers engine
Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
- // Reset round for the relevance manager, which notice only sets a flag
- // to indicate that its information must be recomputed.
- if (d_relManager != nullptr)
- {
- d_relManager->beginRound();
- }
// If in full effort, we have a fake new assertion just to jumpstart the checking
if (Theory::fullEffort(effort)) {
d_factsAsserted = true;
+ // Reset round for the relevance manager, which notice only sets a flag
+ // to indicate that its information must be recomputed.
+ if (d_relManager != nullptr)
+ {
+ d_relManager->beginRound();
+ }
d_tc->resetRound();
}
if (Theory::fullEffort(effort))
{
+ if (d_relManager != nullptr)
+ {
+ d_relManager->endRound();
+ }
if (!d_inConflict && !needCheck())
{
// Do post-processing of model from the theories (e.g. used for
}
if (d_relManager != nullptr)
{
- d_relManager->notifyPreprocessedAssertions(assertions);
+ d_relManager->notifyPreprocessedAssertions(assertions, true);
}
}
return d_sharedSolver->getEqualityStatus(a, b);
}
-const std::unordered_set<TNode>& TheoryEngine::getRelevantAssertions(
- bool& success)
+std::unordered_set<TNode> TheoryEngine::getRelevantAssertions(bool& success)
{
// if we are not in SAT mode, or there is no relevance manager, we fail
if (!d_inSatMode || d_relManager == nullptr)
{
success = false;
- return d_emptyRelevantSet;
+ // return empty set
+ return std::unordered_set<TNode>();
}
return d_relManager->getRelevantAssertions(success);
}
d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
if (options().theory.relevanceFilter && isLemmaPropertyNeedsJustify(p))
{
- d_relManager->notifyPreprocessedAssertion(retLemma);
- d_relManager->notifyPreprocessedAssertions(skAsserts);
+ d_relManager->notifyPreprocessedAssertion(retLemma, false);
+ d_relManager->notifyPreprocessedAssertions(skAsserts, false);
}
d_relManager->notifyLemma(retLemma);
}
* relevance manager failed to compute relevant assertions due to an internal
* error.
*/
- const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
+ std::unordered_set<TNode> getRelevantAssertions(bool& success);
/**
* Get difficulty map, which populates dmap, mapping preprocessed assertions
std::unique_ptr<theory::DecisionManager> d_decManager;
/** The relevance manager */
std::unique_ptr<theory::RelevanceManager> d_relManager;
- /**
- * An empty set of relevant assertions, which is returned as a dummy value for
- * getRelevantAssertions when relevance is disabled.
- */
- std::unordered_set<TNode> d_emptyRelevantSet;
/** are we in eager model building mode? (see setEagerModelBuilding). */
bool d_eager_model_building;
regress0/declare-fun-is-match.smt2
regress0/declare-funs.smt2
regress0/define-fun-model.smt2
+ regress0/difficulty-simple.smt2
+ regress0/difficulty-model-ex.smt2
regress0/distinct.smtv1.smt2
regress0/dump-unsat-core-full.smt2
regress0/echo.smt2
--- /dev/null
+; COMMAND-LINE: --produce-difficulty --difficulty-mode=model-check
+; SCRUBBER: sed 's/.*//g'
+; EXIT: 0
+
+(set-logic ALL)
+(set-option :produce-difficulty true)
+(declare-fun P (Int) Bool)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+
+(assert (= z 78))
+
+(assert (! (= (* x x) z) :named a1))
+
+(assert (= y 0))
+
+(assert (P y))
+
+(check-sat)
+
+(get-difficulty)
--- /dev/null
+; COMMAND-LINE: --produce-difficulty
+; SCRUBBER: sed 's/.*//g'
+; EXIT: 0
+
+(set-logic ALL)
+(set-option :produce-difficulty true)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+
+(assert (or (> a 0) (> b 0) (> c 0)))
+
+(assert (< (ite (> a b) a b) 0))
+
+(check-sat)
+(get-difficulty)
projects / cvc5.git / commitdiff