From: ajreynol Date: Thu, 2 Jul 2015 14:54:10 +0000 (+0200) Subject: On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros... X-Git-Tag: cvc5-1.0.0~6267^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69769dae4886621f82c2905b82db727bf2e8cf3f;p=cvc5.git On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros-quant in incremental. Update casc TFN script. --- diff --git a/contrib/run-script-casc25-tfn b/contrib/run-script-casc25-tfn index d3c5d0344..6888d7b49 100644 --- a/contrib/run-script-casc25-tfn +++ b/contrib/run-script-casc25-tfn @@ -15,7 +15,7 @@ echo "------- cvc4-tfn casc 25 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,11 +25,10 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench } trywith 30 --cbqi2 --decision=internal --full-saturate-quant -trywith 60 --finite-model-find --sort-inference --uf-ss-fair trywith 30 --cbqi --full-saturate-quant trywith 60 --cbqi --cbqi-recurse --full-saturate-quant trywith 60 --fmf-bound-int --macros-quant diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6fdfadbd3..54c97750a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3272,7 +3272,7 @@ void SmtEnginePrivate::processAssertions() { } } dumpAssertions("post-skolem-quant", d_assertions); - if( options::macrosQuant() ){ + if( options::macrosQuant() && !options::incrementalSolving() ){ //quantifiers macro expansion bool success; do{ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 22ffcd278..8e7e3d69c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -706,7 +706,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { */ } -void CegInstantiator::check() { +bool CegInstantiator::check() { for( unsigned r=0; r<2; r++ ){ std::vector< Node > subs; @@ -716,10 +716,11 @@ void CegInstantiator::check() { std::vector< int > subs_typ; //try to add an instantiation if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ - return; + return true; } } Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 54f762720..eb99fc4f6 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -72,7 +72,7 @@ public: //delta Node d_n_delta; //check : add instantiations based on valuation of d_vars - void check(); + bool check(); // get delta lemmas : on-demand force minimality of d_n_delta void getDeltaLemmas( std::vector< Node >& lems ); }; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index fdb64f6b0..da3c0cce0 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1717,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() { for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ if( !getTermDatabase()->d_op_map[it->first].empty() ){ Node nn = getTermDatabase()->d_op_map[it->first][0]; + Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; //check if we have enumerated ground terms if( nn.getKind()==APPLY_UF ){ + Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl; if( !d_cg->hasEnumeratedUf( nn ) ){ do_enum = false; } } if( do_enum ){ + Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl; d_funcs.push_back( it->first ); for( unsigned i=0; ifirst].push_back( nn[i].getType() ); @@ -1738,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() { getTermDatabase()->computeUfEqcTerms( it->first ); } } + Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl; } } //shuffle functions diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index cbf0dbbd9..de80146f9 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -369,6 +369,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { d_check_delta_lemma = true; + d_check_delta_lemma_lc = true; } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { @@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); d_quantEngine->getOutputChannel().lemma( delta_lem ); + d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } cinst->d_n_delta = d_n_delta; for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ @@ -412,8 +416,18 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { } Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; - cinst->check(); + bool addedLemma = cinst->check(); d_curr_quant = Node::null(); + return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; + }else if( e==3 ){ + if( d_check_delta_lemma_lc ){ + d_check_delta_lemma_lc = false; + d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); + d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); + Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } } return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 586cd492c..13e8cf54b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -100,8 +100,10 @@ private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_n_delta; + Node d_n_delta_ub; Node d_curr_quant; bool d_check_delta_lemma; + bool d_check_delta_lemma_lc; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 8c99881d6..189866494 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -945,6 +945,7 @@ Node TermDb::getSkolemizedBody( Node f ){ } Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { + Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); unsigned teIndex; if( it==d_typ_enum_map.end() ){