23 #define _CVC3_TRUSTED_
46 Theorem SimulateTheoremProducer::expandSimulate(
const Expr& e) {
47 const int arity = e.
arity();
50 "SimulateTheoremProducer::expandSimulate: "
51 "expected SIMULATE expression: "
54 e[arity - 1].getRational().isInteger(),
55 "SimulateTheoremProducer::expandSimulate: "
56 "incorrect children in SIMULATE: " + e.
toString());
62 CHECK_SOUND(n >= 0,
"SimulateTheoremProducer::expandSimulate: "
63 "Requested negative number of iterations: "+
int2string(n));
72 for(
int i=0; i<n; ++i) {
75 Expr ri(d_em->newRatExpr(i));
76 for(
int j=2; j<arity-1; ++j)
77 args.push_back(
Expr(e[j].mkOp(), ri));
78 res =
Expr(e[0].mkOp(), args);
83 pf = newPf(
"expand_simulate", e);
84 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);