From 6112e47d0d93b675fe220438c3828b5b6025dde6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jan 2020 14:47:35 -0600
Subject: [PATCH] Eliminate spurious postprocessing step for single invocation
 (#3674)

---
 .../sygus/ce_guided_single_inv.cpp            | 28 -------------------
 .../quantifiers/sygus/ce_guided_single_inv.h  |  1 -
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress1/sygus/issue3644.smt2    |  5 ++++
 4 files changed, 6 insertions(+), 29 deletions(-)
 create mode 100644 test/regress/regress1/sygus/issue3644.smt2

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index b6750c5da..0e7606276 100644
--- 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 0d5af327e..19caa4c79 100644
--- 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 74121ecbd..799219eec 100644
--- 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
index 000000000..60c6ea4ee
--- /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)
-- 
2.30.2