diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-14 21:27:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-14 21:27:07 -0500 |
commit | 136617cbf257a08563ced754f7a3aad186a6cba2 (patch) | |
tree | a4e1f14c36ccdce93ff1435609dc5cf34150b9f0 /src | |
parent | b87e44544862043c4cff523134662c10cfbccf0f (diff) |
Minor improvements to --nl-ext-purify (#1896)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 36 |
1 files changed, 29 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 49eb42447..7f34bb39e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2826,12 +2826,31 @@ Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, s } Node ret = n; if( n.getNumChildren()>0 ){ - if( beneathMult && n.getKind()!=kind::MULT ){ - //new variable - ret = NodeManager::currentNM()->mkSkolem("__purifyNl_var", n.getType(), "Variable introduced in purifyNl pass"); - Node np = purifyNlTerms( n, cache, bcache, var_eq, false ); - var_eq.push_back( np.eqNode( ret ) ); - }else{ + if (beneathMult + && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) + { + // don't do it if it rewrites to a constant + Node nr = Rewriter::rewrite(n); + if (nr.isConst()) + { + // return the rewritten constant + ret = nr; + } + else + { + // new variable + ret = NodeManager::currentNM()->mkSkolem( + "__purifyNl_var", + n.getType(), + "Variable introduced in purifyNl pass"); + Node np = purifyNlTerms(n, cache, bcache, var_eq, false); + var_eq.push_back(np.eqNode(ret)); + Trace("nl-ext-purify") + << "Purify : " << ret << " -> " << np << std::endl; + } + } + else + { bool beneathMultNew = beneathMult || n.getKind()==kind::MULT; bool childChanged = false; std::vector< Node > children; @@ -4027,7 +4046,10 @@ void SmtEnginePrivate::processAssertions() { unordered_map<Node, Node, NodeHashFunction> bcache; std::vector< Node > var_eq; for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq)); + Node a = d_assertions[i]; + d_assertions.replace(i, purifyNlTerms(a, cache, bcache, var_eq)); + Trace("nl-ext-purify") + << "Purify : " << a << " -> " << d_assertions[i] << std::endl; } if( !var_eq.empty() ){ unsigned lastIndex = d_assertions.size()-1; |