summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/options/quantifiers_options4
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp58
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp2
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; 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;
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() );
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback