diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-22 19:26:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-22 19:26:10 -0500 |
commit | c5982fa8fa60f25b01efcf45cf73bca353226d84 (patch) | |
tree | 3002ee0e50ca147a63a209276610c15ec9a62606 /src | |
parent | 2f97221cc16f175568ea240768e5818b35472adf (diff) |
Do not use lazy trie for sygus-rr-verify (#2668)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 61 |
1 files changed, 31 insertions, 30 deletions
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 17ef4f968..a7763bff1 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1096,45 +1096,46 @@ Node SygusSymBreakNew::registerSearchValue(Node a, d_tds, nv, options::sygusSamples(), false); its = d_sampler[a].find(tn); } - - // register the rewritten node with the sampler - Node bvr_sample_ret = its->second.registerTerm(bvr); - // register the current node with the sampler - Node sample_ret = its->second.registerTerm(bv); - + // see if they evaluate to same thing on all sample points + bool ptDisequal = false; + unsigned pt_index = 0; + Node bve, bvre; + for (unsigned i = 0, npoints = its->second.getNumSamplePoints(); + i < npoints; + i++) + { + bve = its->second.evaluate(bv, i); + bvre = its->second.evaluate(bvr, i); + if (bve != bvre) + { + ptDisequal = true; + pt_index = i; + break; + } + } // bv and bvr should be equivalent under examples - if (sample_ret != bvr_sample_ret) + if (ptDisequal) { // we have detected unsoundness in the rewriter Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); std::ostream* out = nodeManagerOptions.getOut(); (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; // debugging information - int pt_index = its->second.getDiffSamplePointIndex(bv, bvr); - if (pt_index >= 0) + (*out) << "; unsound: are not equivalent for : " << std::endl; + std::vector<Node> vars; + its->second.getVariables(vars); + std::vector<Node> pt; + its->second.getSamplePoint(pt_index, pt); + Assert(vars.size() == pt.size()); + for (unsigned i = 0, size = pt.size(); i < size; i++) { - (*out) << "; unsound: are not equivalent for : " << std::endl; - std::vector<Node> vars; - its->second.getVariables(vars); - std::vector<Node> pt; - its->second.getSamplePoint(pt_index, pt); - Assert(vars.size() == pt.size()); - for (unsigned i = 0, size = pt.size(); i < size; i++) - { - (*out) << "; unsound: " << vars[i] << " -> " << pt[i] - << std::endl; - } - Node bv_e = its->second.evaluate(bv, pt_index); - Node pbv_e = its->second.evaluate(bvr, pt_index); - Assert(bv_e != pbv_e); - (*out) << "; unsound: where they evaluate to " << bv_e << " and " - << pbv_e << std::endl; - } - else - { - // no witness point found? - Assert(false); + (*out) << "; unsound: " << vars[i] << " -> " << pt[i] + << std::endl; } + Assert(bve != bvre); + (*out) << "; unsound: where they evaluate to " << bve << " and " + << bvre << std::endl; + if (options::sygusRewVerifyAbort()) { AlwaysAssert( |