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
126
127
128
129
130
131
132
133
134
135
136
137
|
/********************* */
/*! \file bv_inverter.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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 inverse rules for bit-vector operators
**/
#include "cvc4_private.h"
#ifndef __CVC4__BV_INVERTER_H
#define __CVC4__BV_INVERTER_H
#include <map>
#include <unordered_map>
#include <unordered_set>
#include <vector>
#include "expr/node.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
// virtual class for model queries
class BvInverterModelQuery {
public:
BvInverterModelQuery() {}
~BvInverterModelQuery() {}
virtual Node getModelValue(Node n) = 0;
};
// class for storing information about the solved status
class BvInverterStatus {
public:
BvInverterStatus() : d_status(0) {}
~BvInverterStatus() {}
int d_status;
// TODO : may not need this (conditions now appear explicitly in solved
// forms) side conditions
std::vector<Node> d_conds;
};
// inverter class
// TODO : move to theory/bv/ if generally useful?
class BvInverter {
public:
BvInverter() {}
~BvInverter() {}
/** get dummy fresh variable of type tn, used as argument for sv */
Node getSolveVariable(TypeNode tn);
/** get inversion node, if :
*
* f = getInversionSkolemFunctionFor( tn )
*
* This returns f( cond ).
*/
Node getInversionNode(Node cond, TypeNode tn);
/** Get path to pv in lit, replace that occurrence by sv and all others by
* pvs. If return value R is non-null, then : lit.path = pv R.path = sv
* R.path' = pvs for all lit.path' = pv, where path' != path
*/
Node getPathToPv(Node lit, Node pv, Node sv, Node pvs,
std::vector<unsigned>& path);
/** eliminate skolem functions in node n
*
* This eliminates all Skolem functions from Node n and replaces them with
* finalized Skolem variables.
*
* For each skolem variable we introduce, we ensure its associated side
* condition is added to side_conditions.
*
* Apart from Skolem functions, all subterms of n should be eligible for
* instantiation.
*/
Node eliminateSkolemFunctions(TNode n, std::vector<Node>& side_conditions);
/** solve_bv_lit
* solve for sv in lit, where lit.path = sv
* status accumulates side conditions
*/
Node solve_bv_lit(Node sv, Node lit, std::vector<unsigned>& path,
BvInverterModelQuery* m, BvInverterStatus& status);
private:
/** dummy variables for each type */
std::map<TypeNode, Node> d_solve_var;
/** stores the inversion skolems, for each condition */
std::unordered_map<Node, Node, NodeHashFunction> d_inversion_skolem_cache;
/** helper function for getPathToPv */
Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
std::unordered_set<TNode, TNodeHashFunction>& visited);
// is operator k invertible?
bool isInvertible(Kind k, unsigned index);
/** get inversion skolem for condition
* precondition : exists x. cond( x ) is a tautology in BV,
* where x is getSolveVariable( tn ).
* returns fresh skolem k of type tn, where we may assume cond( k ).
*/
Node getInversionSkolemFor(Node cond, TypeNode tn);
/** get inversion skolem function for type tn.
* This is a function of type ( Bool -> tn ) that is used for explicitly
* storing side conditions inside terms. For all ( cond, tn ), if :
*
* f = getInversionSkolemFunctionFor( tn )
* k = getInversionSkolemFor( cond, tn )
* then:
* f( cond ) is a placeholder for k.
*
* In the call eliminateSkolemFunctions, we replace all f( cond ) with k and
* add cond{ x -> k } to side_conditions. The advantage is that f( cond )
* explicitly contains the side condition so it automatically updates with
* substitutions.
*/
Node getInversionSkolemFunctionFor(TypeNode tn);
};
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#endif /* __CVC4__BV_INVERTER_H */
|
