src/theory/quantifiers_engine.h

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