* 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
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 \
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
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
--- /dev/null
+/********************* */
+/*! \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<n.getNumChildren(); i++ ){
+ collectDisjuncts( n[i], d );
+ }
+ }else{
+ d.push_back( n );
+ }
+}
+
+CegConjecture::CegConjecture( QuantifiersEngine * qe )
+ : 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; i<n.getNumChildren(); i++ ){
+ Node nc = convertToEmbedding( n[i], synth_fun_vars, visited );
+ childChanged = childChanged || nc!=n[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( 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<Rational>().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; i<n.getNumChildren(); i++ ){
+ collectConstants( n[i], consts, visited );
+ }
+ }
+}
+
+
+void CegConjecture::assign( Node q ) {
+ Assert( d_embed_quant.isNull() );
+ Assert( q.getKind()==FORALL );
+ Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
+ d_quant = q;
+
+ Node simp_quant = q;
+ //register with single invocation if applicable
+ if( d_qe->getTermDatabase()->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; i<simp_quant[0].getNumChildren(); i++ ){
+ Node v = simp_quant[0][i];
+ Node sf = v.getAttribute(SygusSynthFunAttribute());
+ Assert( !sf.isNull() );
+ Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
+ // sfvl may be null for constant synthesis functions
+ Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+ TypeNode tn;
+ std::stringstream ss;
+ ss << sf;
+ if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
+ tn = v.getType();
+ }else{
+ // make the default grammar
+ tn = d_qe->getTermDatabaseSygus()->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; j<sfvl.getNumChildren(); j++ ){
+ schildren.push_back( sfvl[j] );
+ largs.push_back( NodeManager::currentNM()->mkBoundVar( 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; i<q[0].getNumChildren(); i++ ){
+ vars.push_back( q[0][i] );
+ Node e = NodeManager::currentNM()->mkSkolem( "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<d_candidates.size(); i++ ){
+ Node e = d_candidates[i];
+ if( options::sygusPbe() ){
+ std::vector< std::vector< Node > > 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<d_base_disj.size(); j++ ){
+ Trace("cegqi") << " " << j << " : " << d_base_disj[j] << std::endl;
+ d_inner_vars_disj.push_back( std::vector< Node >() );
+ //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; k<d_base_disj[j][0][0].getNumChildren(); k++ ){
+ d_inner_vars.push_back( d_base_disj[j][0][0][k] );
+ d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] );
+ }
+ }
+ }
+ d_syntax_guided = true;
+ }else if( d_qe->getTermDatabase()->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; i<lems.size(); i++ ){
+ Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
+ d_qe->getOutputChannel().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; i<guarded_lemmas.size(); i++ ){
+ Node lem = NodeManager::currentNM()->mkNode( 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.size(); i++ ){
+ Trace("cegqi-check") << " " << i << " : " << d_candidates[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; i<d.size(); i++ ){
+ Node dr = Rewriter::rewrite( d[i] );
+ if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+ if( constructed_cand ){
+ ic.push_back( d_qe->getTermDatabase()->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; k<d_ce_sk[0].size(); k++ ){
+ Node ce_q = d_ce_sk[0][k];
+ if( !ce_q.isNull() ){
+ Assert( !d_inner_vars_disj[k].empty() );
+ Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->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<d_inner_vars_disj[k].size(); i++ ){
+ sk_vars.push_back( d_inner_vars_disj[k][i] );
+ sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value
+ }
+ }
+ }
+ }
+
+ //for conditional evaluation
+ std::vector< Node > 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; k<d_ce_sk[0].size(); k++ ){
+ Node ce_q = d_ce_sk[0][k];
+ Trace("cegqi-refine-debug") << " For counterexample point, disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl;
+ Node c_disj;
+ if( !ce_q.isNull() ){
+ Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL );
+ c_disj = d_base_disj[k][0][1];
+ }else{
+ if( d_inner_vars_disj[k].empty() ){
+ c_disj = d_base_disj[k].negate();
+ }else{
+ //denegrate case : quantified disjunct was trivially true and does not need to be refined
+ Trace("cegqi-refine-debug") << "*** skip " << d_base_disj[k] << std::endl;
+ }
+ }
+ if( !c_disj.isNull() ){
+ //compute the body, inst_cond
+ //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
+ lem_c.push_back( c_disj );
+ }
+ }
+ Assert( sk_vars.size()==sk_subs.size() );
+
+ Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( 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<n.size(); i++ ){
+ Node nv = getModelValue( n[i] );
+ v.push_back( nv );
+ if( Trace.isOn("cegqi-engine") ){
+ TypeNode tn = nv.getType();
+ Trace("cegqi-engine") << n[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; i<d_candidates.size(); i++ ){
+ Trace(c) << d_candidates[i] << " ";
+ }
+ Trace(c) << std::endl;
+ Trace(c) << " * Candidate ce skolems : ";
+ for( unsigned i=0; i<d_ce_sk.size(); i++ ){
+ Trace(c) << d_ce_sk[i] << " ";
+ }
+}
+
+Node CegConjecture::getCurrentStreamGuard() const {
+ if( d_stream_guards.empty() ){
+ return Node::null();
+ }else{
+ return d_stream_guards.back();
+ }
+}
+
+Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
+ // first, must try the guard
+ // which denotes "this conjecture is feasible"
+ Node feasible_guard = getGuard();
+ bool value;
+ if( !d_qe->getValuation().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; i<clist.size(); i++ ){
+ Node cprog = clist[i];
+ Node sol = cprog;
+ if( !d_cinfo[cprog].d_inst.empty() ){
+ sol = d_cinfo[cprog].d_inst.back();
+ // add to explanation of exclusion
+ d_qe->getTermDatabaseSygus()->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; i<d_embed_quant[0].getNumChildren(); i++ ){
+ Node prog = d_embed_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( singleInvocation ){
+ Assert( d_ceg_si != NULL );
+ sol = d_ceg_si->getSolution( 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 */
--- /dev/null
+/********************* */
+/*! \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<vs.size(); i++ ){
+ d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
+ }
+ }
+ //-------------------------------- sygus stream
+ /** the streaming guards for sygus streaming mode */
+ std::vector< Node > 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
** 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;
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; i<n.getNumChildren(); i++ ){
- Node nc = convertToEmbedding( n[i], synth_fun_vars, visited );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( 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<Rational>().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; i<n.getNumChildren(); i++ ){
- collectConstants( n[i], consts, visited );
- }
- }
-}
-
-
-void CegConjecture::assign( Node q ) {
- Assert( d_quant.isNull() );
- Assert( q.getKind()==FORALL );
- Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
- d_assert_quant = q;
-
- //register with single invocation if applicable
- if( d_qe->getTermDatabase()->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; i<q[0].getNumChildren(); i++ ){
- Node v = q[0][i];
- Node sf = v.getAttribute(SygusSynthFunAttribute());
- Assert( !sf.isNull() );
- Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
- // sfvl may be null for constant synthesis functions
- Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
- TypeNode tn;
- std::stringstream ss;
- ss << sf;
- if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
- tn = v.getType();
- }else{
- // make the default grammar
- tn = d_qe->getTermDatabaseSygus()->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; i<q[0].getNumChildren(); i++ ){
- vars.push_back( q[0][i] );
- Node e = NodeManager::currentNM()->mkSkolem( "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<d_candidates.size(); i++ ){
- Node e = d_candidates[i];
- if( options::sygusPbe() ){
- std::vector< std::vector< Node > > 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<d_base_disj.size(); j++ ){
- Trace("cegqi") << " " << j << " : " << d_base_disj[j] << std::endl;
- d_inner_vars_disj.push_back( std::vector< Node >() );
- //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; k<d_base_disj[j][0][0].getNumChildren(); k++ ){
- d_inner_vars.push_back( d_base_disj[j][0][0][k] );
- d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] );
- }
- }
- }
- d_syntax_guided = true;
- }else if( d_qe->getTermDatabase()->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; i<lems.size(); i++ ){
- Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
- d_qe->getOutputChannel().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; i<guarded_lemmas.size(); i++ ){
- Node lem = NodeManager::currentNM()->mkNode( 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.size(); i++ ){
- Trace("cegqi-check") << " " << i << " : " << d_candidates[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; i<d.size(); i++ ){
- Node dr = Rewriter::rewrite( d[i] );
- if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
- if( constructed_cand ){
- ic.push_back( d_qe->getTermDatabase()->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; k<d_ce_sk[0].size(); k++ ){
- Node ce_q = d_ce_sk[0][k];
- if( !ce_q.isNull() ){
- Assert( !d_inner_vars_disj[k].empty() );
- Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->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<d_inner_vars_disj[k].size(); i++ ){
- sk_vars.push_back( d_inner_vars_disj[k][i] );
- sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value
- }
- }
- }
- }
-
- std::map< Node, Node > 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<d_ce_sk[0].size(); k++ ){
- Node ce_q = d_ce_sk[0][k];
- Trace("cegqi-refine-debug") << " For counterexample point, disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl;
- Node c_disj;
- if( !ce_q.isNull() ){
- Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL );
- c_disj = d_base_disj[k][0][1];
- }else{
- if( d_inner_vars_disj[k].empty() ){
- c_disj = d_base_disj[k].negate();
- }else{
- //denegrate case : quantified disjunct was trivially true and does not need to be refined
- Trace("cegqi-refine-debug") << "*** skip " << d_base_disj[k] << std::endl;
- }
- }
- if( !c_disj.isNull() ){
- //compute the body, inst_cond
- //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
- lem_c.push_back( c_disj );
- }
- }
- Assert( sk_vars.size()==sk_subs.size() );
- //add conditional correctness assumptions
- std::vector< Node > 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<n.size(); i++ ){
- Node nv = getModelValue( n[i] );
- v.push_back( nv );
- if( Trace.isOn("cegqi-engine") ){
- TypeNode tn = nv.getType();
- Trace("cegqi-engine") << n[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; i<d_candidates.size(); i++ ){
- Trace(c) << d_candidates[i] << " ";
- }
- Trace(c) << std::endl;
- Trace(c) << " * Candidate ce skolems : ";
- for( unsigned i=0; i<d_ce_sk.size(); i++ ){
- Trace(c) << d_ce_sk[i] << " ";
- }
-}
-
CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
- d_conj = new CegConjecture( qe, qe->getSatContext() );
+ d_conj = new CegConjecture( qe );
d_last_inst_si = false;
}
}
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;
}
}
-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; i<req_dec.size(); i++ ){
- bool value;
- if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) {
- Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl;
- 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;
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; j<clems.size(); j++ ){
for( unsigned j=0; j<eager_terms.size(); j++ ){
Node lem = NodeManager::currentNM()->mkNode( 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 ) ){
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<cclems.size(); i++ ){
Node lem = cclems[i];
}
}else{
Assert( aq==q );
- std::vector< Node > 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; i<rlems.size(); i++ ){
Node lem = rlems[i];
bool res = d_quantEngine->addLemma( 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;
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; i<d_conj->d_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; j<svl.getNumChildren(); j++ ){
- subs.push_back( Node::fromExpr( svl[j] ) );
- }
- if( sol==sygus_sol ){
- sol = sygus_sol;
- status = 1;
- }else{
- Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
- sol = Rewriter::rewrite( sol );
- Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
- sol = d_conj->reconstructToSyntaxSingleInvocation(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<n.getNumChildren(); i++ ){
- collectDisjuncts( n[i], d );
- }
- }else{
- d.push_back( n );
- }
-}
-
void CegInstantiation::preregisterAssertion( Node n ) {
//check if it sygus conjecture
if( TermDb::isSygusConjecture( n ) ){
#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
-#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
-#include "options/quantifiers_modes.h"
-#include "options/datatypes_modes.h"
-#include "theory/quantifiers/ce_guided_single_inv.h"
-#include "theory/quantifiers/ce_guided_pbe.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-/** a synthesis conjecture */
-class CegConjecture {
-private:
- QuantifiersEngine * d_qe;
- /** 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;
-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<vs.size(); i++ ){
- d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
- }
- }
- Node getCandidate( unsigned int i ) { return d_candidates[i]; }
-
- void debugPrint( const char * c );
-
-private:
- /** single invocation utility */
- CegConjectureSingleInv * d_ceg_si;
- /** program by examples utility */
- CegConjecturePbe * d_ceg_pbe;
-public: //non-syntax guided (deprecated)
- /** guard */
- bool d_syntax_guided;
- Node d_nsg_guard;
-public:
- /** get guard */
- Node getGuard();
- /** is ground */
- bool isGround() { return d_inner_vars.empty(); }
- /** fairness */
- SygusFairMode getCegqiFairMode();
- /** is single invocation */
- bool isSingleInvocation() const;
- /** is single invocation */
- bool isFullySingleInvocation();
- /** needs check */
- bool needsCheck( std::vector< Node >& 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<Node, bool, NodeHashFunction> NodeBoolMap;
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 );
/* 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:
// 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;
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<progs.size(); j++ ){
- Node prog = progs[j];
- std::map< Node, Node >::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<progs.size(); j++ ){
+ Node prog = progs[j];
+ std::map< Node, Node >::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; j<d_sip->d_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; j<q[1][0][0].getNumChildren(); j++ ){
+ new_bv.push_back( q[1][0][0][j] );
+ }
+ d_simp_quant = NodeManager::currentNM()->mkNode( 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;
}
}
}
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
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 );
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 ) ){
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
--- /dev/null
+; 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)
+
projects / cvc5.git / commitdiff