1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 context_params.cpp
7
8 Abstract:
9
10 Goodies for managing context parameters in the cmd_context and
11 api_context
12
13 Author:
14
15 Leonardo (leonardo) 2012-12-01
16
17 Notes:
18
19 --*/
20 #include "util/gparams.h"
21 #include "util/params.h"
22 #include "ast/ast.h"
23 #include "params/context_params.h"
24
context_params()25 context_params::context_params() {
26 updt_params();
27 }
28
set_bool(bool & opt,char const * param,char const * value)29 void context_params::set_bool(bool & opt, char const * param, char const * value) {
30 if (strcmp(value, "true") == 0) {
31 opt = true;
32 }
33 else if (strcmp(value, "false") == 0) {
34 opt = false;
35 }
36 else {
37 std::stringstream strm;
38 strm << "invalid value '" << value << "' for Boolean parameter '" << param << "'";
39 throw default_exception(strm.str());
40 }
41 }
42
set_uint(unsigned & opt,char const * param,char const * value)43 void context_params::set_uint(unsigned & opt, char const * param, char const * value) {
44 bool is_uint = true;
45 size_t sz = strlen(value);
46 for (unsigned i = 0; i < sz; i++) {
47 if (!(value[i] >= '0' && value[i] <= '9'))
48 is_uint = false;
49 }
50
51 if (is_uint) {
52 long val = strtol(value, nullptr, 10);
53 opt = static_cast<unsigned>(val);
54 }
55 else {
56 std::stringstream strm;
57 strm << "invalid value '" << value << "' for unsigned int parameter '" << param << "'";
58 throw default_exception(strm.str());
59 }
60 }
61
set(char const * param,char const * value)62 void context_params::set(char const * param, char const * value) {
63 std::string p = param;
64 unsigned n = static_cast<unsigned>(p.size());
65 for (unsigned i = 0; i < n; i++) {
66 if (p[i] >= 'A' && p[i] <= 'Z')
67 p[i] = p[i] - 'A' + 'a';
68 else if (p[i] == '-')
69 p[i] = '_';
70 }
71 if (p == "timeout") {
72 set_uint(m_timeout, param, value);
73 }
74 else if (p == "rlimit") {
75 set_uint(m_rlimit, param, value);
76 }
77 else if (p == "type_check" || p == "well_sorted_check") {
78 set_bool(m_well_sorted_check, param, value);
79 }
80 else if (p == "auto_config") {
81 set_bool(m_auto_config, param, value);
82 }
83 else if (p == "proof") {
84 set_bool(m_proof, param, value);
85 }
86 else if (p == "model") {
87 set_bool(m_model, param, value);
88 }
89 else if (p == "model_validate") {
90 set_bool(m_model_validate, param, value);
91 }
92 else if (p == "dump_models") {
93 set_bool(m_dump_models, param, value);
94 }
95 else if (p == "stats") {
96 set_bool(m_statistics, param, value);
97 }
98 else if (p == "trace") {
99 set_bool(m_trace, param, value);
100 }
101 else if (p == "trace_file_name") {
102 m_trace_file_name = value;
103 }
104 else if (p == "dot_proof_file") {
105 m_dot_proof_file = value;
106 }
107 else if (p == "unsat_core") {
108 if (!m_unsat_core)
109 set_bool(m_unsat_core, param, value);
110 }
111 else if (p == "debug_ref_count") {
112 set_bool(m_debug_ref_count, param, value);
113 }
114 else if (p == "smtlib2_compliant") {
115 set_bool(m_smtlib2_compliant, param, value);
116 }
117 else {
118 param_descrs d;
119 collect_param_descrs(d);
120 std::stringstream strm;
121 strm << "unknown parameter '" << p << "'\n";
122 strm << "Legal parameters are:\n";
123 d.display(strm, 2, false, false);
124 throw default_exception(strm.str());
125 }
126 }
127
updt_params()128 void context_params::updt_params() {
129 updt_params(gparams::get_ref());
130 }
131
updt_params(params_ref const & p)132 void context_params::updt_params(params_ref const & p) {
133 m_timeout = p.get_uint("timeout", m_timeout);
134 m_rlimit = p.get_uint("rlimit", m_rlimit);
135 m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check));
136 m_auto_config = p.get_bool("auto_config", m_auto_config);
137 m_proof = p.get_bool("proof", m_proof);
138 m_model = p.get_bool("model", m_model);
139 m_model_validate = p.get_bool("model_validate", m_model_validate);
140 m_dump_models = p.get_bool("dump_models", m_dump_models);
141 m_trace = p.get_bool("trace", m_trace);
142 m_trace_file_name = p.get_str("trace_file_name", "z3.log");
143 m_dot_proof_file = p.get_str("dot_proof_file", "proof.dot");
144 m_unsat_core |= p.get_bool("unsat_core", m_unsat_core);
145 m_debug_ref_count = p.get_bool("debug_ref_count", m_debug_ref_count);
146 m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant);
147 m_statistics = p.get_bool("stats", m_statistics);
148 }
149
collect_param_descrs(param_descrs & d)150 void context_params::collect_param_descrs(param_descrs & d) {
151 insert_rlimit(d);
152 insert_timeout(d);
153 d.insert("well_sorted_check", CPK_BOOL, "type checker", "false");
154 d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
155 d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
156 d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
157 d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "false");
158 d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
159 d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
160 d.insert("dot_proof_file", CPK_STRING, "file in which to output graphical proofs", "proof.dot");
161 d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
162 d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
163 d.insert("stats", CPK_BOOL, "enable/disable statistics", "false");
164 // statistics are hidden as they are controlled by the /st option.
165 collect_solver_param_descrs(d);
166 }
167
collect_solver_param_descrs(param_descrs & d)168 void context_params::collect_solver_param_descrs(param_descrs & d) {
169 d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
170 d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
171 d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
172 }
173
merge_default_params(params_ref const & p)174 params_ref context_params::merge_default_params(params_ref const & p) {
175 if (!m_auto_config && !p.contains("auto_config")) {
176 params_ref new_p = p;
177 new_p.set_bool("auto_config", false);
178 return new_p;
179 }
180 else {
181 return p;
182 }
183 }
184
get_solver_params(ast_manager const & m,params_ref & p,bool & proofs_enabled,bool & models_enabled,bool & unsat_core_enabled)185 void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) {
186 proofs_enabled = m.proofs_enabled() && p.get_bool("proof", m_proof);
187 models_enabled = p.get_bool("model", m_model);
188 unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false);
189 p = merge_default_params(p);
190 }
191
mk_ast_manager()192 ast_manager * context_params::mk_ast_manager() {
193 if (m_manager)
194 return m_manager;
195 ast_manager * r = alloc(ast_manager,
196 m_proof ? PGM_ENABLED : PGM_DISABLED,
197 m_trace ? m_trace_file_name.c_str() : nullptr);
198 if (m_smtlib2_compliant)
199 r->enable_int_real_coercions(false);
200 if (m_debug_ref_count)
201 r->debug_ref_count();
202 return r;
203 }
204
205
206