1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mudathir Mohamed |
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 |
|
* Sets state object. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__SETS__TERM_REGISTRY_H |
19 |
|
#define CVC5__THEORY__SETS__TERM_REGISTRY_H |
20 |
|
|
21 |
|
#include <map> |
22 |
|
#include <vector> |
23 |
|
|
24 |
|
#include "context/cdhashmap.h" |
25 |
|
#include "proof/eager_proof_generator.h" |
26 |
|
#include "smt/env_obj.h" |
27 |
|
#include "theory/sets/inference_manager.h" |
28 |
|
#include "theory/sets/skolem_cache.h" |
29 |
|
#include "theory/sets/solver_state.h" |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace theory { |
33 |
|
namespace sets { |
34 |
|
|
35 |
|
/** |
36 |
|
* Term registry, the purpose of this class is to maintain a database of |
37 |
|
* commonly used terms, and mappings from sets to their "proxy variables". |
38 |
|
*/ |
39 |
6268 |
class TermRegistry : protected EnvObj |
40 |
|
{ |
41 |
|
typedef context::CDHashMap<Node, Node> NodeMap; |
42 |
|
|
43 |
|
public: |
44 |
|
TermRegistry(Env& env, |
45 |
|
SolverState& state, |
46 |
|
InferenceManager& im, |
47 |
|
SkolemCache& skc, |
48 |
|
ProofNodeManager* pnm); |
49 |
|
/** Get type constraint skolem |
50 |
|
* |
51 |
|
* The sets theory solver outputs equality lemmas of the form: |
52 |
|
* n = d_tc_skolem[n][tn] |
53 |
|
* where the type of d_tc_skolem[n][tn] is tn, and the type |
54 |
|
* of n is not a subtype of tn. This is required to handle benchmarks like |
55 |
|
* test/regress/regress0/sets/sets-of-sets-subtypes.smt2 |
56 |
|
* where for s : (Set Int) and t : (Set Real), we have that |
57 |
|
* ( s = t ^ y in t ) implies ( exists k : Int. y = k ) |
58 |
|
* The type constraint Skolem for (y, Int) is the skolemization of k above. |
59 |
|
*/ |
60 |
|
Node getTypeConstraintSkolem(Node n, TypeNode tn); |
61 |
|
/** get the proxy variable for set n |
62 |
|
* |
63 |
|
* Proxy variables are used to communicate information that otherwise would |
64 |
|
* not be possible due to rewriting. For example, the literal |
65 |
|
* card( singleton( 0 ) ) = 1 |
66 |
|
* is rewritten to true. Instead, to communicate this fact (e.g. to other |
67 |
|
* theories), we require introducing a proxy variable x for singleton( 0 ). |
68 |
|
* Then: |
69 |
|
* card( x ) = 1 ^ x = singleton( 0 ) |
70 |
|
* communicates the equivalent of the above literal. |
71 |
|
*/ |
72 |
|
Node getProxy(Node n); |
73 |
|
/** Get the empty set of type tn */ |
74 |
|
Node getEmptySet(TypeNode tn); |
75 |
|
/** Get the universe set of type tn if it exists or create a new one */ |
76 |
|
Node getUnivSet(TypeNode tn); |
77 |
|
/** debug print set */ |
78 |
|
void debugPrintSet(Node s, const char* c) const; |
79 |
|
|
80 |
|
private: |
81 |
|
/** Send simple lemma internal */ |
82 |
|
void sendSimpleLemmaInternal(Node n, InferenceId id); |
83 |
|
/** The inference manager */ |
84 |
|
InferenceManager& d_im; |
85 |
|
/** Reference to the skolem cache */ |
86 |
|
SkolemCache& d_skCache; |
87 |
|
/** Map from set terms to their proxy variables */ |
88 |
|
NodeMap d_proxy; |
89 |
|
/** Backwards map of above */ |
90 |
|
NodeMap d_proxy_to_term; |
91 |
|
/** Cache of type constraint skolems (see getTypeConstraintSkolem) */ |
92 |
|
std::map<Node, std::map<TypeNode, Node> > d_tc_skolem; |
93 |
|
/** Map from types to empty set of that type */ |
94 |
|
std::map<TypeNode, Node> d_emptyset; |
95 |
|
/** Map from types to universe set of that type */ |
96 |
|
std::map<TypeNode, Node> d_univset; |
97 |
|
/** Eager proof generator for purification lemmas */ |
98 |
|
std::unique_ptr<EagerProofGenerator> d_epg; |
99 |
|
}; /* class TheorySetsPrivate */ |
100 |
|
|
101 |
|
} // namespace sets |
102 |
|
} // namespace theory |
103 |
|
} // namespace cvc5 |
104 |
|
|
105 |
|
#endif /* CVC5__THEORY__SETS__TERM_REGISTRY_H */ |