/*****************************************************************************/
/*!
* \file search_rules.h
* \brief Abstract proof rules interface to the simple search engine
*
* Author: Sergey Berezin
*
* Created: Mon Feb 24 14:19:48 2003
*
* <hr>
*
* 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.
*
* <hr>
*
*/
/*****************************************************************************/
#ifndef _cvc3__search__search_rules_h_
#define _cvc3__search__search_rules_h_
namespace CVC3 {
class Theorem;
class Expr;
/*! \defgroup SE_Rules Proof Rules for the Search Engines
* \ingroup SE
*/
//! API to the proof rules for the Search Engines
/*! \ingroup SE_Rules */
class SearchEngineRules {
/*! \addtogroup SE_Rules
* @{
*/
public:
//! Destructor
virtual ~SearchEngineRules() { }
/*! Eliminate skolem axioms:
* Gamma, Delta |- false => Gamma|- false
* where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
* and gamma does not contain any of the skolem constants c.
*/
virtual Theorem eliminateSkolemAxioms(const Theorem& tFalse,
const std::vector<Theorem>& delta) = 0;
// !A |- FALSE ==> |- A
/*! @brief Proof by contradiction:
\f[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\f]
*/
/*! \f$\neg A\f$ does not have to be present in the assumptions.
* \param a is the assumption \e A
*
* \param pfFalse is the theorem \f$\Gamma, \neg A \vdash\mathrm{FALSE}\f$
*/
virtual Theorem proofByContradiction(const Expr& a,
const Theorem& pfFalse) = 0;
// A |- FALSE ==> !A
/*! @brief Negation introduction:
\f[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\f]
*/
/*!
* \param not_a is the formula \f$\neg A\f$. We pass the negation
* \f$\neg A\f$, and not just \e A, for efficiency: building
* \f$\neg A\f$ is more expensive (due to uniquifying pointers in
* Expr package) than extracting \e A from \f$\neg A\f$.
*
* \param pfFalse is the theorem \f$\Gamma, A \vdash\mathrm{FALSE}\f$
*/
virtual Theorem negIntro(const Expr& not_a, const Theorem& pfFalse) = 0;
// u1:A |- C, u2:!A |- C ==> |- C
/*! @brief Case split:
\f[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C}
{\Gamma_1\cup\Gamma_2\vdash C}\f]
*/
/*!
* \param a is the assumption A to split on
*
* \param a_proves_c is the theorem \f$\Gamma_1, A\vdash C\f$
*
* \param not_a_proves_c is the theorem \f$\Gamma_2, \neg A\vdash C\f$
*/
virtual Theorem caseSplit(const Expr& a,
const Theorem& a_proves_c,
const Theorem& not_a_proves_c) = 0;
// Gamma, A_1,...,A_n |- FALSE ==> Gamma |- (OR !A_1 ... !A_n)
/*! @brief Conflict clause rule:
\f[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}}
{\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\f]
*/
/*!
* \param thm is the theorem
* \f$\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}\f$
*
* \param lits is the vector of literals <em>A<sub>i</sub></em>.
* They must be present in the set of assumptions of \e thm.
*
* \param gamma FIXME: document this!!
*/
virtual Theorem conflictClause(const Theorem& thm,
const std::vector<Theorem>& lits,
const std::vector<Theorem>& gamma) = 0;
// "Cut" rule: { G_i |- A_i }; G', { A_i } |- B ==> union(G_i)+G' |- B.
/*! @brief Cut rule:
\f[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n
\quad \Gamma', A_1,\ldots,A_n\vdash B}
{\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\f]
*/
/*!
* \param thmsA is a vector of theorems \f$\Gamma_i\vdash A_i\f$
*
* \param as_prove_b is the theorem
* \f$\Gamma', A_1,\ldots,A_n\vdash B\f$
* (the name means "A's prove B")
*/
virtual Theorem cutRule(const std::vector<Theorem>& thmsA,
const Theorem& as_prove_b) = 0;
// { G_j |- !A_j, j in [1..n]-{i} }
// G |- (OR A_1 ... A_i ... A_n) ==> G, G_j |- A_i
/*! @brief Unit propagation rule:
\f[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\}
\quad \Gamma\vdash A_1\vee\cdots\vee A_n}
{\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\f]
*/
/*!
* \param clause is the proof of the clause \f$ \Gamma\vdash
* A_1\vee\cdots\vee A_n\f$
*
* \param i is the index (0..n-1) of the literal to be unit-propagated
*
* \param thms is the vector of theorems \f$\Gamma_j\vdash\neg
* A_j\f$ for all literals except <em>A<sub>i</sub></em>
*/
virtual Theorem unitProp(const std::vector<Theorem>& thms,
const Theorem& clause, unsigned i) = 0;
// { G_j |- !A_j, j in [1..n] } , G |- (OR A_1 ... A_n) ==> FALSE
/*! @brief "Conflict" rule (all literals in a clause become FALSE)
\f[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]
\quad \Gamma\vdash A_1\vee\cdots\vee A_n}
{\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma
\vdash\mathrm{FALSE}}\f]
*/
/*!
* \param clause is the proof of the clause \f$ \Gamma\vdash
* A_1\vee\cdots\vee A_n\f$
*
* \param thms is the vector of theorems \f$\Gamma_j\vdash\neg
* A_j\f$
*/
virtual Theorem conflictRule(const std::vector<Theorem>& thms,
const Theorem& clause) = 0;
// Unit propagation for AND
virtual Theorem propAndrAF(const Theorem& andr_th,
bool left,
const Theorem& b_th) = 0;
virtual Theorem propAndrAT(const Theorem& andr_th,
const Theorem& l_th,
const Theorem& r_th) = 0;
virtual void propAndrLRT(const Theorem& andr_th,
const Theorem& a_th,
Theorem* l_th,
Theorem* r_th) = 0;
virtual Theorem propAndrLF(const Theorem& andr_th,
const Theorem& a_th,
const Theorem& r_th) = 0;
virtual Theorem propAndrRF(const Theorem& andr_th,
const Theorem& a_th,
const Theorem& l_th) = 0;
// Conflicts for AND
virtual Theorem confAndrAT(const Theorem& andr_th,
const Theorem& a_th,
bool left,
const Theorem& b_th) = 0;
virtual Theorem confAndrAF(const Theorem& andr_th,
const Theorem& a_th,
const Theorem& l_th,
const Theorem& r_th) = 0;
// Unit propagation for IFF
virtual Theorem propIffr(const Theorem& iffr_th,
int p,
const Theorem& a_th,
const Theorem& b_th) = 0;
// Conflicts for IFF
virtual Theorem confIffr(const Theorem& iffr_th,
const Theorem& i_th,
const Theorem& l_th,
const Theorem& r_th) = 0;
// Unit propagation for ITE
virtual Theorem propIterIte(const Theorem& iter_th,
bool left,
const Theorem& if_th,
const Theorem& then_th) = 0;
virtual void propIterIfThen(const Theorem& iter_th,
bool left,
const Theorem& ite_th,
const Theorem& then_th,
Theorem* if_th,
Theorem* else_th) = 0;
virtual Theorem propIterThen(const Theorem& iter_th,
const Theorem& ite_th,
const Theorem& if_th) = 0;
// Conflict for ITE
virtual Theorem confIterThenElse(const Theorem& iter_th,
const Theorem& ite_th,
const Theorem& then_th,
const Theorem& else_th) = 0;
virtual Theorem confIterIfThen(const Theorem& iter_th,
bool left,
const Theorem& ite_th,
const Theorem& if_th,
const Theorem& then_th) = 0;
// CNF Rules
//! AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]
virtual Theorem andCNFRule(const Theorem& thm) = 0;
//! OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]
virtual Theorem orCNFRule(const Theorem& thm) = 0;
//! (x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
virtual Theorem impCNFRule(const Theorem& thm) = 0;
//! (x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
virtual Theorem iffCNFRule(const Theorem& thm) = 0;
//! ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]
virtual Theorem iteCNFRule(const Theorem& thm) = 0;
//! ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem iteToClauses(const Theorem& ite) = 0;
//! e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
virtual Theorem iffToClauses(const Theorem& iff) = 0;
/*! @} */ // end of SE_Rules
}; // end of class SearchEngineRules
} // end of namespace CVC3
#endif
syntax highlighted by Code2HTML, v. 0.9.1