diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-21 12:10:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-21 12:10:38 -0500 |
commit | 290f2a718a8ebe9532239fa53fabc9763564b5dc (patch) | |
tree | 59662330ba036b7b93fdbafce7d83066992ac1a7 /src/theory | |
parent | 29b2e5a74eb007f04a18e01d7a9c21eff577c9b1 (diff) |
Use cbqi-full for sygus (#2346)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.cpp | 32 |
1 files changed, 22 insertions, 10 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index b3cb98bc5..1e0b36a3c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -267,20 +267,32 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( !conj->needsRefinement() ){ Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - std::vector<Node> clems; - conj->doSingleInvCheck(clems); - if (!clems.empty()) + if (conj->isSingleInvocation()) { - d_last_inst_si = true; - for (const Node& lem : clems) + std::vector<Node> clems; + conj->doSingleInvCheck(clems); + if (!clems.empty()) { - Trace("cegqi-lemma") - << "Cegqi::Lemma : single invocation instantiation : " << lem + d_last_inst_si = true; + for (const Node& lem : clems) + { + Trace("cegqi-lemma") + << "Cegqi::Lemma : single invocation instantiation : " << lem + << std::endl; + d_quantEngine->addLemma(lem); + } + d_statistics.d_cegqi_si_lemmas += clems.size(); + Trace("cegqi-engine") << " ...try single invocation." << std::endl; + } + else + { + // This can happen for non-monotonic instantiation strategies. We + // set --cbqi-full to ensure that for most strategies (e.g. BV), we + // are using a monotonic strategy. + Trace("cegqi-warn") + << " ...FAILED to add cbqi instantiation for single invocation!" << std::endl; - d_quantEngine->addLemma(lem); } - d_statistics.d_cegqi_si_lemmas += clems.size(); - Trace("cegqi-engine") << " ...try single invocation." << std::endl; return; } |