21 #define _CVC3_TRUSTED_
37 #define CLASS_NAME "CVC3::RecordsTheoremProducer"
40 Theorem RecordsTheoremProducer::rewriteLitSelect(
const Expr &e){
44 pf = newPf(
"rewrite_record_literal_select", e);
52 "expected RECORD child:\n"
55 index = getFieldIndex(e[0], getField(e));
61 "expected TUPLE child:\n"
69 CHECK_SOUND(
false,
"expected TUPLE_SELECT or RECORD_SELECT kind"
75 "selected field did not appear in literal" + e.
toString());
77 return newRWTheorem(e, e[0][index], Assumptions::emptyAssump(), pf);
81 Theorem RecordsTheoremProducer::rewriteUpdateSelect(
const Expr& e) {
87 "expected RECORD_UPDATE child" + e.
toString());
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);
93 return newRWTheorem(e, recordSelect(e[0][0], getField(e)), Assumptions::emptyAssump(), pf);
99 "expected TUPLE_UPDATE child" + e.
toString());
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);
105 return newRWTheorem(e, tupleSelect(e[0][0], getIndex(e)), Assumptions::emptyAssump(), pf);
110 CHECK_SOUND(
false,
"expected RECORD_SELECT or TUPLE_SELECT kind"
115 return newRWTheorem(e, e, Assumptions::emptyAssump(), pf);
126 "expected a RECORD: e = "+e.
toString());
127 index = getFieldIndex(e[0], getField(e));
133 "expected a TUPLE: e = "+ e.
toString());
139 CHECK_SOUND(
false,
"expected RECORD_UPDATE or TUPLE_UPDATE kind"
143 vector<Expr> fieldVals= e[0].
getKids();
146 "update field does not appear in literal"
148 fieldVals[index] = e[1];
151 pf= newPf(
"rewrite record_literal_update", e);
153 return newRWTheorem(e, recordExpr(getFields(e[0]), fieldVals), Assumptions::emptyAssump(), pf);
155 return newRWTheorem(e, tupleExpr(fieldVals), Assumptions::emptyAssump(), pf);
168 "equation expression expected \n" + e.toString());
170 "equation types mismatch \n" + e.toString());
172 "expected TUPLES or RECORDS \n" + e.toString());
174 std::vector<Expr> orChildren;
175 for(
int i=0; i<e0.
arity();i++)
180 const string& field(getField(e0, i));
183 lhs = recordSelect(e[0], field);
184 rhs = recordSelect(e[1], field);
188 lhs = tupleSelect(e[0], i);
189 rhs = tupleSelect(e[1], i);
193 DebugAssert(
false,
"RecordsTheoremProducer::expandNeq: "
194 "Type must be TUPLE or RECORD: "+e0.
toString());
197 orChildren.push_back(!eq);
201 pf= newPf(
"rewrite_record_literal_update", e, neqThrm.
getProof());
212 "equation expression expected \n"
214 CHECK_SOUND(e0.arity() == e1.arity() && e0.getOpKind() == e1.getOpKind(),
219 std::vector<Expr> andChildren;
220 for(
int i=0; i<e0.arity();i++)
223 switch(e0.getOpKind()) {
225 const vector<Expr>& fields(getFields(e0));
226 DebugAssert(fields[i].getString() == getField(e1, i),
228 lhs1 = recordSelect(lhs, fields[i].getString());
229 rhs1 = recordSelect(rhs, fields[i].getString());
233 lhs1 = tupleSelect(lhs, i);
234 rhs1 = tupleSelect(rhs, i);
238 DebugAssert(
false,
"RecordsTheoremProducer::expandEq(): "
239 "Type must be TUPLE or RECORD: "+e0.toString());
242 andChildren.push_back(eq);
246 pf= newPf(
"rewrite record_literal_update",
253 Type tp(d_theoryRecords->getBaseType(e));
256 "expandRecord("+e.
toString()+
"): not a record type");
258 const vector<Expr>& fields = getFields(tp.getExpr());
260 for(vector<Expr>::const_iterator i=fields.begin(), iend=fields.end();
262 kids.push_back(recordSelect(e, (*i).
getString()));
264 if(withProof()) pf = newPf(
"expand_record", e);
265 return newRWTheorem(e, recordExpr(fields, kids), Assumptions::emptyAssump(), pf);
270 Type tp(d_theoryRecords->getBaseType(e));
273 "expandTuple("+e.
toString()+
"): not a tuple type");
275 int size(tp.arity());
277 for(
int i=0; i<size; ++i)
278 kids.push_back(tupleSelect(e, i));
280 if(withProof()) pf = newPf(
"expand_tuple", e);
281 return newRWTheorem(e, tupleExpr(kids), Assumptions::emptyAssump(), pf);
Data structure of expressions in CVC3.
MS C++ specific settings.
Expr eqExpr(const Expr &right) const
#define DebugAssert(cond, str)
#define CHECK_SOUND(cond, msg)
const std::vector< Expr > & getKids() const
Expr orExpr(const std::vector< Expr > &children)
const Expr & getExpr() const
std::string toString() const
Print the expression to a string.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Expr iffExpr(const Expr &right) const
const Expr & getRHS() const
const Assumptions & getAssumptionsRef() const
const Expr & getLHS() const
const std::string & getString() const
Type getType() const
Get the type. Recursively compute if necessary.
Expr andExpr(const std::vector< Expr > &children)