1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* SyGuS instantiator class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H |
19 |
|
#define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H |
20 |
|
|
21 |
|
#include <unordered_map> |
22 |
|
#include <unordered_set> |
23 |
|
|
24 |
|
#include "context/cdhashset.h" |
25 |
|
#include "theory/decision_strategy.h" |
26 |
|
#include "theory/quantifiers/quant_module.h" |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
|
31 |
|
class QuantifiersEngine; |
32 |
|
|
33 |
|
namespace quantifiers { |
34 |
|
|
35 |
|
/** |
36 |
|
* SyGuS quantifier instantion module. |
37 |
|
* |
38 |
|
* This module uses SyGuS techniques to find terms for instantiation and |
39 |
|
* combines it with counterexample guided instantiation. It uses the datatypes |
40 |
|
* solver to find instantiation for each variable based on a specified SyGuS |
41 |
|
* grammar. |
42 |
|
* |
43 |
|
* The CE lemma generated for a quantified formula |
44 |
|
* |
45 |
|
* \forall x . P[x] |
46 |
|
* |
47 |
|
* is |
48 |
|
* |
49 |
|
* ce_lit => ~P[DT_SYGUS_EVAL(dt_x)] |
50 |
|
* |
51 |
|
* where ce_lit is a the counterexample literal for the quantified formula and |
52 |
|
* dt_x is a fresh datatype variable with the SyGuS grammar for x as type. |
53 |
|
* |
54 |
|
* While checking, for active quantifiers, we add (full) evaluation unfolding |
55 |
|
* lemmas as follows (see Reynolds at al. CAV 2019b for more information): |
56 |
|
* |
57 |
|
* explain(dt_x=dt_x^M) => DT_SYGUS_EVAL(dt_x) = t |
58 |
|
* |
59 |
|
* where t = sygusToBuiltin(dt_x^M). |
60 |
|
* |
61 |
|
* We collect the t_i for each bound variable x_i and use them to instantiate |
62 |
|
* the quantified formula. |
63 |
|
*/ |
64 |
|
class SygusInst : public QuantifiersModule |
65 |
|
{ |
66 |
|
public: |
67 |
|
SygusInst(QuantifiersState& qs, |
68 |
|
QuantifiersInferenceManager& qim, |
69 |
|
QuantifiersRegistry& qr, |
70 |
|
TermRegistry& tr); |
71 |
40 |
~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 |
377 |
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>> d_inst_constants; |
114 |
|
|
115 |
|
/* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */ |
116 |
|
std::unordered_map<Node, std::vector<Node>> d_var_eval; |
117 |
|
|
118 |
|
/* Maps quantified formulas to registered counterexample literals. */ |
119 |
|
std::unordered_map<Node, Node> d_ce_lits; |
120 |
|
|
121 |
|
/* Decision strategies registered for quantified formulas. */ |
122 |
|
std::unordered_map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat; |
123 |
|
|
124 |
|
/* Currently active quantifiers. */ |
125 |
|
std::unordered_set<Node> d_active_quant; |
126 |
|
|
127 |
|
/* Currently inactive quantifiers. */ |
128 |
|
std::unordered_set<Node> d_inactive_quant; |
129 |
|
|
130 |
|
/* Registered counterexample lemma cache. */ |
131 |
|
std::unordered_map<Node, Node> d_ce_lemmas; |
132 |
|
|
133 |
|
/* Indicates whether a counterexample lemma was added for a quantified |
134 |
|
* formula in the current context. */ |
135 |
|
context::CDHashSet<Node> d_ce_lemma_added; |
136 |
|
|
137 |
|
/* Set of global ground terms in assertions (outside of quantifiers). */ |
138 |
|
context::CDHashMap<TypeNode, std::unordered_set<Node>> d_global_terms; |
139 |
|
|
140 |
|
/* Assertions sent by ppNotifyAssertions. */ |
141 |
|
context::CDHashSet<Node> d_notified_assertions; |
142 |
|
}; |
143 |
|
|
144 |
|
} // namespace quantifiers |
145 |
|
} // namespace theory |
146 |
|
} // namespace cvc5 |
147 |
|
|
148 |
|
#endif |