src/theory/quantifiers_engine.h

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Theory instantiator, Instantiation Engine classes
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
  20 #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
  21
  22 #include "theory/theory.h"
  23 #include "util/hash.h"
  24 #include "theory/quantifiers/inst_match.h"
  25 #include "theory/rewriterules/rr_inst_match.h"
  26
  27 #include "util/stats.h"
  28
  29 #include <ext/hash_set>
  30 #include <iostream>
  31 #include <map>
  32
  33 namespace CVC4 {
  34
  35 class TheoryEngine;
  36
  37 namespace theory {
  38
  39 class QuantifiersEngine;
  40
  41 class InstStrategy {
  42 public:
  43   enum Status {
  44     STATUS_UNFINISHED,
  45     STATUS_UNKNOWN,
  46     STATUS_SAT,
  47   };/* enum Status */
  48 protected:
  49   /** reference to the instantiation engine */
  50   QuantifiersEngine* d_quantEngine;
  51 protected:
  52   /** giving priorities */
  53   std::vector< InstStrategy* > d_priority_over;
  54   /** do not instantiate list */
  55   std::vector< Node > d_no_instantiate;
  56   std::vector< Node > d_no_instantiate_temp;
  57   /** reset instantiation */
  58   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
  59   /** process method */
  60   virtual int process( Node f, Theory::Effort effort, int e ) = 0;
  61 public:
  62   InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){}
  63   virtual ~InstStrategy(){}
  64
  65   /** reset instantiation */
  66   void resetInstantiationRound( Theory::Effort effort );
  67   /** do instantiation round method */
  68   int doInstantiation( Node f, Theory::Effort effort, int e );
  69   /** update status */
  70   static void updateStatus( int& currStatus, int addStatus ){
  71     if( addStatus==STATUS_UNFINISHED ){
  72       currStatus = STATUS_UNFINISHED;
  73     }else if( addStatus==STATUS_UNKNOWN ){
  74       if( currStatus==STATUS_SAT ){
  75         currStatus = STATUS_UNKNOWN;
  76       }
  77     }
  78   }
  79   /** identify */
  80   virtual std::string identify() const { return std::string("Unknown"); }
  81 public:
  82   /** set priority */
  83   void setPriorityOver( InstStrategy* is ) { d_priority_over.push_back( is ); }
  84   /** set no instantiate */
  85   void setNoInstantiate( Node n ) { d_no_instantiate.push_back( n ); }
  86   /** should instantiate */
  87   bool shouldInstantiate( Node n ) {
  88     return std::find( d_no_instantiate_temp.begin(), d_no_instantiate_temp.end(), n )==d_no_instantiate_temp.end();
  89   }
  90 };/* class InstStrategy */
  91
  92 class QuantifiersModule {
  93 protected:
  94   QuantifiersEngine* d_quantEngine;
  95 public:
  96   QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
  97   ~QuantifiersModule(){}
  98   //get quantifiers engine
  99   QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
 100   /* Call during check registerQuantifier has already been called */
 101   virtual void check( Theory::Effort e ) = 0;
 102   /* Called for new quantifiers */
 103   virtual void registerQuantifier( Node n ) = 0;
 104   virtual void assertNode( Node n ) = 0;
 105   virtual void propagate( Theory::Effort level ) = 0;
 106   virtual Node explain(TNode n) = 0;
 107 };/* class QuantifiersModule */
 108
 109 namespace quantifiers {
 110   class InstantiationEngine;
 111   class ModelEngine;
 112   class TermDb;
 113   class FirstOrderModel;
 114 }/* CVC4::theory::quantifiers */
 115
 116
 117 class QuantifiersEngine {
 118   friend class quantifiers::InstantiationEngine;
 119   friend class quantifiers::ModelEngine;
 120   friend class inst::InstMatch;
 121 private:
 122   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 123   /** reference to theory engine object */
 124   TheoryEngine* d_te;
 125   /** vector of modules for quantifiers */
 126   std::vector< QuantifiersModule* > d_modules;
 127   /** instantiation engine */
 128   quantifiers::InstantiationEngine* d_inst_engine;
 129   /** model engine */
 130   quantifiers::ModelEngine* d_model_engine;
 131   /** equality query class */
 132   EqualityQuery* d_eq_query;
 133 public:
 134   /** list of all quantifiers (pre-rewrite) */
 135   std::vector< Node > d_quants;
 136   /** list of all quantifiers (post-rewrite) */
 137   std::vector< Node > d_r_quants;
 138   /** map from quantifiers to whether they are active */
 139   BoolMap d_active;
 140   /** lemmas produced */
 141   std::map< Node, bool > d_lemmas_produced;
 142   /** lemmas waiting */
 143   std::vector< Node > d_lemmas_waiting;
 144   /** has added lemma this round */
 145   bool d_hasAddedLemma;
 146   /** inst matches produced for each quantifier */
 147   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
 148   /** owner of quantifiers */
 149   std::map< Node, Theory* > d_owner;
 150   /** term database */
 151   quantifiers::TermDb* d_term_db;
 152   /** extended model object */
 153   quantifiers::FirstOrderModel* d_model;
 154   /** has the model been set? */
 155   bool d_model_set;
 156   /** universal quantifiers that have been rewritten */
 157   std::map< Node, std::vector< Node > > d_quant_rewritten;
 158   /** map from rewritten universal quantifiers to the quantifier they are the consequence of */
 159   std::map< Node, Node > d_rewritten_quant;
 160 private:
 161   /** for computing relavance */
 162   /** map from quantifiers to symbols they contain */
 163   std::map< Node, std::vector< Node > > d_syms;
 164   /** map from symbols to quantifiers */
 165   std::map< Node, std::vector< Node > > d_syms_quants;
 166   /** relevance for quantifiers and symbols */
 167   std::map< Node, int > d_relevance;
 168   /** compute symbols */
 169   void computeSymbols( Node n, std::vector< Node >& syms );
 170 private:
 171   /** helper functions compute phase requirements */
 172   static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs );
 173
 174   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 175
 176 public:
 177   QuantifiersEngine(context::Context* c, TheoryEngine* te);
 178   ~QuantifiersEngine();
 179   /** get instantiator for id */
 180   Instantiator* getInstantiator( theory::TheoryId id );
 181   /** get theory engine */
 182   TheoryEngine* getTheoryEngine() { return d_te; }
 183   /** get equality query object for the given type. The default is the
 184       generic one */
 185   inst::EqualityQuery* getEqualityQuery(TypeNode t);
 186   inst::EqualityQuery* getEqualityQuery() {
 187     return d_eq_query;
 188   }
 189   /** get equality query object for the given type. The default is the
 190       one of UF */
 191   rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t);
 192   rrinst::CandidateGenerator* getRRCanGenClass(TypeNode t);
 193   /* generic candidate generator */
 194   rrinst::CandidateGenerator* getRRCanGenClasses();
 195   rrinst::CandidateGenerator* getRRCanGenClass();
 196   /** get instantiation engine */
 197   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
 198   /** get model engine */
 199   quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
 200   /** get default sat context for quantifiers engine */
 201   context::Context* getSatContext();
 202   /** get default output channel for the quantifiers engine */
 203   OutputChannel& getOutputChannel();
 204   /** get default valuation for the quantifiers engine */
 205   Valuation& getValuation();
 206 public:
 207   /** check at level */
 208   void check( Theory::Effort e );
 209   /** register (non-rewritten) quantifier */
 210   void registerQuantifier( Node f );
 211   /** register (non-rewritten) quantifier */
 212   void registerPattern( std::vector<Node> & pattern);
 213   /** assert (universal) quantifier */
 214   void assertNode( Node f );
 215   /** propagate */
 216   void propagate( Theory::Effort level );
 217   /** reset instantiation round */
 218   void resetInstantiationRound( Theory::Effort level );
 219
 220   //create inst variable
 221   std::vector<Node> createInstVariable( std::vector<Node> & vars );
 222 public:
 223   /** add lemma lem */
 224   bool addLemma( Node lem );
 225   /** instantiate f with arguments terms */
 226   bool addInstantiation( Node f, std::vector< Node >& terms );
 227   /** do instantiation specified by m */
 228   bool addInstantiation( Node f, InstMatch& m );
 229   /** split on node n */
 230   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
 231   /** add split equality */
 232   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
 233   /** has added lemma */
 234   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
 235   /** flush lemmas */
 236   void flushLemmas( OutputChannel* out );
 237   /** get number of waiting lemmas */
 238   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
 239 public:
 240   /** get number of quantifiers */
 241   int getNumQuantifiers() { return (int)d_quants.size(); }
 242   /** get quantifier */
 243   Node getQuantifier( int i ) { return d_quants[i]; }
 244   /** set active */
 245   void setActive( Node n, bool val ) { d_active[n] = val; }
 246   /** get active */
 247   bool getActive( Node n ) { return d_active.find( n )!=d_active.end() && d_active[n]; }
 248 public:
 249   /** phase requirements for each quantifier for each instantiation literal */
 250   std::map< Node, std::map< Node, bool > > d_phase_reqs;
 251   std::map< Node, std::map< Node, bool > > d_phase_reqs_equality;
 252   std::map< Node, std::map< Node, Node > > d_phase_reqs_equality_term;
 253 public:
 254   /** is phase required */
 255   bool isPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )!=d_phase_reqs[f].end(); }
 256   /** get phase requirement */
 257   bool getPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )==d_phase_reqs[f].end() ? false : d_phase_reqs[f][ lit ]; }
 258   /** get term req terms */
 259   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
 260   /** helper functions compute phase requirements */
 261   static void computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs );
 262   /** compute phase requirements */
 263   void generatePhaseReqs( Node f, Node n );
 264 public:
 265   /** has owner */
 266   bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); }
 267   /** get owner */
 268   Theory* getOwner( Node f ) { return d_owner[f]; }
 269   /** set owner */
 270   void setOwner( Node f, Theory* t ) { d_owner[f] = t; }
 271 public:
 272   /** get model */
 273   quantifiers::FirstOrderModel* getModel() { return d_model; }
 274   /** get term database */
 275   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
 276   /** add term to database */
 277   void addTermToDatabase( Node n, bool withinQuant = false );
 278 private:
 279   /** set relevance */
 280   void setRelevance( Node s, int r );
 281 public:
 282   /** get relevance */
 283   int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }
 284   /** get number of quantifiers for symbol s */
 285   int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }
 286 public:
 287   /** statistics class */
 288   class Statistics {
 289   public:
 290     IntStat d_num_quant;
 291     IntStat d_instantiation_rounds;
 292     IntStat d_instantiation_rounds_lc;
 293     IntStat d_instantiations;
 294     IntStat d_max_instantiation_level;
 295     IntStat d_splits;
 296     IntStat d_total_inst_var;
 297     IntStat d_total_inst_var_unspec;
 298     IntStat d_inst_unspec;
 299     IntStat d_inst_duplicate;
 300     IntStat d_lit_phase_req;
 301     IntStat d_lit_phase_nreq;
 302     IntStat d_triggers;
 303     IntStat d_simple_triggers;
 304     IntStat d_multi_triggers;
 305     IntStat d_multi_trigger_instantiations;
 306     IntStat d_term_in_termdb;
 307     IntStat d_num_mono_candidates;
 308     IntStat d_num_mono_candidates_new_term;
 309     IntStat d_num_multi_candidates;
 310     IntStat d_mono_candidates_cache_hit;
 311     IntStat d_mono_candidates_cache_miss;
 312     IntStat d_multi_candidates_cache_hit;
 313     IntStat d_multi_candidates_cache_miss;
 314     Statistics();
 315     ~Statistics();
 316   };/* class QuantifiersEngine::Statistics */
 317   Statistics d_statistics;
 318 public:
 319   /** options */
 320   bool d_optInstCheckDuplicate;
 321   bool d_optInstMakeRepresentative;
 322   bool d_optInstAddSplits;
 323   bool d_optMatchIgnoreModelBasis;
 324   bool d_optInstLimitActive;
 325   int d_optInstLimit;
 326 };/* class QuantifiersEngine */
 327
 328
 329
 330 /** equality query object using theory engine */
 331 class EqualityQueryQuantifiersEngine : public EqualityQuery
 332 {
 333 private:
 334   /** pointer to theory engine */
 335   QuantifiersEngine* d_qe;
 336 public:
 337   EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ){}
 338   ~EqualityQueryQuantifiersEngine(){}
 339   /** general queries about equality */
 340   bool hasTerm( Node a );
 341   Node getRepresentative( Node a );
 342   bool areEqual( Node a, Node b );
 343   bool areDisequal( Node a, Node b );
 344   Node getInternalRepresentative( Node a );
 345   eq::EqualityEngine* getEngine();
 346   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
 347 }; /* EqualityQueryQuantifiersEngine */
 348
 349 }/* CVC4::theory namespace */
 350 }/* CVC4 namespace */
 351
 352 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */