Improve relevant domain computation for arithmetic, full saturation strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.

1 files changed, 2 insertions, 7 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 180ccc448..5eca87903 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -118,14 +118,9 @@ Node InstMatch::get( int i ) {
   return d_vals[i];
 }
 
-void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){
+void InstMatch::getTerms( Node f, std::vector< Node >& inst ){
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Node val = get( i );
-    if( val.isNull() ){
-      Node ic =  qe->getTermDatabase()->getInstantiationConstant( f, i );
-      val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() );
-    }
-    inst.push_back( val );
+    inst.push_back( d_vals[i] );
   }
 }