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
|
/********************* */
/*! \file bv_inverter.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Mathias Preiner, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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 {
/** BvInverterQuery
*
* This is a virtual class for queries
* required by the BvInverter class.
*/
class BvInverterQuery
{
public:
BvInverterQuery() {}
virtual ~BvInverterQuery() {}
/** returns the current model value of n */
virtual Node getModelValue(Node n) = 0;
/** returns a bound variable of type tn */
virtual Node getBoundVariable(TypeNode tn) = 0;
};
// 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 path to pv in lit, replace that occurrence by sv and all others by
* pvs (if pvs is non-null). 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
*
* If the flag projectNl is false, we return the null node if the
* literal lit is non-linear with respect to pv.
*/
Node getPathToPv(Node lit,
Node pv,
Node sv,
Node pvs,
std::vector<unsigned>& path,
bool projectNl);
/**
* Same as above, but does not linearize lit for pv.
* Use this version if we know lit is linear wrt pv.
*/
Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
{
return getPathToPv(lit, pv, pv, Node::null(), path, false);
}
/** solveBvLit
*
* Solve for sv in lit, where lit.path = sv. If this function returns a
* non-null node t, then sv = t is the solved form of lit.
*
* If the BvInverterQuery provided to this function call is null, then
* the solution returned by this call will not contain CHOICE expressions.
* If the solved form for lit requires introducing a CHOICE expression,
* then this call will return null.
*/
Node solveBvLit(Node sv,
Node lit,
std::vector<unsigned>& path,
BvInverterQuery* m);
private:
/** Dummy variables for each type */
std::map<TypeNode, Node> d_solve_var;
/** Helper function for getPathToPv */
Node getPathToPv(Node lit,
Node pv,
Node sv,
std::vector<unsigned>& path,
std::unordered_set<TNode, TNodeHashFunction>& visited);
/** Helper function for getInv.
*
* This expects a condition cond where:
* (exists x. cond)
* is a BV tautology where x is getSolveVariable( tn ).
*
* It returns a term of the form:
* (choice y. cond { x -> y })
* where y is a bound variable and x is getSolveVariable( tn ).
*
* In some cases, we may return a term t if cond implies an equality on
* the solve variable. For example, if cond is x = t where x is
* getSolveVariable(tn), then we return t instead of introducing the choice
* function.
*
* This function will return the null node if the BvInverterQuery m provided
* to this call is null.
*/
Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
};
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#endif /* __CVC4__BV_INVERTER_H */
|
