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
|
/********************* */
/*! \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/quantifiers/quant_util.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);
~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;
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);
/* Maps bound variables to corresponding instantiation constants. */
std::unordered_map<Node, Node, NodeHashFunction> d_inst_constants;
/* Maps bound variables to corresponding DT_SYGUS_EVAL term. */
std::unordered_map<Node, 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;
/* Evaluation unfolding lemma. */
context::CDHashSet<Node, NodeHashFunction> d_lemma_cache;
/* 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;
};
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#endif
|
