core_proof_rules.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file core_proof_rules.h
 *\brief Proof rules used by theory_core
 *
 * Author: Clark Barrett
 *
 * Created: Wed Jan 11 15:48:35 2006
 *
 * <hr>
 * Copyright (C) 2006 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>
 * 
 */
/*****************************************************************************/

#ifndef _CVC_lite__core_proof_rules_h_
#define _CVC_lite__core_proof_rules_h_

#include <vector>

namespace CVCL {

  class Theorem;
  class Theorem3;
  class Expr;
  class Op;

  class CoreProofRules {
  public:
    //! Destructor
    virtual ~CoreProofRules() { }

    ////////////////////////////////////////////////////////////////////////
    // TCC rules (3-valued logic)
    ////////////////////////////////////////////////////////////////////////

    //  G1 |- phi   G2 |- D_phi
    // -------------------------
    //       G1,G2 |-_3 phi
    /*!
     * @brief Convert 2-valued formula to 3-valued by discharging its
     *  TCC (\f$D_\phi\f$):
     *  \f[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}}
     *          {\Gamma_1,\,\Gamma_2\vdash_3\phi}\f]
     */
    virtual Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi) = 0;

    //  G0,a1,...,an |-_3 phi  G1 |- D_a1 ... Gn |- D_an
    // -------------------------------------------------
    //    G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi
    /*!
     * @brief 3-valued implication introduction rule:
     * \f[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad
     *          (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}}
     *         {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3
     *              (\bigwedge_{i=1}^n\alpha_i)\to\phi}\f]
     *
     * \param phi is the formula \f$\phi\f$
     * \param assump is the vector of assumptions \f$\alpha_1\ldots\alpha_n\f$
     * \param tccs is the vector of TCCs for assumptions
     *   \f$D_{\alpha_1}\ldots D_{\alpha_n}\f$
     */
    virtual Theorem3 implIntro3(const Theorem3& phi,
                                const std::vector<Expr>& assump,
                                const std::vector<Theorem>& tccs) = 0;


    //! e: T ==> |- typePred_T(e)  [deriving the type predicate of e]
    virtual Theorem typePred(const Expr& e) = 0;

    ////////////////////////////////////////////////////////////////////////
    // Core rewrite rules
    ////////////////////////////////////////////////////////////////////////

    // Rewrite rules used only in TheoryCore to replace LETDECL and
    // CONSTDEF with their definitions
    //! Replace LETDECL with its definition
    /*! Used only in TheoryCore */ 
    virtual Theorem rewriteLetDecl(const Expr& e) = 0;
    //! Replace CONSTDEF with its definition
    /*! Used only in TheoryCore */ 
    virtual Theorem rewriteConstDef(const Expr& e) = 0;
    //! ==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
    virtual Theorem rewriteNotAnd(const Expr& e) = 0;
    //! ==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
    virtual Theorem rewriteNotOr(const Expr& e) = 0;
    //! ==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
    virtual Theorem rewriteNotIff(const Expr& e) = 0;
    //! ==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
    virtual Theorem rewriteNotIte(const Expr& e) = 0;
    //! ==> ITE(TRUE, e1, e2) == e1
    virtual Theorem rewriteIteTrue(const Expr& e) = 0;
    //! ==> ITE(FALSE, e1, e2) == e2
    virtual Theorem rewriteIteFalse(const Expr& e) = 0;
    //! ==> ITE(c, e, e) == e
    virtual Theorem rewriteIteSame(const Expr& e) = 0;
    //! a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
    virtual Theorem rewriteIteThen(const Expr& e, const Theorem& thenThm) = 0;
    //! !a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
    virtual Theorem rewriteIteElse(const Expr& e, const Theorem& elseThm) = 0;
    //! ==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
    virtual Theorem rewriteIteBool(const Expr& c,
                                   const Expr& e1, const Expr& e2) = 0;

    //! |= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
    virtual Theorem orDistributivityRule(const Expr& e) = 0;
    //! |= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
    virtual Theorem andDistributivityRule(const Expr& e) = 0;


    //! ==> IMPLIES(e1,e2) IFF OR(!e1, e2)
    virtual Theorem rewriteImplies(const Expr& e) = 0;

    //! ==> NOT(e) == ITE(e, FALSE, TRUE)
    virtual Theorem NotToIte(const Expr& not_e) = 0;
    //! ==> Or(e) == ITE(e[1], TRUE, e[0])
    virtual Theorem OrToIte(const Expr& e) = 0;
    //! ==> And(e) == ITE(e[1], e[0], FALSE)
    virtual Theorem AndToIte(const Expr& e) = 0;
    //! ==> IFF(a,b) == ITE(a, b, !b)
    virtual Theorem IffToIte(const Expr& e) = 0;
    //! ==> IMPLIES(a,b) == ITE(a, b, TRUE)
    virtual Theorem ImpToIte(const Expr& e) = 0;

    //! ==> ITE(e, FALSE, TRUE) IFF NOT(e)
    virtual Theorem rewriteIteToNot(const Expr& e) = 0;
    //! ==> ITE(a, TRUE, b) IFF OR(a, b)
    virtual Theorem rewriteIteToOr(const Expr& e) = 0;
    //! ==> ITE(a, b, FALSE) IFF AND(a, b)
    virtual Theorem rewriteIteToAnd(const Expr& e) = 0;
    //! ==> ITE(a, b, !b) IFF IFF(a, b)
    virtual Theorem rewriteIteToIff(const Expr& e) = 0;
    //! ==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
    virtual Theorem rewriteIteToImp(const Expr& e) = 0;
    //! ==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
    virtual Theorem rewriteIteCond(const Expr& e) = 0;

    //! |- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
    virtual Theorem ifLiftUnaryRule(const Expr& e) = 0;
    //! ((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
    virtual Theorem iffOrDistrib(const Expr& iff) = 0;
    //! ((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
    virtual Theorem iffAndDistrib(const Expr& iff) = 0;

    // Advanced Boolean transformations

    //! (a & b) <=> a & b[a/true]; takes the index of a
    /*! and rewrites all the other conjuncts. */
    virtual Theorem rewriteAndSubterms(const Expr& e, int idx) = 0;
    //! (a | b) <=> a | b[a/false]; takes the index of a
    /*! and rewrites all the other disjuncts. */
    virtual Theorem rewriteOrSubterms(const Expr& e, int idx) = 0;

  }; // end of class CoreProofRules

} // end of namespace CVCL

#endif

---