(Refactor) Instantiate utility (#1387)

1 files changed, 377 insertions, 0 deletions

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
new file mode 100644
index 000000000..d1973eadb
--- /dev/null
+++ b/src/theory/quantifiers/instantiate.h
@@ -0,0 +1,377 @@
+/*********************                                                        */
+/*! \file instantiate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief instantiate
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDb;
+class TermUtil;
+
+/** instantiation notify
+ *
+ * This class is a listener for all instantiations generated with quantifiers.
+ * By default, no notify classes are used. For an example of an instantiation
+ * notify class, see quantifiers/inst_propagate.h, which has a notify class
+ * that recognizes when the set of enqueued instantiations form a conflict.
+ */
+class InstantiationNotify
+{
+ public:
+  InstantiationNotify() {}
+  virtual ~InstantiationNotify() {}
+  /** notify instantiation
+   *
+   * This is called when an instantiation of quantified formula q is
+   * instantiated by a substitution whose range is terms at quantifier effort
+   * quant_e. Furthermore:
+   *   body is the substituted, preprocessed body of the quantified formula,
+   *   lem is the instantiation lemma ( ~q V body ) after rewriting.
+   */
+  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                                   Node q,
+                                   Node lem,
+                                   std::vector<Node>& terms,
+                                   Node body) = 0;
+  /** filter instantiations
+   *
+   * This is called just before the quantifiers engine flushes its lemmas to the
+   * output channel. During this call, the instantiation notify object may
+   * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation
+   * to remove instantiations that should not be sent on the output channel.
+   */
+  virtual void filterInstantiations() = 0;
+};
+
+/** Instantiate
+ *
+ * This class is used for generating instantiation lemmas.  It maintains an
+ * instantiation trie, which is represented by a different data structure
+ * depending on whether incremental solving is enabled (see d_inst_match_trie
+ * and d_c_inst_match_trie).
+ *
+ * Below, we say an instantiation lemma for q = forall x. F under substitution
+ * { x -> t } is the formula:
+ *   ( ~forall x. F V F * { x -> t } )
+ * where * is application of substitution.
+ *
+ * Its main interface is ::addInstantiation(...), which is called by many of
+ * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
+ * engine via calls to QuantifiersEngine::addLemma.
+ *
+ * It also has utilities for constructing instantiations, and interfaces for
+ * getting the results of the instantiations produced during check-sat calls.
+ */
+class Instantiate : public QuantifiersUtil
+{
+ public:
+  Instantiate(QuantifiersEngine* qe, context::UserContext* u);
+  ~Instantiate();
+
+  /** reset */
+  virtual bool reset(Theory::Effort e) override;
+  /** register quantifier */
+  virtual void registerQuantifier(Node q) override;
+  /** identify */
+  virtual std::string identify() const override { return "Instantiate"; }
+  /** check incomplete */
+  virtual bool checkComplete() override;
+
+  //--------------------------------------notify objects
+  /** add instantiation notify
+   *
+   * Adds an instantiation notify class to listen to the instantiations reported
+   * to this class.
+   */
+  void addNotify(InstantiationNotify* in);
+  /** get number of instantiation notify added to this class */
+  bool hasNotify() const { return !d_inst_notify.empty(); }
+  /** notify flush lemmas
+   *
+   * This is called just before the quantifiers engine flushes its lemmas to
+   * the output channel.
+   */
+  void notifyFlushLemmas();
+  //--------------------------------------end notify objects
+
+  /** do instantiation specified by m
+   *
+   * This function returns true if the instantiation lemma for quantified
+   * formula q for the substitution specified by m is successfully enqueued
+   * via a call to QuantifiersEngine::addLemma.
+   *   mkRep : whether to take the representatives of the terms in the range of
+   *           the substitution m,
+   *   modEq : whether to check for duplication modulo equality in instantiation
+   *           tries (for performance),
+   *   doVts : whether we must apply virtual term substitution to the
+   *           instantiation lemma.
+   *
+   * This call may fail if it can be determined that the instantiation is not
+   * relevant or legal in the current context. This happens if:
+   * (1) The substitution is not well-typed,
+   * (2) The substitution involves terms whose instantiation level is above the
+   *     allowed limit,
+   * (3) The resulting instantiation is entailed in the current context using a
+   *     fast entailment check (see TermDb::isEntailed),
+   * (4) The range of the substitution is a duplicate of that of a previously
+   *     added instantiation,
+   * (5) The instantiation lemma is a duplicate of previously added lemma.
+   *
+   */
+  bool addInstantiation(Node q,
+                        InstMatch& m,
+                        bool mkRep = false,
+                        bool modEq = false,
+                        bool doVts = false);
+  /** add instantiation
+   *
+   * Same as above, but the substitution we are considering maps the variables
+   * of q to the vector terms, in order.
+   */
+  bool addInstantiation(Node q,
+                        std::vector<Node>& terms,
+                        bool mkRep = false,
+                        bool modEq = false,
+                        bool doVts = false);
+  /** remove pending instantiation
+   *
+   * Removes the instantiation lemma lem from the instantiation trie.
+   */
+  bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms);
+  /** record instantiation
+   *
+   * Explicitly record that q has been instantiated with terms. This is the
+   * same as addInstantiation, but does not enqueue an instantiation lemma.
+   */
+  bool recordInstantiation(Node q,
+                           std::vector<Node>& terms,
+                           bool modEq = false,
+                           bool addedLem = true);
+  /** exists instantiation
+   *
+   * Returns true if and only if the instantiation already was added or
+   * recorded by this class.
+   *   modEq : whether to check for duplication modulo equality
+   */
+  bool existsInstantiation(Node q,
+                           std::vector<Node>& terms,
+                           bool modEq = false);
+  //--------------------------------------general utilities
+  /** get instantiation
+   *
+   * Returns the instantiation lemma for q under substitution { vars -> terms }.
+   * doVts is whether to apply virtual term substitution to its body.
+   */
+  Node getInstantiation(Node q,
+                        std::vector<Node>& vars,
+                        std::vector<Node>& terms,
+                        bool doVts = false);
+  /** get instantiation
+   *
+   * Same as above, but with vars/terms specified by InstMatch m.
+   */
+  Node getInstantiation(Node q, InstMatch& m, bool doVts = false);
+  /** get instantiation
+   *
+   * Same as above but with vars equal to the bound variables of q.
+   */
+  Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
+  /** get term for type
+   *
+   * This returns an arbitrary term for type tn.
+   * This term is chosen heuristically to be the best
+   * term for instantiation. Currently, this
+   * heuristic enumerates the first term of the
+   * type if the type is closed enumerable, otherwise
+   * an existing ground term from the term database if
+   * one exists, or otherwise a fresh variable.
+   */
+  Node getTermForType(TypeNode tn);
+  //--------------------------------------end general utilities
+
+  /** debug print, called once per instantiation round. */
+  void debugPrint();
+  /** debug print model, called once, before we terminate with sat/unknown. */
+  void debugPrintModel();
+
+  //--------------------------------------user-level interface utilities
+  /** print instantiations
+   *
+   * Print all instantiations for all quantified formulas on out,
+   * returns true if at least one instantiation was printed.
+   */
+  bool printInstantiations(std::ostream& out);
+  /** get instantiated quantified formulas
+   *
+   * Get the list of quantified formulas that were instantiated in the current
+   * user context, store them in qs.
+   */
+  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+  /** get instantiations
+   *
+   * Get the body of all instantiation lemmas added in the current user context
+   * for quantified formula q, store them in insts.
+   */
+  void getInstantiations(Node q, std::vector<Node>& insts);
+  /** get instantiations
+   *
+   * Get the body of all instantiation lemmas added in the current user context
+   * for all quantified formulas stored in the domain of insts, store them in
+   * the range of insts.
+   */
+  void getInstantiations(std::map<Node, std::vector<Node> >& insts);
+  /** get instantiation term vectors
+   *
+   * Get term vectors corresponding to for all instantiations lemmas added in
+   * the current user context for quantified formula q, store them in tvecs.
+   */
+  void getInstantiationTermVectors(Node q,
+                                   std::vector<std::vector<Node> >& tvecs);
+  /** get instantiation term vectors
+   *
+   * Get term vectors for all instantiations lemmas added in the current user
+   * context for quantified formula q, store them in tvecs.
+   */
+  void getInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node> > >& insts);
+  /** get instantiated conjunction
+   *
+   * This gets a conjunction of the bodies of instantiation lemmas added in the
+   * current user context for quantified formula q.  For example, if we added:
+   *   ~forall x. P( x ) V P( a )
+   *   ~forall x. P( x ) V P( b )
+   * Then, this method returns P( a ) ^ P( b ).
+   */
+  Node getInstantiatedConjunction(Node q);
+  /** get unsat core lemmas
+   *
+   * If this method returns true, then it appends to active_lemmas all lemmas
+   * that are in the unsat core that originated from the theory of quantifiers.
+   * This method returns false if the unsat core is not available.
+   */
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+  /** get unsat core lemmas
+   *
+   * If this method returns true, then it appends to active_lemmas all lemmas
+   * that are in the unsat core that originated from the theory of quantifiers.
+   * This method returns false if the unsat core is not available.
+   *
+   * It also computes a weak implicant for each of these lemmas. For each lemma
+   * L in active_lemmas, this is a formula L' such that:
+   *   L => L'
+   * and replacing L by L' in the unsat core results in a set that is still
+   * unsatisfiable. The map weak_imp stores this formula for each formula in
+   * active_lemmas.
+   */
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+                          std::map<Node, Node>& weak_imp);
+  /** get explanation for instantiation lemmas
+   *
+   *
+   */
+  void getExplanationForInstLemmas(const std::vector<Node>& lems,
+                                   std::map<Node, Node>& quant,
+                                   std::map<Node, std::vector<Node> >& tvec);
+  //--------------------------------------end user-level interface utilities
+
+  /** statistics class
+   *
+   * This tracks statistics on the number of instantiations successfully
+   * enqueued on the quantifiers output channel, and the number of redundant
+   * instantiations encountered by various criteria.
+   */
+  class Statistics
+  {
+   public:
+    IntStat d_instantiations;
+    IntStat d_inst_duplicate;
+    IntStat d_inst_duplicate_eq;
+    IntStat d_inst_duplicate_ent;
+    IntStat d_inst_duplicate_model_true;
+    Statistics();
+    ~Statistics();
+  }; /* class Instantiate::Statistics */
+  Statistics d_statistics;
+
+ private:
+  /** record instantiation, return true if it was not a duplicate
+   *
+   * addedLem : whether an instantiation lemma was added for the vector we are
+   *            recording. If this is false, we bookkeep the vector.
+   * modEq : whether to check for duplication modulo equality in instantiation
+   *         tries (for performance),
+   */
+  bool recordInstantiationInternal(Node q,
+                                   std::vector<Node>& terms,
+                                   bool modEq = false,
+                                   bool addedLem = true);
+  /** remove instantiation from the cache */
+  bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
+
+  /** pointer to the quantifiers engine */
+  QuantifiersEngine* d_qe;
+  /** cache of term database for quantifiers engine */
+  TermDb* d_term_db;
+  /** cache of term util for quantifiers engine */
+  TermUtil* d_term_util;
+  /** instantiation notify classes */
+  std::vector<InstantiationNotify*> d_inst_notify;
+
+  /** statistics for debugging total instantiation */
+  int d_total_inst_count_debug;
+  /** statistics for debugging total instantiations per quantifier */
+  std::map<Node, int> d_total_inst_debug;
+  /** statistics for debugging total instantiations per quantifier per round */
+  std::map<Node, int> d_temp_inst_debug;
+
+  /** list of all instantiations produced for each quantifier
+   *
+   * We store context (dependent, independent) versions. If incremental solving
+   * is disabled, we use d_inst_match_trie for performance reasons.
+   */
+  std::map<Node, inst::InstMatchTrie> d_inst_match_trie;
+  std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie;
+  /**
+   * The list of quantified formulas for which the domain of d_c_inst_match_trie
+   * is valid.
+   */
+  context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
+
+  /** explicitly recorded instantiations
+   *
+   * Sometimes an instantiation is recorded internally but not sent out as a
+   * lemma, for instance, for partial quantifier elimination. This is a map
+   * of these instantiations, for each quantified formula.
+   */
+  std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */