/*****************************************************************************/
/*!
* \file theorem_producer.h
*
* Author: Sergey Berezin
*
* Created: Dec 10 00:37:49 GMT 2002
*
*
*
* 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.
*
*
*
*/
/*****************************************************************************/
// CLASS: Theorem_Producer
//
// AUTHOR: Sergey Berezin, 07/05/02
//
// Abstract:
//
// This class is the only one that can create new Theorem classes.
//
// Only TRUSTED code can use it; a symbol _CVC3_TRUSTED_ must be
// defined in *.cpp file before including this one; otherwise you'll
// get a compiler warning. Custom header files (*.h) which include
// this file should NOT define _CVC3_TRUSTED_. This practice enforces
// the programmer to be aware of which part of his/her code is
// trusted.
//
// It defines a protected NON-virtual method newTheorem() so that any
// subclass can create a new Theorem. This means that no untrusted
// decision procedure's code should see this interface.
// Unfortunately, this has to be a coding policy rather than something
// we can enforce by C++ class structure.
//
// The intended use of this class is to make a subclass and define new
// methods corresponding to proof rules (they take theorems and
// generate new theorems). Each decision procedure should have such a
// subclass for its trusted core. Each new proof rule must be sound;
// that is, each new theorem that it generates must logically follow
// from the theorems in the arguments, or the new theorem must be a
// tautology.
//
// Each such subclass must also inherit from a decision
// procedure-specific abstract interface which declares the new
// methods (other than newTheorem). The decision procedure should only
// use the new abstract interface. Thus, the DP will not even see
// newTheorem() method.
//
// This way the untrusted part of the code will not be able to create
// an unsound theorem.
//
// Proof rules may expect theorems in the arguments be of a certain
// form; if the expectations are not met, the right thing to do is to
// fail in DebugAssert with the appropriate message. In other words,
// it is a coding bug to pass wrong theorems to the wrong rules.
//
// It is also a bug if a wrong theorem is passed but not detected by
// the proof rule, unless such checks are explicitly turned off
// globally for efficiency.
////////////////////////////////////////////////////////////////////////
#ifndef _CVC3_TRUSTED_
#warning "This file should be included only by TRUSTED code. Define _CVC3_TRUSTED_ before including this file."
#endif
#ifndef _cvc3__theorem_producer_h_
#define _cvc3__theorem_producer_h_
#include "theorem.h"
#include "theorem_manager.h"
#include "exception.h"
// Macro to check for soundness. It should only be executed within a
// TheoremProducer class, and only if the -check-proofs option is set.
// When its 'cond' is violated, it will call a function which will
// eventually throw a soundness exception.
#define CHECK_SOUND(cond, msg) if(!(cond)) \
soundError(__FILE__, __LINE__, #cond, msg)
// Flag whether to check soundness or not
#define CHECK_PROOFS *d_checkProofs
namespace CVC3 {
class TheoremProducer {
protected:
TheoremManager* d_tm;
ExprManager* d_em;
// Command-line option whether to check for soundness
const bool* d_checkProofs;
// Operator for creating proof terms
Op d_pfOp;
// Expr for filling in "condition" arguments in flea proofs
Expr d_hole;
// Make it possible for the subclasses to create theorems directly.
//! Create a new theorem. See also newRWTheorem() and newReflTheorem()
Theorem newTheorem(const Expr& thm,
const Assumptions& assump,
const Proof& pf) {
IF_DEBUG(if(!thm.isEq() && !thm.isIff()) {
TRACE("newTheorem", "newTheorem(", thm, ")");
debugger.counter("newTheorem() called on equality")++;
});
return Theorem(d_tm, thm, assump, pf);
}
//! Create a rewrite theorem: lhs = rhs
Theorem newRWTheorem(const Expr& lhs, const Expr& rhs,
const Assumptions& assump,
const Proof& pf) {
return Theorem(d_tm, lhs, rhs, assump, pf);
}
//! Create a reflexivity theorem
Theorem newReflTheorem(const Expr& e) {
return Theorem(e);
}
Theorem newAssumption(const Expr& thm, const Proof& pf, int scope = -1) {
return Theorem(d_tm, thm, Assumptions::emptyAssump(), pf, true, scope);
}
Theorem3 newTheorem3(const Expr& thm,
const Assumptions& assump,
const Proof& pf) {
IF_DEBUG(if(!thm.isEq() && !thm.isIff()) {
TRACE("newTheorem", "newTheorem3(", thm, ")");
debugger.counter("newTheorem3() called on equality")++;
});
return Theorem3(d_tm, thm, assump, pf);
}
Theorem3 newRWTheorem3(const Expr& lhs, const Expr& rhs,
const Assumptions& assump,
const Proof& pf) {
return Theorem3(d_tm, lhs, rhs, assump, pf);
}
void soundError(const std::string& file, int line,
const std::string& cond, const std::string& msg);
public:
// Constructor
TheoremProducer(TheoremManager *tm);
// Destructor
virtual ~TheoremProducer() { }
//! Testing whether to generate proofs
bool withProof() { return d_tm->withProof(); }
//! Testing whether to generate assumptions
bool withAssumptions() { return d_tm->withAssumptions(); }
//! Create a new proof label (bound variable) for an assumption (formula)
Proof newLabel(const Expr& e);
//////////////////////////////////////////////////////////////////
// Functions to create proof terms
//////////////////////////////////////////////////////////////////
// Apply a rule named 'name' to its arguments, Proofs or Exprs
Proof newPf(const std::string& name);
Proof newPf(const std::string& name, const Expr& e);
Proof newPf(const std::string& name, const Proof& pf);
Proof newPf(const std::string& name, const Expr& e1, const Expr& e2);
Proof newPf(const std::string& name, const Expr& e, const Proof& pf);
Proof newPf(const std::string& name, const Expr& e1,
const Expr& e2, const Expr& e3);
Proof newPf(const std::string& name, const Expr& e1,
const Expr& e2, const Proof& pf);
// Methods with iterators.
// Iterators are preferred to vectors, since they are often
// efficient
Proof newPf(const std::string& name,
Expr::iterator begin, const Expr::iterator &end);
Proof newPf(const std::string& name, const Expr& e,
Expr::iterator begin, const Expr::iterator &end);
Proof newPf(const std::string& name,
Expr::iterator begin, const Expr::iterator &end,
const std::vector& pfs);
// Methods with vectors.
Proof newPf(const std::string& name, const std::vector& args);
Proof newPf(const std::string& name, const Expr& e,
const std::vector& args);
Proof newPf(const std::string& name, const Expr& e,
const std::vector& pfs);
Proof newPf(const std::string& name, const Expr& e1, const Expr& e2,
const std::vector& pfs);
Proof newPf(const std::string& name, const std::vector& pfs);
Proof newPf(const std::string& name, const std::vector& args,
const Proof& pf);
Proof newPf(const std::string& name, const std::vector& args,
const std::vector& pfs);
//! Creating LAMBDA-abstraction (LAMBDA label formula proof)
/*! The label must be a variable with a formula as a type, and
* matching the given "frm". */
Proof newPf(const Proof& label, const Expr& frm, const Proof& pf);
//! Creating LAMBDA-abstraction (LAMBDA label proof).
/*! The label must be a variable with a formula as a type. */
Proof newPf(const Proof& label, const Proof& pf);
/*! @brief Similarly, multi-argument lambda-abstractions:
* (LAMBDA (u1,...,un): (f1,...,fn). pf) */
Proof newPf(const std::vector& labels,
const std::vector& frms,
const Proof& pf);
Proof newPf(const std::vector& labels,
const Proof& pf);
}; // end of Theorem_Producer class
}; // end of namespace CVC3
#endif