cnf_rules.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file cnf_rules.h
 * \brief Abstract proof rules for CNF conversion
 * 
 * Author: Clark Barrett
 * 
 * Created: Thu Jan  5 05:24:45 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 _cvcl__sat__cnf_rules_h_
#define _cvcl__sat__cnf_rules_h_

namespace CVCL {

  class Theorem;

/*! \defgroup CNF_Rules Proof Rules for the Search Engines
 * \ingroup CNF
 */
  //! API to the CNF proof rules
  /*! \ingroup CNF_Rules */
  class CNF_Rules {
    /*! \addtogroup CNF_Rules
     * @{ 
     */
  public:
    //! Destructor
    virtual ~CNF_Rules() { }    

    // A_1,...,A_n |- B ==> |- (OR !A_1 ... !A_n B)
    /*! @brief Learned clause rule: 
      \f[\frac{A_1,\ldots,A_n\vdash B}
              {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\f]
     *
     * \param thm is the theorem
     * \f$ A_1,\ldots,A_n\vdash B\f$
     * Each \f$A_i\f$ and \f$B\f$ should be literals
     * \f$B\f$ can also be \f$\mathrm{FALSE}\f$
     */
    virtual Theorem learnedClause(const Theorem& thm) = 0;

    //! |- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
    virtual Theorem ifLiftRule(const Expr& e, int itePos) = 0;

    /*! @} */ // end of CNF_Rules
  }; // end of class CNF_Rules

} // end of namespace CVCL

#endif

---