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): mdeters, bobot
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Theory instantiator, Instantiation Engine classes
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
  18 #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
  19
  20 #include "theory/theory.h"
  21 #include "util/hash.h"
  22 #include "theory/quantifiers/inst_match.h"
  23 #include "theory/rewriterules/rr_inst_match.h"
  24 #include "theory/quantifiers/quant_util.h"
  25
  26 #include "util/statistics_registry.h"
  27
  28 #include <ext/hash_set>
  29 #include <iostream>
  30 #include <map>
  31
  32 namespace CVC4 {
  33
  34 class TheoryEngine;
  35
  36 namespace theory {
  37
  38 class QuantifiersEngine;
  39
  40 class QuantifiersModule {
  41 protected:
  42   QuantifiersEngine* d_quantEngine;
  43 public:
  44   QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
  45   virtual ~QuantifiersModule(){}
  46   //get quantifiers engine
  47   QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
  48   /* whether this module needs to check this round */
  49   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
  50   /* Call during quantifier engine's check */
  51   virtual void check( Theory::Effort e ) = 0;
  52   /* Called for new quantifiers */
  53   virtual void registerQuantifier( Node n ) = 0;
  54   virtual void assertNode( Node n ) = 0;
  55   virtual void propagate( Theory::Effort level ){}
  56   virtual Node getNextDecisionRequest() { return TNode::null(); }
  57   virtual Node explain(TNode n) = 0;
  58 };/* class QuantifiersModule */
  59
  60 namespace quantifiers {
  61   class InstantiationEngine;
  62   class ModelEngine;
  63   class TermDb;
  64   class FirstOrderModel;
  65 }/* CVC4::theory::quantifiers */
  66
  67 namespace inst {
  68   class TriggerTrie;
  69 }/* CVC4::theory::inst */
  70
  71 namespace rrinst {
  72   class TriggerTrie;
  73 }/* CVC4::theory::inst */
  74
  75 class EfficientEMatcher;
  76 class EqualityQueryQuantifiersEngine;
  77
  78 class QuantifiersEngine {
  79   friend class quantifiers::InstantiationEngine;
  80   friend class quantifiers::ModelEngine;
  81   friend class inst::InstMatch;
  82 private:
  83   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
  84   /** reference to theory engine object */
  85   TheoryEngine* d_te;
  86   /** vector of modules for quantifiers */
  87   std::vector< QuantifiersModule* > d_modules;
  88   /** instantiation engine */
  89   quantifiers::InstantiationEngine* d_inst_engine;
  90   /** model engine */
  91   quantifiers::ModelEngine* d_model_engine;
  92   /** equality query class */
  93   EqualityQueryQuantifiersEngine* d_eq_query;
  94   /** for computing relevance of quantifiers */
  95   QuantRelevance d_quant_rel;
  96   /** phase requirements for each quantifier for each instantiation literal */
  97   std::map< Node, QuantPhaseReq* > d_phase_reqs;
  98   /** efficient e-matcher */
  99   EfficientEMatcher* d_eem;
 100 private:
 101   /** list of all quantifiers seen */
 102   std::vector< Node > d_quants;
 103   /** list of all lemmas produced */
 104   std::map< Node, bool > d_lemmas_produced;
 105   /** lemmas waiting */
 106   std::vector< Node > d_lemmas_waiting;
 107   /** has added lemma this round */
 108   bool d_hasAddedLemma;
 109   /** list of all instantiations produced for each quantifier */
 110   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
 111   /** term database */
 112   quantifiers::TermDb* d_term_db;
 113   /** all triggers will be stored in this trie */
 114   inst::TriggerTrie* d_tr_trie;
 115   /** all triggers for rewrite rules will be stored in this trie */
 116   rrinst::TriggerTrie* d_rr_tr_trie;
 117   /** extended model object */
 118   quantifiers::FirstOrderModel* d_model;
 119 private:
 120   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 121 public:
 122   QuantifiersEngine(context::Context* c, TheoryEngine* te);
 123   ~QuantifiersEngine();
 124   /** get instantiator for id */
 125   Instantiator* getInstantiator( theory::TheoryId id );
 126   /** get theory engine */
 127   TheoryEngine* getTheoryEngine() { return d_te; }
 128   /** get equality query object for the given type. The default is the
 129       generic one */
 130   EqualityQuery* getEqualityQuery();
 131   /** get instantiation engine */
 132   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
 133   /** get model engine */
 134   quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
 135   /** get default sat context for quantifiers engine */
 136   context::Context* getSatContext();
 137   /** get default output channel for the quantifiers engine */
 138   OutputChannel& getOutputChannel();
 139   /** get default valuation for the quantifiers engine */
 140   Valuation& getValuation();
 141   /** get quantifier relevance */
 142   QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; }
 143   /** get phase requirement information */
 144   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
 145   /** get phase requirement terms */
 146   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
 147   /** get efficient e-matching utility */
 148   EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
 149 public:
 150   /** check at level */
 151   void check( Theory::Effort e );
 152   /** register quantifier */
 153   void registerQuantifier( Node f );
 154   /** register quantifier */
 155   void registerPattern( std::vector<Node> & pattern);
 156   /** assert universal quantifier */
 157   void assertNode( Node f );
 158   /** propagate */
 159   void propagate( Theory::Effort level );
 160   /** get next decision request */
 161   Node getNextDecisionRequest();
 162 private:
 163   /** compute term vector */
 164   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
 165   /** instantiate f with arguments terms */
 166   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
 167   /** set instantiation level attr */
 168   void setInstantiationLevelAttr( Node n, uint64_t level );
 169 public:
 170   /** get instantiation */
 171   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
 172   /** get instantiation */
 173   Node getInstantiation( Node f, InstMatch& m );
 174   /** exist instantiation ? */
 175   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
 176   /** add lemma lem */
 177   bool addLemma( Node lem );
 178   /** do instantiation specified by m */
 179   bool addInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false, bool mkRep = true );
 180   /** split on node n */
 181   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
 182   /** add split equality */
 183   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
 184   /** has added lemma */
 185   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
 186   /** flush lemmas */
 187   void flushLemmas( OutputChannel* out );
 188   /** get number of waiting lemmas */
 189   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
 190 public:
 191   /** get number of quantifiers */
 192   int getNumQuantifiers() { return (int)d_quants.size(); }
 193   /** get quantifier */
 194   Node getQuantifier( int i ) { return d_quants[i]; }
 195 public:
 196   /** get model */
 197   quantifiers::FirstOrderModel* getModel() { return d_model; }
 198   /** get term database */
 199   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
 200   /** get trigger database */
 201   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
 202   /** get rewrite trigger database */
 203   rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
 204   /** add term to database */
 205   void addTermToDatabase( Node n, bool withinQuant = false );
 206 public:
 207   /** statistics class */
 208   class Statistics {
 209   public:
 210     IntStat d_num_quant;
 211     IntStat d_instantiation_rounds;
 212     IntStat d_instantiation_rounds_lc;
 213     IntStat d_instantiations;
 214     IntStat d_max_instantiation_level;
 215     IntStat d_splits;
 216     IntStat d_total_inst_var;
 217     IntStat d_total_inst_var_unspec;
 218     IntStat d_inst_unspec;
 219     IntStat d_inst_duplicate;
 220     IntStat d_lit_phase_req;
 221     IntStat d_lit_phase_nreq;
 222     IntStat d_triggers;
 223     IntStat d_simple_triggers;
 224     IntStat d_multi_triggers;
 225     IntStat d_multi_trigger_instantiations;
 226     IntStat d_term_in_termdb;
 227     IntStat d_num_mono_candidates;
 228     IntStat d_num_mono_candidates_new_term;
 229     IntStat d_num_multi_candidates;
 230     IntStat d_mono_candidates_cache_hit;
 231     IntStat d_mono_candidates_cache_miss;
 232     IntStat d_multi_candidates_cache_hit;
 233     IntStat d_multi_candidates_cache_miss;
 234     Statistics();
 235     ~Statistics();
 236   };/* class QuantifiersEngine::Statistics */
 237   Statistics d_statistics;
 238 public:
 239   /** options */
 240   bool d_optInstCheckDuplicate;
 241   bool d_optInstMakeRepresentative;
 242   bool d_optInstAddSplits;
 243   bool d_optMatchIgnoreModelBasis;
 244   bool d_optInstLimitActive;
 245   int d_optInstLimit;
 246 };/* class QuantifiersEngine */
 247
 248
 249
 250 /** equality query object using theory engine */
 251 class EqualityQueryQuantifiersEngine : public EqualityQuery
 252 {
 253 private:
 254   /** pointer to theory engine */
 255   QuantifiersEngine* d_qe;
 256   /** internal representatives */
 257   std::map< Node, Node > d_int_rep;
 258   /** rep score */
 259   std::map< Node, int > d_rep_score;
 260   /** reset count */
 261   int d_reset_count;
 262 private:
 263   /** node contains */
 264   Node getInstance( Node n, std::vector< Node >& eqc );
 265   /** get score */
 266   int getRepScore( Node n );
 267 public:
 268   EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
 269   ~EqualityQueryQuantifiersEngine(){}
 270   /** reset */
 271   void reset();
 272   /** general queries about equality */
 273   bool hasTerm( Node a );
 274   Node getRepresentative( Node a );
 275   bool areEqual( Node a, Node b );
 276   bool areDisequal( Node a, Node b );
 277   eq::EqualityEngine* getEngine();
 278   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
 279   /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
 280       If cbqi is active, this will return a term in the equivalence class of "a" that does
 281       not contain instantiation constants, if such a term exists.
 282    */
 283   Node getInternalRepresentative( Node a );
 284 }; /* EqualityQueryQuantifiersEngine */
 285
 286 }/* CVC4::theory namespace */
 287 }/* CVC4 namespace */
 288
 289 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */