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
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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 */
projects / cvc5.git / commitdiff