CVC3  2.4.1
simulate_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file simulate_theorem_producer.cpp
4  *\brief Trusted implementation of the proof rules for symbolic simulator
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Tue Oct 7 10:55:24 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 // This code is trusted
23 #define _CVC3_TRUSTED_
24 
25 #include <algorithm>
26 
28 #include "theory_simulate.h"
29 #include "theory_core.h"
30 
31 using namespace std;
32 using namespace CVC3;
33 
34 ////////////////////////////////////////////////////////////////////
35 // TheoryArith: trusted method for creating ArithTheoremProducer
36 ////////////////////////////////////////////////////////////////////
37 
38 SimulateProofRules* TheorySimulate::createProofRules() {
39  return new SimulateTheoremProducer(theoryCore()->getTM());
40 }
41 
42 ////////////////////////////////////////////////////////////////////
43 // Proof rules
44 ////////////////////////////////////////////////////////////////////
45 
46 Theorem SimulateTheoremProducer::expandSimulate(const Expr& e) {
47  const int arity = e.arity();
48  if (CHECK_PROOFS) {
50  "SimulateTheoremProducer::expandSimulate: "
51  "expected SIMULATE expression: "
52  +e.toString());
53  CHECK_SOUND(arity >= 3 && e[arity - 1].isRational() &&
54  e[arity - 1].getRational().isInteger(),
55  "SimulateTheoremProducer::expandSimulate: "
56  "incorrect children in SIMULATE: " + e.toString());
57  }
58 
59  int n = e[arity - 1].getRational().getInt();
60 
61  if(CHECK_PROOFS) {
62  CHECK_SOUND(n >= 0, "SimulateTheoremProducer::expandSimulate: "
63  "Requested negative number of iterations: "+int2string(n));
64  }
65 
66  // Compute f(f(...f(f(s0, I1(0), I2(0), ...), I1(1), ...), ... ),
67  // I1(n-1), ...)
68  //
69  // We do this by accumulating the expression in 'res':
70  // res_{i+1} = func(res_i, I1(i), ..., Ik(i))
71  Expr res(e[1]);
72  for(int i=0; i<n; ++i) {
73  vector<Expr> args;
74  args.push_back(res);
75  Expr ri(d_em->newRatExpr(i));
76  for(int j=2; j<arity-1; ++j)
77  args.push_back(Expr(e[j].mkOp(), ri));
78  res = Expr(e[0].mkOp(), args);
79  }
80 
81  Proof pf;
82  if(withProof())
83  pf = newPf("expand_simulate", e);
84  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
85 }
int arity() const
Definition: expr.h:1201
Data structure of expressions in CVC3.
Definition: expr.h:133
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
#define CHECK_SOUND(cond, msg)
#define CHECK_PROOFS
bool isRational(const Expr &e)
Definition: theory_arith.h:177
Implementation of a symbolic simulator.
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
int getKind() const
Definition: expr.h:1168
std::string int2string(int n)
Definition: cvc_util.h:46
Implementation of the symbolic simulator proof rules.
int getInt() const