From 8deb9d980d7b0e281a0190539b756896a487c451 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 2 Feb 2015 17:42:31 +0100 Subject: [PATCH] Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes. --- src/Makefile.am | 2 + src/smt/smt_engine.cpp | 3 + src/theory/datatypes/datatypes_sygus.cpp | 136 ++-- src/theory/datatypes/datatypes_sygus.h | 3 +- src/theory/datatypes/theory_datatypes.cpp | 3 +- src/theory/quantifiers/bounded_integers.cpp | 15 +- .../quantifiers/ce_guided_instantiation.cpp | 446 +++----------- .../quantifiers/ce_guided_instantiation.h | 135 ++-- .../quantifiers/ce_guided_single_inv.cpp | 581 ++++++++++++++++++ src/theory/quantifiers/ce_guided_single_inv.h | 80 +++ src/theory/quantifiers/options | 7 +- src/theory/quantifiers/quant_util.cpp | 19 +- src/theory/quantifiers/quant_util.h | 1 + 13 files changed, 937 insertions(+), 494 deletions(-) create mode 100644 src/theory/quantifiers/ce_guided_single_inv.cpp create mode 100644 src/theory/quantifiers/ce_guided_single_inv.h diff --git a/src/Makefile.am b/src/Makefile.am index 184ef5d56..4ae3c16f8 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -327,6 +327,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/conjecture_generator.cpp \ theory/quantifiers/ce_guided_instantiation.h \ theory/quantifiers/ce_guided_instantiation.cpp \ + theory/quantifiers/ce_guided_single_inv.h \ + theory/quantifiers/ce_guided_single_inv.cpp \ theory/quantifiers/local_theory_ext.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/fun_def_process.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0be445f57..3aec77a45 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1346,6 +1346,9 @@ void SmtEngine::setDefaults() { } //apply counterexample guided instantiation options + if( options::cegqiSingleInv() ){ + options::ceGuidedInst.set( true ); + } if( options::ceGuidedInst() ){ if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 5e42ac302..4946e25f9 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -52,7 +52,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > Assert( pdt.isSygus() ); csIndex = Datatype::cindexOf(selectorExpr); sIndex = Datatype::indexOf(selectorExpr); - TypeNode tnnp = n[0].getType(); + tnnp = n[0].getType(); //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex ); @@ -88,17 +88,33 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > //check if we can strengthen the first argument if( !arg1.isNull() ){ const Datatype& dt1 = ((DatatypeType)(tn1).toType()).getDatatype(); + Kind k = d_util->getArgKind( tnnp, csIndex ); + //size comparison for arguments (if necessary) + Node sz_leq; + if( tn1==tnn && d_util->isComm( k ) ){ + sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) ); + } std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i ); if( it!=d_sygus_pc_arg_pos[tnn][csIndex].end() ){ Assert( !it->second.empty() ); std::vector< Node > lem_c; for( unsigned j=0; jsecond.size(); j++ ){ - lem_c.push_back( DatatypesRewriter::mkTester( arg1, it->second[j], dt1 ) ); + Node tt = DatatypesRewriter::mkTester( arg1, it->second[j], dt1 ); + //if commutative operator, and children have same constructor type, then first arg is larger than second arg + if( it->second[j]==(int)i && !sz_leq.isNull() ){ + tt = NodeManager::currentNM()->mkNode( AND, tt, sz_leq ); + } + lem_c.push_back( tt ); } Node argStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c ); Trace("sygus-str") << "...strengthen corresponding first argument of " << test << " : " << argStr << std::endl; test_c.push_back( argStr ); narrow = true; + }else{ + if( !sz_leq.isNull() ){ + test_c.push_back( NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( arg1, i, dt1 ).negate(), sz_leq ) ); + narrow = true; + } } } //other constraints on arguments @@ -282,6 +298,18 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre ); addSplit = !isGenericRedundant( tnnp, g ); } + /* + else{ + Trace("sygus-nf-temp") << "Check " << dt[i].getName() << " as argument " << sIndex << " under " << parentKind << std::endl; + std::map< int, Node > prec; + std::map< TypeNode, int > var_count; + Node gc = d_util->mkGeneric( dt, i, var_count, prec ); + std::map< int, Node > pre; + pre[sIndex] = gc; + Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre ); + bool tmp = !isGenericRedundant( tnnp, g, false ); + } + */ } } d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit ); @@ -394,7 +422,6 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt } Kind nk = UNDEFINED_KIND; Kind reqk = UNDEFINED_KIND; //required kind for all children - std::map< int, Kind > reqk_arg; //TODO if( parent==NOT ){ if( k==AND ) { nk = OR;reqk = NOT; @@ -436,52 +463,51 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt int pcr = d_util->getKindArg( tnp, nk ); if( pcr!=-1 ){ Assert( pcr<(int)pdt.getNumConstructors() ); - //must have same number of arguments - if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){ - bool success = true; - std::map< int, TypeNode > childTypes; - for( unsigned i=0; igetKindArg( tna, reqk ); - if( nindex!=-1 ){ - const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype(); - childTypes[i] = getArgType( adt[nindex], 0 ); - }else{ - Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl; - success = false; - break; - } - }else{ - childTypes[i] = tna; - } - } - if( success ){ - //children types of reduced operator must match types of original + if( reqk!=UNDEFINED_KIND ){ + //must have same number of arguments + if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){ + bool success = true; + std::map< int, TypeNode > childTypes; for( unsigned i=0; igetKindArg( tna, reqk ); + if( nindex!=-1 ){ + const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype(); + if( getArgType( dt[c], i )!=getArgType( adt[nindex], 0 ) ){ + Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl; + success = false; + break; + } + }else{ + Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl; + success = false; + break; + } + }else{ + childTypes[i] = tna; } } - if( !success ){ - //check based on commutativity TODO - } if( success ){ Trace("sygus-split-debug") << "...success" << std::endl; return false; } + }else{ + Trace("sygus-split-debug") << "...#arg mismatch." << std::endl; } }else{ - Trace("sygus-split-debug") << "...#arg mismatch." << std::endl; + return !isTypeMatch( pdt[pcr], dt[c] ); } }else{ Trace("sygus-split-debug") << "...operator not available." << std::endl; } } + } + if( parent==MINUS || parent==BITVECTOR_SUB ){ + + } return true; } @@ -575,25 +601,37 @@ bool SygusSplit::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConst } } -bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) { +bool SygusSplit::isGenericRedundant( TypeNode tn, Node g, bool active ) { //everything added to this cache should be mutually exclusive cases std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g ); if( it==d_gen_redundant[tn].end() ){ Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl; Node gr = d_util->getNormalized( tn, g, false ); Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl; - std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr ); - bool red = true; - if( itg==d_gen_terms[tn].end() ){ - red = false; - d_gen_terms[tn][gr] = g; - Trace("sygus-gnf-debug") << "...not redundant." << std::endl; + if( active ){ + std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr ); + bool red = true; + if( itg==d_gen_terms[tn].end() ){ + red = false; + d_gen_terms[tn][gr] = g; + d_gen_terms_inactive[tn][gr] = g; + Trace("sygus-gnf-debug") << "...not redundant." << std::endl; + }else{ + Trace("sygus-gnf-debug") << "...redundant." << std::endl; + Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl; + } + d_gen_redundant[tn][g] = red; + return red; }else{ - Trace("sygus-gnf-debug") << "...redundant." << std::endl; - Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl; + std::map< Node, Node >::iterator itg = d_gen_terms_inactive[tn].find( gr ); + if( itg==d_gen_terms_inactive[tn].end() ){ + Trace("sygus-nf-temp") << "..." << g << " rewrites to " << gr << std::endl; + d_gen_terms_inactive[tn][gr] = g; + }else{ + Trace("sygus-nf-temp") << "* Note " << g << " and " << itg->second << " both rewrite to " << gr << std::endl; + } + return false; } - d_gen_redundant[tn][g] = red; - return red; }else{ return it->second; } @@ -1064,10 +1102,10 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node }else{ Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl; } - return false; - }else{ - return true; + //for now, continue adding lemmas (since we are not forcing conflicts) + //return false; } + return true; } bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index e1188d5c9..b694bbe9c 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -45,6 +45,7 @@ private: std::map< TypeNode, TypeNode > d_register; //stores sygus type // type to (rewritten) to original std::map< TypeNode, std::map< Node, Node > > d_gen_terms; + std::map< TypeNode, std::map< Node, Node > > d_gen_terms_inactive; std::map< TypeNode, std::map< Node, bool > > d_gen_redundant; private: /** register sygus type */ @@ -64,7 +65,7 @@ private: bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ); private: // generic cache - bool isGenericRedundant( TypeNode tn, Node g ); + bool isGenericRedundant( TypeNode tn, Node g, bool active = true ); public: SygusSplit( SygusUtil * util ) : d_util( util ) {} /** get sygus splits */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c73ec8039..8d1ebd4fa 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -984,7 +984,8 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ }else{ //check if we have reached the maximum number of testers // in this case, add the positive tester - if( lbl->size()==dt.getNumConstructors()-1 ){ + //this should not be done for sygus, since cases may be limited + if( lbl->size()==dt.getNumConstructors()-1 && !dt.isSygus() ){ std::vector< bool > pcons; getPossibleCons( eqc, n, pcons ); int testerIndex = -1; diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 91c04bc80..dda3b1be4 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -179,20 +179,7 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, std::map< Node, Node > msum; if (QuantArith::getMonomialSumLit( lit, msum )){ Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; - for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Trace("bound-int-debug") << " "; - if( !it->second.isNull() ){ - Trace("bound-int-debug") << it->second; - if( !it->first.isNull() ){ - Trace("bound-int-debug") << " * "; - } - } - if( !it->first.isNull() ){ - Trace("bound-int-debug") << it->first; - } - Trace("bound-int-debug") << std::endl; - } - Trace("bound-int-debug") << std::endl; + QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" ); for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){ Node veq; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index a64362c14..addcd5337 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -29,21 +29,12 @@ using namespace std; namespace CVC4 { -void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { - if( n.getKind()==OR ){ - for( unsigned i=0; iinitialize(); } }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ d_syntax_guided = false; @@ -78,282 +70,7 @@ void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } - - -void CegInstantiation::CegConjecture::analyzeSygusConjecture() { - Node q = d_quant; - // conj -> conj* - std::map< Node, std::vector< Node > > children; - // conj X prog -> inv* - std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke; - std::vector< Node > progs; - std::map< Node, std::map< Node, bool > > contains; - for( unsigned i=0; i > invocations; - std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args; - std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from; - for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ - for( unsigned j=0; jsecond.size(); j++ ){ - Node conj = it->second[j]; - Trace("cegqi-analyze-debug") << "Process child " << conj << " from " << it->first << std::endl; - std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj ); - if( itp!=prog_invoke.end() ){ - for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( it2->second.size()>1 ){ - singleInvocation = false; - break; - }else if( it2->second.size()==1 ){ - Node prog = it2->first; - Node inv = it2->second[0]; - Assert( inv[0]==prog ); - invocations[prog].push_back( inv ); - for( unsigned k=1; k pbvs; - std::vector< Node > new_vars; - std::map< Node, std::vector< Node > > new_assumptions; - for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ - Assert( !it->second.empty() ); - Node prog = it->first; - Node inv = it->second[0]; - std::vector< Node > invc; - invc.push_back( inv.getOperator() ); - invc.push_back( prog ); - Node pv = NodeManager::currentNM()->mkBoundVar( "F", inv.getType() ); - d_single_inv_map[prog] = pv; - d_single_inv_map_to_prog[pv] = prog; - pbvs.push_back( pv ); - Trace("cegqi-analyze-debug2") << "Make variable " << pv << " for " << prog << std::endl; - for( unsigned k=1; kmkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); - new_vars.push_back( v ); - invc.push_back( v ); - - for( unsigned i=0; imkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate(); - Trace("cegqi-analyze-debug") << " ..." << arg << " occurs in "; - Trace("cegqi-analyze-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl; - for( unsigned j=0; jmkNode( APPLY_UF, invc ); - Trace("cegqi-analyze") << " " << prog << " -> " << sinv << std::endl; - d_single_inv_app_map[prog] = sinv; - } - //construct the single invocation version of the property - Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl; - //std::vector< Node > si_conj; - Assert( !pbvs.empty() ); - Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); - for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ - //should hold since we prevent miniscoping - Assert( d_single_inv.isNull() ); - std::vector< Node > tmp; - for( unsigned i=0; isecond.size(); i++ ){ - Node c = it->second[i]; - std::vector< Node > disj; - //insert new assumptions - disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() ); - //get replaced version - Node cr; - std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c ); - if( itp!=prog_invoke.end() ){ - std::vector< Node > terms; - std::vector< Node > subs; - for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( !it2->second.empty() ){ - Node prog = it2->first; - Node inv = it2->second[0]; - Assert( it2->second.size()==1 ); - terms.push_back( inv ); - subs.push_back( d_single_inv_map[prog] ); - Trace("cegqi-analyze-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; - } - } - cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - }else{ - cr = c; - } - if( cr.getKind()==OR ){ - for( unsigned j=0; jmkNode( OR, disj ); - Trace("cegqi-analyze") << " " << curr; - tmp.push_back( curr.negate() ); - if( !it->first.isNull() ){ - Trace("cegqi-analyze-debug") << " under " << it->first; - } - Trace("cegqi-analyze") << std::endl; - } - Assert( !tmp.empty() ); - Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( OR, tmp ); - if( !it->first.isNull() ){ - // apply substitution for skolem variables - std::vector< Node > vars; - d_single_inv_arg_sk.clear(); - for( unsigned j=0; jfirst.getNumChildren(); j++ ){ - std::stringstream ss; - ss << "k_" << it->first[j]; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); - vars.push_back( it->first[j] ); - d_single_inv_arg_sk.push_back( v ); - } - bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); - - Trace("cegqi-analyze-debug") << " -> " << bd << std::endl; - } - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); - //equality resolution - for( unsigned j=0; j > case_vals; - bool exh = processSingleInvLiteral( conj, false, case_vals ); - Trace("cegqi-analyze-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){ - Trace("cegqi-analyze-er") << " " << it->first << " -> "; - for( unsigned k=0; ksecond.size(); k++ ){ - Trace("cegqi-analyze-er") << it->second[k] << " "; - } - Trace("cegqi-analyze-er") << std::endl; - } - - } - } - Trace("cegqi-analyze-debug") << "...formula is : " << d_single_inv << std::endl; - }else{ - Trace("cegqi-analyze") << "Property is not single invocation." << std::endl; - } - } -} - -bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) { - if( lit.getKind()==NOT ){ - return processSingleInvLiteral( lit[0], !pol, case_vals ); - }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){ - bool exh = true; - for( unsigned k=0; k::iterator it = d_single_inv_map_to_prog.find( lit[r] ); - if( it!=d_single_inv_map_to_prog.end() ){ - if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){ - case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] ); - return true; - } - } - } - } - } - return false; -} - -bool CegInstantiation::CegConjecture::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 >::iterator it = prog_invoke[n].find( progs[i] ); - Trace("cegqi-analyze") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl; - for( unsigned j=0; jsecond.size(); j++ ){ - Trace("cegqi-analyze") << " " << it->second[j] << std::endl; - } - } - return success; - } - return true; -} - -bool CegInstantiation::CegConjecture::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; imkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); //specify guard behavior @@ -365,30 +82,21 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() ); Trace("cegqi") << "Add candidate lemma : " << lem << std::endl; qe->getOutputChannel().lemma( lem ); - }else if( !d_single_inv.isNull() ){ - Assert( d_single_inv.getKind()==FORALL ); - std::vector< Node > vars; - d_single_inv_sk.clear(); - for( unsigned i=0; imkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); - vars.push_back( d_single_inv[0][i] ); - d_single_inv_sk.push_back( k ); - } - Node inst = d_single_inv[1].substitute( vars.begin(), vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), inst.negate() ); - Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); - if( Trace.isOn("cegqi-debug") ){ - lem = Rewriter::rewrite( lem ); - Trace("cegqi-debug") << "...rewritten : " << lem << std::endl; + }else if( d_ceg_si ){ + Node lem = d_ceg_si->getSingleInvLemma( d_guard ); + if( !lem.isNull() ){ + Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl; + qe->getOutputChannel().lemma( lem ); + if( Trace.isOn("cegqi-debug") ){ + lem = Rewriter::rewrite( lem ); + Trace("cegqi-debug") << "...rewritten : " << lem << std::endl; + } } } } } -Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { +Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { if( d_measure_term.isNull() ){ return Node::null(); }else{ @@ -424,6 +132,7 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ d_conj = new CegConjecture( d_quantEngine->getSatContext() ); + d_last_inst_si = false; } bool CegInstantiation::needsCheck( Theory::Effort e ) { @@ -544,59 +253,72 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( conj->d_ce_sk.empty() ){ Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; if( getTermDatabase()->isQAttrSygus( q ) ){ - + if( conj->d_ceg_si ){ + std::vector< Node > lems; + conj->d_ceg_si->check( d_quantEngine, lems ); + if( !lems.empty() ){ + d_last_inst_si = true; + for( unsigned j=0; jaddLemma( lems[j] ); + } + Trace("cegqi-engine") << " ...try single invocation." << std::endl; + return; + } + } std::vector< Node > model_values; if( getModelValues( conj, conj->d_candidates, model_values ) ){ //check if we must apply fairness lemmas - std::vector< Node > lems; if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){ + std::vector< Node > lems; for( unsigned j=0; jd_candidates.size(); j++ ){ getMeasureLemmas( conj->d_candidates[j], model_values[j], lems ); } - } - if( !lems.empty() ){ - for( unsigned j=0; jaddLemma( lems[j] ); - } - Trace("cegqi-engine") << " ...refine size." << std::endl; - }else{ - //must get a counterexample to the value of the current candidate - Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); - //check whether we will run CEGIS on inner skolem variables - bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 ); - if( sk_refine ){ - conj->d_ce_sk.push_back( std::vector< Node >() ); + if( !lems.empty() ){ + for( unsigned j=0; jaddLemma( lems[j] ); + } + Trace("cegqi-engine") << " ...refine size." << std::endl; + return; } - std::vector< Node > ic; - ic.push_back( q.negate() ); - std::vector< Node > d; - collectDisjuncts( inst, d ); - Assert( d.size()==conj->d_base_disj.size() ); - //immediately skolemize inner existentials - for( unsigned i=0; igetSkolemizedBody( dr[0] ).negate() ); - if( sk_refine ){ - conj->d_ce_sk.back().push_back( dr[0] ); - } - }else{ - ic.push_back( dr ); - if( sk_refine ){ - conj->d_ce_sk.back().push_back( Node::null() ); - } - if( !conj->d_inner_vars_disj[i].empty() ){ - Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; - } + } + //must get a counterexample to the value of the current candidate + Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); + //check whether we will run CEGIS on inner skolem variables + bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 ); + if( sk_refine ){ + conj->d_ce_sk.push_back( std::vector< Node >() ); + } + std::vector< Node > ic; + ic.push_back( q.negate() ); + std::vector< Node > d; + collectDisjuncts( inst, d ); + Assert( d.size()==conj->d_base_disj.size() ); + //immediately skolemize inner existentials + for( unsigned i=0; igetSkolemizedBody( dr[0] ).negate() ); + if( sk_refine ){ + conj->d_ce_sk.back().push_back( dr[0] ); + } + }else{ + ic.push_back( dr ); + if( sk_refine ){ + conj->d_ce_sk.back().push_back( Node::null() ); + } + if( !conj->d_inner_vars_disj[i].empty() ){ + Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; } } - Node lem = NodeManager::currentNM()->mkNode( OR, ic ); - lem = Rewriter::rewrite( lem ); - Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->addLemma( lem ); - Trace("cegqi-engine") << " ...find counterexample." << std::endl; } + Node lem = NodeManager::currentNM()->mkNode( OR, ic ); + lem = Rewriter::rewrite( lem ); + d_last_inst_si = false; + Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem ); + Trace("cegqi-engine") << " ...find counterexample." << std::endl; } }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ @@ -768,10 +490,16 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Assert( dt.isSygus() ); out << dt.getSygusVarList() << " "; out << dt.getSygusType() << " "; - if( d_conj->d_candidate_inst[i].empty() ){ - out << "?"; + if( d_last_inst_si ){ + Assert( d_conj->d_ceg_si ); + Node sol = d_conj->d_ceg_si->getSolution( i, Node::fromExpr( dt.getSygusVarList() ) ); + out << sol; }else{ - printSygusTerm( out, d_conj->d_candidate_inst[i].back() ); + if( d_conj->d_candidate_inst[i].empty() ){ + out << "?"; + }else{ + printSygusTerm( out, d_conj->d_candidate_inst[i].back() ); + } } out << ")" << std::endl; } @@ -802,4 +530,14 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) { out << n; } +void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { + if( n.getKind()==OR ){ + for( unsigned i=0; i d_active; + /** is conjecture infeasible */ + context::CDO< bool > d_infeasible; + /** quantified formula */ + Node d_quant; + /** guard */ + Node d_guard; + /** base instantiation */ + Node d_base_inst; + /** expand base inst to disjuncts */ + std::vector< Node > d_base_disj; + /** guard split */ + Node d_guard_split; + /** is syntax-guided */ + bool d_syntax_guided; + /** list of constants for quantified formula */ + std::vector< Node > d_candidates; + /** list of variables on inner quantification */ + std::vector< Node > d_inner_vars; + std::vector< std::vector< Node > > d_inner_vars_disj; + /** list of terms we have instantiated candidates with */ + std::map< int, std::vector< Node > > d_candidate_inst; + /** initialize guard */ + void initializeGuard( QuantifiersEngine * qe ); + /** measure term */ + Node d_measure_term; + /** measure sum size */ + int d_measure_term_size; + /** refine count */ + unsigned d_refine_count; + /** assign */ + void assign( QuantifiersEngine * qe, Node q ); + /** is assigned */ + bool isAssigned() { return !d_quant.isNull(); } + /** current extential quantifeirs whose couterexamples we must refine */ + std::vector< std::vector< Node > > d_ce_sk; + /** single invocation utility */ + CegConjectureSingleInv * d_ceg_si; +public: //for fairness + /** the cardinality literals */ + std::map< int, Node > d_lits; + /** current cardinality */ + context::CDO< int > d_curr_lit; + /** allocate literal */ + Node getLiteral( QuantifiersEngine * qe, int i ); + /** is ground */ + bool isGround() { return d_inner_vars.empty(); } +}; + + class CegInstantiation : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; private: - /** collect disjuncts */ - static void collectDisjuncts( Node n, std::vector< Node >& ex ); - /** a synthesis conjecture */ - class CegConjecture { - public: - CegConjecture( context::Context* c ); - /** is conjecture active */ - context::CDO< bool > d_active; - /** is conjecture infeasible */ - context::CDO< bool > d_infeasible; - /** quantified formula */ - Node d_quant; - /** guard */ - Node d_guard; - /** base instantiation */ - Node d_base_inst; - /** expand base inst to disjuncts */ - std::vector< Node > d_base_disj; - /** guard split */ - Node d_guard_split; - /** is syntax-guided */ - bool d_syntax_guided; - /** list of constants for quantified formula */ - std::vector< Node > d_candidates; - /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; - std::vector< std::vector< Node > > d_inner_vars_disj; - /** list of terms we have instantiated candidates with */ - std::map< int, std::vector< Node > > d_candidate_inst; - /** initialize guard */ - void initializeGuard( QuantifiersEngine * qe ); - /** measure term */ - Node d_measure_term; - /** measure sum size */ - int d_measure_term_size; - /** refine count */ - unsigned d_refine_count; - /** assign */ - void assign( QuantifiersEngine * qe, Node q ); - /** is assigned */ - bool isAssigned() { return !d_quant.isNull(); } - /** current extential quantifeirs whose couterexamples we must refine */ - std::vector< std::vector< Node > > d_ce_sk; - private: //for single invocation - void analyzeSygusConjecture(); - 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 ); - public: - Node d_single_inv; - //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 skolems for each program - std::vector< Node > d_single_inv_sk; - public: //for fairness - /** the cardinality literals */ - std::map< int, Node > d_lits; - /** current cardinality */ - context::CDO< int > d_curr_lit; - /** allocate literal */ - Node getLiteral( QuantifiersEngine * qe, int i ); - /** is ground */ - bool isGround() { return d_inner_vars.empty(); } - }; /** the quantified formula stating the synthesis conjecture */ CegConjecture * d_conj; + /** last instantiation by single invocation module? */ + bool d_last_inst_si; private: //for enforcing fairness /** measure functions */ std::map< TypeNode, Node > d_uf_measure; @@ -143,6 +130,8 @@ public: std::string identify() const { return "CegInstantiation"; } /** print solution for synthesis conjectures */ void printSynthSolution( std::ostream& out ); + /** collect disjuncts */ + static void collectDisjuncts( Node n, std::vector< Node >& ex ); }; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp new file mode 100644 index 000000000..efe23d6cb --- /dev/null +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -0,0 +1,581 @@ +/********************* */ +/*! \file ce_guided_single_inv.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief utility for processing single invocation synthesis conjectures + ** + **/ + +#include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/datatypes/datatypes_rewriter.h" +#include "util/datatype.h" +#include "theory/quantifiers/quant_util.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace std; + +namespace CVC4 { + +CegConjectureSingleInv::CegConjectureSingleInv( Node q, CegConjecture * p ) : d_parent( p ), d_quant( q ){ + +} + +Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { + if( !d_single_inv.isNull() ) { + Assert( d_single_inv.getKind()==FORALL ); + d_single_inv_var.clear(); + d_single_inv_sk.clear(); + for( unsigned i=0; imkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); + d_single_inv_var.push_back( d_single_inv[0][i] ); + d_single_inv_sk.push_back( k ); + d_single_inv_sk_index[k] = i; + } + Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; + return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst.negate() ); + }else{ + return Node::null(); + } +} + +void CegConjectureSingleInv::initialize() { + Node q = d_quant; + Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl; + // conj -> conj* + std::map< Node, std::vector< Node > > children; + // conj X prog -> inv* + std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke; + std::vector< Node > progs; + std::map< Node, std::map< Node, bool > > contains; + for( unsigned i=0; i > invocations; + std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args; + std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from; + for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ + for( unsigned j=0; jsecond.size(); j++ ){ + Node conj = it->second[j]; + Trace("cegqi-si-debug") << "Process child " << conj << " from " << it->first << std::endl; + std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj ); + if( itp!=prog_invoke.end() ){ + for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ + if( it2->second.size()>1 ){ + singleInvocation = false; + break; + }else if( it2->second.size()==1 ){ + Node prog = it2->first; + Node inv = it2->second[0]; + Assert( inv[0]==prog ); + invocations[prog].push_back( inv ); + for( unsigned k=1; k pbvs; + std::vector< Node > new_vars; + std::map< Node, std::vector< Node > > new_assumptions; + for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ + Assert( !it->second.empty() ); + Node prog = it->first; + Node inv = it->second[0]; + std::vector< Node > invc; + invc.push_back( inv.getOperator() ); + invc.push_back( prog ); + std::stringstream ss; + ss << "F_" << prog; + Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() ); + d_single_inv_map[prog] = pv; + d_single_inv_map_to_prog[pv] = prog; + pbvs.push_back( pv ); + Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl; + for( unsigned k=1; kmkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); + new_vars.push_back( v ); + invc.push_back( v ); + + for( unsigned i=0; imkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate(); + Trace("cegqi-si-debug") << " ..." << arg << " occurs in "; + Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl; + for( unsigned j=0; jmkNode( APPLY_UF, invc ); + Trace("cegqi-si") << " " << prog << " -> " << sinv << std::endl; + d_single_inv_app_map[prog] = sinv; + } + //construct the single invocation version of the property + Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl; + //std::vector< Node > si_conj; + Assert( !pbvs.empty() ); + Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ + //should hold since we prevent miniscoping + Assert( d_single_inv.isNull() ); + std::vector< Node > tmp; + for( unsigned i=0; isecond.size(); i++ ){ + Node c = it->second[i]; + std::vector< Node > disj; + //insert new assumptions + disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() ); + //get replaced version + Node cr; + std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c ); + if( itp!=prog_invoke.end() ){ + std::vector< Node > terms; + std::vector< Node > subs; + for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ + if( !it2->second.empty() ){ + Node prog = it2->first; + Node inv = it2->second[0]; + Assert( it2->second.size()==1 ); + terms.push_back( inv ); + subs.push_back( d_single_inv_map[prog] ); + Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; + } + } + cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + }else{ + cr = c; + } + if( cr.getKind()==OR ){ + for( unsigned j=0; jmkNode( OR, disj ); + Trace("cegqi-si") << " " << curr; + tmp.push_back( curr.negate() ); + if( !it->first.isNull() ){ + Trace("cegqi-si-debug") << " under " << it->first; + } + Trace("cegqi-si") << std::endl; + } + Assert( !tmp.empty() ); + Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( OR, tmp ); + if( !it->first.isNull() ){ + // apply substitution for skolem variables + std::vector< Node > vars; + d_single_inv_arg_sk.clear(); + for( unsigned j=0; jfirst.getNumChildren(); j++ ){ + std::stringstream ss; + ss << "k_" << it->first[j]; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); + vars.push_back( it->first[j] ); + d_single_inv_arg_sk.push_back( v ); + } + bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); + + Trace("cegqi-si-debug") << " -> " << bd << std::endl; + } + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + //equality resolution + for( unsigned j=0; j > case_vals; + bool exh = processSingleInvLiteral( conj, false, case_vals ); + Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){ + Trace("cegqi-si-er") << " " << it->first << " -> "; + for( unsigned k=0; ksecond.size(); k++ ){ + Trace("cegqi-si-er") << it->second[k] << " "; + } + Trace("cegqi-si-er") << std::endl; + } + + } + } + Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; + }else{ + Trace("cegqi-si") << "Property is not single invocation." << std::endl; + if( options::cegqiSingleInvAbort() ){ + Message() << "Property is not single invocation." << std::endl; + exit( 0 ); + } + } + } +} + +bool CegConjectureSingleInv::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) { + if( lit.getKind()==NOT ){ + return processSingleInvLiteral( lit[0], !pol, case_vals ); + }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){ + bool exh = true; + for( unsigned k=0; k::iterator it = d_single_inv_map_to_prog.find( lit[r] ); + if( it!=d_single_inv_map_to_prog.end() ){ + if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){ + case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] ); + return true; + } + } + } + } + } + return false; +} + +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 >::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; jsecond.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& lems ) { + if( !d_single_inv.isNull() ) { + eq::EqualityEngine* ee = qe->getMasterEqualityEngine(); + Trace("cegqi-engine") << " * single invocation: " << std::endl; + std::vector< Node > subs; + std::map< Node, int > subs_from_model; + std::vector< Node > waiting_to_slv; + for( unsigned i=0; i "; + Node slv; + if( ee->hasTerm( pv ) ){ + Node r = ee->getRepresentative( pv ); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + bool isWaitingSlv = false; + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + if( n!=pv ){ + if( slv.isNull() || isWaitingSlv ){ + std::vector< Node > vars; + collectProgVars( n, vars ); + if( slv.isNull() || vars.empty() ){ + // n cannot contain pv + bool isLoop = std::find( vars.begin(), vars.end(), pv )!=vars.end(); + if( !isLoop ){ + for( unsigned j=0; jgetModel()->getValue( pv ); + subs.push_back( mv ); + subs_from_model[pv] = i; + if( Trace.isOn("cegqi-engine") || Trace.isOn("cegqi-engine-debug") ){ + Trace("cegqi-engine") << "M:" << mv; + } + }else{ + subs.push_back( slv ); + Trace("cegqi-engine") << slv; + } + Trace("cegqi-engine") << std::endl; + } + for( int i=(int)(waiting_to_slv.size()-1); i>=0; --i ){ + int index = d_single_inv_sk_index[waiting_to_slv[i]]; + Trace("cegqi-engine-debug") << "Go back and solve " << d_single_inv_sk[index] << std::endl; + Trace("cegqi-engine-debug") << "Substitute " << subs[index] << " to "; + subs[index] = applyProgVarSubstitution( subs[index], subs_from_model, subs ); + Trace("cegqi-engine-debug") << subs[index] << std::endl; + } + //try to improve substitutions : look for terms that contain terms in question + if( !subs_from_model.empty() ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node r = *eqcs_i; + int res = -1; + Node slv_n; + Node const_n; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + if( slv_n.isNull() || const_n.isNull() ){ + std::vector< Node > vars; + int curr_res = classifyTerm( n, subs_from_model ); + Trace("cegqi-si-debug2") << "Term : " << n << " classify : " << curr_res << std::endl; + if( curr_res!=-2 ){ + if( curr_res!=-1 && slv_n.isNull() ){ + res = curr_res; + slv_n = n; + }else if( const_n.isNull() ){ + const_n = n; + } + } + } + ++eqc_i; + } + if( !slv_n.isNull() && !const_n.isNull() ){ + if( slv_n.getType().isInteger() || slv_n.getType().isReal() ){ + Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[res] << " based on " << slv_n << " = " << const_n << std::endl; + subs_from_model.erase( d_single_inv_sk[res] ); + Node prev_subs_res = subs[res]; + subs[res] = d_single_inv_sk[res]; + Node eq = slv_n.eqNode( const_n ); + bool success = false; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Trace("cegqi-si-debug") << "As monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si"); + Node veq; + if( QuantArith::isolate( d_single_inv_sk[res], msum, veq, EQUAL ) ){ + Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[res] << " : " << veq << std::endl; + Node sol; + for( unsigned r=0; r<2; r++ ){ + if( veq[r]==d_single_inv_sk[res] ){ + sol = veq[ r==0 ? 1 : 0 ]; + } + } + if( !sol.isNull() ){ + sol = applyProgVarSubstitution( sol, subs_from_model, subs ); + Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl; + subs[res] = sol; + Trace("cegqi-engine") << " ...by arithmetic, " << d_single_inv_sk[res] << " -> " << sol << std::endl; + success = true; + } + } + } + if( !success ){ + subs[res] = prev_subs_res; + } + } + } + ++eqcs_i; + } + } + Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); + lem = Rewriter::rewrite( lem ); + Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; + if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ + lems.push_back( lem ); + d_lemmas_produced.push_back( lem ); + d_inst.push_back( std::vector< Node >() ); + d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + } + } +} + +Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) { + std::vector< Node > vars; + collectProgVars( n, vars ); + if( !vars.empty() ){ + std::vector< Node > ssubs; + //get substitution + for( unsigned i=0; i& subs_from_model ) { + if( n.getKind()==SKOLEM ){ + std::map< Node, int >::iterator it = subs_from_model.find( n ); + if( it!=subs_from_model.end() ){ + return it->second; + }else{ + // if it is symbolic argument, we are also fine + if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){ + return -1; + }else{ + //if it is another program, we are also fine + if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){ + return -1; + }else{ + return -2; + } + } + } + }else{ + int curr_res = -1; + for( unsigned i=0; i& vars ) { + if( n.getKind()==SKOLEM ){ + if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ + vars.push_back( n ); + } + } + }else{ + for( unsigned i=0; imkNode( ITE, cond, ite1, ite2 ); + } +} + +Node CegConjectureSingleInv::getSolution( unsigned i, Node varList ){ + Assert( !d_lemmas_produced.empty() ); + Node s = constructSolution( i, 0 ); + //TODO : not in grammar + std::vector< Node > vars; + for( unsigned i=0; i >& 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 ); + + Node constructSolution( unsigned i, unsigned index ); + int classifyTerm( Node n, std::map< Node, int >& subs_from_model ); + void collectProgVars( Node n, std::vector< Node >& vars ); + Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); +public: + CegConjectureSingleInv( Node q, CegConjecture * p ); + // original conjecture + Node d_quant; + // single invocation version of quant + Node d_single_inv; + //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 skolems for each program + std::vector< Node > d_single_inv_sk; + std::map< Node, int > d_single_inv_sk_index; + //list of skolems for each program + std::vector< Node > d_single_inv_var; + //lemmas produced + std::vector< Node > d_lemmas_produced; + std::vector< std::vector< Node > > d_inst; +public: + //get the single invocation lemma + Node getSingleInvLemma( Node guard ); + //initialize + void initialize(); + //check + void check( QuantifiersEngine * qe, std::vector< Node >& lems ); + //get solution + Node getSolution( unsigned i, Node varList ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 92285bf12..214f3974e 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,8 +196,13 @@ option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi -option sygusSingleInv --sygus-single-inv bool :default false +option cegqiSingleInv --cegqi-si bool :default false process single invocation synthesis conjectures +option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true + reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvAbort --cegqi-si-abort bool :default false + abort if our synthesis conjecture is not single invocation + option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form option sygusNormalFormArg --sygus-nf-arg bool :default true diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index f73bc7bb2..2dd800592 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -92,7 +92,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind if( r.isOne() ){ veq = negate(veq); }else{ - //TODO + //TODO : lcd computation return false; } } @@ -118,6 +118,23 @@ Node QuantArith::offset( Node t, int i ) { return tt; } +void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) { + for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Trace(c) << " "; + if( !it->second.isNull() ){ + Trace(c) << it->second; + if( !it->first.isNull() ){ + Trace(c) << " * "; + } + } + if( !it->first.isNull() ){ + Trace(c) << it->first; + } + Trace(c) << std::endl; + } + Trace(c) << std::endl; +} + void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index d7e220b2e..1b053cf6a 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -38,6 +38,7 @@ public: static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ); static Node negate( Node t ); static Node offset( Node t, int i ); + static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); }; -- 2.30.2