diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/decision/assertion_list.cpp | 136 | ||||
| -rw-r--r-- | src/decision/assertion_list.h | 108 |
3 files changed, 246 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c03c2d591..e59832896 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -19,6 +19,8 @@ libcvc5_add_sources( api/cpp/cvc5.h api/cpp/cvc5_checks.h 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 diff --git a/src/decision/assertion_list.cpp b/src/decision/assertion_list.cpp new file mode 100644 index 000000000..098378d22 --- /dev/null +++ b/src/decision/assertion_list.cpp @@ -0,0 +1,136 @@ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Implementation of assertion list + */ + +#include "decision/assertion_list.h" + +namespace cvc5 { +namespace decision { + +const char* toString(DecisionStatus s) +{ + switch (s) + { + case DecisionStatus::INACTIVE: return "INACTIVE"; + case DecisionStatus::NO_DECISION: return "NO_DECISION"; + case DecisionStatus::DECISION: return "DECISION"; + case DecisionStatus::BACKTRACK: return "BACKTRACK"; + default: return "?"; + } +} + +std::ostream& operator<<(std::ostream& out, DecisionStatus s) +{ + out << toString(s); + return out; +} + +AssertionList::AssertionList(context::Context* ac, + context::Context* ic, + bool useDyn) + : d_assertions(ac), + d_assertionIndex(ic), + d_usingDynamic(useDyn), + d_dindex(ic) +{ +} + +void AssertionList::presolve() +{ + Trace("jh-status") << "AssertionList::presolve" << std::endl; + d_assertionIndex = 0; + d_dlist.clear(); + d_dindex = 0; +} + +void AssertionList::addAssertion(TNode n) { d_assertions.push_back(n); } + +TNode AssertionList::getNextAssertion() +{ + size_t fromIndex; + if (d_usingDynamic) + { + // is a dynamic assertion ready? + fromIndex = d_dindex.get(); + if (fromIndex < d_dlist.size()) + { + d_dindex = d_dindex.get() + 1; + Trace("jh-status") << "Assertion " << d_dlist[fromIndex].getId() + << " from dynamic list" << std::endl; + return d_dlist[fromIndex]; + } + } + // check if dynamic assertions + fromIndex = d_assertionIndex.get(); + Assert(fromIndex <= d_assertions.size()); + if (fromIndex == d_assertions.size()) + { + return Node::null(); + } + // increment for the next iteration + d_assertionIndex = d_assertionIndex + 1; + Trace("jh-status") << "Assertion " << d_assertions[fromIndex].getId() + << std::endl; + return d_assertions[fromIndex]; +} +size_t AssertionList::size() const { return d_assertions.size(); } + +void AssertionList::notifyStatus(TNode n, DecisionStatus s) +{ + Trace("jh-status") << "Assertion status " << s << " for " << n.getId() + << ", current " << d_dindex.get() << "/" << d_dlist.size() + << std::endl; + if (!d_usingDynamic) + { + // not using dynamic ordering, return + return; + } + if (s == DecisionStatus::NO_DECISION) + { + // no decision does not impact the decision order + return; + } + std::unordered_set<TNode, TNodeHashFunction>::iterator it = + d_dlistSet.find(n); + if (s == DecisionStatus::DECISION) + { + if (it == d_dlistSet.end()) + { + // if we just had a status on an assertion and it didn't occur in dlist, + // then our index should have exhausted dlist + Assert(d_dindex.get() == d_dlist.size()); + if (d_dindex.get() == d_dlist.size()) + { + d_dindex = d_dindex.get() + 1; + } + // add to back of the decision list if not already there + d_dlist.push_back(n); + d_dlistSet.insert(n); + Trace("jh-status") << "...push due to decision" << std::endl; + } + return; + } + if (s == DecisionStatus::BACKTRACK) + { + // backtrack inserts at the current position + if (it == d_dlistSet.end()) + { + d_dlist.insert(d_dlist.begin(), n); + d_dlistSet.insert(n); + } + } +} + +} // namespace decision +} // namespace cvc5 diff --git a/src/decision/assertion_list.h b/src/decision/assertion_list.h new file mode 100644 index 000000000..fdb4bb2d5 --- /dev/null +++ b/src/decision/assertion_list.h @@ -0,0 +1,108 @@ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Assertion list + */ + +#include "cvc5_private.h" + +#ifndef CVC5__DECISION__ASSERTION_LIST_H +#define CVC5__DECISION__ASSERTION_LIST_H + +#include <iosfwd> +#include <unordered_set> +#include <vector> + +#include "context/cdlist.h" +#include "context/cdo.h" +#include "expr/node.h" + +namespace cvc5 { +namespace decision { + +/** + * For monitoring activity of assertions + */ +enum class DecisionStatus +{ + // not currently watching status of the current assertion + INACTIVE, + // no decision was made considering the assertion + NO_DECISION, + // a decision was made considering the assertion + DECISION, + // we backtracked while considering the assertion + BACKTRACK +}; +const char* toString(DecisionStatus s); +std::ostream& operator<<(std::ostream& out, DecisionStatus s); + +/** + * An assertion list used by the justification heuristic. This tracks a list + * of formulas that we must justify. + */ +class AssertionList +{ + public: + /** + * @param ac The context on which the assertions depends on. This is the + * user context for assertions. It is the SAT context for assertions that + * are dynamically relevant based on what is asserted, e.g. lemmas + * corresponding to skolem definitions. + * @param ic The context on which the current index of the assertions + * depends on. This is typically the SAT context. + * @param dyn Whether to use a dynamic ordering of the assertions. If this + * flag is true, then getNextAssertion will return the most important next + * assertion to consider based on heuristics in response to notifyStatus. + */ + AssertionList(context::Context* ac, + context::Context* ic, + bool useDyn = false); + virtual ~AssertionList() {} + /** Presolve, which clears the dynamic assertion order */ + void presolve(); + /** Add the assertion n */ + void addAssertion(TNode n); + /** + * Get the next assertion and increment d_assertionIndex. + */ + TNode getNextAssertion(); + /** Get the number of assertions */ + size_t size() const; + /** + * Notify status, which indicates the status of the assertion n, where n + * is the assertion last returned by getNextAssertion above (independent of + * the context). The status s indicates what happened when we were trying to + * justify n. This impacts its order if useDyn is true. + */ + void notifyStatus(TNode n, DecisionStatus s); + + private: + /** The list of assertions */ + context::CDList<Node> d_assertions; + /** The index of the next assertion to satify */ + context::CDO<size_t> d_assertionIndex; + // --------------------------- dynamic assertions + /** are we using dynamic assertions? */ + bool d_usingDynamic; + /** The list of assertions */ + std::vector<TNode> d_dlist; + /** The set of assertions for fast membership testing in the above vector */ + std::unordered_set<TNode, TNodeHashFunction> d_dlistSet; + /** The index of the next assertion to satify */ + context::CDO<size_t> d_dindex; +}; + +} // namespace decision +} // namespace cvc5 + +#endif /* CVC5__DECISION__ASSERTION_LIST_H */ |