From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 1 Oct 2014 15:48:35 +0000 (+0200)
Subject: Option for more aggressive merging in UEE.
X-Git-Tag: cvc5-1.0.0~6610
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=848ca519a29a77fd2f30497845dc0d9e49f55879;p=cvc5.git

Option for more aggressive merging in UEE.
---

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 799cce9ed..fe3c92323 100755
--- 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{
                 Assert( eq_terms[i].getType()==tn );
                 registerPattern( eq_terms[i], tn );
-                if( isUniversalLessThan( eq_terms[i], t ) ){
+                if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){
                   setUniversalRelevant( eq_terms[i] );
                   assertEq = true;
                 }
@@ -255,6 +255,8 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
               if( assertEq ){
                 Node exp;
                 d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp );
+              }else{
+                Trace("thm-ee-no-add") << "Do not add : " << t << " == " << eq_terms[i] << std::endl;
               }
             }
           }else{
@@ -322,7 +324,6 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
 
 
 Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) {
-  Trace("ajr-temp") << "get canonical term " << n << " " << n.getKind() << " " << n.hasOperator() << std::endl;
   if( n.getKind()==BOUND_VARIABLE ){
     std::map< TNode, TNode >::iterator it = subs.find( n );
     if( it==subs.end() ){
@@ -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.
       //unsigned i = s->d_ccand_eqc[0].size()-1;
       //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
-      //  Trace("ajr-temp") << "Apply this!" << std::endl;
       //  d_status = 6;
       //  return getNextTerm( s, depth );
       //}
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 16df9d9a9..162bbc158 100644
--- 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