summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/datatypes/sygus_extension.cpp70
-rw-r--r--src/theory/quantifiers/sygus/example_eval_cache.cpp4
-rw-r--r--src/theory/quantifiers/sygus/example_eval_cache.h8
-rw-r--r--src/theory/quantifiers/sygus/sygus_enumerator.cpp2
4 files changed, 52 insertions, 32 deletions
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 1e593a664..95b73b2fe 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -952,9 +952,13 @@ void SygusExtension::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool t
Assert(ita != d_term_to_anchor.end());
Node a = ita->second;
Assert(!a.isNull());
- if( std::find( d_cache[a].d_search_terms[tn][d].begin(), d_cache[a].d_search_terms[tn][d].end(), n )==d_cache[a].d_search_terms[tn][d].end() ){
+ SearchCache& sca = d_cache[a];
+ if (std::find(
+ sca.d_search_terms[tn][d].begin(), sca.d_search_terms[tn][d].end(), n)
+ == sca.d_search_terms[tn][d].end())
+ {
Trace("sygus-sb-debug") << " register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl;
- d_cache[a].d_search_terms[tn][d].push_back( n );
+ sca.d_search_terms[tn][d].push_back(n);
if( !options::sygusSymBreakLazy() ){
addSymBreakLemmasFor( tn, n, d, lemmas );
}
@@ -1024,11 +1028,11 @@ Node SygusExtension::registerSearchValue(Node a,
std::map<TypeNode, int> var_count;
Node cnv = d_tds->canonizeBuiltin(nv, var_count);
Trace("sygus-sb-debug") << " ...canonized value is " << cnv << std::endl;
+ SearchCache& sca = d_cache[a];
// must do this for all nodes, regardless of top-level
- if (d_cache[a].d_search_val_proc.find(cnv)
- == d_cache[a].d_search_val_proc.end())
+ if (sca.d_search_val_proc.find(cnv) == sca.d_search_val_proc.end())
{
- d_cache[a].d_search_val_proc.insert(cnv);
+ sca.d_search_val_proc.insert(cnv);
// get the root (for PBE symmetry breaking)
Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end());
quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a];
@@ -1049,11 +1053,16 @@ Node SygusExtension::registerSearchValue(Node a,
a, nv, dbzet, Node::null(), var_count, lemmas);
return Node::null();
}else{
+ std::unordered_map<Node, Node, NodeHashFunction>& scasv =
+ sca.d_search_val[tn];
+ std::unordered_map<Node, unsigned, NodeHashFunction>& scasvs =
+ sca.d_search_val_sz[tn];
std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv =
- d_cache[a].d_search_val[tn].find(bvr);
+ scasv.find(bvr);
Node bad_val_bvr;
bool by_examples = false;
- if( itsv==d_cache[a].d_search_val[tn].end() ){
+ if (itsv == scasv.end())
+ {
// Is it equivalent under examples?
Node bvr_equiv;
if (options::sygusSymBreakPbe())
@@ -1063,17 +1072,17 @@ Node SygusExtension::registerSearchValue(Node a,
quantifiers::ExampleEvalCache* eec = aconj->getExampleEvalCache(a);
if (eec != nullptr)
{
- bvr_equiv = eec->addSearchVal(bvr);
+ bvr_equiv = eec->addSearchVal(tn, bvr);
}
}
if( !bvr_equiv.isNull() ){
if( bvr_equiv!=bvr ){
Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl;
- Assert(d_cache[a].d_search_val[tn].find(bvr_equiv)
- != d_cache[a].d_search_val[tn].end());
- Trace("sygus-sb-debug") << "......search value was " << d_cache[a].d_search_val[tn][bvr_equiv] << std::endl;
+ Assert(scasv.find(bvr_equiv) != scasv.end());
+ Trace("sygus-sb-debug")
+ << "......search value was " << scasv[bvr_equiv] << std::endl;
if( Trace.isOn("sygus-sb-exc") ){
- Node prev = d_tds->sygusToBuiltin( d_cache[a].d_search_val[tn][bvr_equiv], tn );
+ Node prev = d_tds->sygusToBuiltin(scasv[bvr_equiv], tn);
Trace("sygus-sb-exc") << " ......programs " << prev << " and " << bv << " are equivalent up to examples." << std::endl;
}
bad_val_bvr = bvr_equiv;
@@ -1081,14 +1090,16 @@ Node SygusExtension::registerSearchValue(Node a,
}
}
//store rewritten values, regardless of whether it will be considered
- d_cache[a].d_search_val[tn][bvr] = nv;
- d_cache[a].d_search_val_sz[tn][bvr] = sz;
- }else{
+ scasv[bvr] = nv;
+ scasvs[bvr] = sz;
+ }
+ else
+ {
bad_val_bvr = bvr;
if( Trace.isOn("sygus-sb-exc") ){
Node prev_bv = d_tds->sygusToBuiltin( itsv->second, tn );
Trace("sygus-sb-exc") << " ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl;
- }
+ }
}
if (options::sygusRewVerify())
@@ -1111,16 +1122,15 @@ Node SygusExtension::registerSearchValue(Node a,
if( !bad_val_bvr.isNull() ){
Node bad_val = nv;
- Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr];
- Assert(d_cache[a].d_search_val_sz[tn].find(bad_val_bvr)
- != d_cache[a].d_search_val_sz[tn].end());
- unsigned prev_sz = d_cache[a].d_search_val_sz[tn][bad_val_bvr];
+ Node bad_val_o = scasv[bad_val_bvr];
+ Assert(scasvs.find(bad_val_bvr) != scasvs.end());
+ unsigned prev_sz = scasvs[bad_val_bvr];
bool doFlip = (prev_sz > sz);
if (doFlip)
{
//swap : the excluded value is the previous
- d_cache[a].d_search_val_sz[tn][bad_val_bvr] = sz;
- bad_val = d_cache[a].d_search_val[tn][bad_val_bvr];
+ scasvs[bad_val_bvr] = sz;
+ bad_val = scasv[bad_val_bvr];
bad_val_o = nv;
if (Trace.isOn("sygus-sb-exc"))
{
@@ -1196,14 +1206,17 @@ void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz,
Trace("sygus-sb-debug") << " type : " << tn << std::endl;
Trace("sygus-sb-debug") << " size : " << sz << std::endl;
Assert(!a.isNull());
- d_cache[a].d_sb_lemmas[tn][sz].push_back( lem );
+ SearchCache& sca = d_cache[a];
+ sca.d_sb_lemmas[tn][sz].push_back(lem);
TNode x = getFreeVar( tn );
unsigned csz = getSearchSizeForAnchor( a );
int max_depth = ((int)csz)-((int)sz);
NodeManager* nm = NodeManager::currentNM();
for( int d=0; d<=max_depth; d++ ){
- std::map< unsigned, std::vector< Node > >::iterator itt = d_cache[a].d_search_terms[tn].find( d );
- if( itt!=d_cache[a].d_search_terms[tn].end() ){
+ std::map<unsigned, std::vector<Node>>::iterator itt =
+ sca.d_search_terms[tn].find(d);
+ if (itt != sca.d_search_terms[tn].end())
+ {
for (const TNode& t : itt->second)
{
if (!options::sygusSymBreakLazy()
@@ -1233,10 +1246,13 @@ void SygusExtension::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node
Assert(!a.isNull());
Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d
<< " " << a << std::endl;
- std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn );
+ SearchCache& sca = d_cache[a];
+ std::map<TypeNode, std::map<unsigned, std::vector<Node>>>::iterator its =
+ sca.d_sb_lemmas.find(tn);
Node rlv = getRelevancyCondition(t);
NodeManager* nm = NodeManager::currentNM();
- if( its != d_cache[a].d_sb_lemmas.end() ){
+ if (its != sca.d_sb_lemmas.end())
+ {
TNode x = getFreeVar( tn );
//get symmetry breaking lemmas for this term
unsigned csz = getSearchSizeForAnchor( a );
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp
index 2a43335d7..ee5394972 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.cpp
+++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp
@@ -43,7 +43,7 @@ ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds,
ExampleEvalCache::~ExampleEvalCache() {}
-Node ExampleEvalCache::addSearchVal(Node bv)
+Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv)
{
if (!d_indexSearchVals)
{
@@ -53,7 +53,7 @@ Node ExampleEvalCache::addSearchVal(Node bv)
std::vector<Node> vals;
evaluateVec(bv, vals, true);
Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
- Node ret = d_trie.addOrGetTerm(bv, vals);
+ Node ret = d_trie[tn].addOrGetTerm(bv, vals);
Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
// Only save the cache data if necessary: if the enumerated term
// is redundant, its cached data will not be used later and thus should
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h
index 6aa78851f..6c5a65e7f 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.h
+++ b/src/theory/quantifiers/sygus/example_eval_cache.h
@@ -81,6 +81,10 @@ class ExampleEvalCache
* procedure for SyGuS datatypes or the SyGuS fast enumerator when we are
* considering a value of enumerator e passed to the constructor of this
* class whose analog in the signature of builtin theory is bvr.
+ *
+ * The type tn passed to this function is the sygus type of the term whose
+ * builtin equivalent is bvr. Terms with distinct types must be cached
+ * independently since two sygus types may not generate the same terms.
*
* This returns either:
* - A term that is equivalent to bvr up to examples that was passed as the
@@ -94,7 +98,7 @@ class ExampleEvalCache
* result of the evaluation of bvr is cached by this class, and can be
* later accessed by evaluateVec below.
*/
- Node addSearchVal(Node bvr);
+ Node addSearchVal(TypeNode tn, Node bvr);
//----------------------------------- evaluating terms
/** Evaluate vector
*
@@ -149,7 +153,7 @@ class ExampleEvalCache
* This is used for symmetry breaking in quantifier-free reasoning
* about SyGuS datatypes.
*/
- NodeTrie d_trie;
+ std::map< TypeNode, NodeTrie> d_trie;
/** cache for evaluate */
std::map<Node, std::vector<Node>> d_exOutCache;
};
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 551a9d225..3923361b1 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -346,7 +346,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
{
++(d_stats->d_enumTermsExampleEval);
// Is it equivalent under examples?
- Node bne = d_eec->addSearchVal(bnr);
+ Node bne = d_eec->addSearchVal(d_tn, bnr);
if (!bne.isNull())
{
if (bnr != bne)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback