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++) {
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
ExprStream & pop(ExprStream &os)
Restore the indentation.
iterator begin() const
Begin iterator.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
~TheorySimulate()
Destructor.
Data structure of expressions in CVC3.
ExprManager * getEM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
An exception thrown by the parser.
static Type funType(const std::vector< Type > &typeDom, const Type &typeRan)
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
An exception to be thrown at typecheck error.
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
MS C++ specific settings.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Lisp-like format for automatically generated specs.
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
#define DebugAssert(cond, str)
SimulateProofRules * d_rules
Our local proof rules.
virtual Theorem expandSimulate(const Expr &e)=0
SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)
void computeType(const Expr &e)
Compute and store the type of e.
bool isRational(const Expr &e)
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Implementation of a symbolic simulator.
std::string toString() const
Print the expression to a string.
const Expr & falseExpr()
FALSE Expr.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
std::string int2string(int n)
const Expr & getRHS() const
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
std::string toString() const
const Expr & trueExpr()
TRUE Expr.
ExprManager * getEM()
Access to ExprManager.
Abstract interface to the symbolic simulator proof rules.
void setType(const Type &t) const
Set the cached type.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
An exception to be thrown by the smtlib translator.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Theorem reflexivityRule(const Expr &a)
==> a == a
InputLanguage lang() const
Get the current output language.
SimulateProofRules * createProofRules()
Create proof rules for this theory.
Expr andExpr(const std::vector< Expr > &children)
Nice SAL-like language for manually written specs.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end() const
End iterator.