diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 64 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 1 |
4 files changed, 3 insertions, 71 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 3a1ddc73c..aa0af6f1d 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -589,10 +589,9 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, Node sbody = d_base_body.substitute( candidates.begin(), candidates.end(), vals.begin(), vals.end()); Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl; - // do eager unfolding - std::map<Node, Node> visited_n; - sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n); - Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl; + // do eager rewriting + sbody = Rewriter::rewrite(sbody); + Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl; NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 78f2f6a7e..7f48d30d8 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -540,8 +540,6 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) lem = Rewriter::rewrite(lem); // eagerly unfold applications of evaluation function Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; - std::map<Node, Node> visited_n; - lem = d_tds->getEagerUnfold(lem, visited_n); // record the instantiation // this is used for remembering the solution recordInstantiation(candidate_values); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index d4ee11453..d17c343f4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1030,70 +1030,6 @@ Node TermDbSygus::unfold(Node en) return unfold(en, vtm, exp, false); } -Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) { - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv==visited.end() ){ - Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl; - Node ret; - if (n.getKind() == DT_SYGUS_EVAL) - { - TypeNode tn = n[0].getType(); - Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; - if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isSygus() ){ - Trace("cegqi-eager") << "Unfold eager : " << n << std::endl; - Node bTerm = sygusToBuiltin( n[0], tn ); - Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl; - std::vector< Node > vars; - std::vector< Node > subs; - Node var_list = Node::fromExpr( dt.getSygusVarList() ); - Assert(var_list.getNumChildren() + 1 == n.getNumChildren()); - for( unsigned j=0; j<var_list.getNumChildren(); j++ ){ - vars.push_back( var_list[j] ); - } - for( unsigned j=1; j<n.getNumChildren(); j++ ){ - Node nc = getEagerUnfold( n[j], visited ); - subs.push_back( nc ); - Assert(subs[j - 1].getType().isComparableTo( - var_list[j - 1].getType())); - } - Assert(vars.size() == subs.size()); - bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl; - Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl; - Assert(n.getType().isComparableTo(bTerm.getType())); - ret = bTerm; - } - } - } - if( ret.isNull() ){ - if( n.getKind()!=FORALL ){ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nc = getEagerUnfold( n[i], visited ); - childChanged = childChanged || n[i]!=nc; - children.push_back( nc ); - } - if( childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - if( ret.isNull() ){ - ret = n; - } - } - visited[n] = ret; - return ret; - }else{ - return itv->second; - } -} - Node TermDbSygus::evaluateBuiltin(TypeNode tn, Node bn, std::vector<Node>& args, diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 68381fb2a..c591400e1 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -468,7 +468,6 @@ class TermDbSygus { * evaluation heads */ Node unfold(Node en); - Node getEagerUnfold( Node n, std::map< Node, Node >& visited ); }; }/* CVC4::theory::quantifiers namespace */ |