theory_quant.h

Go to the documentation of this file.

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

#include "theory.h"
#include "cdmap.h"
#include "statistics.h"
#include<queue>

namespace CVC3 {

class QuantProofRules;

/*****************************************************************************/
/*!
 *\class TheoryQuant
 *\ingroup Theories
 *\brief This theory handles quantifiers.
 *
 * Author: Daniel Wichs
 *
 * Created: Wednesday July 2,  2003
 */
/*****************************************************************************/

 typedef enum{ Ukn, Pos, Neg, PosNeg} Polarity;

 class Trigger {
 public: 
   Expr trig;
   Polarity polarity;
   
   std::vector<Expr> bvs;
   Expr head;
   bool hasRWOp;
   bool hasTrans;
   bool hasT2; //if has trans of 2,
   bool isSimple; //if of the form g(x,a);
   bool isSuperSimple; //if of the form g(x,y);
   bool isMulti;
   size_t multiIndex; 
   size_t multiId;

   Trigger(TheoryCore* core, Expr e, Polarity pol, std::set<Expr>);
   bool  isPos();
   bool  isNeg();
   Expr  getEx();
   std::vector<Expr> getBVs(); 
   void  setHead(Expr h);
   Expr  getHead();
   void  setRWOp(bool b);
   bool  hasRW(); 
   void  setTrans(bool b);
   bool  hasTr(); 
   void  setTrans2(bool b);
   bool  hasTr2(); 
   void  setSimp();
   bool  isSimp(); 
   void  setSuperSimp();
   bool  isSuperSimp(); 
   void  setMultiTrig();
   bool  isMultiTrig(); 

   
 };

 typedef struct dynTrig{
   Trigger trig;
   size_t univ_id;
   ExprMap<Expr> binds;
   dynTrig(Trigger t, ExprMap<Expr> b, size_t id);
 } dynTrig;
 
 
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; 

  CDList<Theorem> d_rawUnivs; 

  CDList<dynTrig> d_arrayTrigs; 
  CDO<size_t> d_lastArrayPos;

  //! universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground term matched with the trigger is in d_gtermQueue 
  std::queue<Theorem> d_univsQueue;

  std::queue<Theorem> d_simplifiedThmQueue;

  ExprMap<std::set<std::vector<Expr> > >  d_tempBinds;

  //!tracks the possition of preds 
  CDO<size_t> d_lastPredsPos;
  //!tracks the possition of terms 
  CDO<size_t> d_lastTermsPos;

  //!tracks the positions of preds for partial instantiation
  CDO<size_t> d_lastPartPredsPos;
  //!tracks the possition of terms for partial instantiation
  CDO<size_t> d_lastPartTermsPos;
  //!tracks a possition in the database of universals for partial instantiation
  CDO<size_t> d_univsPartSavedPos;
  
  //! the last decision level on which partial instantion is called
  CDO<size_t> d_lastPartLevel;
  
  //!useful gterms for matching
  CDList<Expr> d_usefulGterms; 

  //!tracks the position in d_usefulGterms
  CDO<size_t> d_lastUsefulGtermsPos;
  
  //!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;
  CDO<size_t> d_rawUnivsSavedPos;
  //!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

  //! set if the fullEffort = 1
  int d_inEnd; 

  int d_allout; 

  //! 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;
  //!< chache of expressions
  CDMap<Expr, bool> d_contextCache;
  
  //! 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);

  //  CDO<bool> usedup;
  const bool* d_useNew;//!use new way of instantiation
  const bool* d_useLazyInst;//!use lazy instantiation
  const bool* d_useSemMatch;//!use semantic matching
  const bool* d_useAtomSem;
  const bool* d_translate;//!translate only

  const bool* d_useTrigNew;//!use new trig class, to be deleted
  const bool* d_usePart;//!use partial instantiaion
  const bool* d_useMult;//use 
  const bool* d_useInstEnd;
  const bool* d_useInstLCache;
  const bool* d_useInstGCache;
  const bool* d_useInstTrue;
  const bool* d_usePullVar;
  const bool* d_useExprScore;
  const int* d_useTrigLoop;
  const int* d_maxInst;
  //  const int* d_maxUserScore;
  const bool* d_useTrans;
  const bool* d_useTrans2;
  const bool* d_useInstAll;
  const bool* d_usePolarity;
  const bool* d_useEqu;
  const int* d_maxNaiveCall;

  CDO<int> d_curMaxExprScore;

  bool d_useFullTrig;
  bool d_usePartTrig;
  bool d_useMultTrig;

  //ExprMap<std::vector<Expr> > d_arrayIndic; //map array name to a list of indics
  CDMap<Expr, std::vector<Expr> > d_arrayIndic; //map array name to a list of indics
  void arrayIndexName(const Expr& e);

  std::vector<Expr> d_allInsts; //! all instantiations

  int d_initMaxScore;
  int d_offset_multi_trig ;
  
  int d_instThisRound;
  int d_callThisRound;

  int partial_called;

  //  ExprMap<std::vector<Expr> > d_fullTriggers;
  //for multi-triggers, now we only have one set of multi-triggers.


  ExprMap<std::vector<Expr> > d_multTriggers;
  ExprMap<std::vector<Expr> > d_partTriggers;

  ExprMap<std::vector<Trigger> > d_fullTrigs;
  //for multi-triggers, now we only have one set of multi-triggers.
  ExprMap<std::vector<Trigger> > d_multTrigs;
  ExprMap<std::vector<Trigger> > d_partTrigs;

 
  CDO<size_t> d_exprLastUpdatedPos ;//the position of the last expr updated in d_exprUpdate 

  std::map<ExprIndex, int> d_indexScore;

  std::map<ExprIndex, Expr> d_indexExpr;

  int getExprScore(const Expr& e);

  //!the score for a full trigger
  
  ExprMap<bool> d_hasTriggers;
  ExprMap<bool> d_hasMoreBVs;

  int d_trans_num;
  int d_trans2_num;

  typedef struct{
    std::vector<std::vector<size_t> > common_pos;
    std::vector<std::vector<size_t> > var_pos; 
    
    std::vector<CDMap<Expr, bool>* > var_binds_found;

    std::vector<ExprMap<CDList<Expr>* >* > uncomm_list; //
  } multTrigsInfo ;
  
  ExprMap<multTrigsInfo> d_multitrigs_maps;
  std::vector<multTrigsInfo> d_all_multTrigsInfo;
  
  ExprMap<CDList<Expr>* > d_trans_back;
  ExprMap<CDList<Expr>* > d_trans_forw;
  CDMap<Expr,bool > d_trans_found;
  CDMap<Expr,bool > d_trans2_found;


  inline  bool transFound(const Expr& comb);
  
  inline   void setTransFound(const Expr& comb);

  inline  bool trans2Found(const Expr& comb);

  inline  void setTrans2Found(const Expr& comb);

 
  inline  CDList<Expr> & backList(const Expr& ex);
  
  inline  CDList<Expr> & forwList(const Expr& ex);

  CDList<Expr> null_cdlist;


  inline  void  pushBackList(const Expr& node, Expr ex);
  inline  void  pushForwList(const Expr& node, Expr ex);
  
  
  ExprMap<CDList<std::vector<Expr> >* > d_mtrigs_inst; //map expr to bindings
  
  ExprMap<CDList<Expr>* > d_same_head_expr; //map an expr to a list of expres shard the same head
  ExprMap<CDList<Expr>* > d_eq_list; //the equalities list
  
  CDList<Expr > d_eqs; //the equalities list
  CDO<size_t > d_eqs_pos; //the equalities list

  ExprMap<CDO<size_t>* > d_eq_pos;

  ExprMap<CDList<Expr>* > d_parent_list; 
  void  collectChangedTerms(CDList<Expr>& changed_terms);
  ExprMap<std::vector<Expr> > d_mtrigs_bvorder;

  int loc_gterm(const std::vector<Expr>& border,
    const Expr& gterm, 
    int pos);

  void  recSearchCover(const std::vector<Expr>& border,
           const std::vector<Expr>& mtrigs, 
           int cur_depth, 
           std::vector<std::vector<Expr> >& instSet,
           std::vector<Expr>& cur_inst
           );

  void  searchCover(const Expr& thm, 
        const std::vector<Expr>& border,
        std::vector<std::vector<Expr> >& instSet
        );


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

  StatCounter d_allInstCount ;

  CDO<bool> d_partCalled;;

  std::vector<Theorem> d_cacheTheorem;
  size_t d_cacheThmPos;

  void addNotify(const Expr& e);

  int sendInstNew();

  CDMap<Expr, std::set<std::vector<Expr> > > d_instHistory;//the history of instantiations
  //map univ to the trig, gterm and result
  
  ExprMap<CDMap<Expr, bool>* > d_bindHistory; //the history of instantiations

  ExprMap<std::set<std::vector<Expr> > > d_instHistoryGlobal;//the history of instantiations

  
  ExprMap<std::vector<Expr> > d_subTermsMap;
  //std::map<Expr, std::vector<Expr> > d_subTermsMap;
  const std::vector<Expr>& getSubTerms(const Expr& e);

  //ExprMap<int > d_thmTimes; 
  void enqueueInst(const Theorem, const Theorem); 
  void enqueueInst(const Theorem& univ, const std::vector<Expr>& bind, const Expr& gterm);
  void enqueueInst(size_t univ_id , const std::vector<Expr>& bind, const Expr& gterm);
  void enqueueInst(const Theorem& univ, 
       Trigger& trig,
       const std::vector<Expr>& binds,  
       const Expr& gterm
       );
    
  void synCheckSat(ExprMap<ExprMap<std::vector<dynTrig>* >* >& , bool);
  void synCheckSat(bool);
  void semCheckSat(bool);
  void naiveCheckSat(bool);

  bool insted(const Theorem & univ, const std::vector<Expr>& binds);
  void synInst(const Theorem & univ,  const CDList<Expr>& allterms, size_t tBegin);

  void synFullInst(const Theorem & univ,  const CDList<Expr>& allterms, size_t tBegin);

  void arrayHeuristic(const Trigger& trig, size_t univid);
  

  void synNewInst(size_t univ_id, const std::vector<Expr>& binds, const Expr& gterm, const Trigger& trig );
  void synMultInst(const Theorem & univ,  const CDList<Expr>& allterms,  size_t tBegin);

  void synPartInst(const Theorem & univ,  const CDList<Expr>& allterms,  size_t tBegin);

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


  void goodSynMatch(const Expr& e,
        const std::vector<Expr> & boundVars,
        std::vector<std::vector<Expr> >& instBindsTerm,
        std::vector<Expr>& instGterm,
        const CDList<Expr>& allterms,          
        size_t tBegin);
  void goodSynMatchNewTrig(const Trigger& trig,
         const std::vector<Expr> & boundVars,
         std::vector<std::vector<Expr> >& instBinds,
         std::vector<Expr>& instGterms,
         const CDList<Expr>& allterms,           
         size_t tBegin);

  bool goodSynMatchNewTrig(const Trigger& trig,
         const std::vector<Expr> & boundVars,
         std::vector<std::vector<Expr> >& instBinds,
         std::vector<Expr>& instGterms,
         const Expr& gterm);

  void matchListOld(const CDList<Expr>& list, size_t gbegin, size_t gend);
    //  void matchListOld(const Expr& gterm);
  void matchListNew(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs,
        const CDList<Expr>& list,
        size_t gbegin,
        size_t gend);
  
  void delNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs);
  void combineOldNewTrigs(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs);

  void newTopMatch(const Expr& gterm, 
       const Expr& vterm, 
       std::vector<ExprMap<Expr> >& binds, 
       const Trigger& trig);
    

  bool synMatchTopPred(const Expr& gterm, const Trigger trig, ExprMap<Expr>& env);

  inline bool matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);
  inline void matchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& env);
  inline void add_parent(const Expr& parent);

  bool recSynMatch(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);

  bool hasGoodSynInstNewTrigOld(Trigger& trig, 
        std::vector<Expr> & boundVars, 
        std::vector<std::vector<Expr> >& instBinds, 
        std::vector<Expr>& instGterms, 
        const CDList<Expr>& allterms,          
        size_t tBegin); 
  
  bool hasGoodSynInstNewTrig(Trigger& trig, 
           const std::vector<Expr> & boundVars, 
             std::vector<std::vector<Expr> >& instBinds, 
           std::vector<Expr>& instGterms, 
           const CDList<Expr>& allterms,           
           size_t tBegin); 


  bool hasGoodSynMultiInst(const Expr& e,
         std::vector<Expr>& bVars,
         std::vector<std::vector<Expr> >& instSet,
         const CDList<Expr>& allterms,           
         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);

  bool isTransLike (const std::vector<Expr>& cur_trig);
  bool isTrans2Like (const std::vector<Expr>& all_terms, const Expr& tr2);
  

  static const size_t MAX_TRIG_BVS=15;
  Expr d_mybvs[MAX_TRIG_BVS];
 
  Expr recGeneralTrig(const Expr& trig, ExprMap<Expr>& bvs, size_t& mybvs_count);
  Expr generalTrig(const Expr& trig, ExprMap<Expr>& bvs);

  ExprMap<CDMap<Expr, CDList<dynTrig>* >* > d_allmap_trigs;
  
  CDList<Trigger> d_alltrig_list;

  void registerTrig(ExprMap<ExprMap<std::vector<dynTrig>* >* >& cur_trig_map,
       Trigger trig, 
       const std::vector<Expr> thmBVs, 
       size_t univ_id);
    
  void registerTrigReal(Trigger trig, const std::vector<Expr>, size_t univ_id);

  bool canMatch(const Expr& t1, const Expr& t2, ExprMap<Expr>& env);
  void setGround(const Expr& gterm, const Expr& trig, const Theorem& univ, const std::vector<Expr>& subTerms) ;    

  //  std::string getHead(const Expr& e) ;
  void setupTriggers(const Theorem& thm, size_t univ_id);
  void setupTriggers(ExprMap<ExprMap<std::vector<dynTrig>* >*>& trig_maps,
         const Theorem& thm, 
         size_t univs_id);

  void saveContext();


  /*! \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

---