mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-29 18:52:29 +00:00
Code Activity

working on new parameter framework

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 15:54:34 -08:00
parent be5f933201
commit 589f096e6e
36 changed files with 436 additions and 377 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_util.py
View file

@ -1472,7 +1472,7 @@ def def_module_params(module_name, export, params):
out.write('struct %s_params {\n' % module_name)
out.write(' params_ref const & p;\n')
if export:
out.write(' params_ref const & g;\n')
out.write(' params_ref g;\n')
out.write(' %s_params(params_ref const & _p = params_ref()):\n' % module_name)
out.write(' p(_p)')
if export:

62
src/api/api_config_params.cpp
View file

@ -36,9 +36,45 @@ namespace api {
};
extern "C" {
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
memory::initialize(UINT_MAX);
LOG_Z3_global_param_set(param_id, param_value);
try {
gparams::set(param_id, param_value);
}
catch (z3_exception & ex) {
// The error handler is only available for contexts
// Just throw a warning.
std::ostringstream buffer;
buffer << "Error setting " << param_id << ", " << ex.msg();
warning_msg(buffer.str().c_str());
}
}
std::string g_Z3_global_param_get_buffer;
Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
memory::initialize(UINT_MAX);
LOG_Z3_global_param_get(param_id, param_value);
*param_value = 0;
try {
g_Z3_global_param_get_buffer = gparams::get_value(param_id);
*param_value = g_Z3_global_param_get_buffer.c_str();
return Z3_TRUE;
}
catch (z3_exception & ex) {
// The error handler is only available for contexts
// Just throw a warning.
std::ostringstream buffer;
buffer << "Error setting " << param_id << ", " << ex.msg();
warning_msg(buffer.str().c_str());
return Z3_FALSE;
}
}
Z3_config Z3_API Z3_mk_config() {
memory::initialize(UINT_MAX);
LOG_Z3_mk_config();
memory::initialize(0);
Z3_config r = reinterpret_cast<Z3_config>(alloc(api::config_params));
RETURN_Z3(r);
}
@ -49,35 +85,19 @@ extern "C" {
}
void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
// REMARK: we don't need Z3_config anymore
try {
LOG_Z3_set_param_value(c, param_id, param_value);
gparams::set(param_id, param_value);
}
catch (gparams::exception & ex) {
// The error handler was not set yet.
// Just throw a warning.
std::ostringstream buffer;
buffer << "Error setting " << param_id << ", " << ex.msg();
warning_msg(buffer.str().c_str());
}
LOG_Z3_set_param_value(c, param_id, param_value);
// PARAM-TODO save the parameter
}
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) {
Z3_TRY;
LOG_Z3_update_param_value(c, param_id, param_value);
RESET_ERROR_CODE();
gparams::set(param_id, param_value);
// TODO: set memory limits
// memory::set_high_watermark(static_cast<size_t>(mk_c(c)->fparams().m_memory_high_watermark)*1024*1024);
// memory::set_max_size(static_cast<size_t>(mk_c(c)->fparams().m_memory_max_size)*1024*1024);
Z3_CATCH;
// NOOP in the current version
}
Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) {
LOG_Z3_get_param_value(c, param_id, param_value);
// TODO: we don't really have support for that anymore.
return false;
return Z3_FALSE;
}
};

2
src/api/api_datalog.cpp
View file

@ -344,7 +344,7 @@ extern "C" {
std::istream& s) {
ast_manager& m = mk_c(c)->m();
dl_collected_cmds coll(m);
cmd_context ctx(&mk_c(c)->fparams(), false, &m);
cmd_context ctx(false, &m);
install_dl_collect_cmds(coll, ctx);
ctx.set_ignore_check(true);
if (!parse_smt2_commands(ctx, s)) {

7
src/api/api_model.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include"model.h"
#include"model_v2_pp.h"
#include"model_smt2_pp.h"
#include"model_params.hpp"
extern "C" {
@ -488,7 +489,8 @@ extern "C" {
Z3_model m,
Z3_ast t,
Z3_ast * v) {
return Z3_model_eval(c, m, t, mk_c(c)->fparams().m_model_completion, v);
model_params p;
return Z3_model_eval(c, m, t, p.completion(), v);
}
Z3_bool Z3_API Z3_eval_func_decl(Z3_context c,
@ -660,7 +662,8 @@ extern "C" {
result.resize(result.size()-1);
}
else {
model_v2_pp(buffer, *(to_model_ref(m)), mk_c(c)->fparams().m_model_partial);
model_params p;
model_v2_pp(buffer, *(to_model_ref(m)), p.partial());
result = buffer.str();
}
return mk_c(c)->mk_external_string(result);

4
src/api/api_parsers.cpp
View file

@ -296,7 +296,7 @@ extern "C" {
Z3_symbol const decl_names[],
Z3_func_decl const decls[]) {
Z3_TRY;
cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));
cmd_context ctx(false, &(mk_c(c)->m()));
ctx.set_ignore_check(true);
if (exec) {
ctx.set_solver(alloc(z3_context_solver, *mk_c(c)));
@ -362,7 +362,7 @@ extern "C" {
Z3_symbol decl_names[],
Z3_func_decl decls[]) {
Z3_TRY;
cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));
cmd_context ctx(false, &(mk_c(c)->m()));
std::string s(str);
std::istringstream is(s);
// No logging for this one, since it private.

50
src/api/python/z3.py
View file

@ -169,28 +169,6 @@ class Context:
"""
Z3_interrupt(self.ref())
def set(self, *args, **kws):
"""Set global configuration options.
Z3 command line options can be set using this method.
The option names can be specified in different ways:
>>> ctx = Context()
>>> ctx.set('WELL_SORTED_CHECK', True)
>>> ctx.set(':well-sorted-check', True)
>>> ctx.set(well_sorted_check=True)
"""
if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
for key, value in kws.iteritems():
Z3_update_param_value(self.ctx, str(key).upper(), _to_param_value(value))
prev = None
for a in args:
if prev == None:
prev = a
else:
Z3_update_param_value(self.ctx, str(prev), _to_param_value(a))
prev = None
# Global Z3 context
_main_ctx = None
@ -221,15 +199,37 @@ def _get_ctx(ctx):
return ctx
def set_option(*args, **kws):
"""Update parameters of the global context `main_ctx()`, and global configuration options of Z3Py. See `Context.set()`.
"""Set Z3 global (or module) parameters.
>>> set_option(precision=10)
"""
if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
new_kws = {}
for k, v in kws.iteritems():
if not set_pp_option(k, v):
new_kws[k] = v
main_ctx().set(*args, **new_kws)
for key, value in new_kws.iteritems():
Z3_global_param_set(str(key).upper(), _to_param_value(value))
prev = None
for a in args:
if prev == None:
prev = a
else:
Z3_global_param_set(str(prev), _to_param_value(a))
prev = None
def get_option(name):
"""Return the value of a Z3 global (or module) parameter
>>> get_option('nlsat.reorder')
true
"""
ptr = (ctypes.c_char_p * 1)()
if Z3_global_param_get(str(name), ptr):
r = str(ptr[0])
return r
raise Z3Exception("failed to retrieve value for '%s'" % name)
#########################################
#

95
src/api/z3_api.h
View file

@ -1233,25 +1233,82 @@ extern "C" {
#endif // CAMLIDL
#ifdef CorML3
/**
@name Configuration
*/
/*@{*/
/**
\brief Set a global (or module) parameter.
This setting is shared by all Z3 contexts.
When a Z3 module is initialized it will use the value of these parameters
when Z3_params objects are not provided.
The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'.
The character '.' is a delimiter (more later).
The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION".
This function can be used to set parameters for a specific Z3 module.
This can be done by using <module-name>.<parameter-name>.
For example:
Z3_global_param_set('pp.decimal', 'true')
will set the parameter "decimal" in the module "pp" to true.
def_API('Z3_global_param_set', VOID, (_in(STRING), _in(STRING)))
*/
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value);
/**
\brief Get a global (or module) parameter.
Returns \mlonly \c None \endmlonly \conly \c Z3_FALSE
if the parameter value does not exist.
\sa Z3_global_param_set
The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
\remark This function cannot be invoked simultaneously from different threads without synchronization.
The result string stored in param_value is stored in shared location.
def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING)))
*/
Z3_bool_opt Z3_API Z3_global_param_get(__in Z3_string param_id, __out_opt Z3_string_ptr param_value);
/*@}*/
/**
@name Create configuration
*/
/*@{*/
/**
\brief Create a configuration.
\brief Create a configuration object for the Z3 context object.
Configurations are created in order to assign parameters prior to creating
contexts for Z3 interaction. For example, if the users wishes to use model
contexts for Z3 interaction. For example, if the users wishes to use proof
generation, then call:
\ccode{Z3_set_param_value(cfg\, "MODEL"\, "true")}
\ccode{Z3_set_param_value(cfg\, "proof"\, "true")}
\mlonly \remark Consider using {!mk_context_x} instead of using
explicit configuration objects. The function {!mk_context_x}
receives an array of string pairs. This array represents the
configuration options. \endmlonly
\remark In previous versions of Z3, the \c Z3_config was used to store
global and module configurations. Now, we should use \c Z3_global_param_set.
The following parameters can be set:
- proof (Boolean) Enable proof generation
- debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
- trace (Boolean) Tracing support for VCC
- trace_file_name (String) Trace out file for VCC traces
\sa Z3_set_param_value
\sa Z3_del_config
@ -1271,18 +1328,14 @@ extern "C" {
/**
\brief Set a configuration parameter.
The list of all configuration parameters can be obtained using the Z3 executable:
\verbatim
z3.exe -ini?
\endverbatim
The following parameters can be set for
\sa Z3_mk_config
def_API('Z3_set_param_value', VOID, (_in(CONFIG), _in(STRING), _in(STRING)))
*/
void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value);
/*@}*/
#endif
@ -1367,33 +1420,19 @@ extern "C" {
#endif
/**
\brief Update a mutable configuration parameter.
\brief This is a deprecated function. This is a NOOP in the current version of Z3.
The list of all configuration parameters can be obtained using the Z3 executable:
\verbatim
z3.exe -ini?
\endverbatim
Only a few configuration parameters are mutable once the context is created.
The error handler is invoked when trying to modify an immutable parameter.
\conly \sa Z3_set_param_value
\mlonly \sa Z3_mk_context \endmlonly
\deprecated Use #Z3_global_param_set.
def_API('Z3_update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING)))
*/
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value);
/**
\brief Get a configuration parameter.
\brief This is a deprecated function. This is a NOOP in the current version of Z3.
It always return Z3_FALSE.
Returns \mlonly \c None \endmlonly \conly \c Z3_FALSE
if the parameter value does not exist.
\conly \sa Z3_mk_config
\conly \sa Z3_set_param_value
\mlonly \sa Z3_mk_context \endmlonly
\deprecated Use #Z3_global_param_get
def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
*/

3
src/ast/pattern/expr_pattern_match.cpp
View file

@ -388,8 +388,7 @@ expr_pattern_match::initialize(char const * spec_string) {
m_instrs.push_back(instr(BACKTRACK));
std::istringstream is(spec_string);
front_end_params p;
cmd_context ctx(&p, true, &m_manager);
cmd_context ctx(true, &m_manager);
VERIFY(parse_smt2_commands(ctx, is));
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();

6
src/cmd_context/basic_cmds.cpp
View file

@ -29,6 +29,7 @@ Notes:
#include"eval_cmd.h"
#include"front_end_params.h"
#include"gparams.h"
#include"model_params.hpp"
class help_cmd : public cmd {
svector<symbol> m_cmds;
@ -104,9 +105,10 @@ ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat co
throw cmd_exception("model is not available");
model_ref m;
ctx.get_check_sat_result()->get_model(m);
if (ctx.params().m_model_v1_pp || ctx.params().m_model_v2_pp) {
model_params p;
if (p.v1() || p.v2()) {
std::ostringstream buffer;
model_v2_pp(buffer, *m, ctx.params().m_model_partial);
model_v2_pp(buffer, *m, p.partial());
ctx.regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl;
} else {
ctx.regular_stream() << "(model " << std::endl;

18
src/cmd_context/cmd_context.cpp
View file

@ -316,10 +316,9 @@ public:
}
};
cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager * m, symbol const & l):
cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_main_ctx(main_ctx),
m_params(params == 0 ? alloc(front_end_params) : params),
m_params_owner(params == 0),
m_fparams(alloc(front_end_params)),
m_logic(l),
m_interactive_mode(false),
m_global_decls(false), // :global-decls is false by default.
@ -359,9 +358,7 @@ cmd_context::~cmd_context() {
finalize_probes();
m_solver = 0;
m_check_sat_result = 0;
if (m_params_owner) {
dealloc(m_params);
}
dealloc(m_fparams);
}
void cmd_context::set_produce_models(bool f) {
@ -382,10 +379,6 @@ void cmd_context::set_produce_proofs(bool f) {
params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
}
bool cmd_context::is_smtlib2_compliant() const {
return params().m_smtlib2_compliant;
}
bool cmd_context::produce_models() const {
return params().m_model;
}
@ -599,8 +592,9 @@ void cmd_context::init_manager() {
m_manager = alloc(ast_manager, params().m_proof_mode, params().m_trace_stream);
m_pmanager = alloc(pdecl_manager, *m_manager);
init_manager_core(true);
if (params().m_smtlib2_compliant)
m_manager->enable_int_real_coercions(false);
// PARAM-TODO
// if (params().m_smtlib2_compliant)
// m_manager->enable_int_real_coercions(false);
}
void cmd_context::init_external_manager() {

8
src/cmd_context/cmd_context.h
View file

@ -138,8 +138,7 @@ public:
protected:
bool m_main_ctx;
front_end_params * m_params;
bool m_params_owner;
front_end_params * m_fparams;
symbol m_logic;
bool m_interactive_mode;
bool m_global_decls;
@ -251,9 +250,8 @@ protected:
void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
public:
cmd_context(front_end_params * params = 0, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
~cmd_context();
bool is_smtlib2_compliant() const;
void set_logic(symbol const & s);
bool has_logic() const { return m_logic != symbol::null; }
symbol const & get_logic() const { return m_logic; }
@ -290,7 +288,7 @@ public:
virtual ast_manager & get_ast_manager() { return m(); }
pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
front_end_params & params() const { return *m_params; }
front_end_params & params() const { return *m_fparams; }
void set_solver(solver * s);
solver * get_solver() const { return m_solver.get(); }

9
src/front_end_params/README Normal file
View file

@ -0,0 +1,9 @@
This directory contains the "remains" of the old parameter setting
infrastructure used by Z3. Old code (mostly `smt::context`) is still
based on the front_end_params structure. However, we removed support
for the old INI file infrastructure. Instead, we have functions for
setting the fields of front_end_params using parameter sets
(params_ref). Moreover, many of the parameters in front_end_params
are now "hidden". That is, they can't be set from the command line or
using the command `set-option`.

23
src/front_end_params/front_end_params.cpp
View file

@ -22,9 +22,7 @@ void front_end_params::register_params(ini_params & p) {
p.register_param_vector(m_param_vector.get());
preprocessor_params::register_params(p);
smt_params::register_params(p);
parser_params::register_params(p);
arith_simplifier_params::register_params(p);
model_params::register_params(p);
p.register_bool_param("at_labels_cex", m_at_labels_cex,
"only use labels that contain '@' when building multiple counterexamples");
p.register_bool_param("check_at_labels", m_check_at_labels,
@ -33,14 +31,12 @@ void front_end_params::register_params(ini_params & p) {
p.register_bool_param("type_check", m_well_sorted_check, "enable/disable type checker");
p.register_bool_param("well_sorted_check", m_well_sorted_check, "enable/disable type checker");
p.register_bool_param("interactive", m_interactive, "enable interactive mode using Simplify input format");
p.register_unsigned_param("soft_timeout", m_soft_timeout, "set approximate timeout for each solver query (milliseconds), the value 0 represents no timeout", true);
p.register_double_param("instruction_max", m_instr_out, "set the (approximate) maximal number of instructions per invocation of check", true);
p.register_bool_param("auto_config", m_auto_config, "use heuristics to set Z3 configuration parameters, it is only available for the SMT-LIB input format");
p.register_int_param("proof_mode", 0, 2, reinterpret_cast<int&>(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain");
p.register_bool_param("trace", m_trace, "enable tracing for the Axiom Profiler tool");
p.register_string_param("trace_file_name", m_trace_file_name, "tracing file name");
p.register_bool_param("async_commands", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end.");
p.register_bool_param("display_config", m_display_config, "display configuration used by Z3");
#ifdef _WINDOWS
@ -51,29 +47,10 @@ void front_end_params::register_params(ini_params & p) {
"set hard upper limit for memory consumption (in megabytes)");
#endif
#ifndef _EXTERNAL_RELEASE
// external users should not have access to it.
p.register_bool_param("preprocess", m_preprocess);
#endif
p.register_bool_param("user_theory_preprocess_axioms",
m_user_theory_preprocess_axioms,
"Apply full pre-processing to user theory axioms",
true);
p.register_bool_param("user_theory_persist_axioms",
m_user_theory_persist_axioms,
"Persist user axioms to the base level",
true);
p.register_bool_param("smtlib2_compliant", m_smtlib2_compliant);
p.register_bool_param("ignore_bad_patterns", m_ignore_bad_patterns);
PRIVATE_PARAMS({
p.register_bool_param("ignore_checksat", m_ignore_checksat);
p.register_bool_param("debug_ref_count", m_debug_ref_count);
p.register_bool_param("ignore_user_patterns", m_ignore_user_patterns);
p.register_bool_param("incremental_core_assert", m_incremental_core_assert);
DEBUG_CODE(p.register_int_param("copy_params", m_copy_params););
});

35
src/front_end_params/front_end_params.h
View file

@ -23,22 +23,15 @@ Revision History:
#include"ast.h"
#include"preprocessor_params.h"
#include"smt_params.h"
#include"parser_params.h"
#include"arith_simplifier_params.h"
#include"model_params.h"
struct front_end_params : public preprocessor_params, public smt_params, public parser_params,
public arith_simplifier_params, public model_params
{
struct front_end_params : public preprocessor_params, public smt_params,
public arith_simplifier_params {
ref<param_vector> m_param_vector;
unsigned m_max_num_cex; // maximum number of counterexamples
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_default_qid;
bool m_interactive;
bool m_well_sorted_check;
bool m_ignore_bad_patterns;
bool m_ignore_user_patterns;
bool m_incremental_core_assert; // assert conditions to the core incrementally
unsigned m_soft_timeout;
double m_instr_out;
@ -46,32 +39,26 @@ struct front_end_params : public preprocessor_params, public smt_params, public
unsigned m_memory_max_size;
proof_gen_mode m_proof_mode;
bool m_auto_config;
bool m_smtlib2_compliant;
#ifdef Z3DEBUG
int m_copy_params; // used for testing copy params... Invoke method copy_params(m_copy_params) in main.cpp when diff -1.
#endif
bool m_preprocess; // temporary hack for disabling all preprocessing..
bool m_ignore_checksat; // abort before checksat... for internal debugging
bool m_debug_ref_count;
bool m_trace;
std::string m_trace_file_name;
std::fstream* m_trace_stream;
bool m_async_commands;
bool m_display_config;
bool m_user_theory_preprocess_axioms;
bool m_user_theory_persist_axioms;
bool m_nlsat; // temporary hack until strategic_solver is ported to new tactic framework
bool m_dump_goal_as_smt;
front_end_params():
m_param_vector(alloc(param_vector, this)),
m_max_num_cex(1),
m_at_labels_cex(false),
m_check_at_labels(false),
m_default_qid(false),
m_interactive(false),
m_well_sorted_check(true),
m_ignore_bad_patterns(true),
m_ignore_user_patterns(false),
m_incremental_core_assert(true),
m_soft_timeout(0),
m_instr_out(0.0),
@ -83,25 +70,17 @@ struct front_end_params : public preprocessor_params, public smt_params, public
#else
m_auto_config(false),
#endif
#if 0
m_smtlib2_compliant(true),
#else
m_smtlib2_compliant(false),
#endif
#ifdef Z3DEBUG
m_copy_params(-1),
#endif
m_preprocess(true), // temporary hack for disabling all preprocessing..
m_ignore_checksat(false),
m_debug_ref_count(false),
m_trace(false),
m_trace_file_name("z3.log"),
m_trace_stream(NULL),
m_async_commands(true),
m_display_config(false),
m_user_theory_preprocess_axioms(false),
m_user_theory_persist_axioms(false),
m_nlsat(false) {
m_nlsat(false),
m_dump_goal_as_smt(false) {
}
void register_params(ini_params & p);

35
src/front_end_params/model_params.cpp
View file

@ -1,35 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
model_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-08-23.
Revision History:
--*/
#include"model_params.h"
void model_params::register_params(ini_params & p) {
p.register_bool_param("model_partial", m_model_partial, "enable/disable partial function interpretations", true);
p.register_bool_param("model_v1", m_model_v1_pp,
"use Z3 version 1.x pretty printer", true);
p.register_bool_param("model_v2", m_model_v2_pp,
"use Z3 version 2.x (x <= 16) pretty printer", true);
p.register_bool_param("model_compact", m_model_compact,
"try to compact function graph (i.e., function interpretations that are lookup tables", true);
p.register_bool_param("model_completion", m_model_completion,
"assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
}

43
src/front_end_params/model_params.h
View file

@ -1,43 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
model_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-08-23.
Revision History:
--*/
#ifndef _MODEL_PARAMS_H_
#define _MODEL_PARAMS_H_
#include"ini_file.h"
struct model_params {
bool m_model_partial;
bool m_model_compact;
bool m_model_v1_pp;
bool m_model_v2_pp;
bool m_model_completion;
model_params():
m_model_partial(false),
m_model_compact(false),
m_model_v1_pp(false),
m_model_v2_pp(false),
m_model_completion(false) {
}
void register_params(ini_params & p);
};
#endif /* _MODEL_PARAMS_H_ */

14
src/front_end_params/parser_params.cpp
View file

@ -1,14 +0,0 @@
#include "parser_params.h"
parser_params::parser_params() :
m_dump_goal_as_smt(false),
m_display_error_for_vs(false) {
}
void parser_params::register_params(ini_params & p) {
p.register_bool_param("dump_goal_as_smt", m_dump_goal_as_smt, "write goal back to output in SMT format");
p.register_bool_param("display_error_for_visual_studio", m_display_error_for_vs, "display error messages in Visual Studio format");
}

33
src/front_end_params/parser_params.h
View file

@ -1,33 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
parser_params.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2008-04-21.
Revision History:
--*/
#ifndef _PARSER_PARAMS_H_
#define _PARSER_PARAMS_H_
#include"ini_file.h"
struct parser_params {
bool m_dump_goal_as_smt; // re-print goal as SMT benchmark.
bool m_display_error_for_vs; // print error in vs format.
parser_params();
void register_params(ini_params & p);
};
#endif /* _PARSER_PARAMS_H_ */

12
src/front_end_params/smt_params.cpp
View file

@ -103,5 +103,17 @@ void smt_params::register_params(ini_params & p) {
p.register_bool_param("model_on_final_check", m_model_on_final_check, "display candidate model (in the standard output) whenever Z3 hits a final check", true);
p.register_unsigned_param("progress_sampling_freq", m_progress_sampling_freq, "frequency for progress output in miliseconds");
p.register_bool_param("user_theory_preprocess_axioms",
m_user_theory_preprocess_axioms,
"Apply full pre-processing to user theory axioms",
true);
p.register_bool_param("user_theory_persist_axioms",
m_user_theory_persist_axioms,
"Persist user axioms to the base level",
true);
}

18
src/front_end_params/smt_params.h
View file

@ -169,6 +169,7 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
//
// -----------------------------------
bool m_model;
bool m_model_compact;
bool m_model_validate;
bool m_model_on_timeout;
bool m_model_on_final_check;
@ -187,6 +188,15 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
// -----------------------------------
bool m_display_installed_theories;
// -----------------------------------
//
// From front_end_params
//
// -----------------------------------
bool m_preprocess; // temporary hack for disabling all preprocessing..
bool m_user_theory_preprocess_axioms;
bool m_user_theory_persist_axioms;
smt_params():
m_display_proof(false),
m_display_dot_proof(false),
@ -241,11 +251,17 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
m_display_ll_bool_var2expr(false),
m_abort_after_preproc(false),
m_model(true),
m_model_compact(false),
m_model_validate(false),
m_model_on_timeout(false),
m_model_on_final_check(false),
m_progress_sampling_freq(0),
m_display_installed_theories(false) {
m_display_installed_theories(false),
m_preprocess(true), // temporary hack for disabling all preprocessing..
m_user_theory_preprocess_axioms(false),
m_user_theory_persist_axioms(false)
{
}
void register_params(ini_params & p);

10
src/parsers/smt/smtlib_solver.cpp
View file

@ -28,6 +28,8 @@ Revision History:
#include"solver.h"
#include"smt_strategic_solver.h"
#include"cmd_context.h"
#include"model_params.hpp"
#include"parser_params.hpp"
namespace smtlib {
@ -35,8 +37,9 @@ namespace smtlib {
m_ast_manager(params.m_proof_mode, params.m_trace_stream),
m_params(params),
m_ctx(0),
m_parser(parser::create(m_ast_manager, params.m_ignore_user_patterns)),
m_error_code(0) {
parser_params ps;
m_parser = parser::create(m_ast_manager, ps.ignore_user_patterns());
m_parser->initialize_smtlib();
}
@ -82,7 +85,7 @@ namespace smtlib {
// Hack: it seems SMT-LIB allow benchmarks without any :formula
benchmark.add_formula(m_ast_manager.mk_true());
}
m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic());
m_ctx = alloc(cmd_context, true, &m_ast_manager, benchmark.get_logic());
m_ctx->set_solver(mk_smt_strategic_solver(false));
theory::expr_iterator fit = benchmark.begin_formulas();
theory::expr_iterator fend = benchmark.end_formulas();
@ -105,7 +108,8 @@ namespace smtlib {
model_ref md;
if (r->status() != l_false) r->get_model(md);
if (md.get() != 0 && m_params.m_model) {
model_v2_pp(std::cout, *(md.get()), m_params.m_model_partial);
model_params p;
model_v2_pp(std::cout, *(md.get()), p.partial());
}
}
else {

26
src/parsers/smt2/smt2parser.cpp
View file

@ -28,7 +28,7 @@ Revision History:
#include"rewriter.h"
#include"has_free_vars.h"
#include"ast_smt2_pp.h"
#include"front_end_params.h"
#include"parser_params.hpp"
namespace smt2 {
typedef cmd_exception parser_exception;
@ -106,9 +106,14 @@ namespace smt2 {
ast_manager & m() const { return m_ctx.m(); }
pdecl_manager & pm() const { return m_ctx.pm(); }
sexpr_manager & sm() const { return m_ctx.sm(); }
bool m_ignore_user_patterns;
bool m_ignore_bad_patterns;
bool m_display_error_for_vs;
bool ignore_user_patterns() const { return m_ctx.params().m_ignore_user_patterns; }
bool ignore_bad_patterns() const { return m_ctx.params().m_ignore_bad_patterns; }
bool ignore_user_patterns() const { return m_ignore_user_patterns; }
bool ignore_bad_patterns() const { return m_ignore_bad_patterns; }
bool use_vs_format() const { return m_display_error_for_vs; }
struct psort_frame {
psort_decl * m_decl;
@ -383,8 +388,6 @@ namespace smt2 {
void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); }
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
bool use_vs_format() const { return m_ctx.params().m_display_error_for_vs; }
void error(unsigned line, unsigned pos, char const * msg) {
if (use_vs_format()) {
m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
@ -2354,9 +2357,9 @@ namespace smt2 {
}
public:
parser(cmd_context & ctx, std::istream & is, bool interactive):
parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & _p):
m_ctx(ctx),
m_scanner(ctx, is, interactive),
m_scanner(ctx, is, interactive, _p),
m_curr(scanner::NULL_TOKEN),
m_curr_cmd(0),
m_num_bindings(0),
@ -2393,6 +2396,11 @@ namespace smt2 {
m_num_open_paren(0) {
// the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created.
// SASSERT(!m_ctx.has_manager());
parser_params p(_p);
m_ignore_user_patterns = p.ignore_user_patterns();
m_ignore_bad_patterns = p.ignore_bad_patterns();
m_display_error_for_vs = p.error_for_visual_studio();
}
~parser() {
@ -2487,8 +2495,8 @@ namespace smt2 {
};
};
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive) {
smt2::parser p(ctx, is, interactive);
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps) {
smt2::parser p(ctx, is, interactive, ps);
return p();
}

2
src/parsers/smt2/smt2parser.h
View file

@ -21,6 +21,6 @@ Revision History:
#include"cmd_context.h"
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false);
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref());
#endif

9
src/parsers/smt2/smt2scanner.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include"smt2scanner.h"
#include"parser_params.hpp"
namespace smt2 {
@ -241,7 +242,7 @@ namespace smt2 {
}
}
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive, params_ref const & _p):
m_ctx(ctx),
m_interactive(interactive),
m_spos(0),
@ -253,6 +254,10 @@ namespace smt2 {
m_bend(0),
m_stream(stream),
m_cache_input(false) {
parser_params p(_p);
m_smtlib2_compliant = p.smt2_compliant();
for (int i = 0; i < 256; ++i) {
m_normalized[i] = (char) i;
}
@ -325,7 +330,7 @@ namespace smt2 {
case '#':
return read_bv_literal();
case '-':
if (m_ctx.is_smtlib2_compliant())
if (m_smtlib2_compliant)
return read_symbol();
else
return read_signed_number();

4
src/parsers/smt2/smt2scanner.h
View file

@ -55,6 +55,8 @@ namespace smt2 {
svector<char> m_cache;
svector<char> m_cache_result;
bool m_smtlib2_compliant;
char curr() const { return m_curr; }
void new_line() { m_line++; m_spos = 0; }
void next();
@ -74,7 +76,7 @@ namespace smt2 {
EOF_TOKEN
};
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false, params_ref const & p = params_ref());
~scanner() {}

6
src/parsers/util/parser_params.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params('parser',
export=True,
params=(('ignore_user_patterns', BOOL, False, 'ignore patterns provided by the user'),
('ignore_bad_patterns', BOOL, True, 'ignore malformed patterns'),
('error_for_visual_studio', BOOL, False, 'display error messages in Visual Studio format'),
('smt2_compliant', BOOL, False, 'enable/disable SMT-LIB 2.0 compliance')))

16
src/shell/main.cpp
View file

@ -77,7 +77,7 @@ void display_usage() {
std::cout << " " << OPT << "version prints version number of Z3.\n";
std::cout << " " << OPT << "v:level be verbose, where <level> is the verbosity level.\n";
std::cout << " " << OPT << "nw disable warning messages.\n";
std::cout << " " << OPT << "params display all available parameters.\n";
std::cout << " " << OPT << "ps display all available parameters.\n";
std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n";
std::cout << "\nResources:\n";
// timeout and memout are now available on Linux and OSX too.
@ -184,10 +184,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
if (i < argc - 1)
g_aux_input_file += " ";
}
if (g_front_end_params->m_interactive) {
warning_msg("ignoring input file in interactive mode.");
}
else if (g_input_file) {
if (g_input_file) {
warning_msg("input file was already specified.");
}
else {
@ -284,7 +281,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
else if (strcmp(opt_name, "nw") == 0) {
enable_warning_messages(false);
}
else if (strcmp(opt_name, "params") == 0) {
else if (strcmp(opt_name, "ps") == 0) {
gparams::display(std::cout);
exit(0);
}
@ -324,10 +321,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
gparams::set(key, value);
}
else {
if (g_front_end_params->m_interactive) {
warning_msg("ignoring input file in interactive mode.");
}
else if (g_input_file) {
if (g_input_file) {
warning_msg("input file was already specified.");
}
else {
@ -389,7 +383,7 @@ int main(int argc, char ** argv) {
if (g_input_file && g_standard_input) {
error("using standard input to read formula.");
}
if (!g_input_file && !g_front_end_params->m_interactive && !g_standard_input) {
if (!g_input_file && !g_standard_input) {
error("input file was not specified.");
}

2
src/shell/smtlib_frontend.cpp
View file

@ -97,7 +97,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
g_start_time = clock();
register_on_timeout_proc(on_timeout);
signal(SIGINT, on_ctrl_c);
cmd_context ctx(&front_end_params);
cmd_context ctx;
// temporary hack until strategic_solver is ported to new tactic framework
if (front_end_params.m_nlsat) {

8
src/smt/proto_model/proto_model.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include"proto_model.h"
#include"model_params.hpp"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"var_subst.h"
@ -26,15 +27,16 @@ Revision History:
#include"model_v2_pp.h"
#include"basic_simplifier_plugin.h"
proto_model::proto_model(ast_manager & m, simplifier & s, model_params const & p):
proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
model_core(m),
m_params(p),
m_asts(m),
m_simplifier(s),
m_afid(m.get_family_id(symbol("array"))) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);
m_model_partial = model_params(p).partial();
}
void proto_model::reset_finterp() {
@ -620,7 +622,7 @@ void proto_model::complete_partial_func(func_decl * f) {
\brief Set the (else) field of function interpretations...
*/
void proto_model::complete_partial_funcs() {
if (m_params.m_model_partial)
if (m_model_partial)
return;
// m_func_decls may be "expanded" when we invoke get_some_value.

9
src/smt/proto_model/proto_model.h
View file

@ -29,16 +29,15 @@ Revision History:
#define _PROTO_MODEL_H_
#include"model_core.h"
#include"model_params.h"
#include"value_factory.h"
#include"plugin_manager.h"
#include"simplifier.h"
#include"arith_decl_plugin.h"
#include"func_decl_dependencies.h"
#include"model.h"
#include"params.h"
class proto_model : public model_core {
model_params const & m_params;
ast_ref_vector m_asts;
plugin_manager<value_factory> m_factories;
user_sort_factory * m_user_sort_factory;
@ -47,6 +46,8 @@ class proto_model : public model_core {
func_decl_set m_aux_decls;
ptr_vector<expr> m_tmp;
bool m_model_partial;
void reset_finterp();
expr * mk_some_interp_for(func_decl * d);
@ -60,11 +61,9 @@ class proto_model : public model_core {
public:
proto_model(ast_manager & m, simplifier & s, model_params const & p);
proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref());
virtual ~proto_model();
model_params const & get_model_params() const { return m_params; }
void register_factory(value_factory * f) { m_factories.register_plugin(f); }
bool eval(expr * e, expr_ref & result, bool model_completion = false);

3
src/smt/smt_model_generator.cpp
View file

@ -48,7 +48,8 @@ namespace smt {
void model_generator::init_model() {
SASSERT(!m_model);
m_model = alloc(proto_model, m_manager, m_context->get_simplifier(), m_context->get_fparams());
// PARAM-TODO
m_model = alloc(proto_model, m_manager, m_context->get_simplifier()); // , m_context->get_fparams());
ptr_vector<theory>::const_iterator it = m_context->begin_theories();
ptr_vector<theory>::const_iterator end = m_context->end_theories();
for (; it != end; ++it) {

190
src/util/gparams.cpp
View file

@ -26,7 +26,6 @@ struct gparams::imp {
param_descrs m_param_descrs;
dictionary<params_ref *> m_module_params;
params_ref m_params;
params_ref m_empty;
public:
imp() {
}
@ -49,28 +48,37 @@ public:
}
void register_global(param_descrs & d) {
m_param_descrs.copy(d);
#pragma omp critical (gparams)
{
m_param_descrs.copy(d);
}
}
void register_module(char const * module_name, param_descrs * d) {
symbol s(module_name);
param_descrs * old_d;
if (m_module_param_descrs.find(s, old_d)) {
old_d->copy(*d);
dealloc(d);
}
else {
m_module_param_descrs.insert(s, d);
#pragma omp critical (gparams)
{
symbol s(module_name);
param_descrs * old_d;
if (m_module_param_descrs.find(s, old_d)) {
old_d->copy(*d);
dealloc(d);
}
else {
m_module_param_descrs.insert(s, d);
}
}
}
void display(std::ostream & out, unsigned indent, bool smt2_style) {
m_param_descrs.display(out, indent, smt2_style);
dictionary<param_descrs*>::iterator it = m_module_param_descrs.begin();
dictionary<param_descrs*>::iterator end = m_module_param_descrs.end();
for (; it != end; ++it) {
out << "[module] " << it->m_key << "\n";
it->m_value->display(out, indent + 4, smt2_style);
#pragma omp critical (gparams)
{
m_param_descrs.display(out, indent, smt2_style);
dictionary<param_descrs*>::iterator it = m_module_param_descrs.begin();
dictionary<param_descrs*>::iterator end = m_module_param_descrs.end();
for (; it != end; ++it) {
out << "[module] " << it->m_key << "\n";
it->m_value->display(out, indent + 4, smt2_style);
}
}
}
@ -102,15 +110,13 @@ public:
return m_params;
}
else {
params_ref * p;
if (m_module_params.find(mod_name, p)) {
return *p;
}
else {
params_ref * p = 0;
if (!m_module_params.find(mod_name, p)) {
p = alloc(params_ref);
m_module_params.insert(mod_name, p);
return *p;
}
SASSERT(p != 0);
return *p;
}
}
@ -119,9 +125,9 @@ public:
params_ref & ps = get_params(mod_name);
if (k == CPK_INVALID) {
if (mod_name == symbol::null)
throw default_exception("unknown parameter '%s'", param_name.bare_str());
throw exception("unknown parameter '%s'", param_name.bare_str());
else
throw default_exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
}
else if (k == CPK_UINT) {
long val = strtol(value, 0, 10);
@ -136,9 +142,9 @@ public:
}
else {
if (mod_name == symbol::null)
throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param_name.bare_str());
throw exception("invalid value '%s' for Boolean parameter '%s'", value, param_name.bare_str());
else
throw default_exception("invalid value '%s' for Boolean parameter '%s' at module '%s'", value, param_name.bare_str(), mod_name.bare_str());
throw exception("invalid value '%s' for Boolean parameter '%s' at module '%s'", value, param_name.bare_str(), mod_name.bare_str());
}
}
else if (k == CPK_SYMBOL) {
@ -149,47 +155,125 @@ public:
}
else {
if (mod_name == symbol::null)
throw default_exception("unsupported parameter type '%s'", param_name.bare_str());
throw exception("unsupported parameter type '%s'", param_name.bare_str());
else
throw default_exception("unsupported parameter type '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
throw exception("unsupported parameter type '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
}
}
void set(char const * name, char const * value) {
symbol m, p;
normalize(name, m, p);
if (m == symbol::null) {
set(m_param_descrs, p, value, m);
}
else {
param_descrs * d;
if (m_module_param_descrs.find(m, d)) {
set(*d, p, value, m);
bool error = false;
std::string error_msg;
#pragma omp critical (gparams)
{
try {
symbol m, p;
normalize(name, m, p);
if (m == symbol::null) {
set(m_param_descrs, p, value, m);
}
else {
param_descrs * d;
if (m_module_param_descrs.find(m, d)) {
set(*d, p, value, m);
}
else {
throw exception("invalid parameter, unknown module '%s'", m.bare_str());
}
}
}
else {
throw default_exception("invalid parameter, unknown module '%s'", m.bare_str());
catch (exception & ex) {
// Exception cannot cross critical section boundaries.
error = true;
error_msg = ex.msg();
}
}
if (error)
throw exception(error_msg);
}
std::string get_value(params_ref const & ps, symbol const & p) {
std::ostringstream buffer;
ps.display(buffer, p);
return buffer.str();
}
std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) {
if (!d.contains(p)) {
if (m == symbol::null)
throw exception("unknown parameter '%s'", p.bare_str());
else
throw exception("unknown parameter '%s' at module '%s'", p.bare_str(), m.bare_str());
}
char const * r = d.get_default(p);
if (r == 0)
return "default";
return r;
}
std::string get_value(char const * name) {
// TODO
return "";
std::string r;
bool error = false;
std::string error_msg;
#pragma omp critical (gparams)
{
try {
symbol m, p;
normalize(name, m, p);
if (m == symbol::null) {
if (m_params.contains(p)) {
r = get_value(m_params, p);
}
else {
r = get_default(m_param_descrs, p, m);
}
}
else {
params_ref * ps = 0;
if (m_module_params.find(m, ps) && ps->contains(p)) {
r = get_value(*ps, p);
}
else {
param_descrs * d;
if (m_module_param_descrs.find(m, d)) {
r = get_default(*d, p, m);
}
else {
throw exception("unknown module '%s'", m.bare_str());
}
}
}
}
catch (exception & ex) {
// Exception cannot cross critical section boundaries.
error = true;
error_msg = ex.msg();
}
}
if (error)
throw exception(error_msg);
return r;
}
params_ref const & get_module(symbol const & module_name) {
params_ref get_module(symbol const & module_name) {
params_ref result;
params_ref * ps = 0;
if (m_module_params.find(module_name, ps)) {
return *ps;
}
else {
return m_empty;
#pragma omp critical (gparams)
{
if (m_module_params.find(module_name, ps)) {
result = *ps;
}
}
return result;
}
params_ref const & get() {
return m_params;
params_ref get() {
params_ref result;
#pragma omp critical (gparams)
{
result = m_params;
}
return result;
}
};
@ -226,16 +310,16 @@ void gparams::register_module(char const * module_name, param_descrs * d) {
g_imp->register_module(module_name, d);
}
params_ref const & gparams::get_module(char const * module_name) {
params_ref gparams::get_module(char const * module_name) {
return get_module(symbol(module_name));
}
params_ref const & gparams::get_module(symbol const & module_name) {
params_ref gparams::get_module(symbol const & module_name) {
SASSERT(g_imp != 0);
return g_imp->get_module(module_name);
}
params_ref const & gparams::get() {
params_ref gparams::get() {
SASSERT(g_imp != 0);
return g_imp->get();
}

8
src/util/gparams.h
View file

@ -31,7 +31,7 @@ public:
\brief Set a global parameter \c name with \c value.
The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'.
The character '.' is used a delimiter (more later).
The character '.' is a delimiter (more later).
The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
Thus, the following parameter names are considered equivalent: "auto-config" and "AUTO_CONFIG".
@ -90,13 +90,13 @@ public:
// In this example "p" will contain "decimal" -> true after executing this function.
params_ref const & p = get_module_params("pp")
*/
static params_ref const & get_module(char const * module_name);
static params_ref const & get_module(symbol const & module_name);
static params_ref get_module(char const * module_name);
static params_ref get_module(symbol const & module_name);
/**
\brief Return the global parameter set (i.e., parameters that are not associated with any particular module).
*/
static params_ref const & get();
static params_ref get();
/**
\brief Dump information about available parameters in the given output stream.

25
src/util/memory_manager.cpp
View file

@ -1,9 +1,9 @@
#include<iostream>
#include<stdlib.h>
#include<limits.h>
#include"trace.h"
#include"memory_manager.h"
#include"error_codes.h"
// The following two function are automatically generated by the mk_make.py script.
// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
// For example, rational.h contains
@ -27,6 +27,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
}
volatile bool g_memory_out_of_memory = false;
bool g_memory_initialized = false;
long long g_memory_alloc_size = 0;
long long g_memory_max_size = 0;
long long g_memory_max_used_size = 0;
@ -70,8 +71,20 @@ mem_usage_report g_info;
#endif
void memory::initialize(size_t max_size) {
bool initialize = false;
#pragma omp critical (z3_memory_manager)
{
// only update the maximum size if max_size != UINT_MAX
if (max_size != UINT_MAX)
g_memory_max_size = max_size;
if (!g_memory_initialized) {
g_memory_initialized = true;
initialize = true;
}
}
if (!initialize)
return;
g_memory_out_of_memory = false;
g_memory_max_size = max_size;
mem_initialize();
}
@ -108,8 +121,12 @@ void memory::set_max_size(size_t max_size) {
static bool g_finalizing = false;
void memory::finalize() {
g_finalizing = true;
mem_finalize();
if (g_memory_initialized) {
g_finalizing = true;
mem_finalize();
g_memory_initialized = false;
g_finalizing = false;
}
}
unsigned long long memory::get_allocation_size() {

14
src/util/params.cpp
View file

@ -57,6 +57,10 @@ struct param_descrs::imp {
void erase(symbol const & name) {
m_info.erase(name);
}
bool contains(symbol const & name) const {
return m_info.contains(name);
}
param_kind get_kind(symbol const & name) const {
info i;
@ -157,6 +161,14 @@ void param_descrs::insert(char const * name, param_kind k, char const * descr, c
insert(symbol(name), k, descr, def);
}
bool param_descrs::contains(char const * name) const {
return contains(symbol(name));
}
bool param_descrs::contains(symbol const & name) const {
return m_imp->contains(name);
}
char const * param_descrs::get_descr(char const * name) const {
return get_descr(symbol(name));
}
@ -345,7 +357,7 @@ public:
continue;
switch (it->second.m_kind) {
case CPK_BOOL:
out << it->second.m_bool_value;
out << (it->second.m_bool_value?"true":"false");
return;
case CPK_UINT:
out << it->second.m_uint_value;

2
src/util/params.h
View file

@ -109,6 +109,8 @@ public:
void copy(param_descrs & other);
void insert(char const * name, param_kind k, char const * descr, char const * def = 0);
void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0);
bool contains(char const * name) const;
bool contains(symbol const & name) const;
void erase(char const * name);
void erase(symbol const & name);
param_kind get_kind(char const * name) const;