CVC3

theory_simulate.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file theory_simulate.cpp
00004  *\brief Implementation of class TheorySimulate.
00005  *
00006  * Author: Sergey Berezin
00007  *
00008  * Created: Tue Oct  7 10:28:14 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #include "theory_simulate.h"
00023 #include "simulate_proof_rules.h"
00024 #include "typecheck_exception.h"
00025 #include "parser_exception.h"
00026 #include "smtlib_exception.h"
00027 // For the type REAL
00028 #include "theory_arith.h"
00029 
00030 
00031 using namespace std;
00032 using namespace CVC3;
00033 
00034 
00035 TheorySimulate::TheorySimulate(TheoryCore* core)
00036   : Theory(core, "Simulate") {
00037   // Initialize the proof rules
00038   d_rules = createProofRules();
00039   // Register the kinds
00040   vector<int> kinds;
00041   kinds.push_back(SIMULATE);
00042   // Register the theory with the core
00043   registerTheory(this, kinds, false /* no solver */);
00044 }
00045 
00046 
00047 TheorySimulate::~TheorySimulate() {
00048   delete d_rules;
00049 }
00050 
00051 
00052 Theorem
00053 TheorySimulate::rewrite(const Expr& e) {
00054   switch (e.getKind()) {
00055   case SIMULATE:
00056     return d_rules->expandSimulate(e);
00057     break;
00058   default:
00059     return reflexivityRule(e);
00060   }
00061 }
00062 
00063 
00064 void
00065 TheorySimulate::computeType(const Expr& e) {
00066   switch (e.getKind()) {
00067   case SIMULATE: { // SIMULATE(f, s0, i_1, ..., i_k, N)
00068     const int arity = e.arity();
00069     if (!e[arity - 1].isRational() || 
00070   !e[arity - 1].getRational().isInteger()) {
00071       throw TypecheckException
00072   ("Number of cycles in SIMULATE (last arg) "
00073    "must be an integer constant:\n\n  " + e[arity -1].toString()
00074    +"\n\nIn the following expression:\n\n  "
00075    +e.toString());
00076     }
00077 
00078     const Expr& fn(e[0]);
00079     Type fnType(getBaseType(fn));
00080     // The arity of function is k+1, which is e.arity()-2.
00081     // The arity of the type also includes the result type.
00082     if(fnType.arity() != e.arity()-1)
00083       throw TypecheckException
00084   ("Wrong number of arguments in SIMULATE:\n\n"
00085    +e.toString()
00086    +"\n\nExpected "+int2string(fnType.arity()+1)
00087    +" arguments, but received "+int2string(e.arity())+".");
00088     // Build the function type that SIMULATE expects
00089     vector<Type> argTp;
00090     // The (initial) state type
00091     Type resType(getBaseType(e[1]));
00092     argTp.push_back(resType);
00093     for(int i=2, iend=e.arity()-1; i<iend; ++i) {
00094       Type iTp(e[i].getType());
00095       Type iTpBase(getBaseType(e[i]));
00096       if(!iTp.isFunction() || iTp.arity() != 2 || !isReal(iTpBase[0]))
00097   throw TypecheckException
00098     ("Type mismatch in SIMULATE:\n\n  "
00099      +e.toString()
00100      +"\n\nThe input #"+int2string(i-1)
00101      +" is expected to be of type:\n\n  REAL -> <something>"
00102      "\n\nBut the actual type is:\n\n  "
00103      +iTp.toString());
00104       argTp.push_back(iTpBase[1]);
00105     }
00106     Type expectedFnType(Type::funType(argTp, resType));
00107     if(fnType != expectedFnType)
00108       throw TypecheckException
00109   ("Type mismatch in SIMULATE:\n\n  "
00110    +e.toString()
00111    +"\n\nThe transition function is expected to be of type:\n\n  "
00112    +expectedFnType.toString()
00113    +"\n\nBut the actual type is:\n\n  "
00114    +fnType.toString());
00115 
00116     e.setType(resType);
00117     break;
00118   }
00119   default:
00120     DebugAssert(false,"TheorySimulate::computeType: Unexpected expression: "
00121     +e.toString());
00122   }
00123 }
00124 
00125 ///////////////////////////////////////////////////////////////////////////////
00126 //parseExprOp:
00127 //Recursive call of parseExpr defined in theory_ libaries based on kind of expr 
00128 //being built
00129 ///////////////////////////////////////////////////////////////////////////////
00130 Expr
00131 TheorySimulate::parseExprOp(const Expr& e) {
00132   TRACE("parser", "TheorySimulate::parseExprOp(", e, ")");
00133   // If the expression is not a list, it must have been already
00134   // parsed, so just return it as is.
00135   if(RAW_LIST != e.getKind()) return e;
00136 
00137   DebugAssert(e.arity() > 0,
00138         "TheorySimulate::parseExprOp:\n e = "+e.toString());
00139   /* The first element of the list (e[0] is an ID of the operator. 
00140      ID string values are the dirst element of the expression */ 
00141   const Expr& c1 = e[0][0];
00142   int kind = getEM()->getKind(c1.getString());
00143   switch(kind) {
00144   case SIMULATE: { // Application of SIMULATE to args
00145     vector<Expr> k;
00146     Expr::iterator i = e.begin(), iend=e.end();
00147     // Skip first element of the vector of kids in 'e'.
00148     // The first element is the operator.
00149     ++i; 
00150     // Parse the kids of e and push them into the vector 'k'
00151     for(; i!=iend; ++i) 
00152       k.push_back(parseExpr(*i));
00153     return Expr(SIMULATE, k, e.getEM());
00154     break;
00155   }
00156   default:
00157     DebugAssert(false, "TheorySimulate::parseExprOp: Unexpected operator: "
00158     +e.toString());
00159   }
00160   return e;
00161 }
00162 
00163 Expr
00164 TheorySimulate::computeTCC(const Expr& e) {
00165   switch (e.getKind()) {
00166   case SIMULATE: {
00167     // TCC(SIMULATE(f, s, i1, ..., ik, N)):
00168 
00169     // First, we require that the type of the first argument of f is
00170     // exactly the same as the type of f's result (otherwise we need
00171     // to check subtyping relation, which might be undecidable), and
00172     // whether f is defined on s.
00173     //
00174     // Then, we check that the result type of i_j exactly matches the
00175     // type of the j+1-th argument of f (again, for efficiency and
00176     // decidability reasons), and that each i_j is defined on every
00177     // integer from 0..N-1.
00178     vector<Expr> tccs;
00179     Type fnType(e[0].getType());
00180     DebugAssert(fnType.arity() == e.arity()-1,
00181     "TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
00182     +e.toString());
00183     Type resType(fnType[fnType.arity()-1]);
00184     // Check that the state type matches the 1st arg and the result type in f
00185     if(fnType[0] != resType)
00186       return getEM()->falseExpr();
00187     // Compute TCC for f on the initial state
00188     tccs.push_back(getTypePred(fnType[0], e[1]));
00189 
00190     const Rational& N = e[e.arity()-1].getRational();
00191     // Now, iterate through the inputs
00192     for(int i=2, iend=e.arity()-1; i<iend; ++i) {
00193       Type iTp(e[i].getType());
00194       DebugAssert(iTp.isFunction() && iTp.arity()==2,
00195       "TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "
00196       +e.toString());
00197       // Match the return type of i-th input with f's argument
00198       if(iTp[1] != fnType[i-1])
00199   return getEM()->falseExpr();
00200       // Compute the TCC for i(0) ... i(N-1)
00201       for(Rational j=0; j<N; j = j+1)
00202   tccs.push_back(getTypePred(iTp[0], getEM()->newRatExpr(j)));
00203     }
00204     return rewriteAnd(andExpr(tccs)).getRHS();
00205   }
00206   default: 
00207     DebugAssert(false, "TheorySimulate::computeTCC("+e.toString()
00208     +")\n\nUnknown expression.");
00209     return getEM()->trueExpr();
00210   }
00211 }
00212 
00213 
00214 ExprStream&
00215 TheorySimulate::print(ExprStream& os, const Expr& e) {
00216   switch(os.lang()) {
00217   case PRESENTATION_LANG:
00218     switch(e.getKind()) {
00219     case SIMULATE:{
00220       os << "SIMULATE" << "(" << push;
00221       bool first(true);
00222       for (int i = 0; i < e.arity(); i++) {
00223   if (first) first = false;
00224   else os << push << "," << pop << space;
00225   os << e[i];
00226       }
00227       os << push << ")";
00228       break;
00229     }
00230     default:
00231       // Print the top node in the default LISP format, continue with
00232       // pretty-printing for children.
00233       e.printAST(os);
00234       
00235       break;
00236     }
00237     break;
00238   case SMTLIB_LANG:
00239   case SMTLIB_V2_LANG:
00240     d_theoryUsed = true;
00241     throw SmtlibException("TheorySimulate::print: SMTLIB not supported");
00242     switch(e.getKind()) {
00243     case SIMULATE:{
00244       os << "(" << push << "SIMULATE" << space;
00245       for (int i = 0; i < e.arity(); i++) {
00246   os << space << e[i];
00247       }
00248       os << push << ")";
00249       break;
00250     }
00251     default:
00252       // Print the top node in the default LISP format, continue with
00253       // pretty-printing for children.
00254       e.printAST(os);
00255       
00256       break;
00257     }
00258     break;
00259   case LISP_LANG:
00260     switch(e.getKind()) {
00261     case SIMULATE:{
00262       os << "(" << push << "SIMULATE" << space;
00263       for (int i = 0; i < e.arity(); i++) {
00264   os << space << e[i];
00265       }
00266       os << push << ")";
00267       break;
00268     }
00269     default:
00270       // Print the top node in the default LISP format, continue with
00271       // pretty-printing for children.
00272       e.printAST(os);
00273       
00274       break;
00275     }
00276     break;
00277   default:  // Not a known language
00278     e.printAST(os);
00279     break;
00280   }
00281   return os;
00282 }