From 8d140a28c76095e148acd64e47b5ca0a92ca09be Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 5 Mar 2015 14:59:15 +0100 Subject: [PATCH] Minor fixes. Extend cegqi-si to real arithmetic. --- src/parser/smt2/Smt2.g | 3 + src/parser/smt2/smt2.cpp | 4 + src/smt/smt_engine.cpp | 4 + .../quantifiers/ce_guided_single_inv.cpp | 124 ++++++++++++++---- src/theory/quantifiers/ce_guided_single_inv.h | 5 +- 5 files changed, 109 insertions(+), 31 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 902e745ea..576767c78 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -622,6 +622,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); std::map evals; + if( sorts[0]!=range ){ + PARSER_STATE->parseError(std::string("Bad return type in grammar for SyGuS function ") + fun); + } // make all the evals first, since they are mutually referential for(size_t i = 0; i < datatypeTypes.size(); ++i) { DatatypeType dtt = datatypeTypes[i]; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3db2e252d..20f3c364b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -306,6 +306,10 @@ void Smt2::setLogic(std::string name) { name = "UFLRA"; } else if(name == "LIA") { name = "UFLIA"; + } else if(name == "LRA") { + name = "UFLRA"; + } else if(name == "LIRA") { + name = "UFLIRA"; } else if(name == "BV") { name = "UFBV"; } else { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8ad321602..eca8c9d17 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1367,6 +1367,10 @@ void SmtEngine::setDefaults() { if( !options::miniscopeQuantFreeVar.wasSetByUser() ){ options::miniscopeQuantFreeVar.set( false ); } + //rewrite divk + if( !options::rewriteDivk.wasSetByUser()) { + options::rewriteDivk.set( true ); + } } //implied options... diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 7c004c377..e5f5327c8 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -448,7 +448,6 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Node pv = d_single_inv_sk[i]; TypeNode pvtn = pv.getType(); Node pvr; - Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) //[1] easy case : pv is in the equivalence class as another term not containing pv if( ee->hasTerm( pv ) ){ @@ -463,6 +462,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v //must be an eligible term if( d_inelig.find( n )==d_inelig.end() ){ Node ns; + Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) bool proc = false; if( !d_prog_var[n].empty() ){ ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); @@ -506,6 +506,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v //must be an eligible term if( d_inelig.find( n )==d_inelig.end() ){ Node ns; + Node pv_coeff; if( !d_prog_var[n].empty() ){ ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); if( !ns.isNull() ){ @@ -513,7 +514,6 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } }else{ ns = n; - pv_coeff = Node::null(); } if( !ns.isNull() ){ bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); @@ -629,6 +629,14 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; Node val = vatom[ ires==1 ? 1 : 0 ]; Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + Node veq_c; + if( pvm!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } //push negation downwards if( !pol ){ ires = -ires; @@ -638,13 +646,8 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v }else if( pvtn.isReal() ){ //now is strict inequality ires = ires*2; - } - } - Node veq_c; - if( pvm!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==pv ); + }else{ + Assert( false ); } } if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ @@ -664,8 +667,9 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v //[4] resort to using value in model Node mv = d_qe->getModel()->getValue( pv ); + Node pv_coeff_m; Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl; - return addInstantiationInc( mv, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems ); + return addInstantiationInc( mv, pv, pv_coeff_m, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems ); } } @@ -676,16 +680,42 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff //must ensure variables have been computed for n computeProgVars( n ); //substitute into previous substitutions, when applicable - std::map< int, Node > prev; + std::vector< Node > a_subs; + a_subs.push_back( n ); + std::vector< Node > a_var; + a_var.push_back( pv ); + std::vector< Node > a_coeff; + std::vector< Node > a_has_coeff; + if( !pv_coeff.isNull() ){ + a_coeff.push_back( pv_coeff ); + a_has_coeff.push_back( pv ); + } + + std::map< int, Node > prev_subs; + std::map< int, Node > prev_coeff; + std::vector< Node > new_has_coeff; for( unsigned j=0; jmkNode( MULT, coeff[j], a_pv_coeff ) ); + } + } + if( subs[j]!=prev_subs[j] ){ + computeProgVars( subs[j] ); } } } @@ -711,10 +741,16 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff has_coeff.pop_back(); } subs_typ.pop_back(); - //revert substitution - for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); it++ ){ + //revert substitution information + for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ subs[it->first] = it->second; } + for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ + coeff[it->first] = it->second; + } + for( unsigned i=0; i& subs, s std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j, std::vector< Node >& lems ) { if( j==has_coeff.size() ){ - return addInstantiation( subs, vars, lems ); + return addInstantiation( subs, vars, subs_typ, lems ); }else{ unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); Node prev = subs[index]; @@ -752,7 +788,14 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s if( !veq_c.isNull() ){ subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); if( subs_typ[index]>0 ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], NodeManager::currentNM()->mkConst( Rational( 1 ) ) ); + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ), + NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) + ); } } Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; @@ -761,7 +804,14 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s }else{ //equalities are both upper and lower bounds if( subs_typ[index]==0 && !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], NodeManager::currentNM()->mkConst( Rational( 1 ) ) ); + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ), + NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) + ); if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ return true; } @@ -773,7 +823,6 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s // can always invert subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst() ), subs[index] ); subs[index] = Rewriter::rewrite( subs[index] ); - //TODO : delta rational Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl; if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ return true; @@ -787,7 +836,26 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s } } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& lems ) { +bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems ) { + // do delta rationals + std::map< int, Node > prev; + for( unsigned i=0; imkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); + lems.push_back( NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ) ); + } + subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); + } + } + Trace("cegqi-engine") << " * single invocation: " << std::endl; + for( unsigned j=0; j " << subs[j] << std::endl; + } //check if we have already added this instantiation bool alreadyExists; if( options::incrementalSolving() ){ @@ -795,16 +863,14 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v }else{ alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); } + Trace("cegqi-engine") << " * success = " << !alreadyExists << std::endl; if( alreadyExists ){ + //revert the substitution + for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){ + subs[it->first] = it->second; + } return false; }else{ - Trace("cegqi-engine") << " * single invocation: " << std::endl; - for( unsigned j=0; j " << subs[j] << std::endl; - } Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); lem = Rewriter::rewrite( lem ); Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 0576730b2..b8865d243 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -71,6 +71,7 @@ private: std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; private: + Node d_n_delta; //for adding instantiations during check void computeProgVars( Node n ); bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, @@ -82,9 +83,9 @@ private: bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j, std::vector< Node >& lems ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& lems ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems ); Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); public: CegConjectureSingleInv( CegConjecture * p ); // original conjecture -- 2.30.2