GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus_inst.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
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
38
  ~SygusInst() = default;
71
72
  bool needsCheck(Theory::Effort e) override;
73
74
  QEffort needsModel(Theory::Effort e) override;
75
76
  void reset_round(Theory::Effort e) override;
77
78
  void check(Theory::Effort e, QEffort quant_e) override;
79
80
  bool checkCompleteFor(Node q) override;
81
82
  /* Called once for every quantifier 'q' globally (not dependent on context).
83
   */
84
  void registerQuantifier(Node q) override;
85
86
  /* Called once for every quantifier 'q' per context. */
87
  void preRegisterQuantifier(Node q) override;
88
89
  /* For collecting global terms from all available assertions. */
90
  void ppNotifyAssertions(const std::vector<Node>& assertions);
91
92
379
  std::string identify() const override { return "SygusInst"; }
93
94
 private:
95
  /* Lookup counterexample literal or create a new one for quantifier 'q'. */
96
  Node getCeLiteral(Node q);
97
98
  /* Generate counterexample lemma for quantifier 'q'. This is done once per
99
   * quantifier on registerQuantifier() calls. */
100
  void registerCeLemma(Node q, std::vector<TypeNode>& dtypes);
101
102
  /* Add counterexample lemma for quantifier 'q'. This is done on every
103
   * preRegisterQuantifier() call.*/
104
  void addCeLemma(Node q);
105
106
  /* Send evaluation unfolding lemmas and cache them.
107
   * Returns true if a new lemma (not cached) was added, and false otherwise.
108
   */
109
  bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas);
110
111
  /* Maps quantifiers to a vector of instantiation constants. */
112
  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
113
      d_inst_constants;
114
115
  /* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */
116
  std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_var_eval;
117
118
  /* Maps quantified formulas to registered counterexample literals. */
119
  std::unordered_map<Node, Node, NodeHashFunction> d_ce_lits;
120
121
  /* Decision strategies registered for quantified formulas. */
122
  std::unordered_map<Node, std::unique_ptr<DecisionStrategy>, NodeHashFunction>
123
      d_dstrat;
124
125
  /* Currently active quantifiers. */
126
  std::unordered_set<Node, NodeHashFunction> d_active_quant;
127
128
  /* Currently inactive quantifiers. */
129
  std::unordered_set<Node, NodeHashFunction> d_inactive_quant;
130
131
  /* Registered counterexample lemma cache. */
132
  std::unordered_map<Node, Node, NodeHashFunction> d_ce_lemmas;
133
134
  /* Indicates whether a counterexample lemma was added for a quantified
135
   * formula in the current context. */
136
  context::CDHashSet<Node, NodeHashFunction> d_ce_lemma_added;
137
138
  /* Set of global ground terms in assertions (outside of quantifiers). */
139
  context::CDHashMap<TypeNode,
140
                     std::unordered_set<Node, NodeHashFunction>,
141
                     TypeNodeHashFunction>
142
      d_global_terms;
143
144
  /* Assertions sent by ppNotifyAssertions. */
145
  context::CDHashSet<Node, NodeHashFunction> d_notified_assertions;
146
};
147
148
}  // namespace quantifiers
149
}  // namespace theory
150
}  // namespace CVC4
151
152
#endif