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