diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-03-08 15:46:30 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-08 15:46:30 +0100 |
commit | d7dc81173107bf65b9a90e163a1e85ce7b3c20ff (patch) | |
tree | 84f606979b4a52fa99c7f49d9ed74ffe3a281295 /src/decision | |
parent | 85d00e88892a16e63e520c0c1bde713352316b79 (diff) |
Fix justification heuristic again (#6074)
This PR replaces all TNode types in datatypes by Node within justification heuristic.
Fixes #6073.
Unfortunately, the example from #6073 times out now, thus there is no new regression.
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/justification_heuristic.h | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 1cf2810fd..20dec12d8 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -43,16 +43,16 @@ class JustificationHeuristic : public ITEDecisionStrategy { // TRUE FALSE MEH enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW}; - typedef std::vector<std::pair<TNode, TNode> > SkolemList; - typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache; - typedef std::vector<TNode> ChildList; + typedef std::vector<std::pair<Node, Node> > SkolemList; + typedef context::CDHashMap<Node, SkolemList, NodeHashFunction> SkolemCache; + typedef std::vector<Node> ChildList; typedef context:: - CDHashMap<TNode, std::pair<ChildList, ChildList>, TNodeHashFunction> + CDHashMap<Node, std::pair<ChildList, ChildList>, NodeHashFunction> ChildCache; - typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; - typedef context::CDHashMap<TNode, + typedef context::CDHashMap<Node,Node,NodeHashFunction> SkolemMap; + typedef context::CDHashMap<Node, std::pair<DecisionWeight, DecisionWeight>, - TNodeHashFunction> + NodeHashFunction> WeightCache; // being 'justified' is monotonic with respect to decisions @@ -72,14 +72,11 @@ class JustificationHeuristic : public ITEDecisionStrategy { * directly. Doesn't have ones introduced during during term removal. */ context::CDList<Node> d_assertions; - //TNode is fine since decisionEngine has them too /** map from skolems introduced in term removal to the corresponding assertion */ SkolemMap d_skolemAssertions; - // 'key' being TNode is fine since if a skolem didn't exist anywhere, - // we won't look it up. as for 'value', same reason as d_assertions - + /** Cache for skolems present in a atomic formula */ SkolemCache d_skolemCache; @@ -88,13 +85,13 @@ class JustificationHeuristic : public ITEDecisionStrategy { * splitter. Can happen when exploring assertion corresponding to a * term-ITE. */ - std::unordered_set<TNode,TNodeHashFunction> d_visited; + std::unordered_set<Node,NodeHashFunction> d_visited; /** * Set to track visited nodes in a dfs search done in computeSkolems * function */ - std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems; + std::unordered_set<Node, NodeHashFunction> d_visitedComputeSkolems; /** current decision for the recursive call */ prop::SatLiteral d_curDecision; @@ -174,7 +171,7 @@ public: * For big and/or nodes, a cache to save starting index into children * for efficiently. */ - typedef context::CDHashMap<TNode, int, TNodeHashFunction> StartIndexCache; + typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache; StartIndexCache d_startIndexCache; int getStartIndex(TNode node); void saveStartIndex(TNode node, int val); |