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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
/********************* */
/*! \file equality_query.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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.\endverbatim
**
** \brief Equality query class
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
/** EqualityQueryQuantifiersEngine class
* This is a wrapper class around an equality engine that is used for
* queries required by algorithms in the quantifiers theory.
* It uses an equality engine, as determined by the quantifiers engine it points
* to.
*
* The main extension of this class wrt EqualityQuery 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 EqualityQueryQuantifiersEngine : public EqualityQuery
{
public:
EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
virtual ~EqualityQueryQuantifiersEngine();
/** reset */
bool reset(Theory::Effort e) override;
/* Called for new quantifiers */
void registerQuantifier(Node q) override {}
/** identify */
std::string identify() const override { return "EqualityQueryQE"; }
/** does the equality engine have term a */
bool hasTerm(Node a) override;
/** get the representative of a */
Node getRepresentative(Node a) override;
/** are a and b equal? */
bool areEqual(Node a, Node b) override;
/** are a and b disequal? */
bool areDisequal(Node a, Node b) override;
/** get equality engine
* This may either be the master equality engine or the model's equality
* engine.
*/
eq::EqualityEngine* getEngine() override;
/** get list of members in the equivalence class of a */
void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
/** get congruent term
* If possible, returns a term n such that:
* (1) n is a term in the equality engine from getEngine().
* (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class
* of args[i] for i=1...k
* Otherwise, returns the null node.
*
* Notice that f should be a "match operator", returned by
* TermDb::getMatchOperator.
*/
TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
/** 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, int index);
private:
/** pointer to theory engine */
QuantifiersEngine* d_qe;
/** 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, int > d_rep_score;
/** the number of times reset( e ) has been called */
int 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, TNodeHashFunction>& cache );
/** get score */
int getRepScore( Node n, Node f, int index, TypeNode v_tn );
/** flatten representatives */
void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
|
