diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-18 01:51:28 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-18 01:51:28 +0200 |
commit | b417642a83d1c4ebf6d2ba4182a95cdeec39e4d8 (patch) | |
tree | ff35293c20213f19915f1d4c5bc9ecf838d03241 /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
parent | 75bbe18a3f8f7b814a7716574fd3619bf69ba85b (diff) |
sygusComp2018: pbe multi-enumerator fairness option (#2178)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 3eace0e89..1a8721530 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -410,19 +410,36 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums, Assert( enums.size()==enum_values.size() ); if( !enums.empty() ){ unsigned min_term_size = 0; - std::vector< unsigned > enum_consider; Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl; - for( unsigned i=0; i<enums.size(); i++ ){ - Trace("sygus-pbe-enum") << " " << enums[i] << " -> " << enum_values[i] << std::endl; + std::vector<unsigned> szs; + for (unsigned i = 0, esize = enums.size(); i < esize; i++) + { + 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 ){ - enum_consider.clear(); min_term_size = sz; - enum_consider.push_back( i ); - }else if( sz==min_term_size ){ + } + } + // Assume two enumerators of types T1 and T2. + // If options::sygusPbeMultiFair() is true, + // we ensure that all values of type T1 and size n are enumerated before + // any term of type T2 of size n+d, and vice versa, where d is + // set by options::sygusPbeMultiFairDiff(). If d is zero, then our + // enumeration is such that all terms of T1 or T2 of size n are considered + // before any term of size n+1. + std::vector<unsigned> enum_consider; + for (unsigned i = 0, esize = enums.size(); i < esize; i++) + { + if (!options::sygusPbeMultiFair() + || szs[i] - min_term_size <= options::sygusPbeMultiFairDiff()) + { enum_consider.push_back( i ); } } + // only consider the enumerators that are at minimum size (for fairness) Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl; NodeManager* nm = NodeManager::currentNM(); |