CVC3
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 }