uf_theorem_producer.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file uf_theorem_producer.cpp
 *\brief TRUSTED implementation of uninterpreted function/predicate rules
 *
 * Author: Clark Barrett
 *
 * Created: Tue Aug 31 23:20:27 2004
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


// This code is trusted
#define _CVCL_TRUSTED_


#include "uf_theorem_producer.h"
#include "theory_uf.h"
#include "theory_core.h"


using namespace std;
using namespace CVCL;


////////////////////////////////////////////////////////////////////
// TheoryUF: trusted method for creating UFTheoremProducer
////////////////////////////////////////////////////////////////////


UFProofRules* TheoryUF::createProofRules() {
  return new UFTheoremProducer(theoryCore()->getTM(), this);
}
  

////////////////////////////////////////////////////////////////////
// Proof rules
////////////////////////////////////////////////////////////////////


#define CLASS_NAME "CVCL::UFTheoremProducer"


Theorem UFTheoremProducer::relToClosure(const Theorem& rel)
{
  const Expr& relExpr = rel.getExpr();

  if(CHECK_PROOFS)
    CHECK_SOUND(relExpr.isApply() && relExpr.arity() == 2,
                CLASS_NAME
                "theorem is not a relation or has wrong arity:\n"
                + rel.getExpr().toString());

  Proof pf;
  Assumptions a;

  if (withAssumptions()) a = rel.getAssumptions().copy();
  if(withProof()) {
    pf = newPf("rel_closure", rel.getProof());
  }

  const string& name = relExpr.getOp().getExpr().getName();
  Expr tc = d_theoryUF->transClosureExpr(name, relExpr[0], relExpr[1]);

  return newTheorem(tc, a, pf);
}


Theorem UFTheoremProducer::relTrans(const Theorem& t1, const Theorem& t2)
{
  const Expr& e1 = t1.getExpr();
  const Expr& e2 = t2.getExpr();

  if (CHECK_PROOFS) {
    CHECK_SOUND(e1.getOpKind() == TRANS_CLOSURE &&
                e1.arity() == 2,
                (CLASS_NAME
                 "theorem is not a proper trans_closure expr:\n"
                 + e1.toString()).c_str());
    CHECK_SOUND(e2.getOpKind() == TRANS_CLOSURE &&
                e2.arity() == 2,
                (CLASS_NAME
                 "theorem is not a proper trans_closure expr:\n"
                 + e2.toString()).c_str());
  }

  if (CHECK_PROOFS) {
    CHECK_SOUND(e1.getOpExpr().getName() == e2.getOpExpr().getName() &&
                e1[1] == e2[0],
                (CLASS_NAME
                 "Expr's don't match:\n"
                 + e1.toString() + " and " + e2.toString()).c_str());
  }

  Proof pf;
  Assumptions a;

  if (withAssumptions())
    a = merge(t1, t2);
  if(withProof()) {
    vector<Proof> pfs;
    pfs.push_back(t1.getProof());
    pfs.push_back(t2.getProof());
    pf = newPf("rel_trans", pfs);
  }
  return newTheorem(Expr(e1.getOp(), e1[0], e2[1]), a, pf);
}


Theorem UFTheoremProducer::applyLambda(const Expr& e) {
  if(CHECK_PROOFS) {
    CHECK_SOUND(e.isApply() && e.getOpKind() == LAMBDA,
                "applyLambda("+e.toString()
                +"):\n\n  expression is not an APPLY");
  }
  Expr lambda(e.getOpExpr());
  // Expand the CONSTDEF and LETDECL
//   while(lambda.getKind() == CONSTDEF || lambda.getKind() == LETDECL)
//     lambda = lambda[1];

  if (CHECK_PROOFS) {
    CHECK_SOUND(lambda.isLambda(),
                "applyLambda:\n"
                "Operator is not LAMBDA: " + lambda.toString());
  }

  Expr body(lambda.getBody());
  const vector<Expr>& vars = lambda.getVars();

  if(CHECK_PROOFS) {
    CHECK_SOUND(vars.size() == (size_t)e.arity(), 
                "wrong number of arguments applied to lambda\n");
  }

  // Use the Expr's efficient substitution
  body = body.substExpr(vars, e.getKids());
//   for (unsigned i = 0; i < vars.size(); i++) {
//     body = substFreeTerm(body, vars[i], e[i]);
//   }

  Assumptions a;
  Proof pf;
  if(withProof())
    pf = newPf("apply_lambda", e);
  return newRWTheorem(e, body, a, pf);
}


Theorem UFTheoremProducer::rewriteOpDef(const Expr& e) {
  if(CHECK_PROOFS) {
    CHECK_SOUND(e.isApply(),
                "UFTheoremProducer::rewriteOpDef: 'e' is not a "
                "function application:\n\n "+e.toString());
  }

  Expr op = e.getOpExpr();
  int opKind = op.getKind();

  if(CHECK_PROOFS) {
    CHECK_SOUND(opKind==CONSTDEF || opKind==LETDECL,
                "UFTheoremProducer::rewriteOpDef: operator is not a "
                "named function in:\n\n "+e.toString());
  }
  // Now actually replace the name with the definition
  while(opKind==CONSTDEF || opKind==LETDECL) {
    if(CHECK_PROOFS) {
      CHECK_SOUND(op.arity()==2,
                  "UFTheoremProducer::rewriteOpDef: bad named "
                  "operator in:\n\n "+e.toString());
    }
    op = op[1];
    opKind = op.getKind();
  }
  // ...and construct a Theorem
  Assumptions a;
  Proof pf;
  if(withProof())
    pf = newPf("rewrite_op_def", e);
  return newRWTheorem(e, Expr(op.mkOp(), e.getKids()), a, pf);
}

---