theory_quant.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory_quant.h
 * 
 * Author: Sergey Berezin
 * 
 * Created: Jun 24 21:13:59 GMT 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>
 * 
 * ! Author: Daniel Wichs
 * ! Created: Wednesday July 2, 2003
 * 
 */
/*****************************************************************************/
#ifndef _cvcl__include__theory_quant_h_
#define _cvcl__include__theory_quant_h_

#include "theory.h"
#include "cdmap.h"
#include "statistics.h"

namespace CVCL {

class QuantProofRules;

/*****************************************************************************/
/*!
 *\class TheoryQuant
 *\ingroup Theories
 *\brief This theory handles quantifiers.
 *
 * Author: Daniel Wichs
 *
 * Created: Wednesday July 2,  2003
 */
/*****************************************************************************/
class TheoryQuant :public Theory {
  
  class  TypeComp { //!< needed for typeMap
  public:
    bool operator() (const Type t1, const Type t2) const
      {return (t1.getExpr() < t2.getExpr()); }
  };
  
  //! used to facilitate instantiation of universal quantifiers
  typedef std::map<Type, std::vector<size_t>, TypeComp > typeMap; 

  //! database of universally quantified theorems
  CDList<Theorem> d_univs; 
  
  //!tracks a possition in the savedTerms map
  CDO<size_t> d_savedTermsPos;
  //!tracks a possition in the database of universals
  CDO<size_t> d_univsSavedPos;
  //!tracks a possition in the database of universals
  CDO<size_t> d_univsPosFull;
  //!tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.

  CDO<size_t> d_univsContextPos;
  
  
  CDO<int> d_instCount; //!< number of instantiations made in given context

  //! a map of types to posisitions in the d_contextTerms list
  std::map<Type, CDList<size_t>* ,TypeComp> d_contextMap;
  //! a list of all the terms appearing in the current context
  CDList<Expr> d_contextTerms;
  CDMap<Expr, bool> d_contextCache;//!< chache of expressions
  
  //! a map of types to positions in the d_savedTerms vector
  typeMap d_savedMap;
  ExprMap<bool> d_savedCache; //!< cache of expressions
  //! a vector of all of the terms that have produced conflicts.
  std::vector<Expr> d_savedTerms; 

  //! a map of instantiated universals to a vector of their instantiations
  ExprMap<std::vector<Expr> >  d_insts;

  //! quantifier theorem production rules
  QuantProofRules* d_rules;
  
  const int* d_maxQuantInst; //!< Command line option

  /*! \brief categorizes all the terms contained in an expressions by
   *type.
   *
   * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
   * returns true if the expression does not contain bound variables, false
   * otherwise.
   */
  bool recursiveMap(const Expr& term);

  /*! \brief categorizes all the terms contained in a vector of  expressions by
   * type.
   *
   * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
   */
  void mapTermsByType(const CDList<Expr>& terms);
  
  /*! \brief Queues up all possible instantiations of bound
   * variables.
   *
   * The savedMap boolean indicates whether to use savedMap or
   * d_contextMap the all boolean indicates weather to use all
   * instantiation or only new ones and newIndex is the index where
   * new instantiations begin.
   */
  void instantiate(Theorem univ, bool all, bool savedMap, 
                   size_t newIndex);
  //! does most of the work of the instantiate function.
  void recInstantiate(Theorem& univ , bool all, bool savedMap,size_t newIndex, 
                                   std::vector<Expr>& varReplacements);

  /*! \brief A recursive function used to find instantiated universals
   * in the hierarchy of assumptions.
   */
  void findInstAssumptions(const Theorem& thm);

 
  
  const bool* d_useNew;
  const bool* d_useLazyInst;
  const bool* d_useSemMatch;
  const bool* d_useAtomSem;
  
  int d_instThisRound;
  int d_callThisRound;

  ExprMap<std::vector<Expr> > d_univsTriggers;
  std::map<Type, std::vector<Expr>,TypeComp > d_typeExprMap;
  std::set<std::string> cacheHead;

  StatCounter d_allInstCount ;
  CDO<int> d_instRound;

  void synCheckSat(bool);
  void semCheckSat(bool);
  void naiveCheckSat(bool);

  void synInst(const Theorem & univ,
               size_t tBegin);
  void semInst(const Theorem & univ,
               size_t tBegin);


  void goodSynMatch(const Expr& e,
                    const std::vector<Expr> & boundVars,
                    std::set<std::vector<Expr> >& instSet,
                    size_t tBegin);
  bool recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
  

  bool hasGoodSynInst(const Expr& e,
                   std::vector<Expr>& bVars,
                   std::set<std::vector<Expr> >& instSet,
                   size_t tBegin);
  
  void recGoodSemMatch(const Expr& e,
                       const std::vector<Expr>& bVars,
                       std::vector<Expr>& newInst,
                       std::set<std::vector<Expr> >& instSet);
  
  bool hasGoodSemInst(const Expr& e,
                   std::vector<Expr>& bVars,
                   std::set<std::vector<Expr> >& instSet,
                   size_t tBegin);

  std::string getHead(const Expr& e) ;
  void setupTriggers(const Theorem& thm);
  void enqueueInst(const Theorem thm); 


  /*! \brief categorizes all the terms contained in an expressions by
   *type.
   *
   * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
   * returns true if the expression does not contain bound variables, false
   * otherwise.
   */

  
 public:
  TheoryQuant(TheoryCore* core); //!< Constructor
  ~TheoryQuant(); //! Destructor

  QuantProofRules* createProofRules();
  

 
  void addSharedTerm(const Expr& e) {} //!< Theory interface
  
  /*! \brief Theory interface function to assert quantified formulas
   *
   * pushes in negations and converts to either universally or existentially 
   * quantified theorems. Universals are stored in a database while 
   * existentials are enqueued to be handled by the search engine.
   */
  void assertFact(const Theorem& e); 
  

  /* \brief Checks the satisfiability of the universal theorems stored in a 
   * databse by instantiating them.
   *
   * There are two algorithms that the checkSat function uses to find 
   * instnatiations. The first algortihm looks for instanitations in a saved 
   * database of previous instantiations that worked in proving an earlier
   * theorem unsatifiable. All of the class variables with the word saved in
   * them  are for the use of this algorithm. The other algorithm uses terms 
   * found in the assertions that exist in the particular context when 
   * checkSat is called. All of the class variables with the word context in
   * them are used for the second algorithm.
   */
  void checkSat(bool fullEffort);
  void setup(const Expr& e); 
  void update(const Theorem& e, const Expr& d);
  /*!\brief Used to notify the quantifier algorithm of possible 
   * instantiations that were used in proving a context inconsistent.
   */
  void notifyInconsistent(const Theorem& thm); 
  //! computes the type of a quantified term. Always a  boolean.
  void computeType(const Expr& e); 
  Expr computeTCC(const Expr& e);
  
  virtual Expr parseExprOp(const Expr& e);

  ExprStream& print(ExprStream& os, const Expr& e);
};
 
}

#endif

---