quant_theorem_producer.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file quant_theorem_producer.cpp
 * 
 * Author: Daniel Wichs
 * 
 * Created: Jul 07 22:22:38 GMT 2003
 *
 * <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>
 * 
 * CLASS: QuantProofRules
 * 
 * 
 * Description: TRUSTED implementation of arithmetic proof rules.
 * 
 */
/*****************************************************************************/

// This code is trusted
#define _CVCL_TRUSTED_


#include "quant_theorem_producer.h"
#include "theory_quant.h"
#include "theory_core.h"


using namespace std;
using namespace CVCL;


QuantProofRules* TheoryQuant::createProofRules() {
  return new QuantTheoremProducer(theoryCore()->getTM(), this);
}
  

#define CLASS_NAME "CVCL::QuantTheoremProducer"


//! ==> NOT FORALL (vars): e  IFF EXISTS (vars) NOT e
Theorem
QuantTheoremProducer::rewriteNotForall(const Expr& e) {
  if(CHECK_PROOFS) {
    CHECK_SOUND(e.isNot() && e[0].isForall(),
                "rewriteNotForall: expr must be NOT FORALL:\n"
                +e.toString());
  }
  Assumptions a;
  Proof pf;
  if(withProof())
    pf = newPf("rewrite_not_forall", e);
  return newRWTheorem(e, e.getEM()->newClosureExpr(EXISTS, e[0].getVars(),
                                                   !e[0].getBody()),
                      a, pf);
}


//! ==> NOT EXISTS (vars): e  IFF FORALL (vars) NOT e
Theorem
QuantTheoremProducer::rewriteNotExists(const Expr& e) {
  if(CHECK_PROOFS) {
    CHECK_SOUND(e.isNot() && e[0].isExists(),
                "rewriteNotExists: expr must be NOT FORALL:\n"
                +e.toString());
  }
  Assumptions a;
  Proof pf;
  if(withProof())
    pf = newPf("rewrite_not_exists", e);
  return newRWTheorem(e, e.getEM()->newClosureExpr(FORALL, e[0].getVars(),
                                                   !e[0].getBody()),
                      a, pf);
}

//! Instantiate a  universally quantified formula
/*! From T|-FORALL(var): e generate T|-psi => e' where e' is obtained
 * from e by instantiating bound variables with terms in
 * vector<Expr>& terms.  The vector of terms should be the same
 * size as the vector of bound variables in e. Also elements in
 * each position i need to have matching base types. psi is the conjunction of 
 * subtype predicates for the bound variables of the quanitfied expression.
 * \param t1 is the quantifier (a Theorem)
 * \param terms are the terms to instantiate.
 */
Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const
                                            vector<Expr>& terms)
{

  Expr e = t1.getExpr();
  const vector<Expr>& boundVars = e.getVars();
  if(CHECK_PROOFS) {
    CHECK_SOUND(boundVars.size() == terms.size(), 
                "Universal instantiation: size of terms array does "
                "not match quanitfied variables array size");
    CHECK_SOUND(e.isForall(),
                "universal instantiation: expr must be FORALL:\n"
                +e.toString());
    for(unsigned int i=0; i<terms.size(); i++)
      CHECK_SOUND(d_theoryQuant->getBaseType(boundVars[i]) ==
                  d_theoryQuant->getBaseType(terms[i]),
              "Universal instantiation: type mismatch");

  }

  //build up a conjunction of type predicates for expression
  Expr tr = e.getEM()->trueExpr();
  Expr typePred = tr;
  for(unsigned int i=0; i<terms.size(); i++) {
    Expr p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
    if(p!=tr) {
      if(typePred==tr)
        typePred = p;
      else
        typePred = typePred.andExpr(p);
    }
  }
  Assumptions a;
  Proof pf;
  if(withAssumptions())
    a = t1.getAssumptionsCopy();
  if(withProof()) {
    vector<Proof> pfs;
    vector<Expr> es;
    pfs.push_back(t1.getProof());
    es.push_back(e);
    es.insert(es.end(), terms.begin(), terms.end());
    pf= newPf("universal_elimination", es, pfs);
  }
   Expr inst = e.getBody().substExpr(e.getVars(), terms);
   Expr imp;
   if(typePred == tr)
     imp = inst;
   else
     imp = typePred.impExpr(inst); 
   return(newTheorem(imp, a, pf));
}

//! find all bound variables in e and maps them to true in boundVars
void QuantTheoremProducer::recFindBoundVars(const Expr& e, 
                           ExprMap<bool> & boundVars, ExprMap<bool> &visited) 
{
  if(visited.count(e)>0)
    return;
  else
    visited[e] = true;
  if(e.getKind() == BOUND_VAR)
    boundVars[e] = true;
  if(e.getKind() == EXISTS || e.getKind() == FORALL)
    recFindBoundVars(e.getBody(), boundVars, visited);
  for(Expr::iterator it = e.begin(); it!=e.end(); ++it)
    recFindBoundVars(*it, boundVars, visited);
  
}

/*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
 * where vars' is obtained from vars by removing all bound variables
 *  not used in e. If vars' is empty the produced theorem is just T|-e
 */
Theorem QuantTheoremProducer::boundVarElim(const Theorem& t1)
{
  const Expr e=t1.getExpr();
  const Expr body = e.getBody();
  if(CHECK_PROOFS) {
      CHECK_SOUND(e.isForall() || e.isExists(),
                "bound var elimination: "
                +e.toString());
  }
  ExprMap<bool> boundVars; //a mapping of bound variables in the body to true
  ExprMap<bool> visited; //to make sure expressions aren't traversed
                          //multiple times
  recFindBoundVars(body, boundVars, visited);
  vector<Expr> quantVars;
  const vector<Expr>& origVars = e.getVars();
  for(vector<Expr>::const_iterator it = origVars.begin(), 
        iend=origVars.end(); it!=iend; ++it)
    {
    if(boundVars.count(*it) > 0)
      quantVars.push_back(*it);
    }

  // If all variables are used, just return the original theorem
  if(quantVars.size() == origVars.size())
    return t1;

  Assumptions a;
  Proof pf;
  if(withAssumptions())
    a = t1.getAssumptionsCopy();
  if(withProof()) {
    vector<Expr> es;
    vector<Proof> pfs;
    es.push_back(e);
    es.insert(es.end(), quantVars.begin(), quantVars.end());
    pfs.push_back(t1.getProof());
    pf= newPf("bound_variable_elimination", es, pfs);
  }
  if(quantVars.size() == 0)
    return(newTheorem(e.getBody(), a, pf));
  
  Expr newQuantExpr;
  if(e.isForall())
    newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(FORALL, quantVars, body);
  else
    newQuantExpr = d_theoryQuant->getEM()->newClosureExpr(EXISTS, quantVars, body);

  return(newTheorem(newQuantExpr, a, pf));
}

---