CVC3  2.4.1
records_theorem_producer.cpp
Go to the documentation of this file.
1 
2 /*****************************************************************************/
3 /*!
4  * \file records_theorem_producer.cpp
5  *
6  * Author: Daniel Wichs
7  *
8  * Created: Jul 22 22:59:07 GMT 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 #define _CVC3_TRUSTED_
22 
24 #include "theory_records.h"
25 #include "theory_core.h"
26 
27 
28 using namespace std;
29 using namespace CVC3;
30 
31 
32 RecordsProofRules* TheoryRecords::createProofRules() {
33  return new RecordsTheoremProducer(theoryCore()->getTM(), this);
34 }
35 
36 
37 #define CLASS_NAME "CVC3::RecordsTheoremProducer"
38 
39 //! ==> (SELECT (LITERAL v1 ... vi ...) fi) = vi
40 Theorem RecordsTheoremProducer::rewriteLitSelect(const Expr &e){
41 
42  Proof pf;
43  if(withProof())
44  pf = newPf("rewrite_record_literal_select", e);
45 
46  int index=0;
47  switch(e.getOpKind())
48  {
49  case RECORD_SELECT: {
50  if(CHECK_PROOFS) {
51  CHECK_SOUND(e[0].getOpKind()==RECORD,
52  "expected RECORD child:\n"
53  +e.toString());
54  }
55  index = getFieldIndex(e[0], getField(e));
56  break;
57  }
58  case TUPLE_SELECT: {
59  if(CHECK_PROOFS) {
60  CHECK_SOUND(e[0].getOpKind()==TUPLE,
61  "expected TUPLE child:\n"
62  +e.toString());
63  }
64  index = getIndex(e);
65  break;
66  }
67  default: {
68  if(CHECK_PROOFS)
69  CHECK_SOUND(false, "expected TUPLE_SELECT or RECORD_SELECT kind"
70  + e.toString());
71  }
72  }
73  if(CHECK_PROOFS) {
74  CHECK_SOUND(index!=-1 && index<e[0].arity(),
75  "selected field did not appear in literal" + e.toString());
76  }
77  return newRWTheorem(e, e[0][index], Assumptions::emptyAssump(), pf);
78 }
79 //! ==> (RECORD_SELECT (RECORD_UPDATE r fi vi) fj) = vi
80 //iff j=i, r.fj otherwise (and same for tuples)
81 Theorem RecordsTheoremProducer::rewriteUpdateSelect(const Expr& e) {
82  Proof pf;
83  switch(e.getOpKind()) {
84  case RECORD_SELECT: {
85  if(CHECK_PROOFS)
86  CHECK_SOUND(e[0].getOpKind() == RECORD_UPDATE,
87  "expected RECORD_UPDATE child" + e.toString());
88  if(withProof())
89  pf = newPf("rewrite_record_update_and_select", e);
90  if(getField(e) == getField(e[0]))
91  return newRWTheorem(e, e[0][1], Assumptions::emptyAssump(), pf);
92  else
93  return newRWTheorem(e, recordSelect(e[0][0], getField(e)), Assumptions::emptyAssump(), pf);
94  break;
95  }
96  case TUPLE_SELECT: {
97  if(CHECK_PROOFS)
98  CHECK_SOUND(e[0].getOpKind() == TUPLE_UPDATE,
99  "expected TUPLE_UPDATE child" + e.toString());
100  if(withProof())
101  pf = newPf("rewrite_record_update_and_select", e);
102  if(getIndex(e) == getIndex(e[0]))
103  return newRWTheorem(e, e[0][1], Assumptions::emptyAssump(), pf);
104  else
105  return newRWTheorem(e, tupleSelect(e[0][0], getIndex(e)), Assumptions::emptyAssump(), pf);
106  break;
107  }
108  default:
109  if(CHECK_PROOFS)
110  CHECK_SOUND(false, "expected RECORD_SELECT or TUPLE_SELECT kind"
111  + e.toString());
112  break;
113  }
114  //to avoid warnings
115  return newRWTheorem(e, e, Assumptions::emptyAssump(), pf);
116 }
117 
118 
119 //! ==> (RECORD_UPDATE (RECORD (f1 v1) ... (fi vi) ...) fi v') =(RECORD (f1 v1) ... (fi v') ...) and same for tuples.
120 Theorem RecordsTheoremProducer::rewriteLitUpdate(const Expr& e) {
121  int index =0;
122  switch(e.getOpKind()) {
123  case RECORD_UPDATE: {
124  if(CHECK_PROOFS)
125  CHECK_SOUND(e[0].getOpKind() == RECORD,
126  "expected a RECORD: e = "+e.toString());
127  index = getFieldIndex(e[0], getField(e));
128  break;
129  }
130  case TUPLE_UPDATE: {
131  if(CHECK_PROOFS)
132  CHECK_SOUND(e[0].getOpKind() == TUPLE,
133  "expected a TUPLE: e = "+ e.toString());
134  index = getIndex(e);
135  break;
136  }
137  default:
138  if(CHECK_PROOFS)
139  CHECK_SOUND(false, "expected RECORD_UPDATE or TUPLE_UPDATE kind"
140  + e.toString());
141  }
142 
143  vector<Expr> fieldVals= e[0].getKids();
144  if(CHECK_PROOFS)
145  CHECK_SOUND(index!=-1 && index<e[0].arity(),
146  "update field does not appear in literal"
147  + e.toString());
148  fieldVals[index] = e[1];
149  Proof pf;
150  if(withProof())
151  pf= newPf("rewrite record_literal_update", e);
152  if(e.getOpKind() == RECORD_UPDATE)
153  return newRWTheorem(e, recordExpr(getFields(e[0]), fieldVals), Assumptions::emptyAssump(), pf);
154  else
155  return newRWTheorem(e, tupleExpr(fieldVals), Assumptions::emptyAssump(), pf);
156 }
157 
158 Theorem RecordsTheoremProducer::expandNeq(const Theorem& neqThrm)
159 {
160  Expr e = neqThrm.getExpr();
161  if(CHECK_PROOFS)
162  CHECK_SOUND(e.getKind() == NOT, "expected not expression" + e.toString());
163  e=e[0];
164  Expr e0 = e[0].getType().getExpr() , e1 = e[1].getType().getExpr();
165  if(CHECK_PROOFS)
166  {
167  CHECK_SOUND(e.getKind() == EQ,
168  "equation expression expected \n" + e.toString());
169  CHECK_SOUND(e0.arity()==e1.arity() && e0.getOpKind() == e1.getOpKind(),
170  "equation types mismatch \n" + e.toString());
172  "expected TUPLES or RECORDS \n" + e.toString());
173  }
174  std::vector<Expr> orChildren;
175  for(int i=0; i<e0.arity();i++)
176  {
177  Expr lhs, rhs;
178  switch(e0.getOpKind()) {
179  case RECORD_TYPE: {
180  const string& field(getField(e0, i));
181  DebugAssert(field == getField(e1, i),
182  "equation types mismatch \n" + neqThrm.getExpr().toString());
183  lhs = recordSelect(e[0], field);
184  rhs = recordSelect(e[1], field);
185  break;
186  }
187  case TUPLE_TYPE: {
188  lhs = tupleSelect(e[0], i);
189  rhs = tupleSelect(e[1], i);
190  break;
191  }
192  default:
193  DebugAssert(false, "RecordsTheoremProducer::expandNeq: "
194  "Type must be TUPLE or RECORD: "+e0.toString());
195  }
196  Expr eq = lhs.getType().isBool()? lhs.iffExpr(rhs) : lhs.eqExpr(rhs);
197  orChildren.push_back(!eq);
198  }
199  Proof pf;
200  if(withProof())
201  pf= newPf("rewrite_record_literal_update", e, neqThrm.getProof());
202  return newTheorem(orExpr(orChildren), neqThrm.getAssumptionsRef(), pf);
203 }
204 
205 Theorem RecordsTheoremProducer::expandEq(const Theorem& eqThrm)
206 {
207  Expr lhs(eqThrm.getLHS()), e0 = lhs.getType().getExpr();
208  Expr rhs(eqThrm.getRHS()), e1 = rhs.getType().getExpr();
209  if(CHECK_PROOFS)
210  {
211  CHECK_SOUND(eqThrm.isRewrite(),
212  "equation expression expected \n"
213  + eqThrm.getExpr().toString());
214  CHECK_SOUND(e0.arity() == e1.arity() && e0.getOpKind() == e1.getOpKind(),
215  "equation types mismatch \n" + eqThrm.getExpr().toString());
216  CHECK_SOUND(e0.getOpKind() == RECORD_TYPE || e0.getOpKind() == TUPLE_TYPE,
217  "expected TUPLES or RECORDS \n" + eqThrm.getExpr().toString());
218  }
219  std::vector<Expr> andChildren;
220  for(int i=0; i<e0.arity();i++)
221  {
222  Expr lhs1, rhs1;
223  switch(e0.getOpKind()) {
224  case RECORD_TYPE: {
225  const vector<Expr>& fields(getFields(e0));
226  DebugAssert(fields[i].getString() == getField(e1, i),
227  "equation types mismatch \n" + eqThrm.getExpr().toString());
228  lhs1 = recordSelect(lhs, fields[i].getString());
229  rhs1 = recordSelect(rhs, fields[i].getString());
230  break;
231  }
232  case TUPLE_TYPE: {
233  lhs1 = tupleSelect(lhs, i);
234  rhs1 = tupleSelect(rhs, i);
235  break;
236  }
237  default:
238  DebugAssert(false, "RecordsTheoremProducer::expandEq(): "
239  "Type must be TUPLE or RECORD: "+e0.toString());
240  }
241  Expr eq = lhs1.getType().isBool()? lhs1.iffExpr(rhs1) : lhs1.eqExpr(rhs1);
242  andChildren.push_back(eq);
243  }
244  Proof pf;
245  if(withProof())
246  pf= newPf("rewrite record_literal_update",
247  eqThrm.getExpr(), eqThrm.getProof());
248  return newTheorem(andExpr(andChildren), eqThrm.getAssumptionsRef() , pf);
249 }
250 
251 
252 Theorem RecordsTheoremProducer::expandRecord(const Expr& e) {
253  Type tp(d_theoryRecords->getBaseType(e));
254  if(CHECK_PROOFS) {
255  CHECK_SOUND(isRecordType(tp),
256  "expandRecord("+e.toString()+"): not a record type");
257  }
258  const vector<Expr>& fields = getFields(tp.getExpr());
259  vector<Expr> kids;
260  for(vector<Expr>::const_iterator i=fields.begin(), iend=fields.end();
261  i!=iend; ++i)
262  kids.push_back(recordSelect(e, (*i).getString()));
263  Proof pf;
264  if(withProof()) pf = newPf("expand_record", e);
265  return newRWTheorem(e, recordExpr(fields, kids), Assumptions::emptyAssump(), pf);
266 }
267 
268 
269 Theorem RecordsTheoremProducer::expandTuple(const Expr& e) {
270  Type tp(d_theoryRecords->getBaseType(e));
271  if(CHECK_PROOFS) {
272  CHECK_SOUND(tp.getExpr().getOpKind() == TUPLE_TYPE,
273  "expandTuple("+e.toString()+"): not a tuple type");
274  }
275  int size(tp.arity());
276  vector<Expr> kids;
277  for(int i=0; i<size; ++i)
278  kids.push_back(tupleSelect(e, i));
279  Proof pf;
280  if(withProof()) pf = newPf("expand_tuple", e);
281  return newRWTheorem(e, tupleExpr(kids), Assumptions::emptyAssump(), pf);
282 }
int arity() const
Definition: expr.h:1201
Data structure of expressions in CVC3.
Definition: expr.h:133
MS C++ specific settings.
Definition: type.h:42
Definition: kinds.h:66
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isBool() const
Definition: type.h:60
#define DebugAssert(cond, str)
Definition: debug.h:408
#define CHECK_SOUND(cond, msg)
#define CHECK_PROOFS
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
const Expr & getExpr() const
Definition: type.h:52
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
int getKind() const
Definition: expr.h:1168
const Expr & getRHS() const
Definition: theorem.cpp:246
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr getExpr() const
Definition: theorem.cpp:230
const Expr & getLHS() const
Definition: theorem.cpp:240
Definition: kinds.h:61
const std::string & getString() const
Definition: expr.h:1055
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