00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #define _CVC3_TRUSTED_
00022
00023 #include "records_theorem_producer.h"
00024 #include "theory_records.h"
00025 #include "theory_core.h"
00026
00027
00028 using namespace std;
00029 using namespace CVC3;
00030
00031
00032 RecordsProofRules* TheoryRecords::createProofRules() {
00033 return new RecordsTheoremProducer(theoryCore()->getTM(), this);
00034 }
00035
00036
00037 #define CLASS_NAME "CVC3::RecordsTheoremProducer"
00038
00039
00040 Theorem RecordsTheoremProducer::rewriteLitSelect(const Expr &e){
00041
00042 Proof pf;
00043 if(withProof())
00044 pf = newPf("rewrite_record_literal_select", e);
00045
00046 int index=0;
00047 switch(e.getOpKind())
00048 {
00049 case RECORD_SELECT: {
00050 if(CHECK_PROOFS) {
00051 CHECK_SOUND(e[0].getOpKind()==RECORD,
00052 "expected RECORD child:\n"
00053 +e.toString());
00054 }
00055 index = getFieldIndex(e[0], getField(e));
00056 break;
00057 }
00058 case TUPLE_SELECT: {
00059 if(CHECK_PROOFS) {
00060 CHECK_SOUND(e[0].getOpKind()==TUPLE,
00061 "expected TUPLE childs:\n"
00062 +e.toString());
00063 }
00064 index = getIndex(e);
00065 break;
00066 }
00067 default: {
00068 if(CHECK_PROOFS)
00069 CHECK_SOUND(false, "expected TUPLE_SELECT or RECORD_SELECT kind"
00070 + e.toString());
00071 }
00072 }
00073 if(CHECK_PROOFS) {
00074 CHECK_SOUND(index!=-1 && index<e[0].arity(),
00075 "selected field did not appear in literal" + e.toString());
00076 }
00077 return newRWTheorem(e, e[0][index], Assumptions::emptyAssump(), pf);
00078 }
00079
00080
00081 Theorem RecordsTheoremProducer::rewriteUpdateSelect(const Expr& e) {
00082 Proof pf;
00083 switch(e.getOpKind()) {
00084 case RECORD_SELECT: {
00085 if(CHECK_PROOFS)
00086 CHECK_SOUND(e[0].getOpKind() == RECORD_UPDATE,
00087 "expected RECORD_UPDATE child" + e.toString());
00088 if(withProof())
00089 pf = newPf("rewrite_record_update_and_select", e);
00090 if(getField(e) == getField(e[0]))
00091 return newRWTheorem(e, e[0][1], Assumptions::emptyAssump(), pf);
00092 else
00093 return newRWTheorem(e, recordSelect(e[0][0], getField(e)), Assumptions::emptyAssump(), pf);
00094 break;
00095 }
00096 case TUPLE_SELECT: {
00097 if(CHECK_PROOFS)
00098 CHECK_SOUND(e[0].getOpKind() == TUPLE_UPDATE,
00099 "expected TUPLE_UPDATE child" + e.toString());
00100 if(withProof())
00101 pf = newPf("rewrite_record_update_and_select", e);
00102 if(getIndex(e) == getIndex(e[0]))
00103 return newRWTheorem(e, e[0][1], Assumptions::emptyAssump(), pf);
00104 else
00105 return newRWTheorem(e, tupleSelect(e[0][0], getIndex(e)), Assumptions::emptyAssump(), pf);
00106 break;
00107 }
00108 default:
00109 if(CHECK_PROOFS)
00110 CHECK_SOUND(false, "expected RECORD_SELECT or TUPLE_SELECT kind"
00111 + e.toString());
00112
00113 return newRWTheorem(e, e, Assumptions::emptyAssump(), pf);
00114 }
00115
00116 }
00117
00118
00119
00120 Theorem RecordsTheoremProducer::rewriteLitUpdate(const Expr& e) {
00121 int index =0;
00122 switch(e.getOpKind()) {
00123 case RECORD_UPDATE: {
00124 if(CHECK_PROOFS)
00125 CHECK_SOUND(e[0].getOpKind() == RECORD,
00126 "expected a RECORD: e = "+e.toString());
00127 index = getFieldIndex(e[0], getField(e));
00128 break;
00129 }
00130 case TUPLE_UPDATE: {
00131 if(CHECK_PROOFS)
00132 CHECK_SOUND(e[0].getOpKind() == TUPLE,
00133 "expected a TUPLE: e = "+ e.toString());
00134 index = getIndex(e);
00135 break;
00136 }
00137 default:
00138 if(CHECK_PROOFS)
00139 CHECK_SOUND(false, "expected RECORD_UPDATE or TUPLE_UPDATE kind"
00140 + e.toString());
00141 }
00142
00143 vector<Expr> fieldVals= e[0].getKids();
00144 if(CHECK_PROOFS)
00145 CHECK_SOUND(index!=-1 && index<e[0].arity(),
00146 "update field does not appear in literal"
00147 + e.toString());
00148 fieldVals[index] = e[1];
00149 Proof pf;
00150 if(withProof())
00151 pf= newPf("rewrite record_literal_update", e);
00152 if(e.getOpKind() == RECORD_UPDATE)
00153 return newRWTheorem(e, recordExpr(getFields(e[0]), fieldVals), Assumptions::emptyAssump(), pf);
00154 else
00155 return newRWTheorem(e, tupleExpr(fieldVals), Assumptions::emptyAssump(), pf);
00156 }
00157
00158 Theorem RecordsTheoremProducer::expandNeq(const Theorem& neqThrm)
00159 {
00160 Expr e = neqThrm.getExpr();
00161 if(CHECK_PROOFS)
00162 CHECK_SOUND(e.getKind() == NOT, "expected not expression" + e.toString());
00163 e=e[0];
00164 Expr e0 = e[0].getType().getExpr() , e1 = e[1].getType().getExpr();
00165 if(CHECK_PROOFS)
00166 {
00167 CHECK_SOUND(e.getKind() == EQ,
00168 "equation expression expected \n" + e.toString());
00169 CHECK_SOUND(e0.arity()==e1.arity() && e0.getOpKind() == e1.getOpKind(),
00170 "equation types mismatch \n" + e.toString());
00171 CHECK_SOUND(e0.getOpKind() == RECORD_TYPE || e0.getOpKind() == TUPLE_TYPE,
00172 "expected TUPLES or RECORDS \n" + e.toString());
00173 }
00174 std::vector<Expr> orChildren;
00175 for(int i=0; i<e0.arity();i++)
00176 {
00177 Expr lhs, rhs;
00178 switch(e0.getOpKind()) {
00179 case RECORD_TYPE: {
00180 const string& field(getField(e0, i));
00181 DebugAssert(field == getField(e1, i),
00182 "equation types mismatch \n" + neqThrm.getExpr().toString());
00183 lhs = recordSelect(e[0], field);
00184 rhs = recordSelect(e[1], field);
00185 break;
00186 }
00187 case TUPLE_TYPE: {
00188 lhs = tupleSelect(e[0], i);
00189 rhs = tupleSelect(e[1], i);
00190 break;
00191 }
00192 default:
00193 DebugAssert(false, "RecordsTheoremProducer::expandNeq: "
00194 "Type must be TUPLE or RECORD: "+e0.toString());
00195 }
00196 Expr eq = lhs.getType().isBool()? lhs.iffExpr(rhs) : lhs.eqExpr(rhs);
00197 orChildren.push_back(!eq);
00198 }
00199 Proof pf;
00200 if(withProof())
00201 pf= newPf("rewrite_record_literal_update", e, neqThrm.getProof());
00202 return newTheorem(orExpr(orChildren), neqThrm.getAssumptionsRef(), pf);
00203 }
00204
00205 Theorem RecordsTheoremProducer::expandEq(const Theorem& eqThrm)
00206 {
00207 Expr lhs(eqThrm.getLHS()), e0 = lhs.getType().getExpr();
00208 Expr rhs(eqThrm.getRHS()), e1 = rhs.getType().getExpr();
00209 if(CHECK_PROOFS)
00210 {
00211 CHECK_SOUND(eqThrm.isRewrite(),
00212 "equation expression expected \n"
00213 + eqThrm.getExpr().toString());
00214 CHECK_SOUND(e0.arity() == e1.arity() && e0.getOpKind() == e1.getOpKind(),
00215 "equation types mismatch \n" + eqThrm.getExpr().toString());
00216 CHECK_SOUND(e0.getOpKind() == RECORD_TYPE || e0.getOpKind() == TUPLE_TYPE,
00217 "expected TUPLES or RECORDS \n" + eqThrm.getExpr().toString());
00218 }
00219 std::vector<Expr> andChildren;
00220 for(int i=0; i<e0.arity();i++)
00221 {
00222 Expr lhs1, rhs1;
00223 switch(e0.getOpKind()) {
00224 case RECORD_TYPE: {
00225 const vector<Expr>& fields(getFields(e0));
00226 DebugAssert(fields[i].getString() == getField(e1, i),
00227 "equation types mismatch \n" + eqThrm.getExpr().toString());
00228 lhs1 = recordSelect(lhs, fields[i].getString());
00229 rhs1 = recordSelect(rhs, fields[i].getString());
00230 break;
00231 }
00232 case TUPLE_TYPE: {
00233 lhs1 = tupleSelect(lhs, i);
00234 rhs1 = tupleSelect(rhs, i);
00235 break;
00236 }
00237 default:
00238 DebugAssert(false, "RecordsTheoremProducer::expandEq(): "
00239 "Type must be TUPLE or RECORD: "+e0.toString());
00240 }
00241 Expr eq = lhs1.getType().isBool()? lhs1.iffExpr(rhs1) : lhs1.eqExpr(rhs1);
00242 andChildren.push_back(eq);
00243 }
00244 Proof pf;
00245 if(withProof())
00246 pf= newPf("rewrite record_literal_update",
00247 eqThrm.getExpr(), eqThrm.getProof());
00248 return newTheorem(andExpr(andChildren), eqThrm.getAssumptionsRef() , pf);
00249 }
00250
00251
00252 Theorem RecordsTheoremProducer::expandRecord(const Expr& e) {
00253 Type tp(d_theoryRecords->getBaseType(e));
00254 if(CHECK_PROOFS) {
00255 CHECK_SOUND(isRecordType(tp),
00256 "expandRecord("+e.toString()+"): not a record type");
00257 }
00258 const vector<Expr>& fields = getFields(tp.getExpr());
00259 vector<Expr> kids;
00260 for(vector<Expr>::const_iterator i=fields.begin(), iend=fields.end();
00261 i!=iend; ++i)
00262 kids.push_back(recordSelect(e, (*i).getString()));
00263 Proof pf;
00264 if(withProof()) pf = newPf("expand_record", e);
00265 return newRWTheorem(e, recordExpr(fields, kids), Assumptions::emptyAssump(), pf);
00266 }
00267
00268
00269 Theorem RecordsTheoremProducer::expandTuple(const Expr& e) {
00270 Type tp(d_theoryRecords->getBaseType(e));
00271 if(CHECK_PROOFS) {
00272 CHECK_SOUND(tp.getExpr().getOpKind() == TUPLE_TYPE,
00273 "expandTuple("+e.toString()+"): not a tuple type");
00274 }
00275 int size(tp.arity());
00276 vector<Expr> kids;
00277 for(int i=0; i<size; ++i)
00278 kids.push_back(tupleSelect(e, i));
00279 Proof pf;
00280 if(withProof()) pf = newPf("expand_tuple", e);
00281 return newRWTheorem(e, tupleExpr(kids), Assumptions::emptyAssump(), pf);
00282 }