/*****************************************************************************/
/*!
*\file theory_simulate.cpp
*\brief Implementation of class TheorySimulate.
*
* Author: Sergey Berezin
*
* Created: Tue Oct 7 10:28:14 2003
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#include "theory_simulate.h"
#include "simulate_proof_rules.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
// For the type REAL
#include "theory_arith.h"
using namespace std;
using namespace CVC3;
TheorySimulate::TheorySimulate(TheoryCore* core)
: Theory(core, "Simulate") {
// Initialize the proof rules
d_rules = createProofRules();
// Register the kinds
vector<int> kinds;
kinds.push_back(SIMULATE);
// Register the theory with the core
registerTheory(this, kinds, false /* no solver */);
}
TheorySimulate::~TheorySimulate() {
delete d_rules;
}
Theorem
TheorySimulate::rewrite(const Expr& e) {
switch (e.getKind()) {
case SIMULATE:
return d_rules->expandSimulate(e);
break;
default:
return reflexivityRule(e);
}
}
void
TheorySimulate::computeType(const Expr& e) {
switch (e.getKind()) {
case SIMULATE: { // SIMULATE(f, s0, i_1, ..., i_k, N)
const int arity = e.arity();
if (!e[arity - 1].isRational() ||
!e[arity - 1].getRational().isInteger()) {
throw TypecheckException
("Number of cycles in SIMULATE (last arg) "
"must be an integer constant:\n\n " + e[arity -1].toString()
+"\n\nIn the following expression:\n\n "
+e.toString());
}
const Expr& fn(e[0]);
Type fnType(getBaseType(fn));
// The arity of function is k+1, which is e.arity()-2.
// The arity of the type also includes the result type.
if(fnType.arity() != e.arity()-1)
throw TypecheckException
("Wrong number of arguments in SIMULATE:\n\n"
+e.toString()
+"\n\nExpected "+int2string(fnType.arity()+1)
+" arguments, but received "+int2string(e.arity())+".");
// Build the function type that SIMULATE expects
vector<Type> argTp;
// The (initial) state type
Type resType(getBaseType(e[1]));
argTp.push_back(resType);
for(int i=2, iend=e.arity()-1; i<iend; ++i) {
Type iTp(e[i].getType());
Type iTpBase(getBaseType(e[i]));
if(!iTp.isFunction() || iTp.arity() != 2 || !isReal(iTpBase[0]))
throw TypecheckException
("Type mismatch in SIMULATE:\n\n "
+e.toString()
+"\n\nThe input #"+int2string(i-1)
+" is expected to be of type:\n\n REAL -> <something>"
"\n\nBut the actual type is:\n\n "
+iTp.toString());
argTp.push_back(iTpBase[1]);
}
Type expectedFnType(Type::funType(argTp, resType));
if(fnType != expectedFnType)
throw TypecheckException
("Type mismatch in SIMULATE:\n\n "
+e.toString()
+"\n\nThe transition function is expected to be of type:\n\n "
+expectedFnType.toString()
+"\n\nBut the actual type is:\n\n "
+fnType.toString());
e.setType(resType);
break;
}
default:
DebugAssert(false,"TheorySimulate::computeType: Unexpected expression: "
+e.toString());
}
}
///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//Recursive call of parseExpr defined in theory_ libaries based on kind of expr
//being built
///////////////////////////////////////////////////////////////////////////////
Expr
TheorySimulate::parseExprOp(const Expr& e) {
TRACE("parser", "TheorySimulate::parseExprOp(", e, ")");
// If the expression is not a list, it must have been already
// parsed, so just return it as is.
if(RAW_LIST != e.getKind()) return e;
DebugAssert(e.arity() > 0,
"TheorySimulate::parseExprOp:\n e = "+e.toString());
/* The first element of the list (e[0] is an ID of the operator.
ID string values are the dirst element of the expression */
const Expr& c1 = e[0][0];
int kind = getEM()->getKind(c1.getString());
switch(kind) {
case SIMULATE: { // Application of SIMULATE to args
vector<Expr> k;
Expr::iterator i = e.begin(), iend=e.end();
// Skip first element of the vector of kids in 'e'.
// The first element is the operator.
++i;
// Parse the kids of e and push them into the vector 'k'
for(; i!=iend; ++i)
k.push_back(parseExpr(*i));
return Expr(SIMULATE, k, e.getEM());
break;
}
default:
DebugAssert(false, "TheorySimulate::parseExprOp: Unexpected operator: "
+e.toString());
}
return e;
}
Expr
TheorySimulate::computeTCC(const Expr& e) {
switch (e.getKind()) {
case SIMULATE: {
// TCC(SIMULATE(f, s, i1, ..., ik, N)):
// First, we require that the type of the first argument of f is
// exactly the same as the type of f's result (otherwise we need
// to check subtyping relation, which might be undecidable), and
// whether f is defined on s.
//
// Then, we check that the result type of i_j exactly matches the
// type of the j+1-th argument of f (again, for efficiency and
// decidability reasons), and that each i_j is defined on every
// integer from 0..N-1.
vector<Expr> tccs;
Type fnType(e[0].getType());
DebugAssert(fnType.arity() == e.arity()-1,
"TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
+e.toString());
Type resType(fnType[fnType.arity()-1]);
// Check that the state type matches the 1st arg and the result type in f
if(fnType[0] != resType)
return getEM()->falseExpr();
// Compute TCC for f on the initial state
tccs.push_back(getTypePred(fnType[0], e[1]));
const Rational& N = e[e.arity()-1].getRational();
// Now, iterate through the inputs
for(int i=2, iend=e.arity()-1; i<iend; ++i) {
Type iTp(e[i].getType());
DebugAssert(iTp.isFunction() && iTp.arity()==2,
"TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
+e.toString());
// Match the return type of i-th input with f's argument
if(iTp[1] != fnType[i-1])
return getEM()->falseExpr();
// Compute the TCC for i(0) ... i(N-1)
for(Rational j=0; j<N; j = j+1)
tccs.push_back(getTypePred(iTp[0], getEM()->newRatExpr(j)));
}
return rewriteAnd(andExpr(tccs)).getRHS();
}
default:
DebugAssert(false, "TheorySimulate::computeTCC("+e.toString()
+")\n\nUnknown expression.");
return getEM()->trueExpr();
}
}
ExprStream&
TheorySimulate::print(ExprStream& os, const Expr& e) {
switch(os.lang()) {
case PRESENTATION_LANG:
switch(e.getKind()) {
case SIMULATE:{
os << "SIMULATE" << "(" << push;
bool first(true);
for (int i = 0; i < e.arity(); i++) {
if (first) first = false;
else os << push << "," << pop << space;
os << e[i];
}
os << push << ")";
break;
}
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
break;
case SMTLIB_LANG:
d_theoryUsed = true;
throw SmtlibException("TheorySimulate::print: SMTLIB not supported");
switch(e.getKind()) {
case SIMULATE:{
os << "(" << push << "SIMULATE" << space;
for (int i = 0; i < e.arity(); i++) {
os << space << e[i];
}
os << push << ")";
break;
}
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
break;
case LISP_LANG:
switch(e.getKind()) {
case SIMULATE:{
os << "(" << push << "SIMULATE" << space;
for (int i = 0; i < e.arity(); i++) {
os << space << e[i];
}
os << push << ")";
break;
}
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
break;
default: // Not a known language
e.printAST(os);
break;
}
return os;
}
syntax highlighted by Code2HTML, v. 0.9.1