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-2014  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 namespace quantifiers {
  41   class TermDb;
  42 }
  43
  44 class QuantifiersModule {
  45 protected:
  46   QuantifiersEngine* d_quantEngine;
  47 public:
  48   QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
  49   virtual ~QuantifiersModule(){}
  50   //get quantifiers engine
  51   QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
  52   /** initialize */
  53   virtual void finishInit() {}
  54   /* whether this module needs to check this round */
  55   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
  56   /* reset at a round */
  57   virtual void reset_round( Theory::Effort e ){}
  58   /* Call during quantifier engine's check */
  59   virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
  60   /* Called for new quantifiers */
  61   virtual void registerQuantifier( Node q ) = 0;
  62   virtual void assertNode( Node n ) = 0;
  63   virtual void propagate( Theory::Effort level ){}
  64   virtual Node getNextDecisionRequest() { return TNode::null(); }
  65   virtual Node explain(TNode n) { return TNode::null(); }
  66   /** Identify this module (for debugging, dynamic configuration, etc..) */
  67   virtual std::string identify() const = 0;
  68 public:
  69   eq::EqualityEngine * getEqualityEngine();
  70   bool areDisequal( TNode n1, TNode n2 );
  71   bool areEqual( TNode n1, TNode n2 );
  72   TNode getRepresentative( TNode n );
  73   quantifiers::TermDb * getTermDatabase();
  74 };/* class QuantifiersModule */
  75
  76 namespace quantifiers {
  77   class FirstOrderModel;
  78   //modules
  79   class InstantiationEngine;
  80   class ModelEngine;
  81   class BoundedIntegers;
  82   class QuantConflictFind;
  83   class RewriteEngine;
  84   class RelevantDomain;
  85   class ConjectureGenerator;
  86   class CegInstantiation;
  87 }/* CVC4::theory::quantifiers */
  88
  89 namespace inst {
  90   class TriggerTrie;
  91 }/* CVC4::theory::inst */
  92
  93 //class EfficientEMatcher;
  94 class EqualityQueryQuantifiersEngine;
  95
  96 class QuantifiersEngine {
  97   friend class quantifiers::InstantiationEngine;
  98   friend class quantifiers::ModelEngine;
  99   friend class quantifiers::RewriteEngine;
 100   friend class quantifiers::QuantConflictFind;
 101   friend class inst::InstMatch;
 102 private:
 103   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 104   /** reference to theory engine object */
 105   TheoryEngine* d_te;
 106   /** vector of modules for quantifiers */
 107   std::vector< QuantifiersModule* > d_modules;
 108   /** equality query class */
 109   EqualityQueryQuantifiersEngine* d_eq_query;
 110   /** for computing relevance of quantifiers */
 111   QuantRelevance * d_quant_rel;
 112   /** relevant domain */
 113   quantifiers::RelevantDomain* d_rel_dom;
 114   /** phase requirements for each quantifier for each instantiation literal */
 115   std::map< Node, QuantPhaseReq* > d_phase_reqs;
 116   /** instantiation engine */
 117   quantifiers::InstantiationEngine* d_inst_engine;
 118   /** model engine */
 119   quantifiers::ModelEngine* d_model_engine;
 120   /** bounded integers utility */
 121   quantifiers::BoundedIntegers * d_bint;
 122   /** Conflict find mechanism for quantifiers */
 123   quantifiers::QuantConflictFind* d_qcf;
 124   /** rewrite rules utility */
 125   quantifiers::RewriteEngine * d_rr_engine;
 126   /** subgoal generator */
 127   quantifiers::ConjectureGenerator * d_sg_gen;
 128   /** ceg instantiation */
 129   quantifiers::CegInstantiation * d_ceg_inst;
 130 public: //effort levels
 131   enum {
 132     QEFFORT_CONFLICT,
 133     QEFFORT_STANDARD,
 134     QEFFORT_MODEL,
 135   };
 136 private:
 137   /** list of all quantifiers seen */
 138   std::vector< Node > d_quants;
 139   /** list of all lemmas produced */
 140   //std::map< Node, bool > d_lemmas_produced;
 141   BoolMap d_lemmas_produced_c;
 142   /** lemmas waiting */
 143   std::vector< Node > d_lemmas_waiting;
 144   /** phase requirements waiting */
 145   std::map< Node, bool > d_phase_req_waiting;
 146   /** has added lemma this round */
 147   bool d_hasAddedLemma;
 148   /** has a conflict been found */
 149   bool d_conflict;
 150   /** list of all instantiations produced for each quantifier */
 151   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
 152   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
 153   /** quantifiers that have been skolemized */
 154   std::map< Node, bool > d_skolemized;
 155   /** term database */
 156   quantifiers::TermDb* d_term_db;
 157   /** all triggers will be stored in this trie */
 158   inst::TriggerTrie* d_tr_trie;
 159   /** extended model object */
 160   quantifiers::FirstOrderModel* d_model;
 161   /** statistics for debugging */
 162   std::map< Node, int > d_total_inst_debug;
 163   std::map< Node, int > d_temp_inst_debug;
 164   int d_total_inst_count_debug;
 165 private:
 166   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 167 public:
 168   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
 169   ~QuantifiersEngine();
 170   /** get theory engine */
 171   TheoryEngine* getTheoryEngine() { return d_te; }
 172   /** get equality query object for the given type. The default is the
 173       generic one */
 174   EqualityQueryQuantifiersEngine* getEqualityQuery();
 175   /** get default sat context for quantifiers engine */
 176   context::Context* getSatContext();
 177   /** get default sat context for quantifiers engine */
 178   context::Context* getUserContext();
 179   /** get default output channel for the quantifiers engine */
 180   OutputChannel& getOutputChannel();
 181   /** get default valuation for the quantifiers engine */
 182   Valuation& getValuation();
 183   /** get relevant domain */
 184   quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
 185   /** get quantifier relevance */
 186   QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
 187   /** get phase requirement information */
 188   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
 189   /** get phase requirement terms */
 190   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
 191 public:  //modules
 192   /** get instantiation engine */
 193   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
 194   /** get model engine */
 195   quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
 196   /** get bounded integers utility */
 197   quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
 198   /** Conflict find mechanism for quantifiers */
 199   quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
 200   /** rewrite rules utility */
 201   quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
 202   /** subgoal generator */
 203   quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
 204   /** ceg instantiation */
 205   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
 206 private:
 207   /** owner of quantified formulas */
 208   std::map< Node, QuantifiersModule * > d_owner;
 209 public:
 210   /** get owner */
 211   QuantifiersModule * getOwner( Node q );
 212   /** set owner */
 213   void setOwner( Node q, QuantifiersModule * m );
 214   /** considers */
 215   bool hasOwnership( Node q, QuantifiersModule * m = NULL );
 216 public:
 217   /** initialize */
 218   void finishInit();
 219   /** check at level */
 220   void check( Theory::Effort e );
 221   /** register quantifier */
 222   void registerQuantifier( Node f );
 223   /** register quantifier */
 224   void registerPattern( std::vector<Node> & pattern);
 225   /** assert universal quantifier */
 226   void assertQuantifier( Node q, bool pol );
 227   /** propagate */
 228   void propagate( Theory::Effort level );
 229   /** get next decision request */
 230   Node getNextDecisionRequest();
 231 private:
 232   /** compute term vector */
 233   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
 234   /** instantiate f with arguments terms */
 235   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
 236   /** set instantiation level attr */
 237   static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
 238   /** flush lemmas */
 239   void flushLemmas();
 240 public:
 241   /** get instantiation */
 242   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
 243   /** get instantiation */
 244   Node getInstantiation( Node f, InstMatch& m );
 245   /** get instantiation */
 246   Node getInstantiation( Node f, std::vector< Node >& terms );
 247   /** do substitution */
 248   Node getSubstitute( Node n, std::vector< Node >& terms );
 249   /** exist instantiation ? */
 250   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
 251   /** add lemma lem */
 252   bool addLemma( Node lem, bool doCache = true );
 253   /** add require phase */
 254   void addRequirePhase( Node lit, bool req );
 255   /** do instantiation specified by m */
 256   bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
 257   /** add instantiation */
 258   bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false );
 259   /** split on node n */
 260   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
 261   /** add split equality */
 262   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
 263   /** has added lemma */
 264   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
 265   /** get number of waiting lemmas */
 266   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
 267   /** set instantiation level attr */
 268   static void setInstantiationLevelAttr( Node n, uint64_t level );
 269   /** is term eligble for instantiation? */
 270   bool isTermEligibleForInstantiation( Node n, Node f, bool print = false );
 271 public:
 272   /** get number of quantifiers */
 273   int getNumQuantifiers() { return (int)d_quants.size(); }
 274   /** get quantifier */
 275   Node getQuantifier( int i ) { return d_quants[i]; }
 276 public:
 277   /** get model */
 278   quantifiers::FirstOrderModel* getModel() { return d_model; }
 279   /** get term database */
 280   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
 281   /** get trigger database */
 282   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
 283   /** add term to database */
 284   void addTermToDatabase( Node n, bool withinQuant = false );
 285   /** get the master equality engine */
 286   eq::EqualityEngine* getMasterEqualityEngine() ;
 287 public:
 288   /** print instantiations */
 289   void printInstantiations( std::ostream& out );
 290   /** statistics class */
 291   class Statistics {
 292   public:
 293     IntStat d_num_quant;
 294     IntStat d_instantiation_rounds;
 295     IntStat d_instantiation_rounds_lc;
 296     IntStat d_instantiations;
 297     IntStat d_inst_duplicate;
 298     IntStat d_inst_duplicate_eq;
 299     IntStat d_lit_phase_req;
 300     IntStat d_lit_phase_nreq;
 301     IntStat d_triggers;
 302     IntStat d_simple_triggers;
 303     IntStat d_multi_triggers;
 304     IntStat d_multi_trigger_instantiations;
 305     Statistics();
 306     ~Statistics();
 307   };/* class QuantifiersEngine::Statistics */
 308   Statistics d_statistics;
 309 };/* class QuantifiersEngine */
 310
 311
 312
 313 /** equality query object using theory engine */
 314 class EqualityQueryQuantifiersEngine : public EqualityQuery
 315 {
 316 private:
 317   /** pointer to theory engine */
 318   QuantifiersEngine* d_qe;
 319   /** internal representatives */
 320   std::map< Node, Node > d_int_rep;
 321   /** rep score */
 322   std::map< Node, int > d_rep_score;
 323   /** reset count */
 324   int d_reset_count;
 325
 326   bool d_liberal;
 327 private:
 328   /** node contains */
 329   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
 330   /** get score */
 331   int getRepScore( Node n, Node f, int index );
 332 public:
 333   EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
 334   ~EqualityQueryQuantifiersEngine(){}
 335   /** reset */
 336   void reset();
 337   /** general queries about equality */
 338   bool hasTerm( Node a );
 339   Node getRepresentative( Node a );
 340   bool areEqual( Node a, Node b );
 341   bool areDisequal( Node a, Node b );
 342   eq::EqualityEngine* getEngine();
 343   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
 344   /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
 345       If cbqi is active, this will return a term in the equivalence class of "a" that does
 346       not contain instantiation constants, if such a term exists.
 347    */
 348   Node getInternalRepresentative( Node a, Node f, int index );
 349   /** flatten representatives */
 350   void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 351
 352   void setLiberal( bool l ) { d_liberal = l; }
 353 }; /* EqualityQueryQuantifiersEngine */
 354
 355 }/* CVC4::theory namespace */
 356 }/* CVC4 namespace */
 357
 358 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */