From cbfc0961327831dc43ce6dda600740bab224ff6c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 1 Sep 2016 16:35:06 -0500 Subject: [PATCH] Fix boolean term issue in invariants from sygus. Minor default options changes for cbqi. --- src/options/quantifiers_options | 4 +- .../quantifiers/ce_guided_instantiation.cpp | 58 ++++++++++--------- src/theory/quantifiers/inst_strategy_cbqi.cpp | 2 + 3 files changed, 36 insertions(+), 28 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index f5561ad23..f99333de2 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -301,9 +301,9 @@ option cbqiMidpoint --cbqi-midpoint bool :default false choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation option cbqiNopt --cbqi-nopt bool :default true non-optimal bounds for counterexample-based quantifier instantiation -option cbqiLitDepend --cbqi-lit-dep bool :default false +option cbqiLitDepend --cbqi-lit-dep bool :default true dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation -option cbqiInnermost --cbqi-innermost bool :read-write :default false +option cbqiInnermost --cbqi-innermost bool :read-write :default true only process innermost quantified formulas in counterexample-based quantifier instantiation option cbqiNestedQE --cbqi-nested-qe bool :default false process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 71bf7c426..718d06c32 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -786,39 +786,45 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { for( unsigned j=0; jgetCegConjectureSingleInv(); + const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){ - std::vector& 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& 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& 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; jmkConst(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; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 71c0858bf..2c0e0a32f 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -427,6 +427,8 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi d_nested_qe_info[nr].d_inst_terms.clear(); d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); d_nested_qe_info[nr].d_doVts = doVts; + //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. + Assert( !options::cbqiInnermost() ); } } } -- 2.30.2