diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-08 15:57:45 -0500 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-08-08 15:57:45 -0500 |
| commit | c7489b25e3e50437785e7b739288475e4cdc8626 (patch) | |
| tree | 75a04bd5cd1ec4b7efd6956c81be4902a443d44c /src/theory | |
| parent | 2947a2f2af0e9a40c3be9ba2e84f634c36e0dd0f (diff) | |
Add debug test for sygus subcall verify calls. (#2287)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 37cfc25f1..31a76d933 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -433,6 +433,17 @@ void CegConjecture::doCheck(std::vector<Node>& lems) d_ce_sk_var_mvs.push_back(mv); } Trace("cegqi-engine") << std::endl; +#ifdef CVC4_ASSERTIONS + // the values for the query should be a complete model + Node squery = query.substitute(d_ce_sk_vars.begin(), + d_ce_sk_vars.end(), + d_ce_sk_var_mvs.begin(), + d_ce_sk_var_mvs.end()); + Trace("cegqi-debug") << "...squery : " << squery << std::endl; + squery = Rewriter::rewrite(squery); + Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; + Assert(squery.isConst() && squery.getConst<bool>()); +#endif return; } else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |