Searched refs:NodeTheoryPair (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.h | 61 struct NodeTheoryPair { struct
65 NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0) argument
67 NodeTheoryPair() : theory(theory::THEORY_LAST), timestamp() {} in NodeTheoryPair() function
69 bool operator == (const NodeTheoryPair& pair) const {
77 size_t operator()(const NodeTheoryPair& pair) const { in operator()
389 …typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> Propagation…
608 …void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRe…
|
| H A D | theory_engine.cpp | 1207 NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp); in markPropagation()
1209 NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp); in markPropagation()
1574 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { in mkExplanation()
1663 NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); in getExplanationAndRecipe()
1666 NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain]; in getExplanationAndRecipe()
1673 std::vector<NodeTheoryPair> explanationVector; in getExplanationAndRecipe()
1909 std::vector<NodeTheoryPair> explanationVector; in conflict()
1910 explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); in conflict()
2018 NodeTheoryPair toExplain = explanationVector[i]; in getExplanation()
2044 NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp); in getExplanation()
[all …]
|