Switch to Nodes for conjecture generator (#4026)

Fixes #4022.

4 files changed, 18 insertions, 5 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index bccb33f1d..b25170341 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -237,7 +237,8 @@ bool ConjectureGenerator::areUniversalDisequal( TNode n1, TNode n2 ) {
   return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
 }
 
-TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
+Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
+{
   if( add ){
     if( d_urelevant_terms.find( n )==d_urelevant_terms.end() ){
       setUniversalRelevant( n );
@@ -258,7 +259,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
           Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
           std::vector< Node > eq_terms;
           //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
-          TNode gt = getTermDatabase()->evaluateTerm( t );
+          Node gt = getTermDatabase()->evaluateTerm(t);
           if( !gt.isNull() && gt!=t ){
             eq_terms.push_back( gt );
           }
@@ -850,7 +851,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
         while( !ueqcs_i.isFinished() ){
           TNode r = (*ueqcs_i);
           bool firstTime = true;
-          TNode rr = getUniversalRepresentative( r );
+          Node rr = getUniversalRepresentative(r);
           Trace("thm-ee") << "  " << rr;
           Trace("thm-ee") << " : { ";
           eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine );
@@ -961,7 +962,7 @@ bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
     //do not consider if it is non-canonical, and either:
     //  (1) we are not generating relevant terms, or
     //  (2) its canonical form is a generalization.
-    TNode lnr = getUniversalRepresentative( ln, true );
+    Node lnr = getUniversalRepresentative(ln, true);
     if( lnr==ln ){
       markReportedCanon( ln );
     }else if( !genRelevant || isGeneralization( lnr, ln ) ){
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 384533725..503961ea3 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -310,7 +310,7 @@ private:
   /** are universal disequal */
   bool areUniversalDisequal( TNode n1, TNode n2 );
   /** get universal representative */
-  TNode getUniversalRepresentative( TNode n, bool add = false );
+  Node getUniversalRepresentative(TNode n, bool add = false);
   /** set relevant */
   void setUniversalRelevant( TNode n );
   /** ordering for universal terms */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 691791732..efd378596 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2028,6 +2028,7 @@ set(regress_2_tests
   regress2/sygus/examples-deq.sy
   regress2/sygus/icfp_easy_mt_ite.sy
   regress2/sygus/inv_gen_n_c11.sy
+  regress2/sygus/issue4022-conjecture-gen.smt2
   regress2/sygus/lustre-real.sy
   regress2/sygus/max2-univ.sy
   regress2/sygus/min_IC_1.sy
diff --git a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
new file mode 100644
index 000000000..9c3fe7ac5
--- /dev/null
+++ b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-option :conjecture-filter-model true)
+(set-option :conjecture-gen true)
+(set-option :conjecture-no-filter true)
+(set-option :dt-ref-sk-intro true)
+(set-option :quant-ind true)
+(set-option :sygus-inference true)
+(set-info :status sat)
+(declare-fun a (Int) Bool)
+(assert (exists ((b Int)) (a b)))
+(check-sat)