1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mudathir Mohamed |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Bags state object. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H |
19 |
|
#define CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H |
20 |
|
|
21 |
|
#include <map> |
22 |
|
|
23 |
|
#include "theory/theory_state.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace bags { |
28 |
|
|
29 |
9838 |
class SolverState : public TheoryState |
30 |
|
{ |
31 |
|
public: |
32 |
|
SolverState(context::Context* c, context::UserContext* u, Valuation val); |
33 |
|
|
34 |
|
/** |
35 |
|
* This function adds the bag representative n to the set d_bags if it is not |
36 |
|
* already there. This function is called during postCheck to collect bag |
37 |
|
* terms in the equality engine. See the documentation of |
38 |
|
* @link SolverState::collectBagsAndCountTerms |
39 |
|
*/ |
40 |
|
void registerBag(TNode n); |
41 |
|
|
42 |
|
/** |
43 |
|
* @param n has the form (bag.count e A) |
44 |
|
* @pre bag A needs is already registered using registerBag(A) |
45 |
|
* @return a unique skolem for (bag.count e A) |
46 |
|
*/ |
47 |
|
void registerCountTerm(TNode n); |
48 |
|
/** get all bag terms that are representatives in the equality engine. |
49 |
|
* This function is valid after the current solver is initialized during |
50 |
|
* postCheck. See SolverState::initialize and BagSolver::postCheck |
51 |
|
*/ |
52 |
|
const std::set<Node>& getBags(); |
53 |
|
/** |
54 |
|
* @pre B is a registered bag |
55 |
|
* @return all elements associated with bag B so far |
56 |
|
* Note that associated elements are not necessarily elements in B |
57 |
|
* Example: |
58 |
|
* (assert (= 0 (bag.count x B))) |
59 |
|
* element x is associated with bag B, albeit x is definitely not in B. |
60 |
|
*/ |
61 |
|
const std::set<Node>& getElements(Node B); |
62 |
|
/** initialize bag and count terms */ |
63 |
|
void initialize(); |
64 |
|
/** return disequal bag terms */ |
65 |
|
const std::set<Node>& getDisequalBagTerms(); |
66 |
|
|
67 |
|
private: |
68 |
|
/** clear all bags data structures */ |
69 |
|
void reset(); |
70 |
|
/** |
71 |
|
* collect bags' representatives and all count terms. |
72 |
|
* This function is called during postCheck |
73 |
|
*/ |
74 |
|
void collectBagsAndCountTerms(); |
75 |
|
/** |
76 |
|
* collect disequal bag terms. This function is called during postCheck. |
77 |
|
*/ |
78 |
|
void collectDisequalBagTerms(); |
79 |
|
/** constants */ |
80 |
|
Node d_true; |
81 |
|
Node d_false; |
82 |
|
/** node manager for this solver state */ |
83 |
|
NodeManager* d_nm; |
84 |
|
/** collection of bag representatives */ |
85 |
|
std::set<Node> d_bags; |
86 |
|
/** bag -> associated elements */ |
87 |
|
std::map<Node, std::set<Node>> d_bagElements; |
88 |
|
/** Disequal bag terms */ |
89 |
|
std::set<Node> d_deq; |
90 |
|
}; /* class SolverState */ |
91 |
|
|
92 |
|
} // namespace bags |
93 |
|
} // namespace theory |
94 |
|
} // namespace cvc5 |
95 |
|
|
96 |
|
#endif /* CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H */ |