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
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Mathias Preiner, Tim King
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* Equality query class.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
#include "theory/quantifiers/quant_util.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
class FirstOrderModel;
class QuantifiersState;
/** EqualityQuery class
*
* The main method of this class is the function
* getInternalRepresentative, which is used by instantiation-based methods
* that are agnostic with respect to choosing terms within an equivalence class.
* Examples of such methods are finite model finding and enumerative
* instantiation. Method getInternalRepresentative returns the "best"
* representative based on the internal heuristic, which is currently based on
* choosing the term that was previously chosen as a representative earliest.
*/
class EqualityQuery : public QuantifiersUtil
{
public:
EqualityQuery(QuantifiersState& qs, FirstOrderModel* m);
virtual ~EqualityQuery();
/** reset */
bool reset(Theory::Effort e) override;
/* Called for new quantifiers */
void registerQuantifier(Node q) override {}
/** identify */
std::string identify() const override { return "EqualityQuery"; }
/** gets the current best representative in the equivalence
* class of a, based on some heuristic. Currently, the default heuristic
* chooses terms that were previously chosen as representatives
* on the earliest instantiation round.
*
* If q is non-null, then q/index is the quantified formula
* and variable position that we are choosing for instantiation.
*
* This function avoids certain terms that are "ineligible" for instantiation.
* If cbqi is active, we terms that contain instantiation constants
* are ineligible. As a result, this function may return
* Node::null() if all terms in the equivalence class of a
* are ineligible.
*/
Node getInternalRepresentative(Node a, Node q, size_t index);
private:
/** the quantifiers state */
QuantifiersState& d_qstate;
/** Pointer to the model */
FirstOrderModel* d_model;
/** quantifiers equality inference */
context::CDO< unsigned > d_eqi_counter;
/** internal representatives */
std::map< TypeNode, std::map< Node, Node > > d_int_rep;
/** rep score */
std::map<Node, int32_t> d_rep_score;
/** the number of times reset( e ) has been called */
size_t d_reset_count;
/** processInferences : will merge equivalence classes in master equality engine, if possible */
bool processInferences( Theory::Effort e );
/** node contains */
Node getInstance(Node n,
const std::vector<Node>& eqc,
std::unordered_map<TNode, Node>& cache);
/** get score */
int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn);
}; /* EqualityQuery */
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
|
