CVC3  2.4.1
datatype_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file datatype_theorem_producer.cpp
4  *\brief TRUSTED implementation of recursive datatype rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Jan 10 15:43:39 2005
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 
23 // This code is trusted
24 #define _CVC3_TRUSTED_
25 
26 
28 #include "theory_datatype.h"
29 #include "theory_core.h"
30 
31 
32 using namespace std;
33 using namespace CVC3;
34 
35 
36 ////////////////////////////////////////////////////////////////////
37 // TheoryDatatype: trusted method for creating DatatypeTheoremProducer
38 ////////////////////////////////////////////////////////////////////
39 
40 
42 TheoryDatatype::createProofRules() {
43  return new DatatypeTheoremProducer(this);
44 }
45 
46 
47 ////////////////////////////////////////////////////////////////////
48 // Proof rules
49 ////////////////////////////////////////////////////////////////////
50 
51 
52 Theorem DatatypeTheoremProducer::dummyTheorem(const CDList<Theorem>& facts,
53  const Expr& e) {
54  vector<Theorem> thmVec;
55  for (unsigned i = 0; i < facts.size(); ++i)
56  thmVec.push_back(facts[i]);
57  Assumptions a(thmVec);
58  Proof pf;
59  return newTheorem(e, a, pf);
60 }
61 
62 
63 Theorem DatatypeTheoremProducer::rewriteSelCons(const CDList<Theorem>& facts,
64  const Expr& e) {
65  if (CHECK_PROOFS) {
66  CHECK_SOUND(isSelector(e), "Selector expected");
67  CHECK_SOUND(d_theoryDatatype->canCollapse(e), "Expected canCollapse");
68  }
69  Proof pf;
70  Expr t;
71 
72  pair<Expr, unsigned> selectorInfo =
73  d_theoryDatatype->getSelectorInfo(e.getOpExpr());
74  if (isConstructor(e[0]) &&
75  selectorInfo.first == getConstructor(e[0])) {
76  t = e[0][selectorInfo.second];
77  }
78  else {
79  Expr selTypeExpr = e.getOpExpr().getType().getExpr();
80  Type type = Type(selTypeExpr[selTypeExpr.arity()-1]);
81  t = d_theoryDatatype->getConstant(type);
82  }
83 
84  if (withProof()) pf = newPf("rewriteSelCons", e, t);
85 
86  if (!isConstructor(e[0])) {
87  vector<Theorem> thmVec;
88  for (unsigned i = 0; i < facts.size(); ++i)
89  thmVec.push_back(facts[i]);
90  Assumptions a(thmVec);
91  return newRWTheorem(e, t, a, pf);
92  }
93  else {
94  return newRWTheorem(e, t, Assumptions::emptyAssump(), pf);
95  }
96 }
97 
98 
99 Theorem DatatypeTheoremProducer::rewriteTestCons(const Expr& e) {
100  if (CHECK_PROOFS) {
101  CHECK_SOUND(isTester(e), "Tester expected");
102  CHECK_SOUND(isConstructor(e[0]), "Expected Test(Cons)");
103  }
104  Proof pf;
105  Expr t;
106  Expr cons = d_theoryDatatype->getConsForTester(e.getOpExpr());
107  if (cons == getConstructor(e[0])) {
108  t = d_theoryDatatype->trueExpr();
109  }
110  else {
111  t = d_theoryDatatype->falseExpr();
112  }
113  if (withProof()) pf = newPf("rewriteTestCons", e, t);
114  return newRWTheorem(e, t, Assumptions::emptyAssump(), pf);
115 }
116 
117 
118 Theorem DatatypeTheoremProducer::decompose(const Theorem& e) {
119  if (CHECK_PROOFS) {
120  CHECK_SOUND(e.isRewrite(), "decompose: expected rewrite");
121  }
122  const Expr& lhs = e.getLHS();
123  const Expr& rhs = e.getRHS();
124  if(CHECK_PROOFS) {
125  CHECK_SOUND(isConstructor(lhs) && isConstructor(rhs) &&
126  lhs.isApply() && rhs.isApply() &&
127  lhs.getOpExpr() == rhs.getOpExpr() &&
128  lhs.arity() > 0 && lhs.arity() == rhs.arity(),
129  "decompose precondition violated");
130  }
131  Assumptions a(e);
132  Proof pf;
133  Expr res = lhs[0].eqExpr(rhs[0]);
134  if (lhs.arity() > 1) {
135  vector<Expr> args;
136  args.push_back(res);
137  for (int i = 1; i < lhs.arity(); ++i) {
138  args.push_back(lhs[i].eqExpr(rhs[i]));
139  }
140  res = andExpr(args);
141  }
142  if (withProof()) pf = newPf("decompose", e.getProof());
143  return newTheorem(res, a, pf);
144 }
145 
146 
147 Theorem DatatypeTheoremProducer::noCycle(const Expr& e) {
148  if (CHECK_PROOFS) {
149  CHECK_SOUND(isConstructor(e) && e.isApply() && e.arity() > 0,
150  "noCycle: expected constructor with children");
151  }
152  Proof pf;
153 
154  Type t = e.getOpExpr().getType();
155  t = t[t.arity()-1];
156  const Op& reach = d_theoryDatatype->getReachablePredicate(t);
157 
158  vector<Expr> args;
159  args.push_back(!Expr(reach, e, e));
160  for (int i = 0; i < e.arity(); ++i) {
161  if (isDatatype(e[i].getType()) &&
162  d_theoryDatatype->getReachablePredicate(e[i].getType()) == reach)
163  args.push_back(Expr(reach, e, e[i]));
164  }
165 
166  if (withProof()) pf = newPf("noCycle", e);
167  return newTheorem(andExpr(args), Assumptions::emptyAssump(), pf);
168 }
int arity() const
Definition: expr.h:1201
bool isConstructor(const Expr &e)
bool isDatatype(const Type &t)
Data structure of expressions in CVC3.
Definition: expr.h:133
Expr getConstructor(const Expr &e)
MS C++ specific settings.
Definition: type.h:42
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isSelector(const Expr &e)
#define CHECK_SOUND(cond, msg)
#define CHECK_PROOFS
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
const Expr & getExpr() const
Definition: type.h:52
int arity() const
Definition: type.h:55
const Expr & getRHS() const
Definition: theorem.cpp:246
TRUSTED implementation of recursive datatype proof rules.
Proof getProof() const
Definition: theorem.cpp:402
unsigned size() const
Definition: cdlist.h:64
bool isApply() const
Definition: expr.h:1014
bool isTester(const Expr &e)
const Expr & getLHS() const
Definition: theorem.cpp:240
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isRewrite() const
Definition: theorem.cpp:224
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945