CVC3

records_theorem_producer.cpp

Go to the documentation of this file.
00001 
00002 /*****************************************************************************/
00003 /*!
00004  * \file records_theorem_producer.cpp
00005  * 
00006  * Author: Daniel Wichs
00007  * 
00008  * Created: Jul 22 22:59:07 GMT 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
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 //! ==> (SELECT (LITERAL  v1 ... vi ...) fi) = vi
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 child:\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 //! ==> (RECORD_SELECT (RECORD_UPDATE r fi vi) fj) = vi
00080 //iff j=i, r.fj otherwise  (and same for tuples)
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     break;
00113   }
00114   //to avoid warnings
00115   return newRWTheorem(e, e, Assumptions::emptyAssump(), pf);
00116 }
00117 
00118 
00119 //! ==> (RECORD_UPDATE (RECORD (f1 v1) ... (fi vi) ...) fi v') =(RECORD (f1 v1) ... (fi v') ...) and same for tuples.
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 }