diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-30 14:47:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-30 14:47:35 -0600 |
| commit | 6112e47d0d93b675fe220438c3828b5b6025dde6 (patch) | |
| tree | 879377f37a822a73dfd67869f3a3b6401ca3cc9a | |
| parent | 164e5274e3135b245b8ce5576841bb6c329eecfe (diff) | |
Eliminate spurious postprocessing step for single invocation (#3674)
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 28 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.h | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3644.smt2 | 5 |
4 files changed, 6 insertions, 29 deletions
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) |