24 #define _CVC3_TRUSTED_
51 #define CLASS_NAME "CVC3::UFTheoremProducer"
61 "theorem is not a relation or has wrong arity:\n"
66 pf = newPf(
"rel_closure", rel.
getProof());
70 Expr tc = d_theoryUF->transClosureExpr(name, relExpr[0], relExpr[1]);
85 "theorem is not a proper trans_closure expr:\n"
90 "theorem is not a proper trans_closure expr:\n"
98 "Expr's don't match:\n"
108 pf = newPf(
"rel_trans", pfs);
110 return newTheorem(
Expr(e1.
getOp(), e1[0], e2[1]), a, pf);
118 +
"):\n\n expression is not an APPLY");
125 "Operator is not LAMBDA: " + lambda.toString());
128 Expr body(lambda.getBody());
129 const vector<Expr>& vars = lambda.
getVars();
133 "wrong number of arguments applied to lambda\n");
137 body = body.substExpr(vars, e.
getKids());
144 pf = newPf(
"apply_lambda", e);
145 return newRWTheorem(e, body, Assumptions::emptyAssump(), pf);
152 "UFTheoremProducer::rewriteOpDef: 'e' is not a "
153 "function application:\n\n "+e.
toString());
161 "UFTheoremProducer::rewriteOpDef: operator is not a "
162 "named function in:\n\n "+e.
toString());
168 "UFTheoremProducer::rewriteOpDef: bad named "
177 pf = newPf(
"rewrite_op_def", e);
178 return newRWTheorem(e,
Expr(op.
mkOp(), e.
getKids()), Assumptions::emptyAssump(), pf);
const Expr & getExpr() const
Data structure of expressions in CVC3.
#define CHECK_SOUND(cond, msg)
const std::vector< Expr > & getKids() const
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Op getOp() const
Get operator from expression.
std::string toString() const
Print the expression to a string.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
const Assumptions & getAssumptionsRef() const
TRUSTED implementation of uninterpreted function/predicate proof rules.
const std::string & getName() const
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Op mkOp() const
Make the expr into an operator.