diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-07 13:54:06 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-07 13:54:06 -0600 |
commit | b0ec3155fde9502597f0d1f98971bec4ebe141ca (patch) | |
tree | 5275c90d433dbaaabefc773494eefee314eedbb4 /src/theory/quantifiers/inst_strategy_enumerative.cpp | |
parent | a2746472fb95b523dc838376c84467751f6ef764 (diff) |
Guard relevant domain computation properly, minor. (#1325)
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_enumerative.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 67930ce2b..3bd1ac495 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -129,16 +129,15 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) { Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; + Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; + rd->compute(); + Trace("inst-alg-debug") << "...finished" << std::endl; } else { Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; } - AlwaysAssert(rd); - Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; - rd->compute(); - Trace("inst-alg-debug") << "...finished" << std::endl; unsigned final_max_i = 0; std::vector<unsigned> maxs; std::vector<bool> max_zero; @@ -170,11 +169,11 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) { - Node r = + Node rep = d_quantEngine->getEqualityQuery()->getRepresentative(gt); - if (reps_found.find(r) == reps_found.end()) + if (reps_found.find(rep) == reps_found.end()) { - reps_found[r] = gt; + reps_found[rep] = gt; term_db_list[tn].push_back(gt); } } |