- 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
+ {