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