CVC3  2.4.1
theory_simulate.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_simulate.cpp
4  *\brief Implementation of class TheorySimulate.
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Tue Oct 7 10:28:14 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #include "theory_simulate.h"
23 #include "simulate_proof_rules.h"
24 #include "typecheck_exception.h"
25 #include "parser_exception.h"
26 #include "smtlib_exception.h"
27 // For the type REAL
28 #include "theory_arith.h"
29 
30 
31 using namespace std;
32 using namespace CVC3;
33 
34 
35 TheorySimulate::TheorySimulate(TheoryCore* core)
36  : Theory(core, "Simulate") {
37  // Initialize the proof rules
39  // Register the kinds
40  vector<int> kinds;
41  kinds.push_back(SIMULATE);
42  // Register the theory with the core
43  registerTheory(this, kinds, false /* no solver */);
44 }
45 
46 
48  delete d_rules;
49 }
50 
51 
52 Theorem
54  switch (e.getKind()) {
55  case SIMULATE:
56  return d_rules->expandSimulate(e);
57  break;
58  default:
59  return reflexivityRule(e);
60  }
61 }
62 
63 
64 void
66  switch (e.getKind()) {
67  case SIMULATE: { // SIMULATE(f, s0, i_1, ..., i_k, N)
68  const int arity = e.arity();
69  if (!e[arity - 1].isRational() ||
70  !e[arity - 1].getRational().isInteger()) {
71  throw TypecheckException
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 "
75  +e.toString());
76  }
77 
78  const Expr& fn(e[0]);
79  Type fnType(getBaseType(fn));
80  // The arity of function is k+1, which is e.arity()-2.
81  // The arity of the type also includes the result type.
82  if(fnType.arity() != e.arity()-1)
83  throw TypecheckException
84  ("Wrong number of arguments in SIMULATE:\n\n"
85  +e.toString()
86  +"\n\nExpected "+int2string(fnType.arity()+1)
87  +" arguments, but received "+int2string(e.arity())+".");
88  // Build the function type that SIMULATE expects
89  vector<Type> argTp;
90  // The (initial) state type
91  Type resType(getBaseType(e[1]));
92  argTp.push_back(resType);
93  for(int i=2, iend=e.arity()-1; i<iend; ++i) {
94  Type iTp(e[i].getType());
95  Type iTpBase(getBaseType(e[i]));
96  if(!iTp.isFunction() || iTp.arity() != 2 || !isReal(iTpBase[0]))
97  throw TypecheckException
98  ("Type mismatch in SIMULATE:\n\n "
99  +e.toString()
100  +"\n\nThe input #"+int2string(i-1)
101  +" is expected to be of type:\n\n REAL -> <something>"
102  "\n\nBut the actual type is:\n\n "
103  +iTp.toString());
104  argTp.push_back(iTpBase[1]);
105  }
106  Type expectedFnType(Type::funType(argTp, resType));
107  if(fnType != expectedFnType)
108  throw TypecheckException
109  ("Type mismatch in SIMULATE:\n\n "
110  +e.toString()
111  +"\n\nThe transition function is expected to be of type:\n\n "
112  +expectedFnType.toString()
113  +"\n\nBut the actual type is:\n\n "
114  +fnType.toString());
115 
116  e.setType(resType);
117  break;
118  }
119  default:
120  DebugAssert(false,"TheorySimulate::computeType: Unexpected expression: "
121  +e.toString());
122  }
123 }
124 
125 ///////////////////////////////////////////////////////////////////////////////
126 //parseExprOp:
127 //Recursive call of parseExpr defined in theory_ libaries based on kind of expr
128 //being built
129 ///////////////////////////////////////////////////////////////////////////////
130 Expr
132  TRACE("parser", "TheorySimulate::parseExprOp(", e, ")");
133  // If the expression is not a list, it must have been already
134  // parsed, so just return it as is.
135  if(RAW_LIST != e.getKind()) return e;
136 
137  DebugAssert(e.arity() > 0,
138  "TheorySimulate::parseExprOp:\n e = "+e.toString());
139  /* The first element of the list (e[0] is an ID of the operator.
140  ID string values are the dirst element of the expression */
141  const Expr& c1 = e[0][0];
142  int kind = getEM()->getKind(c1.getString());
143  switch(kind) {
144  case SIMULATE: { // Application of SIMULATE to args
145  vector<Expr> k;
146  Expr::iterator i = e.begin(), iend=e.end();
147  // Skip first element of the vector of kids in 'e'.
148  // The first element is the operator.
149  ++i;
150  // Parse the kids of e and push them into the vector 'k'
151  for(; i!=iend; ++i)
152  k.push_back(parseExpr(*i));
153  return Expr(SIMULATE, k, e.getEM());
154  break;
155  }
156  default:
157  DebugAssert(false, "TheorySimulate::parseExprOp: Unexpected operator: "
158  +e.toString());
159  }
160  return e;
161 }
162 
163 Expr
165  switch (e.getKind()) {
166  case SIMULATE: {
167  // TCC(SIMULATE(f, s, i1, ..., ik, N)):
168 
169  // First, we require that the type of the first argument of f is
170  // exactly the same as the type of f's result (otherwise we need
171  // to check subtyping relation, which might be undecidable), and
172  // whether f is defined on s.
173  //
174  // Then, we check that the result type of i_j exactly matches the
175  // type of the j+1-th argument of f (again, for efficiency and
176  // decidability reasons), and that each i_j is defined on every
177  // integer from 0..N-1.
178  vector<Expr> tccs;
179  Type fnType(e[0].getType());
180  DebugAssert(fnType.arity() == e.arity()-1,
181  "TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
182  +e.toString());
183  Type resType(fnType[fnType.arity()-1]);
184  // Check that the state type matches the 1st arg and the result type in f
185  if(fnType[0] != resType)
186  return getEM()->falseExpr();
187  // Compute TCC for f on the initial state
188  tccs.push_back(getTypePred(fnType[0], e[1]));
189 
190  const Rational& N = e[e.arity()-1].getRational();
191  // Now, iterate through the inputs
192  for(int i=2, iend=e.arity()-1; i<iend; ++i) {
193  Type iTp(e[i].getType());
194  DebugAssert(iTp.isFunction() && iTp.arity()==2,
195  "TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
196  +e.toString());
197  // Match the return type of i-th input with f's argument
198  if(iTp[1] != fnType[i-1])
199  return getEM()->falseExpr();
200  // Compute the TCC for i(0) ... i(N-1)
201  for(Rational j=0; j<N; j = j+1)
202  tccs.push_back(getTypePred(iTp[0], getEM()->newRatExpr(j)));
203  }
204  return rewriteAnd(andExpr(tccs)).getRHS();
205  }
206  default:
207  DebugAssert(false, "TheorySimulate::computeTCC("+e.toString()
208  +")\n\nUnknown expression.");
209  return getEM()->trueExpr();
210  }
211 }
212 
213 
214 ExprStream&
216  switch(os.lang()) {
217  case PRESENTATION_LANG:
218  switch(e.getKind()) {
219  case SIMULATE:{
220  os << "SIMULATE" << "(" << push;
221  bool first(true);
222  for (int i = 0; i < e.arity(); i++) {
223  if (first) first = false;
224  else os << push << "," << pop << space;
225  os << e[i];
226  }
227  os << push << ")";
228  break;
229  }
230  default:
231  // Print the top node in the default LISP format, continue with
232  // pretty-printing for children.
233  e.printAST(os);
234 
235  break;
236  }
237  break;
238  case SMTLIB_LANG:
239  case SMTLIB_V2_LANG:
240  d_theoryUsed = true;
241  throw SmtlibException("TheorySimulate::print: SMTLIB not supported");
242  switch(e.getKind()) {
243  case SIMULATE:{
244  os << "(" << push << "SIMULATE" << space;
245  for (int i = 0; i < e.arity(); i++) {
246  os << space << e[i];
247  }
248  os << push << ")";
249  break;
250  }
251  default:
252  // Print the top node in the default LISP format, continue with
253  // pretty-printing for children.
254  e.printAST(os);
255 
256  break;
257  }
258  break;
259  case LISP_LANG:
260  switch(e.getKind()) {
261  case SIMULATE:{
262  os << "(" << push << "SIMULATE" << space;
263  for (int i = 0; i < e.arity(); i++) {
264  os << space << e[i];
265  }
266  os << push << ")";
267  break;
268  }
269  default:
270  // Print the top node in the default LISP format, continue with
271  // pretty-printing for children.
272  e.printAST(os);
273 
274  break;
275  }
276  break;
277  default: // Not a known language
278  e.printAST(os);
279  break;
280  }
281  return os;
282 }
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
int arity() const
Definition: expr.h:1201
ExprStream & pop(ExprStream &os)
Restore the indentation.
iterator begin() const
Begin iterator.
Definition: expr.h:1211
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
~TheorySimulate()
Destructor.
Data structure of expressions in CVC3.
Definition: expr.h:133
ExprManager * getEM() const
Definition: expr.h:1156
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
An exception thrown by the parser.
static Type funType(const std::vector< Type > &typeDom, const Type &typeRan)
Definition: expr.cpp:641
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
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.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
SMT-LIB v2 format.
Definition: lang.h:52
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Lisp-like format for automatically generated specs.
Definition: lang.h:36
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Definition: theory.h:719
#define DebugAssert(cond, str)
Definition: debug.h:408
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)
Definition: theory_arith.h:177
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
Implementation of a symbolic simulator.
Definition: kinds.h:44
bool d_theoryUsed
Definition: theory.h:79
int arity() const
Definition: type.h:55
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
const Expr & falseExpr()
FALSE Expr.
Definition: expr_manager.h:278
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
std::string int2string(int n)
Definition: cvc_util.h:46
const Expr & getRHS() const
Definition: theorem.cpp:246
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
Definition: theory.cpp:406
std::string toString() const
Definition: type.h:80
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
Abstract interface to the symbolic simulator proof rules.
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
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.
SMT-LIB format.
Definition: lang.h:34
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
bool isReal(Type t)
Definition: theory_arith.h:173
Definition: kinds.h:99
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
bool isFunction() const
Definition: type.h:62
SimulateProofRules * createProofRules()
Create proof rules for this theory.
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
Nice SAL-like language for manually written specs.
Definition: lang.h:32
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end() const
End iterator.
Definition: expr.h:1217