uf_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file uf_theorem_producer.cpp
00004  *\brief TRUSTED implementation of uninterpreted function/predicate rules
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Tue Aug 31 23:20:27 2004
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 
00022 
00023 // This code is trusted
00024 #define _CVC3_TRUSTED_
00025 
00026 
00027 #include "uf_theorem_producer.h"
00028 #include "theory_uf.h"
00029 #include "theory_core.h"
00030 
00031 
00032 using namespace std;
00033 using namespace CVC3;
00034 
00035 
00036 ////////////////////////////////////////////////////////////////////
00037 // TheoryUF: trusted method for creating UFTheoremProducer
00038 ////////////////////////////////////////////////////////////////////
00039 
00040 
00041 UFProofRules* TheoryUF::createProofRules() {
00042   return new UFTheoremProducer(theoryCore()->getTM(), this);
00043 }
00044   
00045 
00046 ////////////////////////////////////////////////////////////////////
00047 // Proof rules
00048 ////////////////////////////////////////////////////////////////////
00049 
00050 
00051 #define CLASS_NAME "CVC3::UFTheoremProducer"
00052 
00053 
00054 Theorem UFTheoremProducer::relToClosure(const Theorem& rel)
00055 {
00056   const Expr& relExpr = rel.getExpr();
00057 
00058   if(CHECK_PROOFS)
00059     CHECK_SOUND(relExpr.isApply() && relExpr.arity() == 2,
00060     CLASS_NAME
00061     "theorem is not a relation or has wrong arity:\n"
00062     + rel.getExpr().toString());
00063 
00064   Proof pf;
00065   if(withProof()) {
00066     pf = newPf("rel_closure", rel.getProof());
00067   }
00068 
00069   const string& name = relExpr.getOp().getExpr().getName();
00070   Expr tc = d_theoryUF->transClosureExpr(name, relExpr[0], relExpr[1]);
00071 
00072   return newTheorem(tc, rel.getAssumptionsRef(), pf);
00073 }
00074 
00075 
00076 Theorem UFTheoremProducer::relTrans(const Theorem& t1, const Theorem& t2)
00077 {
00078   const Expr& e1 = t1.getExpr();
00079   const Expr& e2 = t2.getExpr();
00080 
00081   if (CHECK_PROOFS) {
00082     CHECK_SOUND(e1.getOpKind() == TRANS_CLOSURE &&
00083     e1.arity() == 2,
00084     (CLASS_NAME
00085      "theorem is not a proper trans_closure expr:\n"
00086      + e1.toString()).c_str());
00087     CHECK_SOUND(e2.getOpKind() == TRANS_CLOSURE &&
00088     e2.arity() == 2,
00089     (CLASS_NAME
00090      "theorem is not a proper trans_closure expr:\n"
00091      + e2.toString()).c_str());
00092   }
00093 
00094   if (CHECK_PROOFS) {
00095     CHECK_SOUND(e1.getOpExpr().getName() == e2.getOpExpr().getName() &&
00096     e1[1] == e2[0],
00097     (CLASS_NAME
00098      "Expr's don't match:\n"
00099      + e1.toString() + " and " + e2.toString()).c_str());
00100   }
00101 
00102   Assumptions a(t1, t2);
00103   Proof pf;
00104   if(withProof()) {
00105     vector<Proof> pfs;
00106     pfs.push_back(t1.getProof());
00107     pfs.push_back(t2.getProof());
00108     pf = newPf("rel_trans", pfs);
00109   }
00110   return newTheorem(Expr(e1.getOp(), e1[0], e2[1]), a, pf);
00111 }
00112 
00113 
00114 Theorem UFTheoremProducer::applyLambda(const Expr& e) {
00115   if(CHECK_PROOFS) {
00116     CHECK_SOUND(e.isApply() && e.getOpKind() == LAMBDA,
00117     "applyLambda("+e.toString()
00118     +"):\n\n  expression is not an APPLY");
00119   }
00120   Expr lambda(e.getOpExpr());
00121 
00122   if (CHECK_PROOFS) {
00123     CHECK_SOUND(lambda.isLambda(),
00124     "applyLambda:\n"
00125     "Operator is not LAMBDA: " + lambda.toString());
00126   }
00127 
00128   Expr body(lambda.getBody());
00129   const vector<Expr>& vars = lambda.getVars();
00130 
00131   if(CHECK_PROOFS) {
00132     CHECK_SOUND(vars.size() == (size_t)e.arity(), 
00133     "wrong number of arguments applied to lambda\n");
00134   }
00135 
00136   // Use the Expr's efficient substitution
00137   body = body.substExpr(vars, e.getKids());
00138 //   for (unsigned i = 0; i < vars.size(); i++) {
00139 //     body = substFreeTerm(body, vars[i], e[i]);
00140 //   }
00141 
00142   Proof pf;
00143   if(withProof())
00144     pf = newPf("apply_lambda", e);
00145   return newRWTheorem(e, body, Assumptions::emptyAssump(), pf);
00146 }
00147 
00148 
00149 Theorem UFTheoremProducer::rewriteOpDef(const Expr& e) {
00150   if(CHECK_PROOFS) {
00151     CHECK_SOUND(e.isApply(),
00152     "UFTheoremProducer::rewriteOpDef: 'e' is not a "
00153     "function application:\n\n "+e.toString());
00154   }
00155 
00156   Expr op = e.getOpExpr();
00157   int opKind = op.getKind();
00158 
00159   if(CHECK_PROOFS) {
00160     CHECK_SOUND(opKind==LETDECL,
00161     "UFTheoremProducer::rewriteOpDef: operator is not a "
00162     "named function in:\n\n "+e.toString());
00163   }
00164   // Now actually replace the name with the definition
00165   while(opKind==LETDECL) {
00166     if(CHECK_PROOFS) {
00167       CHECK_SOUND(op.arity()==2,
00168       "UFTheoremProducer::rewriteOpDef: bad named "
00169       "operator in:\n\n "+e.toString());
00170     }
00171     op = op[1];
00172     opKind = op.getKind();
00173   }
00174   // ...and construct a Theorem
00175   Proof pf;
00176   if(withProof())
00177     pf = newPf("rewrite_op_def", e);
00178   return newRWTheorem(e, Expr(op.mkOp(), e.getKids()), Assumptions::emptyAssump(), pf);
00179 }

Generated on Wed Nov 18 16:13:33 2009 for CVC3 by  doxygen 1.5.2