From 9d3f97ea91ffbf9ceea5814281a4d434d8e09a53 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 25 May 2014 09:18:42 -0500
Subject: Improve quantifier instantiation: always use original terms when
 matching (was missing for simple triggers).   Minor updates to scripts.

---
 src/theory/quantifiers/inst_match_generator.cpp | 14 +++++++++++---
 src/theory/quantifiers/quant_conflict_find.cpp  |  2 +-
 src/theory/quantifiers/rewrite_engine.cpp       |  2 +-
 3 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'src/theory/quantifiers')

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++;
                   /*
-- 
cgit v1.2.3