src/theory/quantifiers/instantiate.h

   1 /*********************                                                        */
   2 /*! \file instantiate.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Morgan Deters
   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 instantiate
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
  18 #define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
  19
  20 #include <map>
  21
  22 #include "expr/node.h"
  23 #include "theory/quantifiers/inst_match_trie.h"
  24 #include "theory/quantifiers/quant_util.h"
  25 #include "util/statistics_registry.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 class QuantifiersEngine;
  31
  32 namespace quantifiers {
  33
  34 class TermDb;
  35 class TermUtil;
  36
  37 /** instantiation notify
  38  *
  39  * This class is a listener for all instantiations generated with quantifiers.
  40  * By default, no notify classes are used. For an example of an instantiation
  41  * notify class, see quantifiers/inst_propagate.h, which has a notify class
  42  * that recognizes when the set of enqueued instantiations form a conflict.
  43  */
  44 class InstantiationNotify
  45 {
  46  public:
  47   InstantiationNotify() {}
  48   virtual ~InstantiationNotify() {}
  49   /** notify instantiation
  50    *
  51    * This is called when an instantiation of quantified formula q is
  52    * instantiated by a substitution whose range is terms at quantifier effort
  53    * quant_e. Furthermore:
  54    *   body is the substituted, preprocessed body of the quantified formula,
  55    *   lem is the instantiation lemma ( ~q V body ) after rewriting.
  56    */
  57   virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
  58                                    Node q,
  59                                    Node lem,
  60                                    std::vector<Node>& terms,
  61                                    Node body) = 0;
  62   /** filter instantiations
  63    *
  64    * This is called just before the quantifiers engine flushes its lemmas to the
  65    * output channel. During this call, the instantiation notify object may
  66    * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation
  67    * to remove instantiations that should not be sent on the output channel.
  68    */
  69   virtual void filterInstantiations() = 0;
  70 };
  71
  72 /** Instantiation rewriter
  73  *
  74  * This class is used for cases where instantiation lemmas can be rewritten by
  75  * external utilities. Examples of this include virtual term substitution and
  76  * nested quantifier elimination techniques.
  77  */
  78 class InstantiationRewriter
  79 {
  80  public:
  81   InstantiationRewriter() {}
  82   virtual ~InstantiationRewriter() {}
  83
  84   /** rewrite instantiation
  85    *
  86    * The node inst is the instantiation of quantified formula q for terms.
  87    * This method returns the rewritten form of the instantiation.
  88    *
  89    * The flag doVts is whether we must apply virtual term substitution to the
  90    * instantiation.
  91    */
  92   virtual Node rewriteInstantiation(Node q,
  93                                     std::vector<Node>& terms,
  94                                     Node inst,
  95                                     bool doVts) = 0;
  96 };
  97
  98 /** Instantiate
  99  *
 100  * This class is used for generating instantiation lemmas.  It maintains an
 101  * instantiation trie, which is represented by a different data structure
 102  * depending on whether incremental solving is enabled (see d_inst_match_trie
 103  * and d_c_inst_match_trie).
 104  *
 105  * Below, we say an instantiation lemma for q = forall x. F under substitution
 106  * { x -> t } is the formula:
 107  *   ( ~forall x. F V F * { x -> t } )
 108  * where * is application of substitution.
 109  *
 110  * Its main interface is ::addInstantiation(...), which is called by many of
 111  * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
 112  * engine via calls to QuantifiersEngine::addLemma.
 113  *
 114  * It also has utilities for constructing instantiations, and interfaces for
 115  * getting the results of the instantiations produced during check-sat calls.
 116  */
 117 class Instantiate : public QuantifiersUtil
 118 {
 119  public:
 120   Instantiate(QuantifiersEngine* qe, context::UserContext* u);
 121   ~Instantiate();
 122
 123   /** reset */
 124   bool reset(Theory::Effort e) override;
 125   /** register quantifier */
 126   void registerQuantifier(Node q) override;
 127   /** identify */
 128   std::string identify() const override { return "Instantiate"; }
 129   /** check incomplete */
 130   bool checkComplete() override;
 131
 132   //--------------------------------------notify/rewrite objects
 133   /** add instantiation notify
 134    *
 135    * Adds an instantiation notify class to listen to the instantiations reported
 136    * to this class.
 137    */
 138   void addNotify(InstantiationNotify* in);
 139   /** get number of instantiation notify added to this class */
 140   bool hasNotify() const { return !d_inst_notify.empty(); }
 141   /** add instantiation rewriter */
 142   void addRewriter(InstantiationRewriter* ir);
 143   /** notify flush lemmas
 144    *
 145    * This is called just before the quantifiers engine flushes its lemmas to
 146    * the output channel.
 147    */
 148   void notifyFlushLemmas();
 149   //--------------------------------------end notify objects
 150
 151   /** do instantiation specified by m
 152    *
 153    * This function returns true if the instantiation lemma for quantified
 154    * formula q for the substitution specified by m is successfully enqueued
 155    * via a call to QuantifiersEngine::addLemma.
 156    *   mkRep : whether to take the representatives of the terms in the range of
 157    *           the substitution m,
 158    *   modEq : whether to check for duplication modulo equality in instantiation
 159    *           tries (for performance),
 160    *   doVts : whether we must apply virtual term substitution to the
 161    *           instantiation lemma.
 162    *
 163    * This call may fail if it can be determined that the instantiation is not
 164    * relevant or legal in the current context. This happens if:
 165    * (1) The substitution is not well-typed,
 166    * (2) The substitution involves terms whose instantiation level is above the
 167    *     allowed limit,
 168    * (3) The resulting instantiation is entailed in the current context using a
 169    *     fast entailment check (see TermDb::isEntailed),
 170    * (4) The range of the substitution is a duplicate of that of a previously
 171    *     added instantiation,
 172    * (5) The instantiation lemma is a duplicate of previously added lemma.
 173    *
 174    */
 175   bool addInstantiation(Node q,
 176                         InstMatch& m,
 177                         bool mkRep = false,
 178                         bool modEq = false,
 179                         bool doVts = false);
 180   /** add instantiation
 181    *
 182    * Same as above, but the substitution we are considering maps the variables
 183    * of q to the vector terms, in order.
 184    */
 185   bool addInstantiation(Node q,
 186                         std::vector<Node>& terms,
 187                         bool mkRep = false,
 188                         bool modEq = false,
 189                         bool doVts = false);
 190   /** remove pending instantiation
 191    *
 192    * Removes the instantiation lemma lem from the instantiation trie.
 193    */
 194   bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms);
 195   /** record instantiation
 196    *
 197    * Explicitly record that q has been instantiated with terms. This is the
 198    * same as addInstantiation, but does not enqueue an instantiation lemma.
 199    */
 200   bool recordInstantiation(Node q,
 201                            std::vector<Node>& terms,
 202                            bool modEq = false,
 203                            bool addedLem = true);
 204   /** exists instantiation
 205    *
 206    * Returns true if and only if the instantiation already was added or
 207    * recorded by this class.
 208    *   modEq : whether to check for duplication modulo equality
 209    */
 210   bool existsInstantiation(Node q,
 211                            std::vector<Node>& terms,
 212                            bool modEq = false);
 213   //--------------------------------------general utilities
 214   /** get instantiation
 215    *
 216    * Returns the instantiation lemma for q under substitution { vars -> terms }.
 217    * doVts is whether to apply virtual term substitution to its body.
 218    */
 219   Node getInstantiation(Node q,
 220                         std::vector<Node>& vars,
 221                         std::vector<Node>& terms,
 222                         bool doVts = false);
 223   /** get instantiation
 224    *
 225    * Same as above, but with vars/terms specified by InstMatch m.
 226    */
 227   Node getInstantiation(Node q, InstMatch& m, bool doVts = false);
 228   /** get instantiation
 229    *
 230    * Same as above but with vars equal to the bound variables of q.
 231    */
 232   Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
 233   /** get term for type
 234    *
 235    * This returns an arbitrary term for type tn.
 236    * This term is chosen heuristically to be the best
 237    * term for instantiation. Currently, this
 238    * heuristic enumerates the first term of the
 239    * type if the type is closed enumerable, otherwise
 240    * an existing ground term from the term database if
 241    * one exists, or otherwise a fresh variable.
 242    */
 243   Node getTermForType(TypeNode tn);
 244   //--------------------------------------end general utilities
 245
 246   /** debug print, called once per instantiation round. */
 247   void debugPrint();
 248   /** debug print model, called once, before we terminate with sat/unknown. */
 249   void debugPrintModel();
 250
 251   //--------------------------------------user-level interface utilities
 252   /** print instantiations
 253    *
 254    * Print all instantiations for all quantified formulas on out,
 255    * returns true if at least one instantiation was printed.
 256    */
 257   bool printInstantiations(std::ostream& out);
 258   /** get instantiated quantified formulas
 259    *
 260    * Get the list of quantified formulas that were instantiated in the current
 261    * user context, store them in qs.
 262    */
 263   void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
 264   /** get instantiations
 265    *
 266    * Get the body of all instantiation lemmas added in the current user context
 267    * for quantified formula q, store them in insts.
 268    */
 269   void getInstantiations(Node q, std::vector<Node>& insts);
 270   /** get instantiations
 271    *
 272    * Get the body of all instantiation lemmas added in the current user context
 273    * for all quantified formulas stored in the domain of insts, store them in
 274    * the range of insts.
 275    */
 276   void getInstantiations(std::map<Node, std::vector<Node> >& insts);
 277   /** get instantiation term vectors
 278    *
 279    * Get term vectors corresponding to for all instantiations lemmas added in
 280    * the current user context for quantified formula q, store them in tvecs.
 281    */
 282   void getInstantiationTermVectors(Node q,
 283                                    std::vector<std::vector<Node> >& tvecs);
 284   /** get instantiation term vectors
 285    *
 286    * Get term vectors for all instantiations lemmas added in the current user
 287    * context for quantified formula q, store them in tvecs.
 288    */
 289   void getInstantiationTermVectors(
 290       std::map<Node, std::vector<std::vector<Node> > >& insts);
 291   /** get instantiated conjunction
 292    *
 293    * This gets a conjunction of the bodies of instantiation lemmas added in the
 294    * current user context for quantified formula q.  For example, if we added:
 295    *   ~forall x. P( x ) V P( a )
 296    *   ~forall x. P( x ) V P( b )
 297    * Then, this method returns P( a ) ^ P( b ).
 298    */
 299   Node getInstantiatedConjunction(Node q);
 300   /** get unsat core lemmas
 301    *
 302    * If this method returns true, then it appends to active_lemmas all lemmas
 303    * that are in the unsat core that originated from the theory of quantifiers.
 304    * This method returns false if the unsat core is not available.
 305    */
 306   bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
 307   /** get unsat core lemmas
 308    *
 309    * If this method returns true, then it appends to active_lemmas all lemmas
 310    * that are in the unsat core that originated from the theory of quantifiers.
 311    * This method returns false if the unsat core is not available.
 312    *
 313    * It also computes a weak implicant for each of these lemmas. For each lemma
 314    * L in active_lemmas, this is a formula L' such that:
 315    *   L => L'
 316    * and replacing L by L' in the unsat core results in a set that is still
 317    * unsatisfiable. The map weak_imp stores this formula for each formula in
 318    * active_lemmas.
 319    */
 320   bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
 321                           std::map<Node, Node>& weak_imp);
 322   /** get explanation for instantiation lemmas
 323    *
 324    *
 325    */
 326   void getExplanationForInstLemmas(const std::vector<Node>& lems,
 327                                    std::map<Node, Node>& quant,
 328                                    std::map<Node, std::vector<Node> >& tvec);
 329   //--------------------------------------end user-level interface utilities
 330
 331   /** statistics class
 332    *
 333    * This tracks statistics on the number of instantiations successfully
 334    * enqueued on the quantifiers output channel, and the number of redundant
 335    * instantiations encountered by various criteria.
 336    */
 337   class Statistics
 338   {
 339    public:
 340     IntStat d_instantiations;
 341     IntStat d_inst_duplicate;
 342     IntStat d_inst_duplicate_eq;
 343     IntStat d_inst_duplicate_ent;
 344     IntStat d_inst_duplicate_model_true;
 345     Statistics();
 346     ~Statistics();
 347   }; /* class Instantiate::Statistics */
 348   Statistics d_statistics;
 349
 350  private:
 351   /** record instantiation, return true if it was not a duplicate
 352    *
 353    * addedLem : whether an instantiation lemma was added for the vector we are
 354    *            recording. If this is false, we bookkeep the vector.
 355    * modEq : whether to check for duplication modulo equality in instantiation
 356    *         tries (for performance),
 357    */
 358   bool recordInstantiationInternal(Node q,
 359                                    std::vector<Node>& terms,
 360                                    bool modEq = false,
 361                                    bool addedLem = true);
 362   /** remove instantiation from the cache */
 363   bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
 364
 365   /** pointer to the quantifiers engine */
 366   QuantifiersEngine* d_qe;
 367   /** cache of term database for quantifiers engine */
 368   TermDb* d_term_db;
 369   /** cache of term util for quantifiers engine */
 370   TermUtil* d_term_util;
 371   /** instantiation notify classes */
 372   std::vector<InstantiationNotify*> d_inst_notify;
 373   /** instantiation rewriter classes */
 374   std::vector<InstantiationRewriter*> d_instRewrite;
 375
 376   /** statistics for debugging total instantiation */
 377   int d_total_inst_count_debug;
 378   /** statistics for debugging total instantiations per quantifier */
 379   std::map<Node, int> d_total_inst_debug;
 380   /** statistics for debugging total instantiations per quantifier per round */
 381   std::map<Node, int> d_temp_inst_debug;
 382
 383   /** list of all instantiations produced for each quantifier
 384    *
 385    * We store context (dependent, independent) versions. If incremental solving
 386    * is disabled, we use d_inst_match_trie for performance reasons.
 387    */
 388   std::map<Node, inst::InstMatchTrie> d_inst_match_trie;
 389   std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie;
 390   /**
 391    * The list of quantified formulas for which the domain of d_c_inst_match_trie
 392    * is valid.
 393    */
 394   context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
 395
 396   /** explicitly recorded instantiations
 397    *
 398    * Sometimes an instantiation is recorded internally but not sent out as a
 399    * lemma, for instance, for partial quantifier elimination. This is a map
 400    * of these instantiations, for each quantified formula.
 401    */
 402   std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
 403 };
 404
 405 } /* CVC4::theory::quantifiers namespace */
 406 } /* CVC4::theory namespace */
 407 } /* CVC4 namespace */
 408
 409 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */