From: ajreynol Date: Mon, 16 May 2016 22:30:59 +0000 (-0500) Subject: Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean... X-Git-Tag: cvc5-1.0.0~6049^2~46 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=246fffffafba07aaeadd0d0c99a2e1c4b589a63c;p=cvc5.git Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi. --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 34f399f45..227540f45 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -258,7 +258,7 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true 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 sygusDirectEval --sygus-direct-eval bool :default false +option sygusDirectEval --sygus-direct-eval bool :default true direct unfolding of evaluation functions # approach applied to general quantified formulas diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index cfbadbf32..5fdc549d0 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -459,7 +459,7 @@ Node TBitblaster::getTermModel(TNode node, bool fullModel) { if (Theory::isLeafOf(node, theory::THEORY_BV)) { // if it is a leaf may ask for fullModel - value = getModelFromSatSolver(node, fullModel); + value = getModelFromSatSolver(node, true); Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n"; Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); if (!value.isNull()) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 3b54e3794..a103d1f63 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -216,7 +216,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - Node const_value = getModelFromSatSolver(var, fullModel); + Node const_value = getModelFromSatSolver(var, true); if(const_value != Node()) { Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index c821b50cd..b549c329a 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -491,7 +491,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - Node const_value = getModelFromSatSolver(var, fullModel); + Node const_value = getModelFromSatSolver(var, true); Assert (const_value.isNull() || const_value.isConst()); if(const_value != Node()) { Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 152a335a5..2bcb6ca1b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -349,7 +349,7 @@ Node RewriteRule::apply(TNode node) { Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); + Node a_udiv_b = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b); Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b); Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0); @@ -377,7 +377,7 @@ Node RewriteRule::apply(TNode node) { Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); - Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); + Node a_urem_b = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b); Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b); Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 5bd6680f2..b32a70212 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -420,13 +420,14 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt } } //push - if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG ){ + if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG || k==ITE ){ //negation normal form if( parent==k && isArgDatatype( dt[c], 0, pdt ) ){ return false; } Kind nk = UNDEFINED_KIND; - Kind reqk = UNDEFINED_KIND; //required kind for all children + Kind reqk = UNDEFINED_KIND; //required kind for all children + std::map< unsigned, Kind > reqkc; //required kind for some children if( parent==NOT ){ if( k==AND ) { nk = OR;reqk = NOT; @@ -437,8 +438,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt }else if( k==XOR ) { nk = IFF; } - } - if( parent==BITVECTOR_NOT ){ + }else if( parent==BITVECTOR_NOT ){ if( k==BITVECTOR_AND ) { nk = BITVECTOR_OR;reqk = BITVECTOR_NOT; }else if( k==BITVECTOR_OR ){ @@ -448,16 +448,21 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt }else if( k==BITVECTOR_XOR ) { nk = BITVECTOR_XNOR; } - } - if( parent==UMINUS ){ + }else if( parent==UMINUS ){ if( k==PLUS ){ nk = PLUS;reqk = UMINUS; } - } - if( parent==BITVECTOR_NEG ){ + }else if( parent==BITVECTOR_NEG ){ if( k==PLUS ){ nk = PLUS;reqk = BITVECTOR_NEG; } + }else if( k==ITE ){ + //ITE lifting + if( parent!=ITE ){ + nk = ITE; + reqkc[1] = parent; + reqkc[2] = parent; + } } if( nk!=UNDEFINED_KIND ){ Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk; @@ -468,37 +473,38 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt int pcr = d_tds->getKindArg( tnp, nk ); if( pcr!=-1 ){ Assert( pcr<(int)pdt.getNumConstructors() ); - if( reqk!=UNDEFINED_KIND ){ + if( reqk!=UNDEFINED_KIND || !reqkc.empty() ){ //must have same number of arguments if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){ - bool success = true; - std::map< int, TypeNode > childTypes; for( unsigned i=0; igetArgType( pdt[pcr], i ); Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) ); + std::vector< Kind > rks; if( reqk!=UNDEFINED_KIND ){ - //child must have a NOT - int nindex = d_tds->getKindArg( tna, reqk ); + rks.push_back( reqk ); + } + std::map< unsigned, Kind >::iterator itr = reqkc.find( i ); + if( itr!=reqkc.end() ){ + rks.push_back( itr->second ); + } + for( unsigned j=0; jgetKindArg( tna, rkc ); if( nindex!=-1 ){ const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype(); if( d_tds->getArgType( dt[c], i )!=d_tds->getArgType( adt[nindex], 0 ) ){ Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl; - success = false; - break; + return true; } }else{ - Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl; - success = false; - break; + Trace("sygus-split-debug") << "...argument " << i << " does not have " << rkc << "." << std::endl; + return true; } - }else{ - childTypes[i] = tna; } } - if( success ){ - Trace("sygus-split-debug") << "...success" << std::endl; - return false; - } + Trace("sygus-split-debug") << "...success" << std::endl; + return false; }else{ Trace("sygus-split-debug") << "...#arg mismatch." << std::endl; } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index cae3e730e..8af11b1af 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" #include "prop/prop_engine.h" +#include "theory/bv/theory_bv_rewriter.h" using namespace CVC4::kind; using namespace std; @@ -56,12 +57,15 @@ void CegConjecture::assign( Node q ) { } } d_quant = q; + Assert( d_candidates.empty() ); + std::vector< Node > vars; for( unsigned i=0; imkSkolem( "e", q[0][i].getType() ) ); } Trace("cegqi") << "Base quantified formula is : " << q << std::endl; //construct base instantiation - d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) ); + d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) ); 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 ); @@ -272,9 +276,26 @@ void CegInstantiation::preRegisterQuantifier( Node q ) { if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ - //take ownership of this quantified formula (will use direct evaluation instead of instantiation) - d_quantEngine->setOwner( q, this ); - d_eval_axioms[q] = true; + //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() || ptn.isBitVector() ){ + 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; + } } } } @@ -413,8 +434,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } if( !eager_eval_lem.empty() ){ for( unsigned j=0; jaddLemma( eager_eval_lem[j] ); + Node lem = eager_eval_lem[j]; + if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ + //FIXME: hack to incorporate hacks from BV for division by zero + lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); + } + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl; + d_quantEngine->addLemma( lem ); } return; } @@ -435,6 +461,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } } //must get a counterexample to the value of the current candidate + Assert( conj->d_candidates.size()==model_values.size() ); Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); //check whether we will run CEGIS on inner skolem variables bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 ); @@ -686,6 +713,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) } Assert( subs[j-1].getType()==var_list[j-1].getType() ); } + Assert( vars.size()==subs.size() ); bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl; Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 33856d226..a5d4174dd 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -534,6 +534,7 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ return false; }else{ Trace("cegqi-engine") << siss.str() << std::endl; + Assert( d_single_inv_var.size()==subs.size() ); Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){ Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; @@ -595,6 +596,7 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { for( unsigned i=0; id_all_vars.size(); i++ ){ subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) ); } + Assert( d_sip->d_all_vars.size()==subs.size() ); inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() ); Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl; Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl; @@ -751,6 +753,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& std::sort( indices.begin(), indices.end(), ssii ); Trace("csi-sol") << "Construct solution" << std::endl; s = constructSolution( indices, sol_index, 0 ); + Assert( vars.size()==d_sol->d_varList.size() ); s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() ); } d_orig_solution = s; @@ -922,6 +925,7 @@ void SingleInvocationPartition::process( Node n ) { std::vector< Node > funcs; //normalize the invocations if( !terms.empty() ){ + Assert( terms.size()==subs.size() ); cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); } std::vector< Node > children; @@ -940,6 +944,7 @@ void SingleInvocationPartition::process( Node n ) { } Trace("si-prt") << std::endl; cr = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + Assert( terms.size()==subs.size() ); cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; //now must check if it has other bound variables @@ -974,6 +979,7 @@ void SingleInvocationPartition::process( Node n ) { } } } + Assert( terms.size()==subs.size() ); cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); } cr = Rewriter::rewrite( cr ); @@ -982,6 +988,7 @@ void SingleInvocationPartition::process( Node n ) { TermDb::getBoundVars( cr, d_all_vars ); if( singleInvocation ){ //replace with single invocation formulation + Assert( si_terms.size()==si_subs.size() ); cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() ); cr = Rewriter::rewrite( cr ); Trace("si-prt") << ".....si version=" << cr << std::endl; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index eff641736..e81245034 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2480,8 +2480,8 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; - Assert( n.getKind()==APPLY_CONSTRUCTOR ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( n.getKind()==APPLY_CONSTRUCTOR ); unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); Assert( n.getNumChildren()==dt[i].getNumArgs() ); std::map< TypeNode, int > var_count; @@ -3200,9 +3200,17 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > } } +Node TermDbSygus::getAnchor( Node n ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + return getAnchor( n[0] ); + }else{ + return n; + } +} + void TermDbSygus::registerEvalTerm( Node n ) { if( options::sygusDirectEval() ){ - if( n.getKind()==APPLY_UF ){ + if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl; TypeNode tn = n[0].getType(); if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ @@ -3210,58 +3218,72 @@ void TermDbSygus::registerEvalTerm( Node n ) { if( dt.isSygus() ){ Node f = n.getOperator(); Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl; - Assert( n[0].getKind()!=APPLY_CONSTRUCTOR ); - d_evals[n[0]].push_back( n ); - TypeNode tn = n[0].getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Node var_list = Node::fromExpr( dt.getSygusVarList() ); - Assert( dt.isSygus() ); - d_eval_args[n[0]].push_back( std::vector< Node >() ); - for( unsigned j=1; jmkConst(BitVector(1u, 1u)); - d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); - }else{ - d_eval_args[n[0]].back().push_back( n[j] ); + if( n[0].getKind()!=APPLY_CONSTRUCTOR ){ + d_evals[n[0]].push_back( n ); + TypeNode tn = n[0].getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + Assert( dt.isSygus() ); + d_eval_args[n[0]].push_back( std::vector< Node >() ); + for( unsigned j=1; jmkConst(BitVector(1u, 1u)); + d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); + }else{ + d_eval_args[n[0]].back().push_back( n[j] ); + } } + Node a = getAnchor( n[0] ); + d_subterms[a][n[0]] = true; } - } } } } } -void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) { - std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n ); - if( it!=d_eval_args.end() && !it->second.empty() ){ - unsigned start = d_node_mv_args_proc[n][v]; - Node antec = n.eqNode( v ).negate(); - TypeNode tn = n.getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); - Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl; - Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl; - Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn ); - Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl; - std::vector< Node > vars; - Node var_list = Node::fromExpr( dt.getSygusVarList() ); - for( unsigned j=0; jsecond.size(); i++ ){ - Assert( vars.size()==it->second[i].size() ); - Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); - Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); - lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); - Trace("sygus-eager") << "Lemma : " << lem << std::endl; - lems.push_back( lem ); - } - d_node_mv_args_proc[n][v] = it->second.size(); +void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) { + std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a ); + if( its!=d_subterms.end() ){ + Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl; + for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){ + Node n = itss->first; + Trace("sygus-eager-debug") << "...process : " << n << std::endl; + std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n ); + if( it!=d_eval_args.end() && !it->second.empty() ){ + TNode at = a; + TNode vt = v; + Node vn = n.substitute( at, vt ); + vn = Rewriter::rewrite( vn ); + unsigned start = d_node_mv_args_proc[n][vn]; + Node antec = n.eqNode( vn ).negate(); + TypeNode tn = n.getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl; + Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl; + Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn ); + Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl; + std::vector< Node > vars; + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + for( unsigned j=0; jsecond.size(); i++ ){ + Assert( vars.size()==it->second[i].size() ); + Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); + Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); + lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); + Trace("sygus-eager") << "Lemma : " << lem << std::endl; + lems.push_back( lem ); + } + d_node_mv_args_proc[n][vn] = it->second.size(); + } + } } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 4291587a4..b7b798cd4 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -557,7 +557,6 @@ public: private: std::map< TypeNode, std::map< int, Node > > d_generic_base; std::map< TypeNode, std::vector< Node > > d_generic_templ; - Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); bool getMatch( Node p, Node n, std::map< int, Node >& s ); bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s ); public: @@ -622,6 +621,7 @@ public: /** get value */ Node getTypeMaxValue( TypeNode tn ); TypeNode getSygusTypeForVar( Node v ); + Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node sygusToBuiltin( Node n, TypeNode tn ); Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 ); @@ -641,8 +641,11 @@ public: /** print sygus term */ static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); + /** get anchor */ + static Node getAnchor( Node n ); //for eager instantiation private: + std::map< Node, std::map< Node, bool > > d_subterms; std::map< Node, std::vector< Node > > d_evals; std::map< Node, std::vector< std::vector< Node > > > d_eval_args; std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 21be4ea4f..8984cc5f4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -655,6 +655,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ for( unsigned i=0; iregisterQuantifier( f ); } + //TODO: remove this Node ceBody = d_term_db->getInstConstantBody( f ); //also register it with the strong solver //if( options::finiteModelFind() ){ @@ -887,6 +888,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std Node body; //process partial instantiation if necessary if( d_term_db->d_vars[q].size()!=vars.size() ){ + Assert( vars.size()==terms.size() ); body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); std::vector< Node > uninst_vars; //doing a partial instantiation, must add quantifier for all uninstantiated variables @@ -901,6 +903,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std Trace("partial-inst") << " : " << body << std::endl; }else{ if( options::cbqi() ){ + Assert( vars.size()==terms.size() ); body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); }else{ //do optimized version @@ -933,6 +936,7 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){ } Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) { + Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() ); return getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); } diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 695c52cc6..b503a65b8 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -50,7 +50,8 @@ TESTS = commutative.sy \ no-mention.sy \ max2-univ.sy \ strings-small.sy \ - strings-unconstrained.sy + strings-unconstrained.sy \ + hd-sdiv.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress0/sygus/hd-sdiv.sy new file mode 100644 index 000000000..3ac9334b2 --- /dev/null +++ b/test/regress/regress0/sygus/hd-sdiv.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth +(set-logic BV) + +(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001)) + +(synth-fun f ((x (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvsdiv Start Start) + (bvand Start Start) + x + #x00000001)))) + +(declare-var y (BitVec 32)) +(constraint (= (hd01 y) (f y))) +(check-synth) +