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 | |
parent | 75bbe18a3f8f7b814a7716574fd3619bf69ba85b (diff) |
sygusComp2018: pbe multi-enumerator fairness option (#2178)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 29 |
2 files changed, 29 insertions, 14 deletions
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index c9b3a17f4..49132dc46 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -383,9 +383,8 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) { } Assert( !disj.empty() ); if( excl ){ - cond = disj.size() == 1 - ? disj[0] - : NodeManager::currentNM()->mkNode(kind::AND, disj); + cond = disj.size() == 1 ? disj[0] : NodeManager::currentNM()->mkNode( + kind::AND, disj); } }else{ int sindex = Datatype::cindexOf( selExpr ); @@ -802,8 +801,8 @@ Node SygusSymBreakNew::registerSearchValue( Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); quantifiers::CegConjecture* aconj = d_anchor_to_conj[a]; Assert(aconj != NULL); - Trace("sygus-sb-debug") - << " ...register search value " << cnv << ", type=" << tn << std::endl; + Trace("sygus-sb-debug") << " ...register search value " << cnv + << ", type=" << tn << std::endl; Node bv = d_tds->sygusToBuiltin(cnv, tn); Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); @@ -812,8 +811,8 @@ Node SygusSymBreakNew::registerSearchValue( unsigned sz = d_tds->getSygusTermSize( nv ); if( d_tds->involvesDivByZero( bvr ) ){ quantifiers::DivByZeroSygusInvarianceTest dbzet; - Trace("sygus-sb-mexp-debug") - << "Minimize explanation for div-by-zero in " << bv << std::endl; + Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " + << bv << std::endl; registerSymBreakLemmaForValue( a, nv, dbzet, Node::null(), var_count, lemmas); return Node::null(); @@ -1055,7 +1054,6 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No Trace("sygus-sb-debug2") << "...finished." << std::endl; } - void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) { if( n.isVar() ){ Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl; 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(); |