36 :
Theory(core,
"Simulate") {
68 const int arity = e.
arity();
70 !e[arity - 1].getRational().isInteger()) {
72 (
"Number of cycles in SIMULATE (last arg) "
73 "must be an integer constant:\n\n " + e[arity -1].toString()
74 +
"\n\nIn the following expression:\n\n "
84 (
"Wrong number of arguments in SIMULATE:\n\n"
92 argTp.push_back(resType);
93 for(
int i=2, iend=e.
arity()-1; i<iend; ++i) {
94 Type iTp(e[i].getType());
98 (
"Type mismatch in SIMULATE:\n\n "
101 +
" is expected to be of type:\n\n REAL -> <something>"
102 "\n\nBut the actual type is:\n\n "
104 argTp.push_back(iTpBase[1]);
107 if(fnType != expectedFnType)
109 (
"Type mismatch in SIMULATE:\n\n "
111 +
"\n\nThe transition function is expected to be of type:\n\n "
113 +
"\n\nBut the actual type is:\n\n "
120 DebugAssert(
false,
"TheorySimulate::computeType: Unexpected expression: "
132 TRACE(
"parser",
"TheorySimulate::parseExprOp(", e,
")");
138 "TheorySimulate::parseExprOp:\n e = "+e.
toString());
141 const Expr& c1 = e[0][0];
157 DebugAssert(
false,
"TheorySimulate::parseExprOp: Unexpected operator: "
179 Type fnType(e[0].getType());
181 "TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
185 if(fnType[0] != resType)
192 for(
int i=2, iend=e.
arity()-1; i<iend; ++i) {
193 Type iTp(e[i].getType());
195 "TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
198 if(iTp[1] != fnType[i-1])
208 +
")\n\nUnknown expression.");
220 os <<
"SIMULATE" <<
"(" <<
push;
222 for (
int i = 0; i < e.
arity(); i++) {
223 if (first) first =
false;
224 else os << push <<
"," <<
pop <<
space;
244 os <<
"(" <<
push <<
"SIMULATE" <<
space;
245 for (
int i = 0; i < e.
arity(); i++) {
262 os <<
"(" <<
push <<
"SIMULATE" <<
space;
263 for (
int i = 0; i < e.
arity(); i++) {