diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-24 23:50:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-24 23:50:50 -0500 |
commit | e9c115e82ea1341f1bbc37fb99c005aacec3d7ec (patch) | |
tree | d274291c8b570e1ff383504e8eeccaafbffd7b15 /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
parent | b9cddd75ada97b4e1808b907125e366c3c03c412 (diff) |
Allow partial models for multiple sygus enumerators (#2499)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 9a6645560..647b16637 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -415,6 +415,8 @@ void SygusPbe::getTermList(const std::vector<Node>& candidates, } } +bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); } + bool SygusPbe::constructCandidates(const std::vector<Node>& enums, const std::vector<Node>& enum_values, const std::vector<Node>& candidates, @@ -431,10 +433,18 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Trace("sygus-pbe-enum") << " " << enums[i] << " -> "; TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]); Trace("sygus-pbe-enum") << std::endl; - unsigned sz = d_tds->getSygusTermSize( enum_values[i] ); - szs.push_back(sz); - if( i==0 || sz<min_term_size ){ - min_term_size = sz; + if (!enum_values[i].isNull()) + { + unsigned sz = d_tds->getSygusTermSize(enum_values[i]); + szs.push_back(sz); + if (i == 0 || sz < min_term_size) + { + min_term_size = sz; + } + } + else + { + szs.push_back(0); } } // Assume two enumerators of types T1 and T2. @@ -448,11 +458,14 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, std::vector<unsigned> enum_consider; for (unsigned i = 0, esize = enums.size(); i < esize; i++) { - Assert(szs[i] >= min_term_size); - int diff = szs[i] - min_term_size; - if (!options::sygusPbeMultiFair() || diff <= diffAllow) + if (!enum_values[i].isNull()) { - enum_consider.push_back( i ); + Assert(szs[i] >= min_term_size); + int diff = szs[i] - min_term_size; + if (!options::sygusPbeMultiFair() || diff <= diffAllow) + { + enum_consider.push_back(i); + } } } |