src/theory/quantifiers_engine.h

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 <iostream>
  21 #include <map>
  22 #include <unordered_map>
  23
  24 #include "context/cdchunk_list.h"
  25 #include "context/cdhashset.h"
  26 #include "expr/attribute.h"
  27 #include "options/quantifiers_modes.h"
  28 #include "theory/quantifiers/inst_match.h"
  29 #include "theory/quantifiers/quant_util.h"
  30 #include "theory/theory.h"
  31 #include "util/hash.h"
  32 #include "util/statistics_registry.h"
  33
  34 namespace CVC4 {
  35
  36 class TheoryEngine;
  37
  38 namespace theory {
  39
  40 class QuantifiersEngine;
  41
  42 class InstantiationNotify {
  43 public:
  44   InstantiationNotify(){}
  45   virtual ~InstantiationNotify() {}
  46   virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
  47   virtual void filterInstantiations() = 0;
  48 };
  49
  50 namespace quantifiers {
  51   class TermDb;
  52   class TermDbSygus;
  53   class FirstOrderModel;
  54   //modules
  55   class InstantiationEngine;
  56   class ModelEngine;
  57   class BoundedIntegers;
  58   class QuantConflictFind;
  59   class RewriteEngine;
  60   class RelevantDomain;
  61   class QModelBuilder;
  62   class ConjectureGenerator;
  63   class CegInstantiation;
  64   class LtePartialInst;
  65   class AlphaEquivalence;
  66   class FunDefEngine;
  67   class QuantEqualityEngine;
  68   class FullSaturation;
  69   class InstStrategyCbqi;
  70   class InstStrategyCegqi;
  71   class QuantDSplit;
  72   class QuantAntiSkolem;
  73   class EqualityInference;
  74   class InstPropagator;
  75 }/* CVC4::theory::quantifiers */
  76
  77 namespace inst {
  78   class TriggerTrie;
  79 }/* CVC4::theory::inst */
  80
  81 //class EfficientEMatcher;
  82 class EqualityQueryQuantifiersEngine;
  83
  84 class QuantifiersEngine {
  85   friend class quantifiers::InstantiationEngine;
  86   friend class quantifiers::InstStrategyCbqi;
  87   friend class quantifiers::InstStrategyCegqi;
  88   friend class quantifiers::ModelEngine;
  89   friend class quantifiers::RewriteEngine;
  90   friend class quantifiers::QuantConflictFind;
  91   friend class inst::InstMatch;
  92   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
  93   typedef context::CDChunkList<Node> NodeList;
  94   typedef context::CDChunkList<bool> BoolList;
  95   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  96 private:
  97   /** reference to theory engine object */
  98   TheoryEngine* d_te;
  99   /** vector of utilities for quantifiers */
 100   std::vector< QuantifiersUtil* > d_util;
 101   /** vector of modules for quantifiers */
 102   std::vector< QuantifiersModule* > d_modules;
 103   /** instantiation notify */
 104   std::vector< InstantiationNotify* > d_inst_notify;
 105   /** equality query class */
 106   EqualityQueryQuantifiersEngine* d_eq_query;
 107   /** for computing relevance of quantifiers */
 108   QuantRelevance * d_quant_rel;
 109   /** relevant domain */
 110   quantifiers::RelevantDomain* d_rel_dom;
 111   /** alpha equivalence */
 112   quantifiers::AlphaEquivalence * d_alpha_equiv;
 113   /** model builder */
 114   quantifiers::QModelBuilder* d_builder;
 115   /** utility for effectively propositional logic */
 116   QuantEPR * d_qepr;
 117 private:
 118   /** instantiation engine */
 119   quantifiers::InstantiationEngine* d_inst_engine;
 120   /** model engine */
 121   quantifiers::ModelEngine* d_model_engine;
 122   /** bounded integers utility */
 123   quantifiers::BoundedIntegers * d_bint;
 124   /** Conflict find mechanism for quantifiers */
 125   quantifiers::QuantConflictFind* d_qcf;
 126   /** rewrite rules utility */
 127   quantifiers::RewriteEngine * d_rr_engine;
 128   /** subgoal generator */
 129   quantifiers::ConjectureGenerator * d_sg_gen;
 130   /** ceg instantiation */
 131   quantifiers::CegInstantiation * d_ceg_inst;
 132   /** lte partial instantiation */
 133   quantifiers::LtePartialInst * d_lte_part_inst;
 134   /** function definitions engine */
 135   quantifiers::FunDefEngine * d_fun_def_engine;
 136   /** quantifiers equality engine */
 137   quantifiers::QuantEqualityEngine * d_uee;
 138   /** full saturation */
 139   quantifiers::FullSaturation * d_fs;
 140   /** counterexample-based quantifier instantiation */
 141   quantifiers::InstStrategyCbqi * d_i_cbqi;
 142   /** quantifiers splitting */
 143   quantifiers::QuantDSplit * d_qsplit;
 144   /** quantifiers anti-skolemization */
 145   quantifiers::QuantAntiSkolem * d_anti_skolem;
 146   /** quantifiers instantiation propagtor */
 147   quantifiers::InstPropagator * d_inst_prop;
 148 public: //effort levels
 149   enum {
 150     QEFFORT_CONFLICT,
 151     QEFFORT_STANDARD,
 152     QEFFORT_MODEL,
 153     QEFFORT_LAST_CALL,
 154     //none
 155     QEFFORT_NONE,
 156   };
 157 private:  //this information is reset during check
 158   /** current effort level */
 159   unsigned d_curr_effort_level;
 160   /** are we in conflict */
 161   bool d_conflict;
 162   context::CDO< bool > d_conflict_c;
 163   /** has added lemma this round */
 164   bool d_hasAddedLemma;
 165   /** whether to use model equality engine */
 166   bool d_useModelEe;
 167 private:
 168   /** list of all quantifiers seen */
 169   std::map< Node, bool > d_quants;
 170   /** quantifiers reduced */
 171   BoolMap d_quants_red;
 172   std::map< Node, Node > d_quants_red_lem;
 173   /** list of all lemmas produced */
 174   //std::map< Node, bool > d_lemmas_produced;
 175   BoolMap d_lemmas_produced_c;
 176   /** lemmas waiting */
 177   std::vector< Node > d_lemmas_waiting;
 178   /** phase requirements waiting */
 179   std::map< Node, bool > d_phase_req_waiting;
 180   /** list of all instantiations produced for each quantifier */
 181   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
 182   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
 183   /** recorded instantiations */
 184   std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
 185   /** quantifiers that have been skolemized */
 186   BoolMap d_skolemized;
 187   /** term database */
 188   quantifiers::TermDb* d_term_db;
 189   /** all triggers will be stored in this trie */
 190   inst::TriggerTrie* d_tr_trie;
 191   /** extended model object */
 192   quantifiers::FirstOrderModel* d_model;
 193   /** statistics for debugging */
 194   std::map< Node, int > d_total_inst_debug;
 195   std::map< Node, int > d_temp_inst_debug;
 196   int d_total_inst_count_debug;
 197   /** inst round counters TODO: make context-dependent? */
 198   context::CDO< int > d_ierCounter_c;
 199   int d_ierCounter;
 200   int d_ierCounter_lc;
 201   int d_ierCounterLastLc;
 202   int d_inst_when_phase;
 203   /** has presolve been called */
 204   context::CDO< bool > d_presolve;
 205   /** presolve cache */
 206   NodeSet d_presolve_in;
 207   NodeList d_presolve_cache;
 208   BoolList d_presolve_cache_wq;
 209   BoolList d_presolve_cache_wic;
 210
 211 public:
 212   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
 213   ~QuantifiersEngine();
 214   /** get theory engine */
 215   TheoryEngine* getTheoryEngine() { return d_te; }
 216   /** get equality query */
 217   EqualityQueryQuantifiersEngine* getEqualityQuery();
 218   /** get default sat context for quantifiers engine */
 219   context::Context* getSatContext();
 220   /** get default sat context for quantifiers engine */
 221   context::UserContext* getUserContext();
 222   /** get default output channel for the quantifiers engine */
 223   OutputChannel& getOutputChannel();
 224   /** get default valuation for the quantifiers engine */
 225   Valuation& getValuation();
 226   /** get relevant domain */
 227   quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
 228   /** get quantifier relevance */
 229   QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
 230   /** get the model builder */
 231   quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
 232   /** get utility for EPR */
 233   QuantEPR* getQuantEPR() { return d_qepr; }
 234 public:  //modules
 235   /** get instantiation engine */
 236   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
 237   /** get model engine */
 238   quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
 239   /** get bounded integers utility */
 240   quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
 241   /** Conflict find mechanism for quantifiers */
 242   quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
 243   /** rewrite rules utility */
 244   quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
 245   /** subgoal generator */
 246   quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
 247   /** ceg instantiation */
 248   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
 249   /** local theory ext partial inst */
 250   quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
 251   /** function definition engine */
 252   quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
 253   /** quantifiers equality engine */
 254   quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
 255   /** get full saturation */
 256   quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
 257   /** get inst strategy cbqi */
 258   quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
 259   /** get quantifiers splitting */
 260   quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
 261   /** get quantifiers anti-skolemization */
 262   quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
 263 private:
 264   /** owner of quantified formulas */
 265   std::map< Node, QuantifiersModule * > d_owner;
 266   std::map< Node, int > d_owner_priority;
 267 public:
 268   /** get owner */
 269   QuantifiersModule * getOwner( Node q );
 270   /** set owner */
 271   void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
 272   /** considers */
 273   bool hasOwnership( Node q, QuantifiersModule * m = NULL );
 274   /** is finite bound */
 275   bool isFiniteBound( Node q, Node v );
 276 public:
 277   /** initialize */
 278   void finishInit();
 279   /** presolve */
 280   void presolve();
 281   /** notify preprocessed assertion */
 282   void ppNotifyAssertions(const std::vector<Node>& assertions);
 283   /** check at level */
 284   void check( Theory::Effort e );
 285   /** notify that theories were combined */
 286   void notifyCombineTheories();
 287   /** register quantifier */
 288   bool registerQuantifier( Node f );
 289   /** register quantifier */
 290   void registerPattern( std::vector<Node> & pattern);
 291   /** assert universal quantifier */
 292   void assertQuantifier( Node q, bool pol );
 293   /** propagate */
 294   void propagate( Theory::Effort level );
 295   /** get next decision request */
 296   Node getNextDecisionRequest( unsigned& priority );
 297 private:
 298   /** reduceQuantifier, return true if reduced */
 299   bool reduceQuantifier( Node q );
 300   /** compute term vector */
 301   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
 302   /** record instantiation, return true if it was non-duplicate */
 303   bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
 304   /** remove instantiation */
 305   bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
 306   /** set instantiation level attr */
 307   static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
 308   /** flush lemmas */
 309   void flushLemmas();
 310 public:
 311   /** get instantiation */
 312   Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
 313   /** get instantiation */
 314   Node getInstantiation( Node q, InstMatch& m, bool doVts = false );
 315   /** get instantiation */
 316   Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
 317   /** do substitution */
 318   Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited );
 319   /** add lemma lem */
 320   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
 321   /** remove pending lemma */
 322   bool removeLemma( Node lem );
 323   /** add require phase */
 324   void addRequirePhase( Node lit, bool req );
 325   /** do instantiation specified by m */
 326   bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
 327   /** add instantiation */
 328   bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
 329   /** remove pending instantiation */
 330   bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
 331   /** split on node n */
 332   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
 333   /** add split equality */
 334   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
 335   /** add EPR axiom */
 336   bool addEPRAxiom( TypeNode tn );
 337   /** mark relevant quantified formula, this will indicate it should be checked before the others */
 338   void markRelevant( Node q );
 339   /** has added lemma */
 340   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
 341   /** is in conflict */
 342   bool inConflict() { return d_conflict; }
 343   /** set conflict */
 344   void setConflict();
 345   /** get number of waiting lemmas */
 346   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
 347   /** get needs check */
 348   bool getInstWhenNeedsCheck( Theory::Effort e );
 349   /** get user pat mode */
 350   quantifiers::UserPatMode getInstUserPatMode();
 351   /** set instantiation level attr */
 352   static void setInstantiationLevelAttr( Node n, uint64_t level );
 353 public:
 354   /** get model */
 355   quantifiers::FirstOrderModel* getModel() { return d_model; }
 356   /** get term database */
 357   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
 358   /** get term database sygus */
 359   quantifiers::TermDbSygus* getTermDatabaseSygus();
 360   /** get trigger database */
 361   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
 362   /** add term to database */
 363   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
 364   /** notification when master equality engine is updated */
 365   void eqNotifyNewClass(TNode t);
 366   void eqNotifyPreMerge(TNode t1, TNode t2);
 367   void eqNotifyPostMerge(TNode t1, TNode t2);
 368   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 369   /** get the master equality engine */
 370   eq::EqualityEngine* getMasterEqualityEngine();
 371   /** get the active equality engine */
 372   eq::EqualityEngine* getActiveEqualityEngine();
 373   /** debug print equality engine */
 374   void debugPrintEqualityEngine( const char * c );
 375   /** get internal representative */
 376   Node getInternalRepresentative( Node a, Node q, int index );
 377 public:
 378   /** print instantiations */
 379   void printInstantiations( std::ostream& out );
 380   /** print solution for synthesis conjectures */
 381   void printSynthSolution( std::ostream& out );
 382   /** get list of quantified formulas that were instantiated */
 383   void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
 384   /** get instantiations */
 385   void getInstantiations( Node q, std::vector< Node >& insts );
 386   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
 387   /** get instantiation term vectors */
 388   void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
 389   void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
 390   /** get instantiated conjunction */
 391   Node getInstantiatedConjunction( Node q );
 392   /** get unsat core lemmas */
 393   bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
 394   bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
 395   /** get inst for lemmas */
 396   void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec );
 397   /** statistics class */
 398   class Statistics {
 399   public:
 400     TimerStat d_time;
 401     TimerStat d_qcf_time;
 402     TimerStat d_ematching_time;
 403     IntStat d_num_quant;
 404     IntStat d_instantiation_rounds;
 405     IntStat d_instantiation_rounds_lc;
 406     IntStat d_instantiations;
 407     IntStat d_inst_duplicate;
 408     IntStat d_inst_duplicate_eq;
 409     IntStat d_inst_duplicate_ent;
 410     IntStat d_inst_duplicate_model_true;
 411     IntStat d_triggers;
 412     IntStat d_simple_triggers;
 413     IntStat d_multi_triggers;
 414     IntStat d_multi_trigger_instantiations;
 415     IntStat d_red_alpha_equiv;
 416     IntStat d_instantiations_user_patterns;
 417     IntStat d_instantiations_auto_gen;
 418     IntStat d_instantiations_guess;
 419     IntStat d_instantiations_qcf;
 420     IntStat d_instantiations_qcf_prop;
 421     IntStat d_instantiations_fmf_exh;
 422     IntStat d_instantiations_fmf_mbqi;
 423     IntStat d_instantiations_cbqi;
 424     IntStat d_instantiations_rr;
 425     Statistics();
 426     ~Statistics();
 427   };/* class QuantifiersEngine::Statistics */
 428   Statistics d_statistics;
 429 };/* class QuantifiersEngine */
 430
 431
 432
 433 /** equality query object using theory engine */
 434 class EqualityQueryQuantifiersEngine : public EqualityQuery
 435 {
 436 private:
 437   /** pointer to theory engine */
 438   QuantifiersEngine* d_qe;
 439   /** quantifiers equality inference */
 440   quantifiers::EqualityInference * d_eq_inference;
 441   context::CDO< unsigned > d_eqi_counter;
 442   /** internal representatives */
 443   std::map< TypeNode, std::map< Node, Node > > d_int_rep;
 444   /** rep score */
 445   std::map< Node, int > d_rep_score;
 446   /** reset count */
 447   int d_reset_count;
 448
 449   /** processInferences : will merge equivalence classes in master equality engine, if possible */
 450   bool processInferences( Theory::Effort e );
 451   /** node contains */
 452   Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
 453   /** get score */
 454   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
 455   /** flatten representatives */
 456   void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 457 public:
 458   EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
 459   virtual ~EqualityQueryQuantifiersEngine();
 460   /** reset */
 461   bool reset( Theory::Effort e );
 462   /** identify */
 463   std::string identify() const { return "EqualityQueryQE"; }
 464   /** general queries about equality */
 465   bool hasTerm( Node a );
 466   Node getRepresentative( Node a );
 467   bool areEqual( Node a, Node b );
 468   bool areDisequal( Node a, Node b );
 469   eq::EqualityEngine* getEngine();
 470   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
 471   TNode getCongruentTerm( Node f, std::vector< TNode >& args );
 472   /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
 473       If cbqi is active, this will return a term in the equivalence class of "a" that does
 474       not contain instantiation constants, if such a term exists.
 475    */
 476   Node getInternalRepresentative( Node a, Node f, int index );
 477   /** get quantifiers equality inference */
 478   quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
 479 }; /* EqualityQueryQuantifiersEngine */
 480
 481 }/* CVC4::theory namespace */
 482 }/* CVC4 namespace */
 483
 484 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */