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