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_module.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   /** The quantifiers state object */
  78   quantifiers::QuantifiersState& getState();
  79   /** The quantifiers inference manager */
  80   quantifiers::QuantifiersInferenceManager& getInferenceManager();
  81   /** The quantifiers registry */
  82   quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
  83   //---------------------- end external interface
  84   //---------------------- utilities
  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 quantifiers attributes */
  94   quantifiers::QuantAttributes* getQuantAttributes() const;
  95   /** get instantiate utility */
  96   quantifiers::Instantiate* getInstantiate() const;
  97   /** get skolemize utility */
  98   quantifiers::Skolemize* getSkolemize() const;
  99   /** get term enumeration utility */
 100   quantifiers::TermEnumeration* getTermEnumeration() const;
 101   /** get trigger database */
 102   inst::TriggerTrie* getTriggerDatabase() const;
 103   //---------------------- end utilities
 104  private:
 105   //---------------------- private initialization
 106   /**
 107    * Finish initialize, which passes pointers to the objects that quantifiers
 108    * engine needs but were not available when it was created. This is
 109    * called after theories have been created but before they have finished
 110    * initialization.
 111    *
 112    * @param te The theory engine
 113    * @param dm The decision manager of the theory engine
 114    */
 115   void finishInit(TheoryEngine* te, DecisionManager* dm);
 116   //---------------------- end private initialization
 117  public:
 118   /** does variable v of quantified formula q have a finite bound? */
 119   bool isFiniteBound(Node q, Node v) const;
 120   /** get bound var type
 121    *
 122    * This returns the type of bound that was inferred for variable v of
 123    * quantified formula q.
 124    */
 125   BoundVarType getBoundVarType(Node q, Node v) const;
 126   /**
 127    * Get the indices of bound variables, in the order they should be processed
 128    * in a RepSetIterator.
 129    *
 130    * For details, see BoundedIntegers::getBoundVarIndices.
 131    */
 132   void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
 133   /**
 134    * Get bound elements
 135    *
 136    * This gets the (finite) enumeration of the range of variable v of quantified
 137    * formula q and adds it into the vector elements in the context of the
 138    * iteration being performed by rsi. It returns true if it could successfully
 139    * determine this range.
 140    *
 141    * For details, see BoundedIntegers::getBoundElements.
 142    */
 143   bool getBoundElements(RepSetIterator* rsi,
 144                         bool initial,
 145                         Node q,
 146                         Node v,
 147                         std::vector<Node>& elements) const;
 148
 149  public:
 150   /** presolve */
 151   void presolve();
 152   /** notify preprocessed assertion */
 153   void ppNotifyAssertions(const std::vector<Node>& assertions);
 154   /** check at level */
 155   void check( Theory::Effort e );
 156   /** notify that theories were combined */
 157   void notifyCombineTheories();
 158   /** preRegister quantifier
 159    *
 160    * This function is called after registerQuantifier for quantified formulas
 161    * that are pre-registered to the quantifiers theory.
 162    */
 163   void preRegisterQuantifier(Node q);
 164   /** assert universal quantifier */
 165   void assertQuantifier( Node q, bool pol );
 166 private:
 167  /** (context-indepentent) register quantifier internal
 168   *
 169   * This is called when a quantified formula q is pre-registered to the
 170   * quantifiers theory, and updates the modules in this class with
 171   * context-independent information about how to handle q. This includes basic
 172   * information such as which module owns q.
 173   */
 174  void registerQuantifierInternal(Node q);
 175  /** reduceQuantifier, return true if reduced */
 176  bool reduceQuantifier(Node q);
 177
 178 public:
 179  /** mark relevant quantified formula, this will indicate it should be checked
 180   * before the others */
 181  void markRelevant(Node q);
 182  /** add term to database */
 183  void addTermToDatabase(Node n, bool withinQuant = false);
 184  /** notification when master equality engine is updated */
 185  void eqNotifyNewClass(TNode t);
 186  /** get internal representative
 187   *
 188   * Choose a term that is equivalent to a in the current context that is the
 189   * best term for instantiating the index^th variable of quantified formula q.
 190   * If no legal term can be found, we return null. This can occur if:
 191   * - a's type is not a subtype of the type of the index^th variable of q,
 192   * - a is in an equivalent class with all terms that are restricted not to
 193   * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
 194   * guided instantiation.
 195   */
 196  Node getInternalRepresentative(Node a, Node q, int index);
 197  /**
 198   * Get quantifiers name, which returns a variable corresponding to the name of
 199   * quantified formula q if q has a name, or otherwise returns q itself.
 200   */
 201  Node getNameForQuant(Node q) const;
 202  /**
 203   * Get name for quantified formula. Returns true if q has a name or if req
 204   * is false. Sets name to the result of the above method.
 205   */
 206  bool getNameForQuant(Node q, Node& name, bool req = true) const;
 207
 208 public:
 209  //----------user interface for instantiations (see quantifiers/instantiate.h)
 210  /** print solution for synthesis conjectures */
 211  void printSynthSolution(std::ostream& out);
 212  /** get list of quantified formulas that were instantiated */
 213  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
 214  /** get instantiation term vectors */
 215  void getInstantiationTermVectors(Node q,
 216                                   std::vector<std::vector<Node> >& tvecs);
 217  void getInstantiationTermVectors(
 218      std::map<Node, std::vector<std::vector<Node> > >& insts);
 219  /**
 220   * Get skolemization vectors, where for each quantified formula that was
 221   * skolemized, this is the list of skolems that were used to witness the
 222   * negation of that quantified formula.
 223   */
 224  void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
 225
 226  /** get synth solutions
 227   *
 228   * This method returns true if there is a synthesis solution available. This
 229   * is the case if the last call to check satisfiability originated in a
 230   * check-synth call, and the synthesis engine module of this class
 231   * successfully found a solution for all active synthesis conjectures.
 232   *
 233   * This method adds entries to sol_map that map functions-to-synthesize with
 234   * their solutions, for all active conjectures. This should be called
 235   * immediately after the solver answers unsat for sygus input.
 236   *
 237   * For details on what is added to sol_map, see
 238   * SynthConjecture::getSynthSolutions.
 239   */
 240  bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
 241
 242  //----------end user interface for instantiations
 243
 244  /** statistics class */
 245  class Statistics
 246  {
 247   public:
 248     TimerStat d_time;
 249     TimerStat d_qcf_time;
 250     TimerStat d_ematching_time;
 251     IntStat d_num_quant;
 252     IntStat d_instantiation_rounds;
 253     IntStat d_instantiation_rounds_lc;
 254     IntStat d_triggers;
 255     IntStat d_simple_triggers;
 256     IntStat d_multi_triggers;
 257     IntStat d_multi_trigger_instantiations;
 258     IntStat d_red_alpha_equiv;
 259     IntStat d_instantiations_user_patterns;
 260     IntStat d_instantiations_auto_gen;
 261     IntStat d_instantiations_guess;
 262     IntStat d_instantiations_qcf;
 263     IntStat d_instantiations_qcf_prop;
 264     IntStat d_instantiations_fmf_exh;
 265     IntStat d_instantiations_fmf_mbqi;
 266     IntStat d_instantiations_cbqi;
 267     IntStat d_instantiations_rr;
 268     Statistics();
 269     ~Statistics();
 270   };/* class QuantifiersEngine::Statistics */
 271   Statistics d_statistics;
 272
 273  private:
 274   /** The quantifiers state object */
 275   quantifiers::QuantifiersState& d_qstate;
 276   /** The quantifiers inference manager */
 277   quantifiers::QuantifiersInferenceManager& d_qim;
 278   /** Pointer to theory engine object */
 279   TheoryEngine* d_te;
 280   /** Reference to the decision manager of the theory engine */
 281   DecisionManager* d_decManager;
 282   /** vector of utilities for quantifiers */
 283   std::vector<QuantifiersUtil*> d_util;
 284   /** vector of modules for quantifiers */
 285   std::vector<QuantifiersModule*> d_modules;
 286   //------------- quantifiers utilities
 287   /** The quantifiers registry */
 288   quantifiers::QuantifiersRegistry d_qreg;
 289   /** all triggers will be stored in this trie */
 290   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
 291   /** extended model object */
 292   std::unique_ptr<quantifiers::FirstOrderModel> d_model;
 293   /** model builder */
 294   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
 295   /** term database */
 296   std::unique_ptr<quantifiers::TermDb> d_term_db;
 297   /** equality query class */
 298   std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
 299   /** sygus term database */
 300   std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
 301   /** quantifiers attributes */
 302   std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
 303   /** instantiate utility */
 304   std::unique_ptr<quantifiers::Instantiate> d_instantiate;
 305   /** skolemize utility */
 306   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
 307   /** term enumeration utility */
 308   std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
 309   //------------- end quantifiers utilities
 310   /**
 311    * The modules utility, which contains all of the quantifiers modules.
 312    */
 313   std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
 314   //------------- end temporary information during check
 315  private:
 316   /** list of all quantifiers seen */
 317   std::map<Node, bool> d_quants;
 318   /** quantifiers pre-registered */
 319   NodeSet d_quants_prereg;
 320   /** quantifiers reduced */
 321   BoolMap d_quants_red;
 322   std::map<Node, Node> d_quants_red_lem;
 323   /** has presolve been called */
 324   context::CDO<bool> d_presolve;
 325   /** presolve cache */
 326   NodeSet d_presolve_in;
 327   NodeList d_presolve_cache;
 328 };/* class QuantifiersEngine */
 329
 330 }/* CVC4::theory namespace */
 331 }/* CVC4 namespace */
 332
 333 #endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */