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-2020 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_trie.h"
  28 #include "theory/quantifiers/equality_query.h"
  29 #include "theory/quantifiers/first_order_model.h"
  30 #include "theory/quantifiers/fmf/model_builder.h"
  31 #include "theory/quantifiers/instantiate.h"
  32 #include "theory/quantifiers/quant_util.h"
  33 #include "theory/quantifiers/quantifiers_attributes.h"
  34 #include "theory/quantifiers/quantifiers_inference_manager.h"
  35 #include "theory/quantifiers/quantifiers_state.h"
  36 #include "theory/quantifiers/skolemize.h"
  37 #include "theory/quantifiers/sygus/term_database_sygus.h"
  38 #include "theory/quantifiers/term_database.h"
  39 #include "theory/quantifiers/term_enumeration.h"
  40 #include "theory/quantifiers/term_util.h"
  41 #include "util/statistics_registry.h"
  42
  43 namespace CVC4 {
  44
  45 class TheoryEngine;
  46
  47 namespace theory {
  48
  49 class DecisionManager;
  50
  51 namespace quantifiers {
  52 class QuantifiersModules;
  53 }
  54
  55 // TODO: organize this more/review this, github issue #1163
  56 class QuantifiersEngine {
  57   friend class ::CVC4::TheoryEngine;
  58   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
  59   typedef context::CDList<Node> NodeList;
  60   typedef context::CDList<bool> BoolList;
  61   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  62
  63  public:
  64   QuantifiersEngine(quantifiers::QuantifiersState& qstate,
  65                     quantifiers::QuantifiersInferenceManager& qim,
  66                     ProofNodeManager* pnm);
  67   ~QuantifiersEngine();
  68   //---------------------- external interface
  69   /** get theory engine */
  70   TheoryEngine* getTheoryEngine() const;
  71   /** Get the decision manager */
  72   DecisionManager* getDecisionManager();
  73   /** get default output channel for the quantifiers engine */
  74   OutputChannel& getOutputChannel();
  75   /** get default valuation for the quantifiers engine */
  76   Valuation& getValuation();
  77   /** get the logic info for the quantifiers engine */
  78   const LogicInfo& getLogicInfo() const;
  79   //---------------------- end external interface
  80   //---------------------- utilities
  81   /** get the master equality engine */
  82   eq::EqualityEngine* getMasterEqualityEngine() const;
  83   /** get equality query */
  84   EqualityQuery* getEqualityQuery() const;
  85   /** get the model builder */
  86   quantifiers::QModelBuilder* getModelBuilder() const;
  87   /** get model */
  88   quantifiers::FirstOrderModel* getModel() const;
  89   /** get term database */
  90   quantifiers::TermDb* getTermDatabase() const;
  91   /** get term database sygus */
  92   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
  93   /** get term utilities */
  94   quantifiers::TermUtil* getTermUtil() const;
  95   /** get term canonizer */
  96   expr::TermCanonize* getTermCanonize() const;
  97   /** get quantifiers attributes */
  98   quantifiers::QuantAttributes* getQuantAttributes() const;
  99   /** get instantiate utility */
 100   quantifiers::Instantiate* getInstantiate() const;
 101   /** get skolemize utility */
 102   quantifiers::Skolemize* getSkolemize() const;
 103   /** get term enumeration utility */
 104   quantifiers::TermEnumeration* getTermEnumeration() const;
 105   /** get trigger database */
 106   inst::TriggerTrie* getTriggerDatabase() const;
 107   //---------------------- end utilities
 108  private:
 109   //---------------------- private initialization
 110   /**
 111    * Finish initialize, which passes pointers to the objects that quantifiers
 112    * engine needs but were not available when it was created. This is
 113    * called after theories have been created but before they have finished
 114    * initialization.
 115    *
 116    * @param te The theory engine
 117    * @param dm The decision manager of the theory engine
 118    * @param mee The master equality engine of the theory engine
 119    */
 120   void finishInit(TheoryEngine* te,
 121                   DecisionManager* dm,
 122                   eq::EqualityEngine* mee);
 123   //---------------------- end private initialization
 124   /**
 125    * Maps quantified formulas to the module that owns them, if any module has
 126    * specifically taken ownership of it.
 127    */
 128   std::map< Node, QuantifiersModule * > d_owner;
 129   /**
 130    * The priority value associated with the ownership of quantified formulas
 131    * in the domain of the above map, where higher values take higher
 132    * precendence.
 133    */
 134   std::map< Node, int > d_owner_priority;
 135  public:
 136   /** get owner */
 137   QuantifiersModule * getOwner( Node q );
 138   /**
 139    * Set owner of quantified formula q to module m with given priority. If
 140    * the quantified formula has previously been assigned an owner with
 141    * lower priority, that owner is overwritten.
 142    */
 143   void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
 144   /** set owner of quantified formula q based on its attributes qa. */
 145   void setOwner(Node q, quantifiers::QAttributes& qa);
 146   /** considers */
 147   bool hasOwnership( Node q, QuantifiersModule * m = NULL );
 148   /** does variable v of quantified formula q have a finite bound? */
 149   bool isFiniteBound(Node q, Node v) const;
 150   /** get bound var type
 151    *
 152    * This returns the type of bound that was inferred for variable v of
 153    * quantified formula q.
 154    */
 155   BoundVarType getBoundVarType(Node q, Node v) const;
 156   /**
 157    * Get the indices of bound variables, in the order they should be processed
 158    * in a RepSetIterator.
 159    *
 160    * For details, see BoundedIntegers::getBoundVarIndices.
 161    */
 162   void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
 163   /**
 164    * Get bound elements
 165    *
 166    * This gets the (finite) enumeration of the range of variable v of quantified
 167    * formula q and adds it into the vector elements in the context of the
 168    * iteration being performed by rsi. It returns true if it could successfully
 169    * determine this range.
 170    *
 171    * For details, see BoundedIntegers::getBoundElements.
 172    */
 173   bool getBoundElements(RepSetIterator* rsi,
 174                         bool initial,
 175                         Node q,
 176                         Node v,
 177                         std::vector<Node>& elements) const;
 178
 179  public:
 180   /** presolve */
 181   void presolve();
 182   /** notify preprocessed assertion */
 183   void ppNotifyAssertions(const std::vector<Node>& assertions);
 184   /** check at level */
 185   void check( Theory::Effort e );
 186   /** notify that theories were combined */
 187   void notifyCombineTheories();
 188   /** preRegister quantifier
 189    *
 190    * This function is called after registerQuantifier for quantified formulas
 191    * that are pre-registered to the quantifiers theory.
 192    */
 193   void preRegisterQuantifier(Node q);
 194   /** register quantifier */
 195   void registerPattern( std::vector<Node> & pattern);
 196   /** assert universal quantifier */
 197   void assertQuantifier( Node q, bool pol );
 198 private:
 199  /** (context-indepentent) register quantifier internal
 200   *
 201   * This is called when a quantified formula q is pre-registered to the
 202   * quantifiers theory, and updates the modules in this class with
 203   * context-independent information about how to handle q. This includes basic
 204   * information such as which module owns q.
 205   */
 206  void registerQuantifierInternal(Node q);
 207  /** reduceQuantifier, return true if reduced */
 208  bool reduceQuantifier(Node q);
 209  /** flush lemmas */
 210  void flushLemmas();
 211
 212 public:
 213  /**
 214   * Add lemma to the lemma buffer of this quantifiers engine.
 215   * @param lem The lemma to send
 216   * @param doCache Whether to cache the lemma (to check for duplicate lemmas)
 217   * @param doRewrite Whether to rewrite the lemma
 218   * @return true if the lemma was successfully added to the buffer
 219   */
 220  bool addLemma(Node lem, bool doCache = true, bool doRewrite = true);
 221  /**
 222   * Add trusted lemma lem, same as above, but where a proof generator may be
 223   * provided along with the lemma.
 224   */
 225  bool addTrustedLemma(TrustNode tlem,
 226                       bool doCache = true,
 227                       bool doRewrite = true);
 228  /** remove pending lemma */
 229  bool removeLemma(Node lem);
 230  /** add require phase */
 231  void addRequirePhase(Node lit, bool req);
 232  /** mark relevant quantified formula, this will indicate it should be checked
 233   * before the others */
 234  void markRelevant(Node q);
 235  /** has added lemma */
 236  bool hasAddedLemma() const;
 237  /** theory engine needs check
 238   *
 239   * This is true if the theory engine has more constraints to process. When
 240   * it is false, we are tentatively going to terminate solving with
 241   * sat/unknown. For details, see TheoryEngine::needCheck.
 242   */
 243  bool theoryEngineNeedsCheck() const;
 244  /** is in conflict */
 245  bool inConflict() { return d_conflict; }
 246  /** set conflict */
 247  void setConflict();
 248  /** get current q effort */
 249  QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
 250  /** get number of waiting lemmas */
 251  unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
 252  /** get needs check */
 253  bool getInstWhenNeedsCheck(Theory::Effort e);
 254  /** get user pat mode */
 255  options::UserPatMode getInstUserPatMode();
 256
 257 public:
 258  /** add term to database */
 259  void addTermToDatabase(Node n,
 260                         bool withinQuant = false,
 261                         bool withinInstClosure = false);
 262  /** notification when master equality engine is updated */
 263  void eqNotifyNewClass(TNode t);
 264  /** debug print equality engine */
 265  void debugPrintEqualityEngine(const char* c);
 266  /** get internal representative
 267   *
 268   * Choose a term that is equivalent to a in the current context that is the
 269   * best term for instantiating the index^th variable of quantified formula q.
 270   * If no legal term can be found, we return null. This can occur if:
 271   * - a's type is not a subtype of the type of the index^th variable of q,
 272   * - a is in an equivalent class with all terms that are restricted not to
 273   * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
 274   * guided instantiation.
 275   */
 276  Node getInternalRepresentative(Node a, Node q, int index);
 277
 278 public:
 279  //----------user interface for instantiations (see quantifiers/instantiate.h)
 280  /** print instantiations */
 281  void printInstantiations(std::ostream& out);
 282  /** print solution for synthesis conjectures */
 283  void printSynthSolution(std::ostream& out);
 284  /** get list of quantified formulas that were instantiated */
 285  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
 286  /** get instantiation term vectors */
 287  void getInstantiationTermVectors(Node q,
 288                                   std::vector<std::vector<Node> >& tvecs);
 289  void getInstantiationTermVectors(
 290      std::map<Node, std::vector<std::vector<Node> > >& insts);
 291
 292  /** get synth solutions
 293   *
 294   * This method returns true if there is a synthesis solution available. This
 295   * is the case if the last call to check satisfiability originated in a
 296   * check-synth call, and the synthesis engine module of this class
 297   * successfully found a solution for all active synthesis conjectures.
 298   *
 299   * This method adds entries to sol_map that map functions-to-synthesize with
 300   * their solutions, for all active conjectures. This should be called
 301   * immediately after the solver answers unsat for sygus input.
 302   *
 303   * For details on what is added to sol_map, see
 304   * SynthConjecture::getSynthSolutions.
 305   */
 306  bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
 307
 308  //----------end user interface for instantiations
 309
 310  /** statistics class */
 311  class Statistics
 312  {
 313   public:
 314     TimerStat d_time;
 315     TimerStat d_qcf_time;
 316     TimerStat d_ematching_time;
 317     IntStat d_num_quant;
 318     IntStat d_instantiation_rounds;
 319     IntStat d_instantiation_rounds_lc;
 320     IntStat d_triggers;
 321     IntStat d_simple_triggers;
 322     IntStat d_multi_triggers;
 323     IntStat d_multi_trigger_instantiations;
 324     IntStat d_red_alpha_equiv;
 325     IntStat d_instantiations_user_patterns;
 326     IntStat d_instantiations_auto_gen;
 327     IntStat d_instantiations_guess;
 328     IntStat d_instantiations_qcf;
 329     IntStat d_instantiations_qcf_prop;
 330     IntStat d_instantiations_fmf_exh;
 331     IntStat d_instantiations_fmf_mbqi;
 332     IntStat d_instantiations_cbqi;
 333     IntStat d_instantiations_rr;
 334     Statistics();
 335     ~Statistics();
 336   };/* class QuantifiersEngine::Statistics */
 337   Statistics d_statistics;
 338
 339  private:
 340   /** The quantifiers state object */
 341   quantifiers::QuantifiersState& d_qstate;
 342   /** The quantifiers inference manager */
 343   quantifiers::QuantifiersInferenceManager& d_qim;
 344   /** Pointer to theory engine object */
 345   TheoryEngine* d_te;
 346   /** Reference to the decision manager of the theory engine */
 347   DecisionManager* d_decManager;
 348   /** Pointer to the master equality engine */
 349   eq::EqualityEngine* d_masterEqualityEngine;
 350   /** vector of utilities for quantifiers */
 351   std::vector<QuantifiersUtil*> d_util;
 352   /** vector of modules for quantifiers */
 353   std::vector<QuantifiersModule*> d_modules;
 354   //------------- quantifiers utilities
 355   /** equality query class */
 356   std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
 357   /** all triggers will be stored in this trie */
 358   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
 359   /** extended model object */
 360   std::unique_ptr<quantifiers::FirstOrderModel> d_model;
 361   /** model builder */
 362   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
 363   /** term utilities */
 364   std::unique_ptr<quantifiers::TermUtil> d_term_util;
 365   /** term utilities */
 366   std::unique_ptr<expr::TermCanonize> d_term_canon;
 367   /** term database */
 368   std::unique_ptr<quantifiers::TermDb> d_term_db;
 369   /** sygus term database */
 370   std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
 371   /** quantifiers attributes */
 372   std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
 373   /** instantiate utility */
 374   std::unique_ptr<quantifiers::Instantiate> d_instantiate;
 375   /** skolemize utility */
 376   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
 377   /** term enumeration utility */
 378   std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
 379   //------------- end quantifiers utilities
 380   /**
 381    * The modules utility, which contains all of the quantifiers modules.
 382    */
 383   std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
 384   //------------- temporary information during check
 385   /** current effort level */
 386   QuantifiersModule::QEffort d_curr_effort_level;
 387   /** are we in conflict */
 388   bool d_conflict;
 389   context::CDO<bool> d_conflict_c;
 390   /** has added lemma this round */
 391   bool d_hasAddedLemma;
 392   //------------- end temporary information during check
 393  private:
 394   /** list of all quantifiers seen */
 395   std::map<Node, bool> d_quants;
 396   /** quantifiers pre-registered */
 397   NodeSet d_quants_prereg;
 398   /** quantifiers reduced */
 399   BoolMap d_quants_red;
 400   std::map<Node, Node> d_quants_red_lem;
 401   /** list of all lemmas produced */
 402   // std::map< Node, bool > d_lemmas_produced;
 403   BoolMap d_lemmas_produced_c;
 404   /** lemmas waiting */
 405   std::vector<Node> d_lemmas_waiting;
 406   /** map from waiting lemmas to their proof generators */
 407   std::map<Node, ProofGenerator*> d_lemmasWaitingPg;
 408   /** phase requirements waiting */
 409   std::map<Node, bool> d_phase_req_waiting;
 410   /** inst round counters TODO: make context-dependent? */
 411   context::CDO<int> d_ierCounter_c;
 412   int d_ierCounter;
 413   int d_ierCounter_lc;
 414   int d_ierCounterLastLc;
 415   int d_inst_when_phase;
 416   /** has presolve been called */
 417   context::CDO<bool> d_presolve;
 418   /** presolve cache */
 419   NodeSet d_presolve_in;
 420   NodeList d_presolve_cache;
 421   BoolList d_presolve_cache_wq;
 422   BoolList d_presolve_cache_wic;
 423 };/* class QuantifiersEngine */
 424
 425 }/* CVC4::theory namespace */
 426 }/* CVC4 namespace */
 427
 428 #endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */