From 59de53bf6fd95bcf1e51aeb1ea9ce3dc42af4357 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 30 Sep 2017 06:35:12 -0500 Subject: [PATCH] SyGuS streaming solution mode (#1131) * Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode. * Infrastructure for streaming guards, more cleanup. * Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup. * More cleanup, add comments. * Update comments * Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter. * Fix makefile. * Cleanup. * Remove unused includes. * Minor --- src/Makefile.am | 2 + src/options/quantifiers_options | 5 + .../quantifiers/ce_guided_conjecture.cpp | 785 ++++++++++++++++++ src/theory/quantifiers/ce_guided_conjecture.h | 170 ++++ .../quantifiers/ce_guided_instantiation.cpp | 724 +--------------- .../quantifiers/ce_guided_instantiation.h | 132 +-- .../quantifiers/ce_guided_single_inv.cpp | 215 ++--- src/theory/quantifiers/ce_guided_single_inv.h | 13 +- .../quantifiers/quantifiers_rewriter.cpp | 3 +- test/regress/regress0/sygus/Makefile.am | 3 +- .../regress0/sygus/triv-type-mismatch-si.sy | 13 + 11 files changed, 1135 insertions(+), 930 deletions(-) create mode 100644 src/theory/quantifiers/ce_guided_conjecture.cpp create mode 100644 src/theory/quantifiers/ce_guided_conjecture.h create mode 100644 test/regress/regress0/sygus/triv-type-mismatch-si.sy diff --git a/src/Makefile.am b/src/Makefile.am index 3a41b30ab..7b9a607a1 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -350,6 +350,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/bv_inverter.h \ theory/quantifiers/candidate_generator.cpp \ theory/quantifiers/candidate_generator.h \ + theory/quantifiers/ce_guided_conjecture.cpp \ + theory/quantifiers/ce_guided_conjecture.h \ theory/quantifiers/ce_guided_instantiation.cpp \ theory/quantifiers/ce_guided_instantiation.h \ theory/quantifiers/ce_guided_single_inv.cpp \ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index d5619ed77..44fbc4ee7 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -270,6 +270,8 @@ option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false aggressively minimize sygus grammars option sygusAddConstGrammar --sygus-add-const-grammar bool :default true statically add constants appearing in conjecture to grammars +option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false + embed sygus templates into grammars option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode template mode for sygus invariant synthesis @@ -287,6 +289,9 @@ option sygusCRefEval --sygus-cref-eval bool :default true option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true use min explain for direct evaluation of refinement lemmas for conflict analysis +option sygusStream --sygus-stream bool :default false + enumerate a stream of solutions instead of terminating after the first one + # CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp new file mode 100644 index 000000000..fbf08e909 --- /dev/null +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -0,0 +1,785 @@ +/********************* */ +/*! \file ce_guided_conjecture.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief implementation of class that encapsulates counterexample-guided instantiation + ** techniques for a single SyGuS synthesis conjecture + **/ +#include "theory/quantifiers/ce_guided_conjecture.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" +#include "prop/prop_engine.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database_sygus.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +// recursion is not an issue since OR nodes are flattened by the (quantifiers) rewriter +// this function is for sanity since solution correctness in SyGuS depends on fully miniscoping based on this function +void collectDisjuncts( Node n, std::vector< Node >& d ) { + if( n.getKind()==OR ){ + for( unsigned i=0; i& synth_fun_vars, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + Node ret = n; + + std::vector< Node > children; + bool childChanged = false; + bool madeOp = false; + Kind ret_k = n.getKind(); + Node op; + if( n.getNumChildren()>0 ){ + if( n.getKind()==kind::APPLY_UF ){ + op = n.getOperator(); + } + }else{ + op = n; + } + // is it a synth function? + std::map< Node, Node >::iterator its = synth_fun_vars.find( op ); + if( its!=synth_fun_vars.end() ){ + Assert( its->second.getType().isDatatype() ); + // make into evaluation function + const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype(); + Assert( dt.isSygus() ); + children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); + children.push_back( its->second ); + madeOp = true; + childChanged = true; + ret_k = kind::APPLY_UF; + } + if( n.getNumChildren()>0 || childChanged ){ + if( !madeOp ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + } + for( unsigned i=0; imkNode( ret_k, children ); + } + } + visited[n] = ret; + return ret; + }else{ + return it->second; + } +} + +void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.isConst() ){ + TypeNode tn = n.getType(); + Node nc = n; + if( tn.isReal() ){ + nc = NodeManager::currentNM()->mkConst( n.getConst().abs() ); + } + if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){ + Trace("cegqi-debug") << "...consider const : " << nc << std::endl; + consts[tn].push_back( nc ); + } + } + + for( unsigned i=0; igetTermDatabase()->isQAttrSygus( d_quant ) ){ + d_ceg_si->initialize( d_quant ); + simp_quant = d_ceg_si->getSimplifiedConjecture(); + } + + // convert to deep embedding and finalize single invocation here + // now, construct the grammar + Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; + std::map< TypeNode, std::vector< Node > > extra_cons; + Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; + if( options::sygusAddConstGrammar() ){ + std::map< Node, bool > visited; + collectConstants( q[1], extra_cons, visited ); + } + bool has_ites = true; + bool is_syntax_restricted = false; + std::vector< Node > qchildren; + std::map< Node, Node > visited; + std::map< Node, Node > synth_fun_vars; + std::vector< Node > ebvl; + Node qbody_subs = simp_quant[1]; + for( unsigned i=0; igetTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons ); + } + Node templ = d_ceg_si->getTemplate( sf ); + if( !templ.isNull() ){ + TNode templ_arg = d_ceg_si->getTemplateArg( sf ); + Assert( !templ_arg.isNull() ); + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; + // if there is a template for this argument, make a sygus type on top of it + if( options::sygusTemplEmbedGrammar() ){ + Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; + tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); + }else{ + // otherwise, apply it as a preprocessing pass + Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl; + std::vector< Node > schildren; + std::vector< Node > largs; + for( unsigned j=0; jmkBoundVar( sfvl[j].getType() ) ); + } + std::vector< Node > subsfn_children; + subsfn_children.push_back( sf ); + subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() ); + Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children ); + TNode subsf = subsfn; + Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " << subsf << std::endl; + templ = templ.substitute( templ_arg, subsf ); + // substitute lambda arguments + templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() ); + Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ ); + TNode var = sf; + TNode subs = subsn; + Trace("cegqi-debug") << " substitute : " << var << " -> " << subs << std::endl; + qbody_subs = qbody_subs.substitute( var, subs ); + Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; + } + } + d_qe->getTermDatabaseSygus()->registerSygusType( tn ); + // check grammar restrictions + if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ + if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ + has_ites = false; + } + } + Assert( tn.isDatatype() ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + if( !dt.getSygusAllowAll() ){ + is_syntax_restricted = true; + } + + // ev is the first-order variable corresponding to this synth fun + std::stringstream ssf; + ssf << "f" << sf; + Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn ); + ebvl.push_back( ev ); + synth_fun_vars[sf] = ev; + Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; + } + qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) ); + if( qbody_subs!=simp_quant[1] ){ + Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl; + qbody_subs = Rewriter::rewrite( qbody_subs ); + Trace("cegqi") << "...got : " << qbody_subs << std::endl; + } + qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars, visited ) ); + if( q.getNumChildren()==3 ){ + qchildren.push_back( q[2] ); + } + q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren ); + Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl; + d_embed_quant = q; + + // we now finalize the single invocation module, based on the syntax restrictions + if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ + d_ceg_si->finishInit( is_syntax_restricted, has_ites ); + } + + Assert( d_candidates.empty() ); + std::vector< Node > vars; + for( unsigned i=0; imkSkolem( "e", q[0][i].getType() ); + d_candidates.push_back( e ); + } + Trace("cegqi") << "Base quantified formula is : " << q << std::endl; + //construct base instantiation + d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) ); + + // register this term with sygus database + std::vector< Node > guarded_lemmas; + if( !isSingleInvocation() ){ + if( options::sygusPbe() ){ + d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas ); + } + for( unsigned i=0; i > exs; + std::vector< Node > exos; + std::vector< Node > exts; + // use the PBE examples, regardless of the search algorith, since these help search space pruning + if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){ + d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts ); + } + }else{ + d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e ); + } + } + } + + Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; + if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){ + collectDisjuncts( d_base_inst, d_base_disj ); + Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; + //store the inner variables for each disjunct + for( unsigned j=0; j() ); + //if the disjunct is an existential, store it + if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){ + for( unsigned k=0; kgetTermDatabase()->isQAttrSynthesis( d_quant ) ){ + d_syntax_guided = false; + }else{ + Assert( false ); + } + + // initialize the guard + if( !d_syntax_guided ){ + if( d_nsg_guard.isNull() ){ + d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); + d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard ); + AlwaysAssert( !d_nsg_guard.isNull() ); + d_qe->getOutputChannel().requirePhase( d_nsg_guard, true ); + // negated base as a guarded lemma + guarded_lemmas.push_back( d_base_inst.negate() ); + } + }else if( d_ceg_si->getGuard().isNull() ){ + std::vector< Node > lems; + d_ceg_si->getInitialSingleInvLemma( lems ); + for( unsigned i=0; igetOutputChannel().lemma( lems[i] ); + if( Trace.isOn("cegqi-debug") ){ + Node rlem = Rewriter::rewrite( lems[i] ); + Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; + } + } + } + Assert( !getGuard().isNull() ); + Node gneg = getGuard().negate(); + for( unsigned i=0; imkNode( OR, gneg, guarded_lemmas[i] ); + Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl; + d_qe->getOutputChannel().lemma( lem ); + } + + Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; +} + +Node CegConjecture::getGuard() { + return !d_syntax_guided ? d_nsg_guard : d_ceg_si->getGuard(); +} + +bool CegConjecture::isSingleInvocation() const { + return d_ceg_si->isSingleInvocation(); +} + +bool CegConjecture::needsCheck( std::vector< Node >& lem ) { + if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ + return false; + }else{ + bool value; + Assert( !getGuard().isNull() ); + // non or fully single invocation : look at guard only + if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) { + if( !value ){ + Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; + return false; + } + }else{ + Assert( false ); + } + return true; + } +} + + +void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) { + if( d_ceg_si!=NULL ){ + d_ceg_si->check(lems); + } +} + +void CegConjecture::doBasicCheck(std::vector< Node >& lems) { + std::vector< Node > model_terms; + std::vector< Node > clist; + getCandidateList( clist, true ); + Assert( clist.size()==d_quant[0].getNumChildren() ); + getModelValues( clist, model_terms ); + if( d_qe->addInstantiation( d_quant, model_terms ) ){ + //record the instantiation + recordInstantiation( model_terms ); + }else{ + Assert( false ); + } +} + +bool CegConjecture::needsRefinement() { + return !d_ce_sk.empty(); +} + +void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) { + if( d_ceg_pbe->isPbe() && !forceOrig ){ + d_ceg_pbe->getCandidateList( d_candidates, clist ); + }else{ + clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() ); + } +} + +bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, + std::vector< Node >& lems ) { + Assert( clist.size()==model_values.size() ); + if( d_ceg_pbe->isPbe() ){ + return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems ); + }else{ + Assert( model_values.size()==d_candidates.size() ); + candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() ); + } + return true; +} + +void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& model_values) { + std::vector< Node > clist; + getCandidateList( clist ); + std::vector< Node > c_model_values; + Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl; + bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems ); + + //must get a counterexample to the value of the current candidate + Node inst; + if( constructed_cand ){ + if( Trace.isOn("cegqi-check") ){ + Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl; + for( unsigned i=0; i " << c_model_values[i] << std::endl; + } + } + Assert( c_model_values.size()==d_candidates.size() ); + inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() ); + }else{ + inst = d_base_inst; + } + + //check whether we will run CEGIS on inner skolem variables + bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand ); + if( sk_refine ){ + Assert( d_ce_sk.empty() ); + d_ce_sk.push_back( std::vector< Node >() ); + }else{ + if( !constructed_cand ){ + return; + } + } + + std::vector< Node > ic; + ic.push_back( d_quant.negate() ); + std::vector< Node > d; + collectDisjuncts( inst, d ); + Assert( d.size()==d_base_disj.size() ); + //immediately skolemize inner existentials + for( unsigned i=0; igetTermDatabase()->getSkolemizedBody( dr[0] ).negate() ); + } + if( sk_refine ){ + Assert( !isGround() ); + d_ce_sk.back().push_back( dr[0] ); + } + }else{ + if( constructed_cand ){ + ic.push_back( dr ); + if( !d_inner_vars_disj[i].empty() ){ + Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; + } + } + if( sk_refine ){ + d_ce_sk.back().push_back( Node::null() ); + } + } + } + if( constructed_cand ){ + Node lem = NodeManager::currentNM()->mkNode( OR, ic ); + lem = Rewriter::rewrite( lem ); + //eagerly unfold applications of evaluation function + if( options::sygusDirectEval() ){ + Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; + std::map< Node, Node > visited_n; + lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n ); + } + if( options::sygusStream() ){ + // if we are in streaming mode, we guard with the current stream guard + Node curr_stream_guard = getCurrentStreamGuard(); + Assert( !curr_stream_guard.isNull() ); + lem = NodeManager::currentNM()->mkNode( kind::OR, curr_stream_guard.negate(), lem ); + } + lems.push_back( lem ); + recordInstantiation( c_model_values ); + } +} + +void CegConjecture::doRefine( std::vector< Node >& lems ){ + Assert( lems.empty() ); + Assert( d_ce_sk.size()==1 ); + + //first, make skolem substitution + Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl; + std::vector< Node > sk_vars; + std::vector< Node > sk_subs; + //collect the substitution over all disjuncts + for( unsigned k=0; kgetTermDatabase()->d_skolem_constants[ce_q].size() ); + std::vector< Node > model_values; + getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values ); + sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); + sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); + }else{ + if( !d_inner_vars_disj[k].empty() ){ + //denegrate case : quantified disjunct was trivially true and does not need to be refined + //add trivial substitution (in case we need substitution for previous cex's) + for( unsigned i=0; i lem_c; + Assert( d_ce_sk[0].size()==d_base_disj.size() ); + std::vector< Node > inst_cond_c; + Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; + for( unsigned k=0; kmkNode( AND, lem_c ); + + Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl; + + Node lem = base_lem; + + base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + base_lem = Rewriter::rewrite( base_lem ); + d_refinement_lemmas_base.push_back( base_lem ); + + lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem ); + + lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + lem = Rewriter::rewrite( lem ); + d_refinement_lemmas.push_back( lem ); + lems.push_back( lem ); + + d_ce_sk.clear(); +} + +void CegConjecture::preregisterConjecture( Node q ) { + d_ceg_si->preregisterConjecture( q ); +} + +void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { + Trace("cegqi-engine") << " * Value is : "; + for( unsigned i=0; i "; + std::stringstream ss; + std::vector< Node > lvs; + TermDbSygus::printSygusTerm( ss, nv, lvs ); + Trace("cegqi-engine") << ss.str() << " "; + } + Assert( !nv.isNull() ); + } + Trace("cegqi-engine") << std::endl; +} + +Node CegConjecture::getModelValue( Node n ) { + Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; + return d_qe->getModel()->getValue( n ); +} + +void CegConjecture::debugPrint( const char * c ) { + Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl; + Trace(c) << " * Candidate program/output symbol : "; + for( unsigned i=0; igetValuation().hasSatValue( feasible_guard, value ) ) { + priority = 0; + return feasible_guard; + }else{ + if( value ){ + // the conjecture is feasible + if( options::sygusStream() ){ + Assert( !isSingleInvocation() ); + // if we are in sygus streaming mode, then get the "next guard" + // which denotes "we have not yet generated the next solution to the conjecture" + Node curr_stream_guard = getCurrentStreamGuard(); + bool needs_new_stream_guard = false; + if( curr_stream_guard.isNull() ){ + needs_new_stream_guard = true; + }else{ + // check the polarity of the guard + if( !d_qe->getValuation().hasSatValue( curr_stream_guard, value ) ) { + priority = 0; + return curr_stream_guard; + }else{ + if( !value ){ + Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl; + // we have generated a solution, print it + // get the current output stream + // this output stream should coincide with wherever --dump-synth is output on + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + printSynthSolution( *nodeManagerOptions.getOut(), false ); + // need to make the next stream guard + needs_new_stream_guard = true; + + // We will not refine the current candidate solution since it is a solution + // thus, we clear information regarding the current refinement + d_ce_sk.clear(); + // However, we need to exclude the current solution using an explicit refinement + // so that we proceed to the next solution. + std::vector< Node > clist; + getCandidateList( clist ); + Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl; + std::vector< Node > exp; + for( unsigned i=0; igetTermDatabaseSygus()->getExplanationForConstantEquality( cprog, sol, exp ); + } + Trace("cegqi-debug") << " " << cprog << " -> " << sol << std::endl; + } + Assert( !exp.empty() ); + Node exc_lem = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ); + exc_lem = exc_lem.negate(); + Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " << exc_lem << std::endl; + d_qe->getOutputChannel().lemma( exc_lem ); + } + } + } + if( needs_new_stream_guard ){ + // generate a new stream guard + curr_stream_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G_Stream", NodeManager::currentNM()->booleanType() ) ); + curr_stream_guard = d_qe->getValuation().ensureLiteral( curr_stream_guard ); + AlwaysAssert( !curr_stream_guard.isNull() ); + d_qe->getOutputChannel().requirePhase( curr_stream_guard, true ); + d_stream_guards.push_back( curr_stream_guard ); + Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : " << curr_stream_guard << std::endl; + // return it as a decision + priority = 0; + return curr_stream_guard; + } + } + }else{ + Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." << std::endl; + } + } + return Node::null(); +} + +void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) { + Trace("cegqi-debug") << "Printing synth solution..." << std::endl; + Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() ); + for( unsigned i=0; igetSolution( i, tn, status, true ); + if( !sol.isNull() ){ + sol = sol.getKind()==LAMBDA ? sol[1] : sol; + } + }else{ + Node cprog = getCandidate( i ); + if( !d_cinfo[cprog].d_inst.empty() ){ + // the solution is just the last instantiated term + sol = d_cinfo[cprog].d_inst.back(); + status = 1; + + //check if there was a template + Node sf = d_quant[0][i].getAttribute(SygusSynthFunAttribute()); + Node templ = d_ceg_si->getTemplate( sf ); + if( !templ.isNull() ){ + Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl; + // if it was not embedded into the grammar + if( !options::sygusTemplEmbedGrammar() ){ + TNode templa = d_ceg_si->getTemplateArg( sf ); + // make the builtin version of the full solution + TermDbSygus* sygusDb = d_qe->getTermDatabase()->getTermDatabaseSygus(); + sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " + << sol << ", type : " << sol.getType() + << std::endl; + TNode tsol = sol; + sol = templ.substitute( templa, tsol ); + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = Rewriter::rewrite( sol ); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + // now, reconstruct to the syntax + sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); + sol = sol.getKind()==LAMBDA ? sol[1] : sol; + Trace("cegqi-inv-debug") << "Reconstructed to syntax : " << sol << std::endl; + }else{ + Trace("cegqi-inv-debug") << "...was embedding into grammar." << std::endl; + } + }else{ + Trace("cegqi-inv-debug") << sf << " did not use template" << std::endl; + } + }else{ + Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl; + } + } + if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){ + out << "(define-fun " << f << " "; + if( dt.getSygusVarList().isNull() ){ + out << "() "; + }else{ + out << dt.getSygusVarList() << " "; + } + out << dt.getSygusType() << " "; + if( status==0 ){ + out << sol; + }else{ + std::vector< Node > lvs; + TermDbSygus::printSygusTerm( out, sol, lvs ); + } + out << ")" << std::endl; + } + } +} + +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h new file mode 100644 index 000000000..1263778d3 --- /dev/null +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -0,0 +1,170 @@ +/********************* */ +/*! \file ce_guided_conjecture.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief class that encapsulates counterexample-guided instantiation + ** techniques for a single SyGuS synthesis conjecture + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H +#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H + +#include "context/cdhashmap.h" +#include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers/ce_guided_pbe.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** a synthesis conjecture */ +class CegConjecture { +public: + CegConjecture( QuantifiersEngine * qe ); + ~CegConjecture(); + /** get original version of conjecture */ + Node getConjecture() { return d_quant; } + /** get deep embedding version of conjecture */ + Node getEmbeddedConjecture() { return d_embed_quant; } + /** get next decision request */ + Node getNextDecisionRequest( unsigned& priority ); + /** increment the number of times we have successfully done candidate refinement */ + void incrementRefineCount() { d_refine_count++; } + /** whether the conjecture is waiting for a call to do_Check below */ + bool needsCheck( std::vector< Node >& lem ); + /** whether the conjecture is waiting for a call to doRefine below */ + bool needsRefinement(); + /** get the list of candidates */ + void getCandidateList( std::vector< Node >& clist, bool forceOrig = false ); + /** do single invocation check + * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015. + */ + void doSingleInvCheck(std::vector< Node >& lems); + /** do syntax-guided enumerative check + * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. + */ + void doCheck(std::vector< Node >& lems, std::vector< Node >& model_values); + /** do basic check + * This is called for non-SyGuS synthesis conjectures + */ + void doBasicCheck(std::vector< Node >& lems); + /** do refinement + * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. + */ + void doRefine(std::vector< Node >& lems); + /** Print the synthesis solution + * singleInvocation is whether the solution was found by single invocation techniques. + */ + void printSynthSolution( std::ostream& out, bool singleInvocation ); + /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */ + Node getGuard(); + /** is ground */ + bool isGround() { return d_inner_vars.empty(); } + /** does this conjecture correspond to a syntax-guided synthesis input */ + bool isSyntaxGuided() const { return d_syntax_guided; } + /** are we using single invocation techniques */ + bool isSingleInvocation() const; + /** preregister conjecture + * This is used as a heuristic for solution reconstruction, so that we + * remember expressions in the conjecture before preprocessing, since they + * may be helpful during solution reconstruction (Figure 5 of Reynolds et al CAV 2015) + */ + void preregisterConjecture( Node q ); + /** assign conjecture q to this class */ + void assign( Node q ); + /** has a conjecture been assigned to this class */ + bool isAssigned() { return !d_embed_quant.isNull(); } + /** get model values for terms n, store in vector v */ + void getModelValues( std::vector< Node >& n, std::vector< Node >& v ); + /** get model value for term n */ + Node getModelValue( Node n ); + /** get number of refinement lemmas we have added so far */ + unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } + /** get refinement lemma */ + Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; } + /** get refinement lemma */ + Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; } + /** print out debug information about this conjecture */ + void debugPrint( const char * c ); +private: + /** reference to quantifier engine */ + QuantifiersEngine * d_qe; + /** single invocation utility */ + CegConjectureSingleInv * d_ceg_si; + /** program by examples utility */ + CegConjecturePbe * d_ceg_pbe; + /** list of constants for quantified formula */ + std::vector< Node > d_candidates; + /** base instantiation */ + Node d_base_inst; + /** expand base inst to disjuncts */ + std::vector< Node > d_base_disj; + /** list of variables on inner quantification */ + std::vector< Node > d_inner_vars; + std::vector< std::vector< Node > > d_inner_vars_disj; + /** current extential quantifeirs whose couterexamples we must refine */ + std::vector< std::vector< Node > > d_ce_sk; + /** refinement lemmas */ + std::vector< Node > d_refinement_lemmas; + std::vector< Node > d_refinement_lemmas_base; + /** quantified formula asserted */ + Node d_quant; + /** quantified formula (after processing) */ + Node d_embed_quant; + /** candidate information */ + class CandidateInfo { + public: + CandidateInfo(){} + /** list of terms we have instantiated candidates with */ + std::vector< Node > d_inst; + }; + std::map< Node, CandidateInfo > d_cinfo; + /** number of times we have called doRefine */ + unsigned d_refine_count; + /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */ + Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ); + /** collect constants */ + void collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ); + /** construct candidates */ + bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, + std::vector< Node >& candidate_values, std::vector< Node >& lems ); + /** get candidadate */ + Node getCandidate( unsigned int i ) { return d_candidates[i]; } + /** record instantiation (this is used to construct solutions later) */ + void recordInstantiation( std::vector< Node >& vs ) { + Assert( vs.size()==d_candidates.size() ); + for( unsigned i=0; i d_stream_guards; + /** get current stream guard */ + Node getCurrentStreamGuard() const; + //-------------------------------- end sygus stream + //-------------------------------- non-syntax guided (deprecated) + /** Whether we are syntax-guided (e.g. was the input in SyGuS format). + * This includes SyGuS inputs where no syntactic restrictions are provided. + */ + bool d_syntax_guided; + /** the guard for non-syntax-guided synthesis */ + Node d_nsg_guard; + //-------------------------------- end non-syntax guided (deprecated) +}; + +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 38247c84c..2ad55bb07 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -10,18 +10,16 @@ ** directory for licensing information.\endverbatim ** ** \brief counterexample guided instantiation class + ** This class is the entry point for both synthesis algorithms in Reynolds et al CAV 2015 ** **/ #include "theory/quantifiers/ce_guided_instantiation.h" -#include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "options/datatypes_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database_sygus.h" #include "theory/theory_engine.h" -#include "prop/prop_engine.h" +#include "theory/quantifiers/term_database_sygus.h" +//FIXME : remove this include (github issue #1156) #include "theory/bv/theory_bv_rewriter.h" using namespace CVC4::kind; @@ -31,539 +29,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { - -CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) - : d_qe( qe ) { - d_refine_count = 0; - d_ceg_si = new CegConjectureSingleInv( qe, this ); - d_ceg_pbe = new CegConjecturePbe( qe, this ); -} - -CegConjecture::~CegConjecture() { - delete d_ceg_si; - delete d_ceg_pbe; -} - -Node CegConjecture::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ){ - std::map< Node, Node >::iterator it = visited.find( n ); - if( it==visited.end() ){ - Node ret = n; - - std::vector< Node > children; - bool childChanged = false; - bool madeOp = false; - Kind ret_k = n.getKind(); - Node op; - if( n.getNumChildren()>0 ){ - if( n.getKind()==kind::APPLY_UF ){ - op = n.getOperator(); - } - }else{ - op = n; - } - // is it a synth function? - std::map< Node, Node >::iterator its = synth_fun_vars.find( op ); - if( its!=synth_fun_vars.end() ){ - Assert( its->second.getType().isDatatype() ); - // make into evaluation function - const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype(); - Assert( dt.isSygus() ); - children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); - children.push_back( its->second ); - madeOp = true; - childChanged = true; - ret_k = kind::APPLY_UF; - } - if( n.getNumChildren()>0 || childChanged ){ - if( !madeOp ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - } - for( unsigned i=0; imkNode( ret_k, children ); - } - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.isConst() ){ - TypeNode tn = n.getType(); - Node nc = n; - if( tn.isReal() ){ - nc = NodeManager::currentNM()->mkConst( n.getConst().abs() ); - } - if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){ - Trace("cegqi-debug") << "...consider const : " << nc << std::endl; - consts[tn].push_back( nc ); - } - } - - for( unsigned i=0; igetTermDatabase()->isQAttrSygus( d_assert_quant ) ){ - d_ceg_si->initialize( d_assert_quant ); - } - - // convert to deep embedding and finalize single invocation here - // now, construct the grammar - Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; - std::map< TypeNode, std::vector< Node > > extra_cons; - Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; - if( options::sygusAddConstGrammar() ){ - std::map< Node, bool > visited; - collectConstants( q[1], extra_cons, visited ); - } - bool has_ites = true; - bool is_syntax_restricted = false; - std::vector< Node > qchildren; - std::map< Node, Node > visited; - std::map< Node, Node > synth_fun_vars; - std::vector< Node > ebvl; - for( unsigned i=0; igetTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons ); - } - // if there is a template for this argument, make a sygus type on top of it - Node templ = d_ceg_si->getTemplate( sf ); - if( !templ.isNull() ){ - Node templ_arg = d_ceg_si->getTemplateArg( sf ); - Assert( !templ_arg.isNull() ); - if( Trace.isOn("cegqi-debug") ){ - Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; - Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; - } - tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); - } - d_qe->getTermDatabaseSygus()->registerSygusType( tn ); - // check grammar restrictions - if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ - if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ - has_ites = false; - } - } - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); - if( !dt.getSygusAllowAll() ){ - is_syntax_restricted = true; - } - - // ev is the first-order variable corresponding to this synth fun - std::stringstream ssf; - ssf << "f" << sf; - Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn ); - ebvl.push_back( ev ); - synth_fun_vars[sf] = ev; - Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; - } - qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) ); - qchildren.push_back( convertToEmbedding( q[1], synth_fun_vars, visited ) ); - if( q.getNumChildren()==3 ){ - qchildren.push_back( q[2] ); - } - q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren ); - Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl; - d_quant = q; - - // we now finalize the single invocation module, based on the syntax restrictions - if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ - d_ceg_si->finishInit( is_syntax_restricted, has_ites ); - } - - Assert( d_candidates.empty() ); - std::vector< Node > vars; - for( unsigned i=0; imkSkolem( "e", q[0][i].getType() ); - d_candidates.push_back( e ); - } - Trace("cegqi") << "Base quantified formula is : " << q << std::endl; - //construct base instantiation - d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) ); - - // register this term with sygus database - std::vector< Node > guarded_lemmas; - if( !isSingleInvocation() ){ - if( options::sygusPbe() ){ - d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas ); - } - for( unsigned i=0; i > exs; - std::vector< Node > exos; - std::vector< Node > exts; - // use the PBE examples, regardless of the search algorith, since these help search space pruning - if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){ - d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts ); - } - }else{ - d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e ); - } - } - } - - 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; - //store the inner variables for each disjunct - for( unsigned j=0; j() ); - //if the disjunct is an existential, store it - if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){ - for( unsigned k=0; kgetTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ - d_syntax_guided = false; - }else{ - Assert( false ); - } - - // initialize the guard - if( !d_syntax_guided ){ - if( d_nsg_guard.isNull() ){ - d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); - d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard ); - AlwaysAssert( !d_nsg_guard.isNull() ); - d_qe->getOutputChannel().requirePhase( d_nsg_guard, true ); - // negated base as a guarded lemma - guarded_lemmas.push_back( d_base_inst.negate() ); - } - }else if( d_ceg_si->d_si_guard.isNull() ){ - std::vector< Node > lems; - d_ceg_si->getInitialSingleInvLemma( lems ); - for( unsigned i=0; igetOutputChannel().lemma( lems[i] ); - if( Trace.isOn("cegqi-debug") ){ - Node rlem = Rewriter::rewrite( lems[i] ); - Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; - } - } - } - Assert( !getGuard().isNull() ); - Node gneg = getGuard().negate(); - for( unsigned i=0; imkNode( OR, gneg, guarded_lemmas[i] ); - Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma( lem ); - } - - Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; -} - -Node CegConjecture::getGuard() { - return !d_syntax_guided ? d_nsg_guard : d_ceg_si->d_si_guard; -} - -bool CegConjecture::isSingleInvocation() const { - return d_ceg_si->isSingleInvocation(); -} - -bool CegConjecture::needsCheck( std::vector< Node >& lem ) { - if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ - return false; - }else{ - bool value; - Assert( !getGuard().isNull() ); - // non or fully single invocation : look at guard only - if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) { - if( !value ){ - Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; - return false; - } - }else{ - Assert( false ); - } - - return true; - } -} - - -void CegConjecture::doCegConjectureSingleInvCheck(std::vector< Node >& lems) { - if( d_ceg_si!=NULL ){ - d_ceg_si->check(lems); - } -} - -bool CegConjecture::needsRefinement() { - return !d_ce_sk.empty(); -} - -void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) { - if( d_ceg_pbe->isPbe() && !forceOrig ){ - //Assert( isGround() ); - d_ceg_pbe->getCandidateList( d_candidates, clist ); - }else{ - clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() ); - } -} - -bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, - std::vector< Node >& lems ) { - Assert( clist.size()==model_values.size() ); - if( d_ceg_pbe->isPbe() ){ - //Assert( isGround() ); - return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems ); - }else{ - Assert( model_values.size()==d_candidates.size() ); - candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() ); - } - return true; -} - -void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values) { - std::vector< Node > clist; - getCandidateList( clist ); - std::vector< Node > c_model_values; - Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl; - bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems ); - - //must get a counterexample to the value of the current candidate - Node inst; - if( constructed_cand ){ - if( Trace.isOn("cegqi-check") ){ - Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl; - for( unsigned i=0; i " << c_model_values[i] << std::endl; - } - } - Assert( c_model_values.size()==d_candidates.size() ); - inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() ); - }else{ - inst = d_base_inst; - } - - //check whether we will run CEGIS on inner skolem variables - bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand ); - if( sk_refine ){ - Assert( d_ce_sk.empty() ); - d_ce_sk.push_back( std::vector< Node >() ); - }else{ - if( !constructed_cand ){ - return; - } - } - - std::vector< Node > ic; - ic.push_back( d_assert_quant.negate() ); - std::vector< Node > d; - CegInstantiation::collectDisjuncts( inst, d ); - Assert( d.size()==d_base_disj.size() ); - //immediately skolemize inner existentials - for( unsigned i=0; igetTermDatabase()->getSkolemizedBody( dr[0] ).negate() ); - } - if( sk_refine ){ - Assert( !isGround() ); - d_ce_sk.back().push_back( dr[0] ); - } - }else{ - if( constructed_cand ){ - ic.push_back( dr ); - if( !d_inner_vars_disj[i].empty() ){ - Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; - } - } - if( sk_refine ){ - d_ce_sk.back().push_back( Node::null() ); - } - } - } - if( constructed_cand ){ - Node lem = NodeManager::currentNM()->mkNode( OR, ic ); - lem = Rewriter::rewrite( lem ); - //eagerly unfold applications of evaluation function - if( options::sygusDirectEval() ){ - Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; - std::map< Node, Node > visited_n; - lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n ); - } - lems.push_back( lem ); - recordInstantiation( c_model_values ); - } -} - -void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ - Assert( lems.empty() ); - Assert( d_ce_sk.size()==1 ); - - //first, make skolem substitution - Trace("cegqi-refine") << "doCegConjectureRefine : construct skolem substitution..." << std::endl; - std::vector< Node > sk_vars; - std::vector< Node > sk_subs; - //collect the substitution over all disjuncts - for( unsigned k=0; kgetTermDatabase()->d_skolem_constants[ce_q].size() ); - std::vector< Node > model_values; - getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values ); - sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); - sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); - }else{ - if( !d_inner_vars_disj[k].empty() ){ - //denegrate case : quantified disjunct was trivially true and does not need to be refined - //add trivial substitution (in case we need substitution for previous cex's) - for( unsigned i=0; i csol_active; - std::map< Node, std::vector< Node > > csol_ccond_nodes; - std::map< Node, std::map< Node, bool > > csol_cpol; - - //for conditional evaluation - std::map< Node, Node > psubs_visited; - std::map< Node, Node > psubs; - std::vector< Node > lem_c; - Assert( d_ce_sk[0].size()==d_base_disj.size() ); - std::vector< Node > inst_cond_c; - Trace("cegqi-refine") << "doCegConjectureRefine : Construct refinement lemma..." << std::endl; - for( unsigned k=0; k psubs_cond_ant; - std::vector< Node > psubs_cond_conc; - std::map< Node, std::vector< Node > > psubs_apply; - std::vector< Node > paux_vars; - Assert( psubs.empty() ); - - Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); - - Trace("cegqi-refine") << "doCegConjectureRefine : construct and finalize lemmas..." << std::endl; - - Node lem = base_lem; - - base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - base_lem = Rewriter::rewrite( base_lem ); - d_refinement_lemmas_base.push_back( base_lem ); - - lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem ); - - lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - lem = Rewriter::rewrite( lem ); - d_refinement_lemmas.push_back( lem ); - lems.push_back( lem ); - - d_ce_sk.clear(); -} - -void CegConjecture::preregisterConjecture( Node q ) { - d_ceg_si->preregisterConjecture( q ); -} - -void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { - Trace("cegqi-engine") << " * Value is : "; - for( unsigned i=0; i "; - std::stringstream ss; - std::vector< Node > lvs; - TermDbSygus::printSygusTerm( ss, nv, lvs ); - Trace("cegqi-engine") << ss.str() << " "; - } - Assert( !nv.isNull() ); - } - Trace("cegqi-engine") << std::endl; -} - -Node CegConjecture::getModelValue( Node n ) { - Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_qe->getModel()->getValue( n ); -} - -void CegConjecture::debugPrint( const char * c ) { - Trace(c) << "Synthesis conjecture : " << d_quant << std::endl; - Trace(c) << " * Candidate program/output symbol : "; - for( unsigned i=0; igetSatContext() ); + d_conj = new CegConjecture( qe ); d_last_inst_si = false; } @@ -576,19 +43,17 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { } unsigned CegInstantiation::needsModel( Theory::Effort e ) { - return d_conj->getCegConjectureSingleInv()->isSingleInvocation() - ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; + return d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; } void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { - unsigned echeck = d_conj->getCegConjectureSingleInv()->isSingleInvocation() ? - QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; + unsigned echeck = d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; if( quant_e==echeck ){ Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; bool active = false; bool value; - if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) { + if( d_quantEngine->getValuation().hasSatValue( d_conj->getConjecture(), value ) ) { active = value; }else{ Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl; @@ -608,83 +73,33 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { } } -void CegInstantiation::preRegisterQuantifier( Node q ) { -/* - if( options::sygusDirectEval() ){ - if( q.getNumChildren()==3 && q[2].getKind()==INST_PATTERN_LIST && q[2][0].getKind()==INST_PATTERN ){ - //check whether it is an evaluation axiom - Node pat = q[2][0][0]; - if( pat.getKind()==APPLY_UF ){ - TypeNode tn = pat[0].getType(); - if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isSygus() ){ - //do unfolding if it induces Boolean structure, - //do direct evaluation if it does not induce Boolean structure, - // the reasoning is unfolding over these terms does not lead to helpful conflict analysis, and introduces many shared terms - bool directEval = true; - TypeNode ptn = pat.getType(); - if( ptn.isBoolean() ){ - directEval = false; - }else{ - unsigned cindex = Datatype::indexOf(pat[0].getOperator().toExpr() ); - Node base = d_quantEngine->getTermDatabaseSygus()->getGenericBase( tn, dt, cindex ); - Trace("cegqi-debug") << "Generic base term for " << pat[0] << " is " << base << std::endl; - if( base.getKind()==ITE ){ - directEval = false; - } - } - if( directEval ){ - //take ownership of this quantified formula (will use direct evaluation instead of unfolding instantiation) - d_quantEngine->setOwner( q, this ); - d_eval_axioms[q] = true; - } - } - } - } - } - } - */ -} - void CegInstantiation::registerQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==this ){ // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ if( !d_conj->isAssigned() ){ Trace("cegqi") << "Register conjecture : " << q << std::endl; d_conj->assign( q ); }else{ - Assert( d_conj->d_quant==q ); + Assert( d_conj->getEmbeddedConjecture()==q ); } }else{ Trace("cegqi-debug") << "Register quantifier : " << q << std::endl; } } -void CegInstantiation::assertNode( Node n ) { -} - Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { if( d_conj->isAssigned() ){ - std::vector< Node > req_dec; - req_dec.push_back( d_conj->getGuard() ); - // other decision requests should ask the conjecture - for( unsigned i=0; igetValuation().hasSatValue( req_dec[i], value ) ) { - Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl; - priority = 0; - return req_dec[i]; - }else{ - Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl; - } + Node dec_req = d_conj->getNextDecisionRequest( priority ); + if( !dec_req.isNull() ){ + Trace("cegqi-debug") << "CEGQI : Decide next on : " << dec_req << "..." << std::endl; + return dec_req; } } return Node::null(); } void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { - Node q = conj->d_quant; - Node aq = conj->d_assert_quant; + Node q = conj->getEmbeddedConjecture(); + Node aq = conj->getConjecture(); if( Trace.isOn("cegqi-engine-debug") ){ conj->debugPrint("cegqi-engine-debug"); Trace("cegqi-engine-debug") << std::endl; @@ -692,9 +107,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( !conj->needsRefinement() ){ Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - if( conj->d_syntax_guided ){ + if( conj->isSyntaxGuided() ){ std::vector< Node > clems; - conj->doCegConjectureSingleInvCheck( clems ); + conj->doSingleInvCheck( clems ); if( !clems.empty() ){ d_last_inst_si = true; for( unsigned j=0; jmkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) ); if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ - //FIXME: hack to incorporate hacks from BV for division by zero + //FIXME: hack to incorporate hacks from BV for division by zero (github issue #1156) lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); } if( d_quantEngine->addLemma( lem ) ){ @@ -759,7 +174,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; std::vector< Node > cclems; - conj->doCegConjectureCheck( cclems, model_values ); + conj->doCheck( cclems, model_values ); bool addedLemma = false; for( unsigned i=0; i model_terms; - std::vector< Node > clist; - conj->getCandidateList( clist, true ); - Assert( clist.size()==q[0].getNumChildren() ); - conj->getModelValues( clist, model_terms ); - if( d_quantEngine->addInstantiation( q, model_terms ) ){ - conj->recordInstantiation( model_terms ); - }else{ - Assert( false ); - } + Trace("cegqi-engine") << " *** Check candidate phase (non-SyGuS)." << std::endl; + std::vector< Node > lems; + conj->doBasicCheck(lems); + Assert(lems.empty()); } }else{ Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; std::vector< Node > rlems; - conj->doCegConjectureRefine( rlems ); + conj->doRefine( rlems ); bool addedLemma = false; for( unsigned i=0; iaddLemma( lem ); if( res ){ ++(d_statistics.d_cegqi_lemmas_refine); - conj->d_refine_count++; + conj->incrementRefineCount(); addedLemma = true; }else{ Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; @@ -890,94 +299,13 @@ void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vecto void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_conj->isAssigned() ){ - Trace("cegqi-debug") << "Printing synth solution..." << std::endl; - //if( !(Trace.isOn("cegqi-stats")) ){ - // out << "Solution:" << std::endl; - //} - for( unsigned i=0; id_quant[0].getNumChildren(); i++ ){ - Node prog = d_conj->d_quant[0][i]; - Trace("cegqi-debug") << " print solution for " << prog << std::endl; - std::stringstream ss; - ss << prog; - std::string f(ss.str()); - f.erase(f.begin()); - TypeNode tn = prog.getType(); - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); - //get the solution - Node sol; - int status = -1; - if( d_last_inst_si ){ - Assert( d_conj->getCegConjectureSingleInv() != NULL ); - sol = d_conj->getSingleInvocationSolution( i, tn, status ); - if( !sol.isNull() ){ - sol = sol.getKind()==LAMBDA ? sol[1] : sol; - } - }else{ - Node cprog = d_conj->getCandidate( i ); - if( !d_conj->d_cinfo[cprog].d_inst.empty() ){ - sol = d_conj->d_cinfo[cprog].d_inst.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; - std::vector< Node > subs; - Expr svl = dt.getSygusVarList(); - for( unsigned j=0; jreconstructToSyntaxSingleInvocation(sol, tn, status); - sol = sol.getKind()==LAMBDA ? sol[1] : sol; - } - }else{ - status = 1; - } - }else{ - Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl; - } - } - if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){ - out << "(define-fun " << f << " "; - if( dt.getSygusVarList().isNull() ){ - out << "() "; - }else{ - out << dt.getSygusVarList() << " "; - } - out << dt.getSygusType() << " "; - if( status==0 ){ - out << sol; - }else{ - std::vector< Node > lvs; - TermDbSygus::printSygusTerm( out, sol, lvs ); - } - out << ")" << std::endl; - } - } + // print the conjecture + d_conj->printSynthSolution( out, d_last_inst_si ); }else{ Assert( false ); } } -void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { - if( n.getKind()==OR ){ - for( unsigned i=0; i d_candidates; - /** base instantiation */ - Node d_base_inst; - /** expand base inst to disjuncts */ - std::vector< Node > d_base_disj; - /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; - std::vector< std::vector< Node > > d_inner_vars_disj; - /** current extential quantifeirs whose couterexamples we must refine */ - std::vector< std::vector< Node > > d_ce_sk; - /** refinement lemmas */ - std::vector< Node > d_refinement_lemmas; - std::vector< Node > d_refinement_lemmas_base; -private: - /** get embedding */ - Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ); - /** collect constants */ - void collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ); -public: - CegConjecture( QuantifiersEngine * qe, context::Context* c ); - ~CegConjecture(); - - /** quantified formula asserted */ - Node d_assert_quant; - /** quantified formula (after processing) */ - Node d_quant; - - class CandidateInfo { - public: - CandidateInfo(){} - /** list of terms we have instantiated candidates with */ - std::vector< Node > d_inst; - }; - std::map< Node, CandidateInfo > d_cinfo; - - /** measure sum size */ - int d_measure_term_size; - /** refine count */ - unsigned d_refine_count; - - const CegConjectureSingleInv* getCegConjectureSingleInv() const { - return d_ceg_si; - } - - bool needsRefinement(); - void getCandidateList( std::vector< Node >& clist, bool forceOrig = false ); - bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, - std::vector< Node >& candidate_values, std::vector< Node >& lems ); - - void doCegConjectureSingleInvCheck(std::vector< Node >& lems); - void doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values); - void doCegConjectureRefine(std::vector< Node >& lems); - - Node getSingleInvocationSolution(unsigned sol_index, TypeNode stn, - int& reconstructed, bool rconsSygus=true){ - return d_ceg_si->getSolution(sol_index, stn, reconstructed, rconsSygus); - } - - Node reconstructToSyntaxSingleInvocation( - Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true ) { - return d_ceg_si->reconstructToSyntax(s, stn, reconstructed, rconsSygus); - } - - void recordInstantiation( std::vector< Node >& vs ) { - Assert( vs.size()==d_candidates.size() ); - for( unsigned i=0; i& lem ); - /** preregister conjecture */ - void preregisterConjecture( Node q ); - /** assign */ - void assign( Node q ); - /** is assigned */ - bool isAssigned() { return !d_quant.isNull(); } - /** get model values */ - void getModelValues( std::vector< Node >& n, std::vector< Node >& v ); - /** get model value */ - Node getModelValue( Node n ); - /** get number of refinement lemmas */ - unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } - /** get refinement lemma */ - Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; } - /** get refinement lemma */ - Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; } -}; - - class CegInstantiation : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; @@ -156,8 +33,6 @@ private: CegConjecture * d_conj; /** last instantiation by single invocation module? */ bool d_last_inst_si; - /** evaluation axioms */ - //std::map< Node, bool > d_eval_axioms; private: //for direct evaluation /** get refinement evaluation */ void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ); @@ -173,16 +48,13 @@ public: /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ - void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); - void assertNode( Node n ); + /** get the next decision request */ Node getNextDecisionRequest( unsigned& priority ); /** Identify this module (for debugging, dynamic configuration, etc..) */ 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 ); /** preregister assertion (before rewrite) */ void preregisterAssertion( Node n ); public: diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 2fa993b97..edd9c4fa3 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -119,6 +119,8 @@ void CegConjectureSingleInv::initialize( Node q ) { // can only register one quantified formula with this Assert( d_quant.isNull() ); d_quant = q; + d_simp_quant = q; + Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl; // infer single invocation-ness std::vector< Node > progs; std::map< Node, std::vector< Node > > prog_vars; @@ -140,112 +142,131 @@ void CegConjectureSingleInv::initialize( Node q ) { qq = TermDb::simpleNegate( q[1] ); } //process the single invocation-ness of the property - d_sip->init( progs, qq ); - Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; - d_sip->debugPrint( "cegqi-si" ); - - //map from program to bound variables - std::vector< Node > order_vars; - std::map< Node, Node > single_inv_app_map; - for( unsigned j=0; j::iterator it_fov = d_sip->d_func_fo_var.find( prog ); - if( it_fov!=d_sip->d_func_fo_var.end() ){ - Node pv = it_fov->second; - Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() ); - Node inv = d_sip->d_func_inv[prog]; - 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 ); - }else{ - Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl; + if( !d_sip->init( progs, qq ) ){ + Trace("cegqi-si") << "...not single invocation (type mismatch)" << std::endl; + }else{ + Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; + d_sip->debugPrint( "cegqi-si" ); + + //map from program to bound variables + std::vector< Node > order_vars; + std::map< Node, Node > single_inv_app_map; + for( unsigned j=0; j::iterator it_fov = d_sip->d_func_fo_var.find( prog ); + if( it_fov!=d_sip->d_func_fo_var.end() ){ + Node pv = it_fov->second; + Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() ); + Node inv = d_sip->d_func_inv[prog]; + 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 ); + }else{ + Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl; + } } - } - //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() ){ - if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ - //if we are doing invariant templates, then construct the template - Trace("cegqi-si") << "- Do transition inference..." << std::endl; - d_ti[q].process( qq ); - Trace("cegqi-inv") << std::endl; - if( !d_ti[q].d_func.isNull() ){ - // map the program back via non-single invocation map - Node prog = d_ti[q].d_func; - std::vector< Node > prog_templ_vars; - prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() ); - d_trans_pre[prog] = d_ti[q].getComponent( 1 ); - d_trans_post[prog] = d_ti[q].getComponent( -1 ); - 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(), prog_templ_vars.begin(), prog_templ_vars.end() ); - Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - - //construct template argument - d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() ); - - //construct template - Node templ; - if( options::sygusInvAutoUnfold() ){ - if( d_ti[q].isComplete() ){ - Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl; - // auto-unfold - DetTrace dt; - int init_dt = d_ti[q].initializeTrace( dt ); - if( init_dt==0 ){ - Trace("cegqi-inv-auto-unfold") << " Init : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << std::endl; - unsigned counter = 0; - unsigned status = 0; - while( counter<100 && status==0 ){ - status = d_ti[q].incrementTrace( dt ); - counter++; - Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; + //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() ){ + if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + //if we are doing invariant templates, then construct the template + Trace("cegqi-si") << "- Do transition inference..." << std::endl; + d_ti[q].process( qq ); + Trace("cegqi-inv") << std::endl; + if( !d_ti[q].d_func.isNull() ){ + // map the program back via non-single invocation map + Node prog = d_ti[q].d_func; + std::vector< Node > prog_templ_vars; + prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() ); + d_trans_pre[prog] = d_ti[q].getComponent( 1 ); + d_trans_post[prog] = d_ti[q].getComponent( -1 ); + 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(), prog_templ_vars.begin(), prog_templ_vars.end() ); + Trace("cegqi-inv") << " invariant : " << invariant << std::endl; + + // store simplified version of quantified formula + d_simp_quant = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] ); + std::vector< Node > new_bv; + for( unsigned j=0; jd_si_vars.size(); j++ ){ + new_bv.push_back( NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ) ); + } + d_simp_quant = d_simp_quant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_bv.begin(), new_bv.end() ); + Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); + for( unsigned j=0; jmkNode( kind::FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_bv ), d_simp_quant ).negate(); + d_simp_quant = Rewriter::rewrite( d_simp_quant ); + d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, q[0], d_simp_quant, q[2] ); + Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; + + //construct template argument + d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() ); + + //construct template + Node templ; + if( options::sygusInvAutoUnfold() ){ + if( d_ti[q].isComplete() ){ + Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl; + // auto-unfold + DetTrace dt; + int init_dt = d_ti[q].initializeTrace( dt ); + if( init_dt==0 ){ + Trace("cegqi-inv-auto-unfold") << " Init : "; dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl; - } - if( status==1 ){ - // we have a trivial invariant - templ = d_ti[q].constructFormulaTrace( dt ); - Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl; - Trace("cegqi-inv") << " " << templ << std::endl; - // FIXME : this should be unnecessary - templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] ); + Trace("cegqi-inv-auto-unfold") << std::endl; + unsigned counter = 0; + unsigned status = 0; + while( counter<100 && status==0 ){ + status = d_ti[q].incrementTrace( dt ); + counter++; + Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl; + } + if( status==1 ){ + // we have a trivial invariant + templ = d_ti[q].constructFormulaTrace( dt ); + Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl; + Trace("cegqi-inv") << " " << templ << std::endl; + // FIXME : this should be unnecessary + templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] ); + } + }else{ + Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; } - }else{ - Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; } } - } - if( templ.isNull() ){ - if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ - //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); - templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] ); - }else{ - Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); - //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); - templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] ); + if( templ.isNull() ){ + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); + templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] ); + }else{ + Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); + //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); + templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] ); + } } + Trace("cegqi-inv") << " template (pre-substitution) : " << templ << std::endl; + Assert( !templ.isNull() ); + // subsitute the template arguments + templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() ); + Trace("cegqi-inv") << " template : " << templ << std::endl; + d_templ[prog] = templ; } - Trace("cegqi-inv") << " template (pre-substitution) : " << templ << std::endl; - Assert( !templ.isNull() ); - // subsitute the template arguments - templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() ); - Trace("cegqi-inv") << " template : " << templ << std::endl; - d_templ[prog] = templ; } + }else{ + //we are fully single invocation + d_single_invocation = true; } - }else{ - //we are fully single invocation - d_single_invocation = true; } } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index ad0f4f595..ffcdb7075 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -164,11 +164,9 @@ class CegConjectureSingleInv { bool isEligibleForInstantiation( Node n ); // add lemma bool addLemma( Node lem ); - public: - CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); - ~CegConjectureSingleInv(); // conjecture Node d_quant; + Node d_simp_quant; // are we single invocation? bool d_single_invocation; // single invocation portion of quantified formula @@ -181,6 +179,15 @@ class CegConjectureSingleInv { std::map< Node, Node > d_templ; // the template argument for each function to synthesize (occurs in exactly one position of its template) std::map< Node, Node > d_templ_arg; + + public: + CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); + ~CegConjectureSingleInv(); + + // get simplified conjecture + Node getSimplifiedConjecture() { return d_simp_quant; } + // get single invocation guard + Node getGuard() { return d_si_guard; } public: //get the single invocation lemma(s) void getInitialSingleInvLemma( std::vector< Node >& lems ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 4cb41e19e..02f1b8509 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -931,7 +931,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto return true; } } - if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol ) || ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){ + if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol && options::varElimQuant() ) || + ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){ //for arithmetic, solve the (in)equality std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( lit, msum ) ){ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 01f3be1a1..d8f675af1 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -63,7 +63,8 @@ TESTS = commutative.sy \ qe.sy \ cggmp.sy \ parse-bv-let.sy \ - cegar1.sy + cegar1.sy \ + triv-type-mismatch-si.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/triv-type-mismatch-si.sy b/test/regress/regress0/sygus/triv-type-mismatch-si.sy new file mode 100644 index 000000000..e2935af51 --- /dev/null +++ b/test/regress/regress0/sygus/triv-type-mismatch-si.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic LIA) + +(synth-fun R ((y Int)) Bool) +(synth-fun e () Int) + +(declare-var x Int) + +(constraint (=> (= x e) (R x))) + +(check-synth) + -- 2.30.2