summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_instantiation.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp724
1 files changed, 26 insertions, 698 deletions
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; 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;
}
@@ -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; 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;
@@ -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; j<clems.size(); j++ ){
@@ -743,7 +158,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
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 ) ){
@@ -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<cclems.size(); i++ ){
Node lem = cclems[i];
@@ -788,21 +203,15 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
}
}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];
@@ -810,7 +219,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
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;
@@ -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; 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 ) ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback