diff options
Diffstat (limited to 'src/decision/assertion_list.h')
-rw-r--r-- | src/decision/assertion_list.h | 108 |
1 files changed, 108 insertions, 0 deletions
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 */ |