src/theory/quantifiers_engine.h

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 <map>
  21 #include <unordered_map>
  22
  23 #include "context/cdhashset.h"
  24 #include "context/cdlist.h"
  25 #include "expr/attribute.h"
  26 #include "expr/term_canonize.h"
  27 #include "theory/quantifiers/ematching/trigger.h"
  28 #include "theory/quantifiers/equality_infer.h"
  29 #include "theory/quantifiers/equality_query.h"
  30 #include "theory/quantifiers/first_order_model.h"
  31 #include "theory/quantifiers/fmf/model_builder.h"
  32 #include "theory/quantifiers/instantiate.h"
  33 #include "theory/quantifiers/quant_epr.h"
  34 #include "theory/quantifiers/quant_util.h"
  35 #include "theory/quantifiers/quantifiers_attributes.h"
  36 #include "theory/quantifiers/relevant_domain.h"
  37 #include "theory/quantifiers/skolemize.h"
  38 #include "theory/quantifiers/sygus/synth_engine.h"
  39 #include "theory/quantifiers/sygus/term_database_sygus.h"
  40 #include "theory/quantifiers/term_database.h"
  41 #include "theory/quantifiers/term_enumeration.h"
  42 #include "theory/quantifiers/term_util.h"
  43 #include "util/statistics_registry.h"
  44
  45 namespace CVC4 {
  46
  47 class TheoryEngine;
  48
  49 namespace theory {
  50
  51 class QuantifiersEnginePrivate;
  52
  53 // TODO: organize this more/review this, github issue #1163
  54 class QuantifiersEngine {
  55   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
  56   typedef context::CDList<Node> NodeList;
  57   typedef context::CDList<bool> BoolList;
  58   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  59
  60 public:
  61   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
  62   ~QuantifiersEngine();
  63   //---------------------- external interface
  64   /** get theory engine */
  65   TheoryEngine* getTheoryEngine() const { return d_te; }
  66   /** get default sat context for quantifiers engine */
  67   context::Context* getSatContext();
  68   /** get default sat context for quantifiers engine */
  69   context::UserContext* getUserContext();
  70   /** get default output channel for the quantifiers engine */
  71   OutputChannel& getOutputChannel();
  72   /** get default valuation for the quantifiers engine */
  73   Valuation& getValuation();
  74   /** get the logic info for the quantifiers engine */
  75   const LogicInfo& getLogicInfo() const;
  76   //---------------------- end external interface
  77   //---------------------- utilities
  78   /** get the master equality engine */
  79   eq::EqualityEngine* getMasterEqualityEngine() const;
  80   /** get the active equality engine */
  81   eq::EqualityEngine* getActiveEqualityEngine() const;
  82   /** get equality query */
  83   EqualityQuery* getEqualityQuery() const;
  84   /** get the model builder */
  85   quantifiers::QModelBuilder* getModelBuilder() const;
  86   /** get utility for EPR */
  87   quantifiers::QuantEPR* getQuantEPR() const;
  88   /** get model */
  89   quantifiers::FirstOrderModel* getModel() const;
  90   /** get term database */
  91   quantifiers::TermDb* getTermDatabase() const;
  92   /** get term database sygus */
  93   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
  94   /** get term utilities */
  95   quantifiers::TermUtil* getTermUtil() const;
  96   /** get term canonizer */
  97   expr::TermCanonize* getTermCanonize() const;
  98   /** get quantifiers attributes */
  99   quantifiers::QuantAttributes* getQuantAttributes() const;
 100   /** get instantiate utility */
 101   quantifiers::Instantiate* getInstantiate() const;
 102   /** get skolemize utility */
 103   quantifiers::Skolemize* getSkolemize() const;
 104   /** get term enumeration utility */
 105   quantifiers::TermEnumeration* getTermEnumeration() const;
 106   /** get trigger database */
 107   inst::TriggerTrie* getTriggerDatabase() const;
 108   //---------------------- end utilities
 109   //---------------------- utilities (TODO move these utilities #1163)
 110   /** get the equality inference */
 111   quantifiers::EqualityInference* getEqualityInference() const;
 112   /** get relevant domain */
 113   quantifiers::RelevantDomain* getRelevantDomain() const;
 114   //---------------------- end utilities
 115   //---------------------- modules (TODO remove these #1163)
 116   /** ceg instantiation */
 117   quantifiers::SynthEngine* getSynthEngine() const;
 118   //---------------------- end modules
 119  private:
 120   /**
 121    * Maps quantified formulas to the module that owns them, if any module has
 122    * specifically taken ownership of it.
 123    */
 124   std::map< Node, QuantifiersModule * > d_owner;
 125   /**
 126    * The priority value associated with the ownership of quantified formulas
 127    * in the domain of the above map, where higher values take higher
 128    * precendence.
 129    */
 130   std::map< Node, int > d_owner_priority;
 131 public:
 132   /** get owner */
 133   QuantifiersModule * getOwner( Node q );
 134   /**
 135    * Set owner of quantified formula q to module m with given priority. If
 136    * the quantified formula has previously been assigned an owner with
 137    * lower priority, that owner is overwritten.
 138    */
 139   void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
 140   /** set owner of quantified formula q based on its attributes qa. */
 141   void setOwner(Node q, quantifiers::QAttributes& qa);
 142   /** considers */
 143   bool hasOwnership( Node q, QuantifiersModule * m = NULL );
 144   /** does variable v of quantified formula q have a finite bound? */
 145   bool isFiniteBound(Node q, Node v) const;
 146   /** get bound var type
 147    *
 148    * This returns the type of bound that was inferred for variable v of
 149    * quantified formula q.
 150    */
 151   BoundVarType getBoundVarType(Node q, Node v) const;
 152   /**
 153    * Get the indices of bound variables, in the order they should be processed
 154    * in a RepSetIterator.
 155    *
 156    * For details, see BoundedIntegers::getBoundVarIndices.
 157    */
 158   void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
 159   /**
 160    * Get bound elements
 161    *
 162    * This gets the (finite) enumeration of the range of variable v of quantified
 163    * formula q and adds it into the vector elements in the context of the
 164    * iteration being performed by rsi. It returns true if it could successfully
 165    * determine this range.
 166    *
 167    * For details, see BoundedIntegers::getBoundElements.
 168    */
 169   bool getBoundElements(RepSetIterator* rsi,
 170                         bool initial,
 171                         Node q,
 172                         Node v,
 173                         std::vector<Node>& elements) const;
 174
 175  public:
 176   /** presolve */
 177   void presolve();
 178   /** notify preprocessed assertion */
 179   void ppNotifyAssertions(const std::vector<Node>& assertions);
 180   /** check at level */
 181   void check( Theory::Effort e );
 182   /** notify that theories were combined */
 183   void notifyCombineTheories();
 184   /** preRegister quantifier
 185    *
 186    * This function is called after registerQuantifier for quantified formulas
 187    * that are pre-registered to the quantifiers theory.
 188    */
 189   void preRegisterQuantifier(Node q);
 190   /** register quantifier */
 191   void registerPattern( std::vector<Node> & pattern);
 192   /** assert universal quantifier */
 193   void assertQuantifier( Node q, bool pol );
 194 private:
 195  /** (context-indepentent) register quantifier internal
 196   *
 197   * This is called when a quantified formula q is pre-registered to the
 198   * quantifiers theory, and updates the modules in this class with
 199   * context-independent information about how to handle q. This includes basic
 200   * information such as which module owns q.
 201   */
 202  void registerQuantifierInternal(Node q);
 203  /** reduceQuantifier, return true if reduced */
 204  bool reduceQuantifier(Node q);
 205  /** flush lemmas */
 206  void flushLemmas();
 207
 208 public:
 209   /** add lemma lem */
 210   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
 211   /** remove pending lemma */
 212   bool removeLemma( Node lem );
 213   /** add require phase */
 214   void addRequirePhase( Node lit, bool req );
 215   /** mark relevant quantified formula, this will indicate it should be checked before the others */
 216   void markRelevant( Node q );
 217   /** has added lemma */
 218   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
 219   /** is in conflict */
 220   bool inConflict() { return d_conflict; }
 221   /** set conflict */
 222   void setConflict();
 223   /** get current q effort */
 224   QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
 225   /** get number of waiting lemmas */
 226   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
 227   /** get needs check */
 228   bool getInstWhenNeedsCheck( Theory::Effort e );
 229   /** get user pat mode */
 230   quantifiers::UserPatMode getInstUserPatMode();
 231 public:
 232   /** add term to database */
 233   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
 234   /** notification when master equality engine is updated */
 235   void eqNotifyNewClass(TNode t);
 236   void eqNotifyPreMerge(TNode t1, TNode t2);
 237   void eqNotifyPostMerge(TNode t1, TNode t2);
 238   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 239   /** use model equality engine */
 240   bool usingModelEqualityEngine() const { return d_useModelEe; }
 241   /** debug print equality engine */
 242   void debugPrintEqualityEngine( const char * c );
 243   /** get internal representative */
 244   Node getInternalRepresentative( Node a, Node q, int index );
 245
 246  public:
 247   //----------user interface for instantiations (see quantifiers/instantiate.h)
 248   /** print instantiations */
 249   void printInstantiations(std::ostream& out);
 250   /** print solution for synthesis conjectures */
 251   void printSynthSolution(std::ostream& out);
 252   /** get list of quantified formulas that were instantiated */
 253   void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
 254   /** get instantiations */
 255   void getInstantiations(Node q, std::vector<Node>& insts);
 256   void getInstantiations(std::map<Node, std::vector<Node> >& insts);
 257   /** get instantiation term vectors */
 258   void getInstantiationTermVectors(Node q,
 259                                    std::vector<std::vector<Node> >& tvecs);
 260   void getInstantiationTermVectors(
 261       std::map<Node, std::vector<std::vector<Node> > >& insts);
 262   /** get instantiated conjunction */
 263   Node getInstantiatedConjunction(Node q);
 264   /** get unsat core lemmas */
 265   bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
 266   bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
 267                           std::map<Node, Node>& weak_imp);
 268   /** get explanation for instantiation lemmas */
 269   void getExplanationForInstLemmas(const std::vector<Node>& lems,
 270                                    std::map<Node, Node>& quant,
 271                                    std::map<Node, std::vector<Node> >& tvec);
 272
 273   /** get synth solutions
 274    *
 275    * This function adds entries to sol_map that map functions-to-synthesize with
 276    * their solutions, for all active conjectures. This should be called
 277    * immediately after the solver answers unsat for sygus input.
 278    *
 279    * For details on what is added to sol_map, see
 280    * CegConjecture::getSynthSolutions.
 281    */
 282   void getSynthSolutions(std::map<Node, Node>& sol_map);
 283
 284   //----------end user interface for instantiations
 285
 286   /** statistics class */
 287   class Statistics {
 288   public:
 289     TimerStat d_time;
 290     TimerStat d_qcf_time;
 291     TimerStat d_ematching_time;
 292     IntStat d_num_quant;
 293     IntStat d_instantiation_rounds;
 294     IntStat d_instantiation_rounds_lc;
 295     IntStat d_triggers;
 296     IntStat d_simple_triggers;
 297     IntStat d_multi_triggers;
 298     IntStat d_multi_trigger_instantiations;
 299     IntStat d_red_alpha_equiv;
 300     IntStat d_instantiations_user_patterns;
 301     IntStat d_instantiations_auto_gen;
 302     IntStat d_instantiations_guess;
 303     IntStat d_instantiations_qcf;
 304     IntStat d_instantiations_qcf_prop;
 305     IntStat d_instantiations_fmf_exh;
 306     IntStat d_instantiations_fmf_mbqi;
 307     IntStat d_instantiations_cbqi;
 308     IntStat d_instantiations_rr;
 309     Statistics();
 310     ~Statistics();
 311   };/* class QuantifiersEngine::Statistics */
 312   Statistics d_statistics;
 313
 314  private:
 315   /** reference to theory engine object */
 316   TheoryEngine* d_te;
 317   /** vector of utilities for quantifiers */
 318   std::vector<QuantifiersUtil*> d_util;
 319   /** vector of modules for quantifiers */
 320   std::vector<QuantifiersModule*> d_modules;
 321   //------------- quantifiers utilities
 322   /** equality query class */
 323   std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
 324   /** equality inference class */
 325   std::unique_ptr<quantifiers::EqualityInference> d_eq_inference;
 326   /** all triggers will be stored in this trie */
 327   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
 328   /** extended model object */
 329   std::unique_ptr<quantifiers::FirstOrderModel> d_model;
 330   /** relevant domain */
 331   std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
 332   /** model builder */
 333   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
 334   /** utility for effectively propositional logic */
 335   std::unique_ptr<quantifiers::QuantEPR> d_qepr;
 336   /** term utilities */
 337   std::unique_ptr<quantifiers::TermUtil> d_term_util;
 338   /** term utilities */
 339   std::unique_ptr<expr::TermCanonize> d_term_canon;
 340   /** term database */
 341   std::unique_ptr<quantifiers::TermDb> d_term_db;
 342   /** sygus term database */
 343   std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
 344   /** quantifiers attributes */
 345   std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
 346   /** instantiate utility */
 347   std::unique_ptr<quantifiers::Instantiate> d_instantiate;
 348   /** skolemize utility */
 349   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
 350   /** term enumeration utility */
 351   std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
 352   //------------- end quantifiers utilities
 353   /**
 354    * The private utility, which contains all of the quantifiers modules.
 355    */
 356   std::unique_ptr<QuantifiersEnginePrivate> d_private;
 357   //------------- temporary information during check
 358   /** current effort level */
 359   QuantifiersModule::QEffort d_curr_effort_level;
 360   /** are we in conflict */
 361   bool d_conflict;
 362   context::CDO<bool> d_conflict_c;
 363   /** has added lemma this round */
 364   bool d_hasAddedLemma;
 365   /** whether to use model equality engine */
 366   bool d_useModelEe;
 367   //------------- end temporary information during check
 368  private:
 369   /** list of all quantifiers seen */
 370   std::map<Node, bool> d_quants;
 371   /** quantifiers pre-registered */
 372   NodeSet d_quants_prereg;
 373   /** quantifiers reduced */
 374   BoolMap d_quants_red;
 375   std::map<Node, Node> d_quants_red_lem;
 376   /** list of all lemmas produced */
 377   // std::map< Node, bool > d_lemmas_produced;
 378   BoolMap d_lemmas_produced_c;
 379   /** lemmas waiting */
 380   std::vector<Node> d_lemmas_waiting;
 381   /** phase requirements waiting */
 382   std::map<Node, bool> d_phase_req_waiting;
 383   /** inst round counters TODO: make context-dependent? */
 384   context::CDO<int> d_ierCounter_c;
 385   int d_ierCounter;
 386   int d_ierCounter_lc;
 387   int d_ierCounterLastLc;
 388   int d_inst_when_phase;
 389   /** has presolve been called */
 390   context::CDO<bool> d_presolve;
 391   /** presolve cache */
 392   NodeSet d_presolve_in;
 393   NodeList d_presolve_cache;
 394   BoolList d_presolve_cache_wq;
 395   BoolList d_presolve_cache_wic;
 396 };/* class QuantifiersEngine */
 397
 398 }/* CVC4::theory namespace */
 399 }/* CVC4 namespace */
 400
 401 #endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */