src/theory/quantifiers/sygus_inst.h

   1 /*********************                                                        */
   2 /*! \file sygus_inst.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 SyGuS instantiator class.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
  18 #define CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
  19
  20 #include <unordered_map>
  21 #include <unordered_set>
  22
  23 #include "context/cdhashset.h"
  24 #include "theory/decision_strategy.h"
  25 #include "theory/quantifiers/quant_module.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 class QuantifiersEngine;
  31
  32 namespace quantifiers {
  33
  34 /**
  35  * SyGuS quantifier instantion module.
  36  *
  37  * This module uses SyGuS techniques to find terms for instantiation and
  38  * combines it with counterexample guided instantiation. It uses the datatypes
  39  * solver to find instantiation for each variable based on a specified SyGuS
  40  * grammar.
  41  *
  42  * The CE lemma generated for a quantified formula
  43  *
  44  *   \forall x . P[x]
  45  *
  46  * is
  47  *
  48  *   ce_lit => ~P[DT_SYGUS_EVAL(dt_x)]
  49  *
  50  * where ce_lit is a the counterexample literal for the quantified formula and
  51  * dt_x is a fresh datatype variable with the SyGuS grammar for x as type.
  52  *
  53  * While checking, for active quantifiers, we add (full) evaluation unfolding
  54  * lemmas as follows (see Reynolds at al. CAV 2019b for more information):
  55  *
  56  *   explain(dt_x=dt_x^M) => DT_SYGUS_EVAL(dt_x) = t
  57  *
  58  * where t = sygusToBuiltin(dt_x^M).
  59  *
  60  * We collect the t_i for each bound variable x_i and use them to instantiate
  61  * the quantified formula.
  62  */
  63 class SygusInst : public QuantifiersModule
  64 {
  65  public:
  66   SygusInst(QuantifiersEngine* qe,
  67             QuantifiersState& qs,
  68             QuantifiersInferenceManager& qim,
  69             QuantifiersRegistry& qr,
  70             TermRegistry& tr);
  71   ~SygusInst() = default;
  72
  73   bool needsCheck(Theory::Effort e) override;
  74
  75   QEffort needsModel(Theory::Effort e) override;
  76
  77   void reset_round(Theory::Effort e) override;
  78
  79   void check(Theory::Effort e, QEffort quant_e) override;
  80
  81   bool checkCompleteFor(Node q) override;
  82
  83   /* Called once for every quantifier 'q' globally (not dependent on context).
  84    */
  85   void registerQuantifier(Node q) override;
  86
  87   /* Called once for every quantifier 'q' per context. */
  88   void preRegisterQuantifier(Node q) override;
  89
  90   /* For collecting global terms from all available assertions. */
  91   void ppNotifyAssertions(const std::vector<Node>& assertions);
  92
  93   std::string identify() const override { return "SygusInst"; }
  94
  95  private:
  96   /* Lookup counterexample literal or create a new one for quantifier 'q'. */
  97   Node getCeLiteral(Node q);
  98
  99   /* Generate counterexample lemma for quantifier 'q'. This is done once per
 100    * quantifier on registerQuantifier() calls. */
 101   void registerCeLemma(Node q, std::vector<TypeNode>& dtypes);
 102
 103   /* Add counterexample lemma for quantifier 'q'. This is done on every
 104    * preRegisterQuantifier() call.*/
 105   void addCeLemma(Node q);
 106
 107   /* Send evaluation unfolding lemmas and cache them.
 108    * Returns true if a new lemma (not cached) was added, and false otherwise.
 109    */
 110   bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas);
 111
 112   /* Maps quantifiers to a vector of instantiation constants. */
 113   std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
 114       d_inst_constants;
 115
 116   /* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */
 117   std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_var_eval;
 118
 119   /* Maps quantified formulas to registered counterexample literals. */
 120   std::unordered_map<Node, Node, NodeHashFunction> d_ce_lits;
 121
 122   /* Decision strategies registered for quantified formulas. */
 123   std::unordered_map<Node, std::unique_ptr<DecisionStrategy>, NodeHashFunction>
 124       d_dstrat;
 125
 126   /* Currently active quantifiers. */
 127   std::unordered_set<Node, NodeHashFunction> d_active_quant;
 128
 129   /* Currently inactive quantifiers. */
 130   std::unordered_set<Node, NodeHashFunction> d_inactive_quant;
 131
 132   /* Registered counterexample lemma cache. */
 133   std::unordered_map<Node, Node, NodeHashFunction> d_ce_lemmas;
 134
 135   /* Indicates whether a counterexample lemma was added for a quantified
 136    * formula in the current context. */
 137   context::CDHashSet<Node, NodeHashFunction> d_ce_lemma_added;
 138
 139   /* Set of global ground terms in assertions (outside of quantifiers). */
 140   context::CDHashMap<TypeNode,
 141                      std::unordered_set<Node, NodeHashFunction>,
 142                      TypeNodeHashFunction>
 143       d_global_terms;
 144
 145   /* Assertions sent by ppNotifyAssertions. */
 146   context::CDHashSet<Node, NodeHashFunction> d_notified_assertions;
 147 };
 148
 149 }  // namespace quantifiers
 150 }  // namespace theory
 151 }  // namespace CVC4
 152
 153 #endif