Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
switch(k) {
- case kind::NOT : if(lhs.getType().isSet()) { k = kind::COMPLIMENT; } break;
case kind::LEQ : if(lhs.getType().isSet()) { k = kind::SUBSET; } break;
case kind::MINUS : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break;
case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break;
default: break;
}
Expr e = em->mkExpr(k, lhs, rhs);
- return negate ? em->mkExpr(kind::NOT, e) : e;
+ return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLIMENT : kind::NOT, e) : e;
}/* createPrecedenceTree() recursive variant */
Expr createPrecedenceTree(Parser* parser, ExprManager* em,
/** Add n NOTs to the front of e and return the result. */
Expr addNots(ExprManager* em, size_t n, Expr e) {
+ Kind k = e.getType().isSet() ? kind::COMPLIMENT : kind::NOT;
while(n-- > 0) {
- e = em->mkExpr(kind::NOT, e);
+ e = em->mkExpr(k, e);
}
return e;
}/* addNots() */