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
|
/********************************************************************
* AUTHORS: Vijay Ganesh, David L. Dill
*
* BEGIN DATE: November, 2005
*
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
// -*- c++ -*-
#ifndef ASTUTIL_H
#define ASTUTIL_H
#include <cstring>
#include <iostream>
#include <vector>
#ifdef EXT_HASH_MAP
#include <ext/hash_set>
#include <ext/hash_map>
#else
#include <hash_set>
#include <hash_map>
#endif
using namespace std;
namespace BEEV {
#ifdef EXT_HASH_MAP
using namespace __gnu_cxx;
#endif
//some global variables that are set through commandline options. it
//is best that these variables remain global. Default values set
//here
//
//collect statistics on certain functions
extern bool stats;
//print DAG nodes
extern bool print_nodes;
//tentative global var to allow for variable activity optimization
//in the SAT solver. deprecated.
extern bool variable_activity_optimize;
//run STP in optimized mode
extern bool optimize;
//do sat refinement, i.e. underconstraint the problem, and feed to
//SAT. if this works, great. else, add a set of suitable constraints
//to re-constraint the problem correctly, and call SAT again, until
//all constraints have been added.
extern bool arrayread_refinement;
//switch to control write refinements
extern bool arraywrite_refinement;
//check the counterexample against the original input to STP
extern bool check_counterexample;
//construct the counterexample in terms of original variable based
//on the counterexample returned by SAT solver
extern bool construct_counterexample;
extern bool print_counterexample;
//if this option is true then print the way dawson wants using a
//different printer. do not use this printer.
extern bool print_arrayval_declaredorder;
//flag to decide whether to print "valid/invalid" or not
extern bool print_output;
//do linear search in the array values of an input array. experimental
extern bool linear_search;
//print the variable order chosen by the sat solver while it is
//solving.
extern bool print_sat_varorder;
//turn on word level bitvector solver
extern bool wordlevel_solve;
//XOR flattening optimizations.
extern bool xor_flatten;
//this flag indicates that the BVSolver() succeeded
extern bool toplevel_solved;
//the smtlib parser has been turned on
extern bool smtlib_parser_enable;
//print the input back
extern bool print_STPinput_back;
extern void (*vc_error_hdlr)(const char* err_msg);
/*Spacer class is basically just an int, but the new class allows
overloading of << with a special definition that prints the int as
that many spaces. */
class Spacer {
public:
int _spaces;
Spacer(int spaces) { _spaces = spaces; }
friend ostream& operator<<(ostream& os, const Spacer &ind);
};
inline Spacer spaces(int width) {
Spacer sp(width);
return sp;
}
struct eqstr {
bool operator()(const char* s1, const char* s2) const {
return strcmp(s1, s2) == 0;
}
};
typedef hash_map<const char*,int,
hash<const char *>,eqstr> function_counters;
void CountersAndStats(const char * functionname);
//global function which accepts an integer and looks up the
//corresponding ASTNode and prints a char* of that ASTNode
void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
int decision, int polarity=0);
} // end namespace.
#endif
|
