diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rwxr-xr-x | src/theory/quantifiers/ce_guided_instantiation.cpp | 60 |
1 files changed, 33 insertions, 27 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 71bf7c426..54415d974 100755 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Assert( dt.isSygus() ); //get the solution Node sol; - int status; + int status = -1; if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); @@ -786,39 +786,45 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { for( unsigned j=0; j<svl.getNumChildren(); j++ ){ subs.push_back( Node::fromExpr( svl[j] ) ); } + bool templIsPost = false; + Node templ; if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ - const CegConjectureSingleInv* ceg_si = - d_conj->getCegConjectureSingleInv(); + const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){ - std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); - Assert(templ_vars.size() == subs.size()); - Node pre = ceg_si->getTransPre(prog); - pre = pre.substitute( templ_vars.begin(), templ_vars.end(), - subs.begin(), subs.end() ); - TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); - Trace("cegqi-inv") << "Builtin version of solution is : " - << sol << ", type : " << sol.getType() - << std::endl; - sol = NodeManager::currentNM()->mkNode( OR, sol, pre ); + templ = ceg_si->getTransPre(prog); + templIsPost = false; } }else if(options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST){ - const CegConjectureSingleInv* ceg_si = - d_conj->getCegConjectureSingleInv(); + const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); if(ceg_si->d_trans_post.find(prog) != ceg_si->d_trans_post.end()){ - std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); - Assert( templ_vars.size()==subs.size() ); - Node post = ceg_si->getTransPost(prog); - post = post.substitute( templ_vars.begin(), templ_vars.end(), - subs.begin(), subs.end() ); - TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); - Trace("cegqi-inv") << "Builtin version of solution is : " - << sol << ", type : " << sol.getType() - << std::endl; - sol = NodeManager::currentNM()->mkNode( AND, sol, post ); + templ = ceg_si->getTransPost(prog); + templIsPost = true; } } + if( !templ.isNull() ){ + std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); + + //take into consideration Boolean term conversion (this step can be eliminated when boolean term conversion is eliminated) + std::vector< Node > vars; + vars.insert( vars.end(), templ_vars.begin(), templ_vars.end() ); + Node vl = Node::fromExpr( dt.getSygusVarList() ); + Assert(vars.size() == subs.size()); + for( unsigned j=0; j<templ_vars.size(); j++ ){ + if( vl[j].getType().isBoolean() ){ + Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + vars[j] = vars[j].eqNode( c ); + } + Assert( vars[j].getType()==subs[j].getType() ); + } + + templ = templ.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); + sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " + << sol << ", type : " << sol.getType() + << std::endl; + sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ ); + } if( sol==sygus_sol ){ sol = sygus_sol; status = 1; |