namespace CVC4 {
-CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_curr_lit( c, 0 ){
d_refine_count = 0;
d_ceg_si = new CegConjectureSingleInv( qe, this );
}
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
}
- Trace("cegqi") << "Base quantified fm is : " << q << std::endl;
+ Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
//construct base instantiation
d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) );
- Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
+ Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
qe->getOutputChannel().lemma( lem );
}else if( d_ceg_si ){
std::vector< Node > lems;
- d_ceg_si->getSingleInvLemma( d_guard, lems );
+ d_ceg_si->getInitialSingleInvLemma( d_guard, lems );
for( unsigned i=0; i<lems.size(); i++ ){
Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl;
qe->getOutputChannel().lemma( lems[i] );
return d_ceg_si->isSingleInvocation();
}
+bool CegConjecture::isFullySingleInvocation() {
+ return d_ceg_si->isFullySingleInvocation();
+}
+
bool CegConjecture::needsCheck() {
- return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
+ return !isSingleInvocation() || d_ceg_si->needsCheck();
}
void CegConjecture::preregisterConjecture( Node q ) {
if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
Trace("cegqi-engine-debug") << std::endl;
- Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
- if( d_conj->needsCheck() ){
+ bool active = false;
+ bool feasible = false;
+ bool value;
+ if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) {
+ active = value;
+ }else{
+ Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl;
+ }
+ if( d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+ feasible = value;
+ }else{
+ Trace("cegqi-engine-debug") << "...no value for guard." << std::endl;
+ }
+ Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << " feasible : " << feasible << std::endl;
+ if( active && feasible && d_conj->needsCheck() ){
checkCegConjecture( d_conj );
}
Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
}
void CegInstantiation::assertNode( Node n ) {
- Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl;
- bool pol = n.getKind()!=NOT;
- Node lit = n.getKind()==NOT ? n[0] : n;
- if( lit==d_conj->d_guard ){
- //d_guard_assertions[lit] = pol;
- d_conj->d_infeasible = !pol;
- }
- if( lit==d_conj->d_assert_quant ){
- d_conj->d_active = true;
- }
}
Node CegInstantiation::getNextDecisionRequest() {
//enforce fairness
if( d_conj->isAssigned() ){
d_conj->initializeGuard( d_quantEngine );
- bool value;
- if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
- //if( d_conj->d_guard_split.isNull() ){
- // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
- // d_quantEngine->getOutputChannel().lemma( lem );
- //}
- Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
- return d_conj->d_guard;
+ std::vector< Node > req_dec;
+ req_dec.push_back( d_conj->d_guard );
+ if( d_conj->d_ceg_si && !d_conj->d_ceg_si->d_ns_guard.isNull() ){
+ req_dec.push_back( d_conj->d_ceg_si->d_ns_guard );
+ }
+ for( unsigned i=0; i<req_dec.size(); i++ ){
+ bool value;
+ if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) {
+ Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl;
+ return req_dec[i];
+ }
}
if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+ bool value;
if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
if( !value ){
d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
//if( !(Trace.isOn("cegqi-stats")) ){
// out << "Solution:" << std::endl;
//}
- for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){
+ for( unsigned i=0; i<d_conj->d_quant[0].getNumChildren(); i++ ){
Node prog = d_conj->d_quant[0][i];
std::stringstream ss;
ss << prog;
if( d_last_inst_si ){
Assert( d_conj->d_ceg_si );
sol = d_conj->d_ceg_si->getSolution( i, tn, status );
+ sol = sol.getKind()==LAMBDA ? sol[1] : sol;
}else{
if( !d_conj->d_candidate_inst[i].empty() ){
sol = d_conj->d_candidate_inst[i].back();
//check if this was based on a template, if so, we must do reconstruction
if( d_conj->d_assert_quant!=d_conj->d_quant ){
+ Node sygus_sol = sol;
Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
- sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() );
- Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
std::vector< Node > subs;
Expr svl = dt.getSygusVarList();
for( unsigned j=0; j<svl.getNumChildren(); j++ ){
subs.push_back( Node::fromExpr( svl[j] ) );
}
if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
- Node pre = d_conj->d_ceg_si->d_trans_pre[prog];
- pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
- subs.begin(), subs.end() );
- sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
- }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){
- Node post = d_conj->d_ceg_si->d_trans_post[prog];
- post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+ if( d_conj->d_ceg_si->d_trans_pre.find( prog )!=d_conj->d_ceg_si->d_trans_pre.end() ){
+ Assert( d_conj->d_ceg_si->d_prog_templ_vars[prog].size()==subs.size() );
+ Node pre = d_conj->d_ceg_si->d_trans_pre[prog];
+ pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
subs.begin(), subs.end() );
- sol = NodeManager::currentNM()->mkNode( AND, sol, post );
+ sol = getTermDatabase()->getTermDatabaseSygus()->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 );
+ }
+ }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){
+ if( d_conj->d_ceg_si->d_trans_post.find( prog )!=d_conj->d_ceg_si->d_trans_post.end() ){
+ Assert( d_conj->d_ceg_si->d_prog_templ_vars[prog].size()==subs.size() );
+ Node post = d_conj->d_ceg_si->d_trans_post[prog];
+ post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+ subs.begin(), subs.end() );
+ sol = getTermDatabase()->getTermDatabaseSygus()->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 );
+ }
+ }
+ if( sol==sygus_sol ){
+ sol = sygus_sol;
+ status = 1;
+ }else{
+ Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
+ sol = Rewriter::rewrite( sol );
+ Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
+ sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status );
+ sol = sol.getKind()==LAMBDA ? sol[1] : sol;
}
- Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
- sol = Rewriter::rewrite( sol );
- Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
- sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status );
}else{
status = 1;
}
d_cinst = new CegInstantiator( qe, cosi, false, false );
d_sol = new CegConjectureSingleInvSol( qe );
-
+
d_sip = new SingleInvocationPartition;
}
-void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) {
+void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ) {
if( !d_single_inv.isNull() ) {
d_single_inv_var.clear();
d_single_inv_sk.clear();
std::map< Node, Node > visited;
std::vector< TypeNode > types;
std::vector< Node > order_vars;
+ std::map< Node, Node > single_inv_app_map;
int type_valid = 0;
qq = removeDeepEmbedding( qq, progs, types, type_valid, visited );
Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl;
std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op );
if( it_fov!=d_sip->d_func_fo_var.end() ){
Node pv = it_fov->second;
- d_single_inv_map[prog] = pv;
- d_single_inv_map_to_prog[pv] = prog;
Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() );
Node inv = d_sip->d_func_inv[op];
- d_single_inv_app_map[prog] = inv;
+ single_inv_app_map[prog] = inv;
Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl;
d_prog_to_sol_index[prog] = order_vars.size();
order_vars.push_back( pv );
//does not mention the function
}
}
+ //reorder the variables
+ Assert( d_sip->d_func_vars.size()==order_vars.size() );
+ d_sip->d_func_vars.clear();
+ d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() );
+
//check if it is single invocation
if( !d_sip->d_conjuncts[1].empty() ){
singleInvocation = false;
- //if we are doing invariant templates, then construct the template
- if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+ if( options::cegqiSingleInvPartial() ){
+ /* TODO : this enables partially single invocation techniques
+ d_nsingle_inv = d_sip->getNonSingleInvocation();
+ d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv );
+ d_full_inv = d_sip->getFullSpecification();
+ d_full_inv = TermDb::simpleNegate( d_full_inv );
+ singleInvocation = true;
+ */
+ }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+ //if we are doing invariant templates, then construct the template
std::map< Node, bool > has_inv;
std::map< Node, std::vector< Node > > inv_pre_post[2];
for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){
std::vector< Node > disjuncts;
Node func;
int pol = -1;
- Trace("cegqi-si-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl;
+ Trace("cegqi-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl;
d_sip->extractInvariant( d_sip->d_conjuncts[2][i], func, pol, disjuncts );
if( pol>=0 ){
Assert( d_nsi_op_map_to_prog.find( func )!=d_nsi_op_map_to_prog.end() );
Node prog = d_nsi_op_map_to_prog[func];
- Trace("cegqi-si-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl;
+ Trace("cegqi-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl;
Node c = disjuncts.empty() ? d_qe->getTermDatabase()->d_false : ( disjuncts.size()==1 ? disjuncts[0] : NodeManager::currentNM()->mkNode( OR, disjuncts ) );
c = pol==0 ? TermDb::simpleNegate( c ) : c;
- Trace("cegqi-si-inv-debug") << "...extracted : " << c << std::endl;
+ Trace("cegqi-inv-debug") << "...extracted : " << c << std::endl;
inv_pre_post[pol][prog].push_back( c );
has_inv[prog] = true;
}else{
- Trace("cegqi-si-inv") << "...no status." << std::endl;
+ Trace("cegqi-inv") << "...no status." << std::endl;
}
}
- Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl;
+ Trace("cegqi-inv") << "Constructing invariant templates..." << std::endl;
//now, contruct the template for the invariant(s)
std::map< Node, Node > prog_templ;
for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){
Node prog = iti->first;
- Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl;
- Trace("cegqi-si-inv") << " args : ";
+ Trace("cegqi-inv") << "...for " << prog << "..." << std::endl;
+ Trace("cegqi-inv") << " args : ";
for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
- Node v = NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() );
+ std::stringstream ss;
+ ss << "i_" << j;
+ Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() );
d_prog_templ_vars[prog].push_back( v );
- Trace("cegqi-si-inv") << v << " ";
+ Trace("cegqi-inv") << v << " ";
}
- Trace("cegqi-si-inv") << std::endl;
+ Trace("cegqi-inv") << std::endl;
Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) :
( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) );
d_trans_pre[prog] = pre.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) :
( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) );
d_trans_post[prog] = post.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
- Trace("cegqi-si-inv") << " precondition : " << d_trans_pre[prog] << std::endl;
- Trace("cegqi-si-inv") << " postcondition : " << d_trans_post[prog] << std::endl;
- Node invariant = d_single_inv_app_map[prog];
+ Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl;
+ Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl;
+ Node invariant = single_inv_app_map[prog];
invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
- Trace("cegqi-si-inv") << " invariant : " << invariant << std::endl;
+ Trace("cegqi-inv") << " invariant : " << invariant << std::endl;
//construct template
Node templ;
if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
}
visited.clear();
templ = addDeepEmbedding( templ, visited );
- Trace("cegqi-si-inv") << " template : " << templ << std::endl;
+ Trace("cegqi-inv") << " template : " << templ << std::endl;
prog_templ[prog] = templ;
}
Node bd = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] );
visited.clear();
bd = addDeepEmbedding( bd, visited );
- Trace("cegqi-si-inv") << " body : " << bd << std::endl;
+ Trace("cegqi-inv") << " body : " << bd << std::endl;
bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars );
- Trace("cegqi-si-inv-debug") << " templ-subs body : " << bd << std::endl;
+ Trace("cegqi-inv-debug") << " templ-subs body : " << bd << std::endl;
//make inner existential
std::vector< Node > new_var_bv;
for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
- new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ) );
+ std::stringstream ss;
+ ss << "ss_" << j;
+ new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ) );
}
bd = bd.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_var_bv.begin(), new_var_bv.end() );
Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL );
//make outer universal
bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd );
bd = Rewriter::rewrite( bd );
- Trace("cegqi-si-inv") << " rtempl-subs body : " << bd << std::endl;
+ Trace("cegqi-inv") << " rtempl-subs body : " << bd << std::endl;
d_quant = bd;
}
}else{
Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl;
singleInvocation = false;
}
- if( options::cegqiSingleInvPartial() ){
- //TODO: set up outer loop
- }
if( singleInvocation ){
d_single_inv = d_sip->getSingleInvocation();
d_single_inv = TermDb::simpleNegate( d_single_inv );
- if( !order_vars.empty() ){
- Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, order_vars );
+ if( !d_sip->d_func_vars.empty() ){
+ Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_func_vars );
d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv );
}
//now, introduce the skolems
//just invoke the presolve now
d_cinst->presolve( d_single_inv );
}
+ if( !d_nsingle_inv.isNull() ){
+ //initialize information as next single invocation conjecture
+ initializeNextSiConjecture();
+ Trace("cegqi-si") << "Non-single invocation formula is : " << d_nsingle_inv << std::endl;
+ Trace("cegqi-si") << "Full specification is : " << d_full_inv << std::endl;
+ }
}else{
Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
if( options::cegqiSingleInvAbort() ){
}
}
-bool CegConjectureSingleInv::doVariableElimination( Node v, std::vector< Node >& conjuncts ) {
- //all conjuncts containing v must contain a literal v != s for some s
- // if so, do DER on all such conjuncts
- TNode s;
- for( unsigned i=0; i<conjuncts.size(); i++ ){
- int status = 0;
- if( getVariableEliminationTerm( true, true, v, conjuncts[i], s, status ) ){
- Trace("cegqi-si-debug") << "Substitute " << s << " for " << v << " in " << conjuncts[i] << std::endl;
- Assert( !s.isNull() );
- conjuncts[i] = conjuncts[i].substitute( v, s );
- }else{
- if( status==1 ){
- Trace("cegqi-si-debug") << "Conjunct " << conjuncts[i] << " contains " << v << " but not in disequality." << std::endl;
- return false;
- }else{
- Trace("cegqi-si-debug") << "Conjunct does not contain " << v << "." << std::endl;
- }
- }
- }
- return true;
-}
-
-bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, Node v, Node n, TNode& s, int& status ) {
- if( hasPol ){
- if( n.getKind()==NOT ){
- return getVariableEliminationTerm( !pol, true, v, n[0], s, status );
- }else if( pol && ( n.getKind()==EQUAL || n.getKind()==IFF ) ){
- Node ss = QuantArith::solveEqualityFor( n, v );
- if( !ss.isNull() ){
- if( s.isNull() ){
- s = ss;
- }
- return ss==s;
- }
- }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){
- return true;
- }
- }
- return false;
- }
- }
- if( n==v ){
- status = 1;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- getVariableEliminationTerm( pol, false, v, n[i], s, status );
- }
- }
- return false;
-}
-
-int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) {
- if( n.getKind()==NOT ){
- return extractInvariantPolarity( n[0], inv, curr_disj, !pol );
- }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
- int curr_pol = -1;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol );
- if( eipc!=-1 ){
- if( curr_pol==-1 ){
- curr_pol = eipc;
- }else{
- return -1;
- }
- }else{
- curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) );
- }
- }
- return curr_pol;
- }else if( n==inv ){
- return pol ? 1 : 0;
- }else{
- return -1;
- }
-}
-
Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) {
if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
std::map< Node, Node >::iterator it = prog_templ.find( n[0] );
}
}
-bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
- std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
- std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
- if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
- return false;
- }
- }
- }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){
- if( !p.isNull() ){
- //do not allow nested quantifiers
- return false;
- }
- analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false );
- }else{
- if( pol ){
- n = TermDb::simpleNegate( n );
- }
- Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl;
- children[p].push_back( n );
- for( unsigned i=0; i<progs.size(); i++ ){
- prog_invoke[n][progs[i]].clear();
- }
- bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] );
- for( unsigned i=0; i<progs.size(); i++ ){
- std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] );
- Trace("cegqi-si") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
- for( unsigned j=0; j<it->second.size(); j++ ){
- Trace("cegqi-si") << " " << it->second[j] << std::endl;
- }
- }
- return success;
- }
- return true;
-}
-
-bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) {
- if( n.getNumChildren()>0 ){
- if( n.getKind()==FORALL ){
- //do not allow nested quantifiers
- return false;
- }
- //look at first argument in evaluator
- Node p = n[0];
- std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p );
- if( it!=prog_invoke.end() ){
- if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){
- it->second.push_back( n );
- }
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){
- return false;
- }
- }
+void CegConjectureSingleInv::initializeNextSiConjecture() {
+ d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) );
+ d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard );
+ AlwaysAssert( !d_ns_guard.isNull() );
+ d_qe->getOutputChannel().requirePhase( d_ns_guard, true );
+ d_lemmas_produced.clear();
+ if( options::incrementalSolving() ){
+ delete d_c_inst_match_trie;
+ d_c_inst_match_trie = new inst::CDInstMatchTrie( d_qe->getUserContext() );
}else{
- //record this conjunct contains n
- contains[n] = true;
+ d_inst_match_trie.clear();
}
- return true;
+ Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture, guard = " << d_ns_guard << std::endl;
+ Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl;
}
bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){
if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
siss << " * single invocation: " << std::endl;
for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
- Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
- siss << " * " << v;
+ Assert( d_sip->d_fo_var_to_func.find( d_single_inv[0][j] )!=d_sip->d_fo_var_to_func.end() );
+ Node op = d_sip->d_fo_var_to_func[d_single_inv[0][j]];
+ Assert( d_nsi_op_map_to_prog.find( op )!=d_nsi_op_map_to_prog.end() );
+ Node prog = d_nsi_op_map_to_prog[op];
+ siss << " * " << prog;
siss << " (" << d_single_inv_sk[j] << ")";
siss << " -> " << subs[j] << std::endl;
}
Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem );
}
+ //add guard if not fully single invocation
+ if( !isFullySingleInvocation() ){
+ lem = NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), lem );
+ }
Trace("cegqi-engine-debug") << "Rewrite..." << std::endl;
lem = Rewriter::rewrite( lem );
Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
if( !d_single_inv.isNull() ) {
+ if( !d_ns_guard.isNull() ){
+ //if partially single invocation, check if we have constructed a candidate by refutation
+ bool value;
+ if( d_qe->getValuation().hasSatValue( d_ns_guard, value ) ) {
+ if( !value ){
+ //construct candidate solution
+ Trace("cegqi-nsi") << "NSI : refuted current candidate conjecture, construct corresponding solution..." << std::endl;
+ d_ns_guard = Node::null();
+
+ std::map< Node, Node > lams;
+ for( unsigned i=0; i<d_quant[0].getNumChildren(); i++ ){
+ Node prog = d_quant[0][i];
+ int rcons;
+ Node sol = getSolution( i, prog.getType(), rcons, false );
+ Trace("cegqi-nsi") << " solution for " << prog << " : " << sol << std::endl;
+ //make corresponding lambda
+ std::map< Node, Node >::iterator it_nso = d_nsi_op_map.find( prog );
+ if( it_nso!=d_nsi_op_map.end() ){
+ lams[it_nso->second] = sol;
+ }else{
+ Assert( false );
+ }
+ }
+
+ //now, we will check if this candidate solution satisfies the non-single-invocation portion of the specification
+ Node inst = d_sip->getSpecificationInst( 1, lams );
+ Trace("cegqi-nsi") << "NSI : specification instantiation : " << inst << std::endl;
+ inst = TermDb::simpleNegate( inst );
+ std::vector< Node > subs;
+ for( unsigned i=0; i<d_sip->d_all_vars.size(); i++ ){
+ subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) );
+ }
+ inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() );
+ Trace("cegqi-nsi") << "NSI : verification lemma : " << inst << std::endl;
+ lems.push_back( inst );
+ return;
+ }else{
+ //currently trying to construct candidate by refutation (by d_cinst->check below)
+ }
+ }else{
+ //should be assigned a SAT value
+ Assert( false );
+ }
+ }else if( !isFullySingleInvocation() ){
+ //create next candidate conjecture
+ Trace("cegqi-nsi") << "NSI : create next candidate conjecture..." << std::endl;
+ exit( 10 );
+ }
d_curr_lemmas.clear();
//call check for instantiator
d_cinst->check();
}
-Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
+Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus ){
Assert( d_sol!=NULL );
Assert( !d_lemmas_produced.empty() );
const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
Node varList = Node::fromExpr( dt.getSygusVarList() );
Node prog = d_quant[0][sol_index];
std::vector< Node > vars;
- bool success = true;
- Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
+ Node s;
if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
- success = false;
+ s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
}else{
+ Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
sol_index = d_prog_to_sol_index[prog];
- d_varList.clear();
d_sol->d_varList.clear();
Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() );
for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){
}else{
vars.push_back( d_single_inv_arg_sk[i] );
}
- d_varList.push_back( varList[i] );
d_sol->d_varList.push_back( varList[i] );
}
- }
- Trace("csi-sol") << std::endl;
+ Trace("csi-sol") << std::endl;
- //construct the solution
- Node s;
- if( success ){
+ //construct the solution
Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
Assert( d_lemmas_produced.size()==d_inst.size() );
std::vector< unsigned > indices;
std::sort( indices.begin(), indices.end(), ssii );
Trace("csi-sol") << "Construct solution" << std::endl;
s = constructSolution( indices, sol_index, 0 );
- s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
- d_orig_solution = s;
- }else{
- //function is unconstrained : make ground term of correct sort
- s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
+ s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
}
+ d_orig_solution = s;
//simplify the solution
Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
s = d_sol->simplifySolution( s, stn );
Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
- return reconstructToSyntax( s, stn, reconstructed );
+ return reconstructToSyntax( s, stn, reconstructed, rconsSygus );
}
-Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) {
+Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) {
d_solution = s;
const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
//reconstruct the solution into sygus if necessary
reconstructed = 0;
- if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() ){
+ if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus ){
d_sol->preregisterConjecture( d_orig_conjecture );
d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed );
if( reconstructed==1 ){
Trace("csi-sol") << "Post-process solution..." << std::endl;
Node prev = d_solution;
d_solution = postProcessSolution( d_solution );
- if( prev!=d_solution ){
+ if( prev!=d_solution ){
Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl;
}
}
}
Trace("cegqi-stats") << std::endl;
}
+ Node sol;
if( reconstructed==1 ){
- return d_sygus_solution;
+ sol = d_sygus_solution;
}else{
- return d_solution;
+ sol = d_solution;
+ }
+ //make into lambda
+ if( !dt.getSygusVarList().isNull() ){
+ Node varList = Node::fromExpr( dt.getSygusVarList() );
+ return NodeManager::currentNM()->mkNode( LAMBDA, varList, sol );
+ }else{
+ return sol;
}
}
Assert( d_si_vars.empty() );
d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() );
for( unsigned j=0; j<d_arg_types.size(); j++ ){
- Node si_v = NodeManager::currentNM()->mkBoundVar( d_arg_types[j] );
+ std::stringstream ss;
+ ss << "s_" << j;
+ Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] );
d_si_vars.push_back( si_v );
}
}
Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
//do DER on conjunct
Node cr = TermDb::getQuantSimplify( conj[i] );
- Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
+ if( cr!=conj[i] ){
+ Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
+ }
std::map< Node, bool > visited;
// functions to arguments
std::vector< Node > args;
}else{
Trace("si-prt") << "...not single invocation." << std::endl;
singleInvocation = false;
+ //rename bound variables with maximal overlap with si_vars
+ std::vector< Node > bvs;
+ TermDb::getBoundVars( cr, bvs );
+ std::vector< Node > terms;
+ std::vector< Node > subs;
+ for( unsigned j=0; j<bvs.size(); j++ ){
+ TypeNode tn = bvs[j].getType();
+ Trace("si-prt-debug") << "Fit bound var #" << j << " : " << bvs[j] << " with si." << std::endl;
+ for( unsigned k=0; k<d_si_vars.size(); k++ ){
+ if( tn==d_arg_types[k] ){
+ if( std::find( subs.begin(), subs.end(), d_si_vars[k] )==subs.end() ){
+ terms.push_back( bvs[j] );
+ subs.push_back( d_si_vars[k] );
+ Trace("si-prt-debug") << " ...use " << d_si_vars[k] << std::endl;
+ break;
+ }
+ }
+ }
+ }
+ cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
}
- Trace("si-prt") << "..... got si=" << singleInvocation << ", result : " << cr << std::endl;
+ cr = Rewriter::rewrite( cr );
+ Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl;
d_conjuncts[2].push_back( cr );
+ TermDb::getBoundVars( cr, d_all_vars );
if( singleInvocation ){
//replace with single invocation formulation
cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() );
- Trace("si-prt") << "..... si version=" << cr << std::endl;
+ cr = Rewriter::rewrite( cr );
+ Trace("si-prt") << ".....si version=" << cr << std::endl;
d_conjuncts[0].push_back( cr );
}else{
d_conjuncts[1].push_back( cr );
return true;
}
-bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
+bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
std::vector< Node >& terms, std::vector< Node >& subs ) {
std::map< Node, bool >::iterator it = visited.find( n );
if( it!=visited.end() ){
//arguments must be the same as those already recorded
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( args[i]!=n[i] ){
- Trace("si-prt-debug") << "... bad invocation : " << n << " at arg " << i << "." << std::endl;
+ Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl;
ret = false;
break;
}
}
Node SingleInvocationPartition::getConjunct( int index ) {
- return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) :
+ return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) :
( d_conjuncts[index].size()==1 ? d_conjuncts[index][0] : NodeManager::currentNM()->mkNode( AND, d_conjuncts[index] ) );
}
-void SingleInvocationPartition::extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts ) {
- if( n.getKind()==OR ){
+Node SingleInvocationPartition::getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ) {
+ std::map< Node, Node >::iterator it = visited.find( n );
+ if( it!=visited.end() ){
+ return it->second;
+ }else{
+ bool childChanged = false;
+ std::vector< Node > children;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- extractInvariant( n[i], func, pol, disjuncts );
+ Node nn = getSpecificationInst( n[i], lam, visited );
+ children.push_back( nn );
+ childChanged = childChanged || ( nn!=n[i] );
}
- }else{
- bool lit_pol = n.getKind()!=NOT;
- Node lit = n.getKind()==NOT ? n[0] : n;
- std::map< Node, Node >::iterator it = d_inv_to_func.find( lit );
- if( it!=d_inv_to_func.end() ){
- if( pol==-1 ){
- pol = lit_pol ? 0 : 1;
- func = it->second;
- }else{
- //mixing multiple invariants
- pol = -2;
+ Node ret;
+ if( n.getKind()==APPLY_UF ){
+ std::map< Node, Node >::iterator itl = lam.find( n.getOperator() );
+ if( itl!=lam.end() ){
+ Assert( itl->second[0].getNumChildren()==children.size() );
+ std::vector< Node > terms;
+ std::vector< Node > subs;
+ for( unsigned i=0; i<itl->second[0].getNumChildren(); i++ ){
+ terms.push_back( itl->second[0][i] );
+ subs.push_back( children[i] );
+ }
+ ret = itl->second[1].substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+ ret = Rewriter::rewrite( ret );
+ }
+ }
+ if( ret.isNull() ){
+ ret = n;
+ if( childChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ return ret;
+ }
+}
+
+Node SingleInvocationPartition::getSpecificationInst( int index, std::map< Node, Node >& lam ) {
+ Node conj = getConjunct( index );
+ std::map< Node, Node > visited;
+ return getSpecificationInst( conj, lam, visited );
+}
+
+void SingleInvocationPartition::extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts ) {
+ std::map< Node, bool > visited;
+ extractInvariant2( n, func, pol, disjuncts, true, visited );
+}
+
+void SingleInvocationPartition::extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited ) {
+ if( visited.find( n )==visited.end() && pol!=-2 ){
+ Trace("cegqi-inv-debug2") << "Extract : " << n << " " << hasPol << ", pol = " << pol << std::endl;
+ visited[n] = true;
+ if( n.getKind()==OR && hasPol ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ extractInvariant2( n[i], func, pol, disjuncts, true, visited );
}
}else{
- disjuncts.push_back( n );
+ if( hasPol ){
+ bool lit_pol = n.getKind()!=NOT;
+ Node lit = n.getKind()==NOT ? n[0] : n;
+ std::map< Node, Node >::iterator it = d_inv_to_func.find( lit );
+ if( it!=d_inv_to_func.end() ){
+ if( pol==-1 ){
+ pol = lit_pol ? 0 : 1;
+ func = it->second;
+ }else{
+ //mixing multiple invariants
+ pol = -2;
+ }
+ return;
+ }else{
+ disjuncts.push_back( n );
+ }
+ }
+ //if another part mentions UF or a free variable, then fail
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ if( d_funcs.find( op )!=d_funcs.end() ){
+ pol = -2;
+ return;
+ }
+ }else if( n.getKind()==BOUND_VARIABLE && std::find( d_si_vars.begin(), d_si_vars.end(), n )==d_si_vars.end() ){
+ pol = -2;
+ return;
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ extractInvariant2( n[i], func, pol, disjuncts, false, visited );
+ }
}
}
}
CegConjectureSingleInvSol * d_sol;
//the instantiator
CegInstantiator * d_cinst;
- //for recognizing when conjecture is single invocation
- bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
- std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
- std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol );
- bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
- bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
- bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
- bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
//for recognizing templates for invariant synthesis
- int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol );
Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
// partially single invocation
Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited );
Node addDeepEmbedding( Node n, std::map< Node, Node >& visited );
+ //initialize next candidate si conjecture
+ void initializeNextSiConjecture();
//presolve
void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
Node postProcessSolution( Node n );
private:
- //map from programs to variables in single invocation property
- std::map< Node, Node > d_single_inv_map;
- std::map< Node, Node > d_single_inv_map_to_prog;
- //map from programs to evaluator term representing the above variable
- std::map< Node, Node > d_single_inv_app_map;
//list of skolems for each argument of programs
std::vector< Node > d_single_inv_arg_sk;
//list of variables/skolems for each program
//original conjecture
Node d_orig_conjecture;
// solution
- std::vector< Node > d_varList;
Node d_orig_solution;
Node d_solution;
Node d_sygus_solution;
CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
// original conjecture
Node d_quant;
- // single invocation version of quantified formula
+ // single invocation portion of quantified formula
Node d_single_inv;
+ // non-single invocation portion of quantified formula
+ Node d_nsingle_inv;
+ // full version quantified formula
+ Node d_full_inv;
+ // current guard
+ Node d_ns_guard;
// transition relation version per program
std::map< Node, Node > d_trans_pre;
std::map< Node, Node > d_trans_post;
std::map< Node, Node > d_prog_to_eval_op;
public:
//get the single invocation lemma(s)
- void getSingleInvLemma( Node guard, std::vector< Node >& lems );
+ void getInitialSingleInvLemma( Node guard, std::vector< Node >& lems );
//initialize
void initialize( Node q );
//check
void check( std::vector< Node >& lems );
//get solution
- Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+ Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true );
//reconstruct to syntax
- Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed );
+ Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true );
// has ites
bool hasITEs() { return d_has_ites; }
// is single invocation
bool isSingleInvocation() { return !d_single_inv.isNull(); }
+ // is single invocation
+ bool isFullySingleInvocation() { return d_nsingle_inv.isNull(); }
//needs check
bool needsCheck();
/** preregister conjecture */
};
// partitions any formulas given to it into single invocation/non-single invocation
-// only processes functions having argument types exactly matching "d_arg_types",
+// only processes functions having argument types exactly matching "d_arg_types",
// and all invocations are in the same order across all functions
class SingleInvocationPartition
{
private:
bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj );
- bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
+ bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
std::vector< Node >& terms, std::vector< Node >& subs );
- std::map< Node, Node > d_inv_to_func;
- std::map< Node, Node > d_fo_var_to_func;
+ Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited );
+ void extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited );
public:
void init( std::vector< TypeNode >& typs );
//inputs
void process( Node n );
std::vector< TypeNode > d_arg_types;
-
+
//outputs (everything is with bound var)
std::map< Node, bool > d_funcs;
std::map< Node, Node > d_func_inv;
+ std::map< Node, Node > d_inv_to_func;
std::map< Node, Node > d_func_fo_var;
- std::vector< Node > d_func_vars;
- std::vector< Node > d_si_vars;
+ std::map< Node, Node > d_fo_var_to_func;
+ std::vector< Node > d_func_vars; //the first-order variables corresponding to all functions
+ std::vector< Node > d_si_vars; //the arguments that we based the anti-skolemization on
+ std::vector< Node > d_all_vars; //every free variable of conjuncts[2]
// si, nsi, all
std::vector< Node > d_conjuncts[3];
-
+
bool isAntiSkolemizableType( Node f );
-
+
Node getConjunct( int index );
Node getSingleInvocation() { return getConjunct( 0 ); }
Node getNonSingleInvocation() { return getConjunct( 1 ); }
Node getFullSpecification() { return getConjunct( 2 ); }
-
+
+ Node getSpecificationInst( int index, std::map< Node, Node >& lam );
+
void extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts );
-
+
void debugPrint( const char * c );
};
projects / cvc5.git / commitdiff