Eliminate spurious postprocessing step for single invocation (#3674)

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index b6750c5da969cf681324a2e6941a582f4605807f..0e76062768921a32cbb371993a7fce368acf9ea0 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -437,33 +437,6 @@ struct sortSiInstanceIndices {
   }
 };
 
-Node CegSingleInv::postProcessSolution(Node n)
-{
-  bool childChanged = false;
-  Kind k = n.getKind();
-  if( n.getKind()==INTS_DIVISION_TOTAL ){
-    k = INTS_DIVISION;
-    childChanged = true;
-  }else if( n.getKind()==INTS_MODULUS_TOTAL ){
-    k = INTS_MODULUS;
-    childChanged = true;
-  }
-  std::vector< Node > children;
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    Node nn = postProcessSolution( n[i] );
-    children.push_back( nn );
-    childChanged = childChanged || nn!=n[i];
-  }
-  if( childChanged ){
-    if( n.hasOperator() && k==n.getKind() ){
-      children.insert( children.begin(), n.getOperator() );
-    }
-    return NodeManager::currentNM()->mkNode( k, children );
-  }else{
-    return n;
-  }
-}
-
 Node CegSingleInv::getSolution(unsigned sol_index,
                                TypeNode stn,
                                int& reconstructed,
@@ -584,7 +557,6 @@ Node CegSingleInv::reconstructToSyntax(Node s,
           d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(
               d_solution);
     }
-    d_solution = postProcessSolution( d_solution );
     if( prev!=d_solution ){
       Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl;
     }

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 0d5af327e7210bf35c619b7b0b3b697b373036db..19caa4c794eda4752aa4f20414a8b55f291d8e25 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -49,7 +49,6 @@ class CegSingleInv
                                std::vector< Node >& terms,
                                std::map< Node, std::vector< Node > >& teq,
                                Node n, std::vector< Node >& conj );
-  Node postProcessSolution(Node n);
  private:
   /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 74121ecbd2449e8945e11e0e27d7df45415c0e58..799219eec9dccf71f343860a3a3e2fb537f31502 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1794,6 +1794,7 @@ set(regress_1_tests
   regress1/sygus/issue3633.smt2
   regress1/sygus/issue3634.smt2
   regress1/sygus/issue3635.smt2
+  regress1/sygus/issue3644.smt2
   regress1/sygus/issue3648.smt2
   regress1/sygus/issue3654.sy
   regress1/sygus/large-const-simp.sy

diff --git a/test/regress/regress1/sygus/issue3644.smt2 b/test/regress/regress1/sygus/issue3644.smt2
new file mode 100644 (file)
index 0000000..60c6ea4
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3644.smt2
@@ -0,0 +1,5 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference --no-check-models
+(set-logic LIA)
+(assert (forall ((a Int)) (=> (> a 0) (exists ((b Int)) (> a (* b 2))))))
+(check-sat)