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
|
/********************************************************************
* AUTHORS: Vijay Ganesh, David L. Dill
*
* BEGIN DATE: November, 2005
*
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
// -*- c++ -*-
#include "../AST/AST.h"
#include "../AST/ASTUtil.h"
namespace BEEV {
//This class represents the bitvector arithmetic linear solver.
//
//The bitvector solver is a partial solver, i.e. it does not solve
//for all variables in the system of equations. it is
//best-effort. it relies on the SAT solver to be complete.
//
//The BVSolver assumes that the input equations are normalized, and
//have liketerms combined etc.
//
//0. Traverse top-down over the input DAG, looking for a conjunction
//0. of equations. if you find one, then for each equation in the
//0. conjunction, do the following steps.
//
//1. check for Linearity of the input equation
//
//2. Solve for a "chosen" variable. The variable should occur
//2. exactly once and must have an odd coeff. Refer STP's CAV 2007
//2. paper for actual solving procedure
//
//4. Outside the solver, Substitute and Re-normalize the input DAG
class BVSolver {
//Ptr to toplevel manager that manages bit-vector expressions
//(i.e. construct various kinds of expressions), and also has
//member functions that simplify bit-vector expressions
BeevMgr * _bm;
ASTNode ASTTrue, ASTFalse;
//Those formulas which have already been solved. If the same
//formula occurs twice then do not solve the second occurence, and
//instead drop it
ASTNodeMap FormulasAlreadySolvedMap;
//this map is useful while traversing terms and uniquely
//identifying variables in the those terms. Prevents double
//counting.
ASTNodeMap TermsAlreadySeenMap;
ASTNodeMap TermsAlreadySeenMap_ForArrays;
//count is used in the creation of new variables
unsigned int _symbol_count;
//solved variables list: If a variable has been solved for then do
//not solve for it again
ASTNodeSet DoNotSolve_TheseVars;
//checks if var has been solved for or not. if yes, then return
//true else return false
bool DoNotSolveThis(const ASTNode& var);
//traverses a term, and creates a multiset of all variables in the
//term. Does memoization to avoid double counting.
void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v);
void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v);
//choose a suitable var from the term
ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm);
//accepts an equation and solves for a variable or a monom in it
ASTNode BVSolve_Odd(const ASTNode& eq);
//solves equations of the form a*x=t where 'a' is even. Has a
//return value, unlike the normal BVSolve()
ASTNode BVSolve_Even(const ASTNode& eq);
ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag);
//Checks for arrayreads in a term. if yes then returns true, else
//return false
bool CheckForArrayReads(const ASTNode& term);
bool CheckForArrayReads_TopLevel(const ASTNode& term);
//Creates new variables used in solving
ASTNode NewVar(unsigned int n);
//this function return true if the var occurs in term, else the
//function returns false
bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
//takes an even number "in" as input, and returns an odd number
//(return value) and a power of 2 (as number_shifts by reference),
//such that in = (odd_number * power_of_2).
//
//Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on
//bit-vector arithmetic published in DAC 1998) paper for precise
//understanding of the algorithm
ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts);
//Once a formula has been solved, then update the alreadysolvedmap
//with the formula, and the solved value. The solved value can be
//described using the following example: Suppose input to the
//solver is
//
// input key: x = 2 AND y = x + t
//
// output value: y = 2 + t
void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value);
//This function checks if the key (formula) has already been
//solved for.
//
//If yes it returns TRUE and fills the "output" with the
//solved-value (call by reference argument),
//
//else returns FALSE
bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
public:
//constructor
BVSolver(BeevMgr * bm) : _bm(bm), _symbol_count(0) {
ASTTrue = _bm->CreateNode(TRUE);
ASTFalse = _bm->CreateNode(FALSE);
};
//Destructor
~BVSolver() {
TermsAlreadySeenMap.clear();
DoNotSolve_TheseVars.clear();
}
//Top Level Solver: Goes over the input DAG, identifies the
//equation to be solved, solves them,
ASTNode TopLevelBVSolve(const ASTNode& a);
}; //end of class bvsolver
};//end of namespace BEEV
|
