simulate_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file simulate_theorem_producer.cpp
00004  *\brief Trusted implementation of the proof rules for symbolic simulator
00005  *
00006  * Author: Sergey Berezin
00007  *
00008  * Created: Tue Oct  7 10:55:24 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 // This code is trusted
00023 #define _CVC3_TRUSTED_
00024 
00025 #include <algorithm>
00026 
00027 #include "simulate_theorem_producer.h"
00028 #include "theory_simulate.h"
00029 #include "theory_core.h"
00030 
00031 using namespace std;
00032 using namespace CVC3;
00033 
00034 ////////////////////////////////////////////////////////////////////
00035 // TheoryArith: trusted method for creating ArithTheoremProducer
00036 ////////////////////////////////////////////////////////////////////
00037 
00038 SimulateProofRules* TheorySimulate::createProofRules() {
00039   return new SimulateTheoremProducer(theoryCore()->getTM());
00040 }
00041   
00042 ////////////////////////////////////////////////////////////////////
00043 // Proof rules
00044 ////////////////////////////////////////////////////////////////////
00045 
00046 Theorem SimulateTheoremProducer::expandSimulate(const Expr& e) {
00047   const int arity = e.arity();
00048   if (CHECK_PROOFS) {
00049     CHECK_SOUND(e.getKind() == SIMULATE, 
00050     "SimulateTheoremProducer::expandSimulate: "
00051     "expected SIMULATE expression: "
00052     +e.toString());
00053     CHECK_SOUND(arity >= 3 && e[arity - 1].isRational() && 
00054     e[arity - 1].getRational().isInteger(), 
00055     "SimulateTheoremProducer::expandSimulate: "
00056     "incorrect children in SIMULATE: " + e.toString());
00057   }
00058 
00059   int n = e[arity - 1].getRational().getInt();
00060 
00061   if(CHECK_PROOFS) {
00062     CHECK_SOUND(n >= 0, "SimulateTheoremProducer::expandSimulate: "
00063     "Requested negative number of iterations: "+int2string(n));
00064   }
00065  
00066   // Compute f(f(...f(f(s0, I1(0), I2(0), ...), I1(1), ...), ... ),
00067   //           I1(n-1), ...)
00068   //
00069   // We do this by accumulating the expression in 'res':
00070   // res_{i+1} = func(res_i, I1(i), ..., Ik(i))
00071   Expr res(e[1]);
00072   for(int i=0; i<n; ++i) {
00073     vector<Expr> args;
00074     args.push_back(res);
00075     Expr ri(d_em->newRatExpr(i));
00076     for(int j=2; j<arity-1; ++j)
00077       args.push_back(Expr(e[j].mkOp(), ri));
00078     res = Expr(e[0].mkOp(), args);
00079   }
00080 
00081   Proof pf;
00082   if(withProof())
00083     pf = newPf("expand_simulate", e);
00084   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00085 }

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2