Option for more aggressive merging in UEE.

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 799cce9ed93bd5d18270fa58fe3bf1734875aa3f..fe3c92323573a790bf435fccb099089571c708c4 100755 (executable)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -247,7 +247,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
               }else{\r
                 Assert( eq_terms[i].getType()==tn );\r
                 registerPattern( eq_terms[i], tn );\r
-                if( isUniversalLessThan( eq_terms[i], t ) ){\r
+                if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){\r
                   setUniversalRelevant( eq_terms[i] );\r
                   assertEq = true;\r
                 }\r
@@ -255,6 +255,8 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
               if( assertEq ){\r
                 Node exp;\r
                 d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp );\r
+              }else{\r
+                Trace("thm-ee-no-add") << "Do not add : " << t << " == " << eq_terms[i] << std::endl;\r
               }\r
             }\r
           }else{\r
@@ -322,7 +324,6 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
 \r
 \r
 Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) {\r
-  Trace("ajr-temp") << "get canonical term " << n << " " << n.getKind() << " " << n.hasOperator() << std::endl;\r
   if( n.getKind()==BOUND_VARIABLE ){\r
     std::map< TNode, TNode >::iterator it = subs.find( n );\r
     if( it==subs.end() ){\r
@@ -1539,7 +1540,6 @@ bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
       //check if there is only one feasible equivalence class.  if so, don't make pattern any more specific.\r
       //unsigned i = s->d_ccand_eqc[0].size()-1;\r
       //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){\r
-      //  Trace("ajr-temp") << "Apply this!" << std::endl;\r
       //  d_status = 6;\r
       //  return getNextTerm( s, depth );\r
       //}\r

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 16df9d9a9d5ba0d4d31f16a6c32bede86dfc4e39..162bbc1588cf44d814582e081743c3f84db374eb 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -171,4 +171,6 @@ option conjectureFilterModel --conjecture-filter-model bool :read-write :default
  filter based on model
 option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
  number of ground terms to generate for model filtering
+option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
+ more aggressive merging for universal equality engine, introduces terms
 endmodule