1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* 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 |
|
* Higher-order term database class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H |
19 |
|
#define CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H |
20 |
|
|
21 |
|
#include <map> |
22 |
|
|
23 |
|
#include "expr/node.h" |
24 |
|
#include "theory/quantifiers/term_database.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace quantifiers { |
29 |
|
|
30 |
|
/** |
31 |
|
* Higher-order term database, which extends the normal term database based on |
32 |
|
* techniques from Barbosa et al CADE 2019. |
33 |
|
*/ |
34 |
|
class HoTermDb : public TermDb |
35 |
|
{ |
36 |
|
public: |
37 |
|
HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr); |
38 |
|
~HoTermDb(); |
39 |
|
/** identify */ |
40 |
934 |
std::string identify() const override { return "HoTermDb"; } |
41 |
|
/** get higher-order type match predicate |
42 |
|
* |
43 |
|
* This predicate is used to force certain functions f of type tn to appear as |
44 |
|
* first-class representatives in the quantifier-free UF solver. For a typical |
45 |
|
* use case, we call getHoTypeMatchPredicate which returns a fresh predicate |
46 |
|
* P of type (tn -> Bool). Then, we add P( f ) as a lemma. |
47 |
|
*/ |
48 |
|
static Node getHoTypeMatchPredicate(TypeNode tn); |
49 |
|
|
50 |
|
private: |
51 |
|
/** |
52 |
|
* Reset internal, called when reset(e) is called. Returning false will cause |
53 |
|
* the overall reset to terminate early, returning false. |
54 |
|
*/ |
55 |
|
bool resetInternal(Theory::Effort e) override; |
56 |
|
/** Performs merging of term indices based on higher-order reasoning */ |
57 |
|
bool finishResetInternal(Theory::Effort e) override; |
58 |
|
/** add term higher-order |
59 |
|
* |
60 |
|
* This registers additional terms corresponding to (possibly multiple) |
61 |
|
* purifications of a higher-order term n. |
62 |
|
* |
63 |
|
* Consider the example: |
64 |
|
* g : Int -> Int, f : Int x Int -> Int |
65 |
|
* constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3 |
66 |
|
* pattern: (g x) |
67 |
|
* where @ is HO_APPLY. |
68 |
|
* We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1). |
69 |
|
* With the standard registration in addTerm, we construct term indices for |
70 |
|
* f, g, @ : Int x Int -> Int, @ : Int -> Int. |
71 |
|
* However, to match (g x) with (@ (@ f 0) 1), we require that |
72 |
|
* [1] -> (@ (@ f 0) 1) |
73 |
|
* is an entry in the term index of g. To do this, we maintain a term |
74 |
|
* index for a fresh variable pfun, the purification variable for |
75 |
|
* (@ f 0). Thus, we register the term (pfun 1) in the call to this function |
76 |
|
* for (@ (@ f 0) 1). This ensures that, when processing the equality |
77 |
|
* (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry |
78 |
|
* [1] -> (@ (@ f 0) 1) |
79 |
|
* is added to the term index of g, assuming g is the representative of |
80 |
|
* the equivalence class of g and pfun. |
81 |
|
* |
82 |
|
* Above, we set d_hoFunOpPurify[(@ f 0)] = pfun, and |
83 |
|
* d_hoPurifyToTerm[(pfun 1)] = (@ (@ f 0) 1). |
84 |
|
*/ |
85 |
|
void addTermInternal(Node n) override; |
86 |
|
/** Get operators that we know are equivalent to f */ |
87 |
|
void getOperatorsFor(TNode f, std::vector<TNode>& ops) override; |
88 |
|
/** get the chosen representative for operator op */ |
89 |
|
Node getOperatorRepresentative(TNode op) const override; |
90 |
|
/** check if we are in conflict based on congruent terms a and b */ |
91 |
|
bool checkCongruentDisequal(TNode a, |
92 |
|
TNode b, |
93 |
|
std::vector<Node>& exp) override; |
94 |
|
//------------------------------higher-order term indexing |
95 |
|
/** |
96 |
|
* Map from non-variable function terms to the operator used to purify it in |
97 |
|
* this database. For details, see addTermHo. |
98 |
|
*/ |
99 |
|
std::map<Node, Node> d_hoFunOpPurify; |
100 |
|
/** |
101 |
|
* Map from terms to the term that they purified. For details, see addTermHo. |
102 |
|
*/ |
103 |
|
std::map<Node, Node> d_hoPurifyToTerm; |
104 |
|
/** |
105 |
|
* Map from terms in the domain of the above map to an equality between that |
106 |
|
* term and its range in the above map. |
107 |
|
*/ |
108 |
|
std::map<Node, Node> d_hoPurifyToEq; |
109 |
|
/** a map from matchable operators to their representative */ |
110 |
|
std::map<TNode, TNode> d_hoOpRep; |
111 |
|
/** for each representative matchable operator, the list of other matchable |
112 |
|
* operators in their equivalence class */ |
113 |
|
std::map<TNode, std::vector<TNode> > d_hoOpSlaves; |
114 |
|
}; |
115 |
|
|
116 |
|
} // namespace quantifiers |
117 |
|
} // namespace theory |
118 |
|
} // namespace cvc5 |
119 |
|
|
120 |
|
#endif /* CVC5__THEORY__QUANTIFIERS__HO_TERM_DATABASE_H */ |