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 /src/theory/quantifiers | |
parent | 164e5274e3135b245b8ce5576841bb6c329eecfe (diff) |
Eliminate spurious postprocessing step for single invocation (#3674)
Diffstat (limited to 'src/theory/quantifiers')
-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 |
2 files changed, 0 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; |