1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Tim King |
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 |
|
* Equality query class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H |
19 |
|
#define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H |
20 |
|
|
21 |
|
#include "context/cdo.h" |
22 |
|
#include "context/context.h" |
23 |
|
#include "expr/node.h" |
24 |
|
#include "theory/quantifiers/quant_util.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace quantifiers { |
29 |
|
|
30 |
|
class FirstOrderModel; |
31 |
|
class QuantifiersState; |
32 |
|
|
33 |
|
/** EqualityQuery class |
34 |
|
* |
35 |
|
* The main method of this class is the function |
36 |
|
* getInternalRepresentative, which is used by instantiation-based methods |
37 |
|
* that are agnostic with respect to choosing terms within an equivalence class. |
38 |
|
* Examples of such methods are finite model finding and enumerative |
39 |
|
* instantiation. Method getInternalRepresentative returns the "best" |
40 |
|
* representative based on the internal heuristic, which is currently based on |
41 |
|
* choosing the term that was previously chosen as a representative earliest. |
42 |
|
*/ |
43 |
|
class EqualityQuery : public QuantifiersUtil |
44 |
|
{ |
45 |
|
public: |
46 |
|
EqualityQuery(QuantifiersState& qs, FirstOrderModel* m); |
47 |
|
virtual ~EqualityQuery(); |
48 |
|
|
49 |
|
/** reset */ |
50 |
|
bool reset(Theory::Effort e) override; |
51 |
|
/* Called for new quantifiers */ |
52 |
25053 |
void registerQuantifier(Node q) override {} |
53 |
|
/** identify */ |
54 |
24825 |
std::string identify() const override { return "EqualityQuery"; } |
55 |
|
/** gets the current best representative in the equivalence |
56 |
|
* class of a, based on some heuristic. Currently, the default heuristic |
57 |
|
* chooses terms that were previously chosen as representatives |
58 |
|
* on the earliest instantiation round. |
59 |
|
* |
60 |
|
* If q is non-null, then q/index is the quantified formula |
61 |
|
* and variable position that we are choosing for instantiation. |
62 |
|
* |
63 |
|
* This function avoids certain terms that are "ineligible" for instantiation. |
64 |
|
* If cbqi is active, we terms that contain instantiation constants |
65 |
|
* are ineligible. As a result, this function may return |
66 |
|
* Node::null() if all terms in the equivalence class of a |
67 |
|
* are ineligible. |
68 |
|
*/ |
69 |
|
Node getInternalRepresentative(Node a, Node q, size_t index); |
70 |
|
|
71 |
|
private: |
72 |
|
/** the quantifiers state */ |
73 |
|
QuantifiersState& d_qstate; |
74 |
|
/** Pointer to the model */ |
75 |
|
FirstOrderModel* d_model; |
76 |
|
/** quantifiers equality inference */ |
77 |
|
context::CDO< unsigned > d_eqi_counter; |
78 |
|
/** internal representatives */ |
79 |
|
std::map< TypeNode, std::map< Node, Node > > d_int_rep; |
80 |
|
/** rep score */ |
81 |
|
std::map<Node, int32_t> d_rep_score; |
82 |
|
/** the number of times reset( e ) has been called */ |
83 |
|
size_t d_reset_count; |
84 |
|
/** processInferences : will merge equivalence classes in master equality engine, if possible */ |
85 |
|
bool processInferences( Theory::Effort e ); |
86 |
|
/** node contains */ |
87 |
|
Node getInstance(Node n, |
88 |
|
const std::vector<Node>& eqc, |
89 |
|
std::unordered_map<TNode, Node>& cache); |
90 |
|
/** get score */ |
91 |
|
int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn); |
92 |
|
}; /* EqualityQuery */ |
93 |
|
|
94 |
|
} // namespace quantifiers |
95 |
|
} // namespace theory |
96 |
|
} // namespace cvc5 |
97 |
|
|
98 |
|
#endif /* CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ |