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