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