diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 44 |
1 files changed, 30 insertions, 14 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 9a6645560..b7e6e0c65 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); + } } } @@ -468,14 +481,17 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Node c = d_enum_to_candidate[e]; std::vector<Node> enum_lems; d_sygus_unif[c].notifyEnumeration(e, v, enum_lems); - // the lemmas must be guarded by the active guard of the enumerator - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + if (!enum_lems.empty()) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + // the lemmas must be guarded by the active guard of the enumerator + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + { + enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + } + lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } - lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } } for( unsigned i=0; i<candidates.size(); i++ ){ |