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