diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-01-25 14:38:45 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-25 14:38:45 -0600 |
commit | eaad5bdc7a38fcc38baa0e3b73f6c39a0ec6fb05 (patch) | |
tree | 42452e177fa8a24a523ce715aa3a40a99644ab17 /src/theory/bags/solver_state.h | |
parent | 7f851ea2e2b40f7e5d6e0c0fbe4e9c6ea0450209 (diff) |
Refactor bags::SolverState (#5783)
Couple of changes:
SolverState now keep tracks of elements per bag instead of per type.
bags::InferInfo now stores multiple conclusions (conjuncts).
BagSolver applies upward/downward closures for bag elements
Diffstat (limited to 'src/theory/bags/solver_state.h')
-rw-r--r-- | src/theory/bags/solver_state.h | 50 |
1 files changed, 39 insertions, 11 deletions
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 8d70ee8f7..175317529 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -31,24 +31,52 @@ class SolverState : public TheoryState public: SolverState(context::Context* c, context::UserContext* u, Valuation val); - void registerClass(TNode n); + /** + * This function adds the bag representative n to the set d_bags if it is not + * already there. This function is called during postCheck to collect bag + * terms in the equality engine. See the documentation of + * @link SolverState::collectBagsAndCountTerms + */ + void registerBag(TNode n); - Node registerBagElement(TNode n); - - std::set<Node>& getBags(); - - std::set<Node>& getElements(TypeNode t); - - std::map<Node, Node>& getBagElements(Node B); + /** + * @param n has the form (bag.count e A) + * @pre bag A needs is already registered using registerBag(A) + * @return a unique skolem for (bag.count e A) + */ + void registerCountTerm(TNode n); + /** get all bag terms that are representatives in the equality engine. + * This function is valid after the current solver is initialized during + * postCheck. See SolverState::initialize and BagSolver::postCheck + */ + const std::set<Node>& getBags(); + /** + * @pre B is a registered bag + * @return all elements associated with bag B so far + * Note that associated elements are not necessarily elements in B + * Example: + * (assert (= 0 (bag.count x B))) + * element x is associated with bag B, albeit x is definitely not in B. + */ + const std::set<Node>& getElements(Node B); + /** initialize bag and count terms */ + void initialize(); private: + /** clear all bags data structures */ + void reset(); + /** collect bags' representatives and all count terms. + * This function is called during postCheck */ + void collectBagsAndCountTerms(); /** constants */ Node d_true; Node d_false; + /** node manager for this solver state */ + NodeManager* d_nm; + /** collection of bag representatives */ std::set<Node> d_bags; - std::map<TypeNode, std::set<Node>> d_elements; - /** bag -> element -> multiplicity */ - std::map<Node, std::map<Node, Node>> d_count; + /** bag -> associated elements */ + std::map<Node, std::set<Node>> d_bagElements; }; /* class SolverState */ } // namespace bags |