diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-14 07:46:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-14 07:46:52 -0500 |
commit | 26977381d8e026718a056adee0fa6dea1a76555d (patch) | |
tree | 4d9905ad7cb3c2c452c85aa7453d0844c484b6f1 /src/theory/quantifiers/sygus_sampler.cpp | |
parent | 1744dc5f3140f9dc2aeb71f99c530feb83264a04 (diff) |
Generalize sygus-rr-verify for fast enumerator (#2829)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 27ca270cc..9727149be 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -769,6 +769,56 @@ void SygusSampler::registerSygusType(TypeNode tn) } } +void SygusSampler::checkEquivalent(Node bv, Node bvr) +{ + Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr + << std::endl; + + // 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 = getNumSamplePoints(); i < npoints; i++) + { + bve = evaluate(bv, i); + bvre = evaluate(bvr, i); + if (bve != bvre) + { + ptDisequal = true; + pt_index = i; + break; + } + } + // bv and bvr should be equivalent under examples + 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 + (*out) << "; unsound: are not equivalent for : " << std::endl; + std::vector<Node> vars; + getVariables(vars); + std::vector<Node> pt; + 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; + } + Assert(bve != bvre); + (*out) << "; unsound: where they evaluate to " << bve << " and " << bvre + << std::endl; + + if (options::sygusRewVerifyAbort()) + { + AlwaysAssert(false, + "--sygus-rr-verify detected unsoundness in the rewriter!"); + } + } +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ |