search_theorem_producer.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file search_theorem_producer.h
 * \brief Implementation API to proof rules for the simple search engine
 * 
 * Author: Sergey Berezin
 * 
 * Created: Mon Feb 24 14:48:03 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>
 * 
 */
/*****************************************************************************/

#ifndef _cvcl__search__search_theorem_producer_h_
#define _cvcl__search__search_theorem_producer_h_

#include "theorem_producer.h"
#include "search_rules.h"

namespace CVCL {

class CommonProofRules;

  class SearchEngineTheoremProducer
    : public SearchEngineRules,
      public TheoremProducer {
  private:
    CommonProofRules* d_commonRules;

    void verifyConflict(const Theorem& thm, TheoremMap& m);
     
    void checkSoundNoSkolems(const Expr& e, ExprMap<bool>& visited, 
                             const ExprMap<bool>& skolems);
    void checkSoundNoSkolems(const Theorem& t, ExprMap<bool>& visited, 
                             const ExprMap<bool>& skolems);
  public:
    SearchEngineTheoremProducer(TheoremManager* tm);
    // Destructor
    virtual ~SearchEngineTheoremProducer() { }
    
    // Proof by contradiction: !A |- FALSE ==> |- A.  "!A" doesn't
    // have to be present in the assumptions.
    virtual Theorem proofByContradiction(const Expr& a,
                                         const Theorem& pfFalse);
    
    // Similar rule, only negation introduction:
    // A |- FALSE ==> !A
    virtual Theorem negIntro(const Expr& not_a, const Theorem& pfFalse);
    
    // Case split: u1:A |- C, u2:!A |- C  ==>  |- C
    virtual Theorem caseSplit(const Expr& a,
                              const Theorem& a_proves_c,
                              const Theorem& not_a_proves_c);


   

    
    /*! 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);
 

    // Conflict clause rule: 
    // Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B !A_1 ... !A_n)
    // The assumptions A_i are given by the vector 'lits'.
    // If B==FALSE, it is omitted from the result.
    
    // NOTE: here "!A_i" means an inverse of A_i, not just a negation.
    // That is, if A_i is NOT C, then !A_i is C.

    // NOTE: Theorems with same expressions must 
    // be eliminated before passing as lits.
    virtual Theorem conflictClause(const Theorem& thm,
                                   const std::vector<Theorem>& lits, 
                                   const std::vector<Theorem>& gamma);

    // "Cut" rule: { G_i |- A_i };  G', { A_i } |- B ==> union(G_i)+G' |- B.
    virtual Theorem cutRule(const std::vector<Theorem>& thmsA,
                            const Theorem& as_prove_b);

    // "Unit propagation" rule:
    // G_j |- !l_j, j in [1..n]-{i}
    // G |- (OR l_1 ... l_i ... l_n) ==> G, G_j |- l_i
    virtual Theorem unitProp(const std::vector<Theorem>& thms,
                             const Theorem& clause, unsigned i);

    // "Conflict" rule (all literals in a clause become FALSE)
    // { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE
    virtual Theorem conflictRule(const std::vector<Theorem>& thms,
                                 const Theorem& clause);
 
    // Unit propagation for AND
    virtual Theorem propAndrAF(const Theorem& andr_th,
                               bool left,
                               const Theorem& b_th);

    virtual Theorem propAndrAT(const Theorem& andr_th,
                               const Theorem& l_th,
                               const Theorem& r_th);
    

    virtual void propAndrLRT(const Theorem& andr_th,
                             const Theorem& a_th,
                             Theorem* l_th,
                             Theorem* r_th);

    virtual Theorem propAndrLF(const Theorem& andr_th,
                               const Theorem& a_th,
                               const Theorem& r_th);

    virtual Theorem propAndrRF(const Theorem& andr_th,
                               const Theorem& a_th,
                               const Theorem& l_th);

    // Conflicts for AND
    virtual Theorem confAndrAT(const Theorem& andr_th,
                               const Theorem& a_th,
                               bool left,
                               const Theorem& b_th);

    virtual Theorem confAndrAF(const Theorem& andr_th,
                               const Theorem& a_th,
                               const Theorem& l_th,
                               const Theorem& r_th);

    // Unit propagation for IFF
    virtual Theorem propIffr(const Theorem& iffr_th,
                             int p,
                             const Theorem& a_th,
                             const Theorem& b_th);

    // Conflicts for IFF
    virtual Theorem confIffr(const Theorem& iffr_th,
                             const Theorem& i_th,
                             const Theorem& l_th,
                             const Theorem& r_th);

    // Unit propagation for ITE
    virtual Theorem propIterIte(const Theorem& iter_th,
                                bool left,
                                const Theorem& if_th,
                                const Theorem& then_th);

    virtual void propIterIfThen(const Theorem& iter_th,
                                bool left,
                                const Theorem& ite_th,
                                const Theorem& then_th,
                                Theorem* if_th,
                                Theorem* else_th);

    virtual Theorem propIterThen(const Theorem& iter_th,
                                 const Theorem& ite_th,
                                 const Theorem& if_th);

    // Conflicts for ITE
    virtual Theorem confIterThenElse(const Theorem& iter_th,
                                     const Theorem& ite_th,
                                     const Theorem& then_th,
                                     const Theorem& else_th);

    virtual Theorem confIterIfThen(const Theorem& iter_th,
                                   bool left,
                                   const Theorem& ite_th,
                                   const Theorem& if_th,
                                   const Theorem& then_th);

    // CNF Rules
    Theorem andCNFRule(const Theorem& thm);
    Theorem orCNFRule(const Theorem& thm);
    Theorem impCNFRule(const Theorem& thm);
    Theorem iffCNFRule(const Theorem& thm);
    Theorem iteCNFRule(const Theorem& thm);
    Theorem iteToClauses(const Theorem& ite);
    Theorem iffToClauses(const Theorem& iff);

    /////////////////////////////////////////////////////////////////////////
    //// helper functions for CNF (Conjunctive Normal Form) conversion
    /////////////////////////////////////////////////////////////////////////
    private:
    Theorem opCNFRule(const Theorem& thm, int kind,
                      const std::string& ruleName);
    
    Expr convertToCNF(const Expr& v, const Expr & phi);      

    //! checks if phi has v in local cache of opCNFRule, if so reuse v.
    /*! similarly for ( ! ... ! (phi)) */
    Expr findInLocalCache(const Expr& i, 
                          ExprMap<Expr>& localCache,
                          std::vector<Expr>& boundVars);

  }; // end of class SearchEngineRules
} // end of namespace CVCL
#endif

---