Improve quantifier instantiation: always use original terms when matching (was missin...

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index 5309fc93bdd24cbe29e6c93d6ff919bdba2fe707..9e754ffc72991704365bd2fd59a1ba51f35ee247 100755 (executable)
--- 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 a863f70b52c5e89916a4852b2e95415f0ae1cc45..2e4f4d0b925c54e48a8e17e0165b4ada1c461c3c 100755 (executable)
--- 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 41aec13359eb0a7f1b422d7c0e945269f0f75399..5dd1a9d98c92b0edb0331e0d2eac0d69d1288f89 100755 (executable)
--- 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 9031104c87a8d3938bac0a8ae2375c1cbbf2ef92..5ee73d006128c6f38ae2f0b89ff351d054c078aa 100644 (file)
--- 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 7c71313de909e86e2448c33ecdf6847c2d310a53..24f17d0c18acfecbce366ed38982eea4323348d3 100755 (executable)
--- 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 );\r
                       //}\r
                     }\r
-                    if( d_quantEngine->addInstantiation( q, terms ) ){\r
+                    if( d_quantEngine->addInstantiation( q, terms, false ) ){\r
                       Trace("qcf-check") << "   ... Added instantiation" << std::endl;\r
                       Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;\r
                       qi->debugPrintMatch("qcf-inst");\r

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 75f54d7d9baa9899f3938e42731c76a30e94c323..f0c2de6dae21610243f34721cf08cc5582f97c61 100644 (file)
--- 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 a8eccf4ad2ae731e466f5d1f8edc3c423fc9b6a9..9ba2d84d30c0e06e373073ab3d7e3f7a08ea89c1 100644 (file)
--- 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)