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