From: Andrew Reynolds Date: Sun, 25 May 2014 14:18:42 +0000 (-0500) Subject: Improve quantifier instantiation: always use original terms when matching (was missin... X-Git-Tag: cvc5-1.0.0~6893 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d3f97ea91ffbf9ceea5814281a4d434d8e09a53;p=cvc5.git Improve quantifier instantiation: always use original terms when matching (was missing for simple triggers). Minor updates to scripts. --- diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 5309fc93b..9e754ffc7 100755 --- a/contrib/run-script-cascj7-fnt +++ b/contrib/run-script-cascj7-fnt @@ -33,4 +33,4 @@ trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=interna trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair trywith 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round -echo "% SZS status" "GaveUp for $filename" +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index a863f70b5..2e4f4d0b9 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -35,4 +35,4 @@ trywith 30 --relevant-triggers --full-saturate-quant trywith 15 --finite-model-find --decision=justification-stoponly trywith 30 --pre-skolem-quant --full-saturate-quant finishwith --quant-cf --full-saturate-quant -echo "% SZS status" "GaveUp for $filename" +# echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 41aec1335..5dd1a9d98 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -15,7 +15,7 @@ echo "------- cvc4-tff casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -35,4 +35,4 @@ trywith 20 --finite-model-find trywith 30 --full-saturate-quant trywith 60 --quant-cf --full-saturate-quant finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant -echo "% SZS status" "GaveUp for $filename" +# echo "% SZS status" "GaveUp for $filename" diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 9031104c8..5ee73d006 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -244,7 +244,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi }else{ if( d_active_add ){ Trace("active-add") << "Active Adding instantiation " << m << std::endl; - success = qe->addInstantiation( f, m ); + success = qe->addInstantiation( f, m, false ); Trace("active-add") << "Success = " << success << std::endl; } } @@ -631,8 +631,15 @@ int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, Q void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){ Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; if( argIndex==(int)d_match_pattern.getNumChildren() ){ - //m is an instantiation - if( qe->addInstantiation( d_f, m ) ){ + Assert( !tat->d_data.empty() ); + Node t = tat->d_data.begin()->first; + Debug("simple-trigger") << "Actual term is " << t << std::endl; + //convert to actual used terms + for( std::map< int, int >::iterator it = d_var_num.begin(); it != d_var_num.end(); ++it ){ + Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl; + m.setValue( it->second, t[it->first] ); + } + if( qe->addInstantiation( d_f, m, false ) ){ addedLemmas++; Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; } @@ -642,6 +649,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ Node t = it->first; Node prev = m.get( v ); + //using representatives, just check if equal if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern[argIndex].getType() ) ){ m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 7c71313de..24f17d0c1 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2196,7 +2196,7 @@ void QuantConflictFind::check( Theory::Effort level ) { Assert( evaluate( inst )==-1 || e>effort_conflict ); //} } - if( d_quantEngine->addInstantiation( q, terms ) ){ + if( d_quantEngine->addInstantiation( q, terms, false ) ){ Trace("qcf-check") << " ... Added instantiation" << std::endl; Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; qi->debugPrintMatch("qcf-inst"); diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 75f54d7d9..f0c2de6da 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -153,7 +153,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { if( inst.size()>f[0].getNumChildren() ){ inst.resize( f[0].getNumChildren() ); } - if( d_quantEngine->addInstantiation( f, inst ) ){ + if( d_quantEngine->addInstantiation( f, inst, false ) ){ addedLemmas++; tempAddedLemmas++; /* diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 index a8eccf4ad..9ba2d84d3 100644 --- a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 +++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-option :print-success false) (set-logic AUFLIA_SETS) (set-info :status unsat)