mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-12-02 15:33:24 -08:00
commit 6a3e2d0f00
301 changed files with 3699 additions and 5652 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_ast.cpp
View file

@ -36,6 +36,7 @@ Revision History:
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"scoped_timer.h"
#include"pp_params.hpp"
extern "C" {
@ -674,8 +675,8 @@ extern "C" {
ast_manager & m = mk_c(c)->m();
expr * a = to_expr(_a);
params_ref p = to_param_ref(_p);
unsigned timeout = p.get_uint(":timeout", UINT_MAX);
bool use_ctrl_c = p.get_bool(":ctrl-c", false);
unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = p.get_bool("ctrl_c", false);
th_rewriter m_rw(m, p);
expr_ref result(m);
cancel_eh<th_rewriter> eh(m_rw);
@ -833,7 +834,8 @@ extern "C" {
break;
case Z3_PRINT_SMTLIB_COMPLIANT: {
ast_smt_pp pp(mk_c(c)->m());
pp.set_simplify_implies(get_pp_default_params().m_pp_simplify_implies);
pp_params params;
pp.set_simplify_implies(params.simplify_implies());
ast* a1 = to_ast(a);
pp.set_logic(mk_c(c)->fparams().m_smtlib_logic.c_str());
if (!is_expr(a1)) {
@ -886,7 +888,8 @@ extern "C" {
pp.set_logic(logic);
pp.set_status(status);
pp.add_attributes(attributes);
pp.set_simplify_implies(get_pp_default_params().m_pp_simplify_implies);
pp_params params;
pp.set_simplify_implies(params.simplify_implies());
for (unsigned i = 0; i < num_assumptions; ++i) {
pp.add_assumption(to_expr(assumptions[i]));
}

126
src/api/api_config_params.cpp
View file

@ -17,106 +17,92 @@ Revision History:
--*/
#include"z3.h"
#include"api_context.h"
#include"api_config_params.h"
#include"pp.h"
#include"api_log_macros.h"
#include"api_util.h"
#include"cmd_context.h"
#include"symbol.h"
namespace api {
config_params::config_params():
m_ini(false /* do not abort on errors */) {
register_verbosity_level(m_ini);
register_warning(m_ini);
m_params.register_params(m_ini);
register_pp_params(m_ini);
}
config_params::config_params(front_end_params const & p):m_params(p) {
register_verbosity_level(m_ini);
register_warning(m_ini);
register_pp_params(m_ini);
}
};
extern std::string smt_keyword2opt_name(symbol const & opt);
#include"gparams.h"
#include"env_params.h"
#include"context_params.h"
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);
env_params::updt_params();
}
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));
Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
RETURN_Z3(r);
}
void Z3_API Z3_del_config(Z3_config c) {
LOG_Z3_del_config(c);
dealloc((reinterpret_cast<api::config_params*>(c)));
dealloc((reinterpret_cast<context_params*>(c)));
}
void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
try {
LOG_Z3_set_param_value(c, param_id, param_value);
api::config_params* p = reinterpret_cast<api::config_params*>(c);
if (param_id != 0 && param_id[0] == ':') {
// Allow SMT2 style paramater names such as :model, :relevancy, etc
std::string new_param_id = smt_keyword2opt_name(symbol(param_id));
p->m_ini.set_param_value(new_param_id.c_str(), param_value);
}
else {
p->m_ini.set_param_value(param_id, param_value);
}
LOG_Z3_set_param_value(c, param_id, param_value);
try {
context_params * p = reinterpret_cast<context_params*>(c);
p->set(param_id, param_value);
}
catch (set_get_param_exception & ex) {
// The error handler was not set yet.
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.get_msg();
buffer << "Error setting " << param_id << ": " << ex.msg();
warning_msg(buffer.str().c_str());
}
}
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();
ini_params ini;
mk_c(c)->fparams().register_params(ini);
register_pp_params(ini);
register_verbosity_level(ini);
register_warning(ini);
if (mk_c(c)->has_solver()) {
ini.freeze();
}
if (param_id != 0 && param_id[0] == ':') {
// Allow SMT2 style paramater names such as :model, :relevancy, etc
std::string new_param_id = smt_keyword2opt_name(symbol(param_id));
ini.set_param_value(new_param_id.c_str(), param_value);
}
else {
ini.set_param_value(param_id, param_value);
}
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);
mk_c(c)->params().set(param_id, param_value);
Z3_CATCH;
}
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);
ini_params ini;
mk_c(c)->fparams().register_params(ini);
register_verbosity_level(ini);
register_pp_params(ini);
register_warning(ini);
std::string param_value_s;
if (!ini.get_param_value(param_id, param_value_s)) {
if (param_value) *param_value = 0;
return false;
}
if (param_value) {
*param_value = mk_c(c)->mk_external_string(param_value_s);
}
return true;
// TODO
return Z3_FALSE;
}
};

36
src/api/api_config_params.h
View file

@ -1,36 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
api_config_params.h
Abstract:
Configuration parameters
Author:
Leonardo de Moura (leonardo) 2012-02-29.
Revision History:
--*/
#ifndef _API_CONFIG_PARAMS_H_
#define _API_CONFIG_PARAMS_H_
#include"ini_file.h"
#include"front_end_params.h"
namespace api {
class config_params {
public:
ini_params m_ini;
front_end_params m_params;
config_params();
config_params(front_end_params const & p);
};
};
#endif

36
src/api/api_context.cpp
View file

@ -18,7 +18,6 @@ Revision History:
--*/
#include"api_context.h"
#include"api_config_params.h"
#include"smtparser.h"
#include"version.h"
#include"ast_pp.h"
@ -54,14 +53,6 @@ namespace api {
return static_cast<Z3_search_failure>(f);
}
context::param_ini::param_ini(front_end_params & p) : m_params(p) {
p.open_trace_file();
}
context::param_ini::~param_ini() {
m_params.close_trace_file();
}
context::add_plugins::add_plugins(ast_manager & m) {
reg_decl_plugins(m);
}
@ -88,11 +79,10 @@ namespace api {
}
}
context::context(config_params * p, bool user_ref_count):
m_params(p ? p->m_params : front_end_params()),
m_param_ini(m_params),
context::context(context_params * p, bool user_ref_count):
m_params(*p),
m_user_ref_count(user_ref_count),
m_manager(m_params.m_proof_mode, m_params.m_trace_stream),
m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED, m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
m_plugins(m_manager),
m_arith_util(m_manager),
m_bv_util(m_manager),
@ -115,8 +105,6 @@ namespace api {
//
// Configuration parameter settings.
//
memory::set_high_watermark(static_cast<size_t>(m_params.m_memory_high_watermark)*1024*1024);
memory::set_max_size(static_cast<size_t>(m_params.m_memory_max_size)*1024*1024);
if (m_params.m_debug_ref_count) {
m_manager.debug_ref_count();
}
@ -335,7 +323,8 @@ namespace api {
smt::kernel & context::get_smt_kernel() {
if (!m_solver) {
m_solver = alloc(smt::kernel, m_manager, m_params);
m_fparams.updt_params(m_params);
m_solver = alloc(smt::kernel, m_manager, m_fparams);
}
return *m_solver;
}
@ -420,15 +409,15 @@ extern "C" {
Z3_context Z3_API Z3_mk_context(Z3_config c) {
LOG_Z3_mk_context(c);
memory::initialize(0);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<api::config_params*>(c), false));
memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
RETURN_Z3(r);
}
Z3_context Z3_API Z3_mk_context_rc(Z3_config c) {
LOG_Z3_mk_context_rc(c);
memory::initialize(0);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<api::config_params*>(c), true));
memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
RETURN_Z3(r);
}
@ -574,11 +563,4 @@ ast_manager & Z3_API Z3_get_manager(__in Z3_context c) {
return mk_c(c)->m();
}
front_end_params& Z3_API Z3_get_parameters(__in Z3_context c) {
return mk_c(c)->fparams();
}
Z3_context Z3_mk_context_from_params(front_end_params const& p) {
api::config_params cp(p);
return reinterpret_cast<Z3_context>(alloc(api::context, &cp));
}

35
src/api/api_context.h
View file

@ -28,32 +28,22 @@ Revision History:
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"smt_kernel.h"
#include"front_end_params.h"
#include"smt_params.h"
#include"event_handler.h"
#include"tactic_manager.h"
#include"context_params.h"
namespace smtlib {
class parser;
};
namespace api {
class config_params;
Z3_search_failure mk_Z3_search_failure(smt::failure f);
class context : public tactic_manager {
class param_ini {
front_end_params & m_params;
public:
param_ini(front_end_params & p);
~param_ini();
};
struct add_plugins { add_plugins(ast_manager & m); };
front_end_params m_params;
param_ini m_param_ini;
context_params m_params;
bool m_user_ref_count; //!< if true, the user is responsible for managing referenc counters.
ast_manager m_manager;
add_plugins m_plugins;
@ -62,8 +52,11 @@ namespace api {
bv_util m_bv_util;
datalog::dl_decl_util m_datalog_util;
// Support for old solver API
smt_params m_fparams;
smt::kernel * m_solver; // General purpose solver for backward compatibility
// -------------------------------
ast_ref_vector m_last_result; //!< used when m_user_ref_count == true
ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false
unsigned_vector m_ast_lim;
@ -103,11 +96,16 @@ namespace api {
//
// ------------------------
context(config_params * p, bool user_ref_count = false);
context(context_params * p, bool user_ref_count = false);
~context();
front_end_params & fparams() { return m_params; }
ast_manager & m() { return m_manager; }
context_params & params() { return m_params; }
bool produce_proofs() const { return m_manager.proofs_enabled(); }
bool produce_models() const { return m_params.m_model; }
bool produce_unsat_cores() const { return m_params.m_unsat_core; }
bool use_auto_config() const { return m_params.m_auto_config; }
unsigned get_timeout() const { return m_params.m_timeout; }
arith_util & autil() { return m_arith_util; }
bv_util & bvutil() { return m_bv_util; }
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
@ -168,12 +166,13 @@ namespace api {
static void out_of_memory_handler(void * _ctx);
void check_sorts(ast * n);
// ------------------------
//
// Solver interface for backward compatibility
//
// ------------------------
smt_params & fparams() { return m_fparams; }
bool has_solver() const { return m_solver != 0; }
smt::kernel & get_smt_kernel();
void assert_cnstr(expr * a);

8
src/api/api_datalog.cpp
View file

@ -32,7 +32,7 @@ Revision History:
namespace api {
fixedpoint_context::fixedpoint_context(ast_manager& m, front_end_params& p) :
fixedpoint_context::fixedpoint_context(ast_manager& m, smt_params& p) :
m_state(0),
m_reduce_app(0),
m_reduce_assign(0),
@ -265,7 +265,7 @@ extern "C" {
RESET_ERROR_CODE();
lbool r = l_undef;
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
unsigned timeout = to_fixedpoint(d)->m_params.get_uint(":timeout", UINT_MAX);
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
api::context::set_interruptable(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);
@ -289,7 +289,7 @@ extern "C" {
LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations);
RESET_ERROR_CODE();
lbool r = l_undef;
unsigned timeout = to_fixedpoint(d)->m_params.get_uint(":timeout", UINT_MAX);
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
api::context::set_interruptable(*(mk_c(c)), eh);
{
@ -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)) {

4
src/api/api_datalog.h
View file

@ -21,7 +21,7 @@ Revision History:
#include"z3.h"
#include"ast.h"
#include"front_end_params.h"
#include"smt_params.h"
#include"dl_external_relation.h"
#include"dl_decl_plugin.h"
#include"smt_kernel.h"
@ -40,7 +40,7 @@ namespace api {
datalog::context m_context;
ast_ref_vector m_trail;
public:
fixedpoint_context(ast_manager& m, front_end_params& p);
fixedpoint_context(ast_manager& m, smt_params& p);
virtual ~fixedpoint_context() {}
family_id get_family_id() const { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); }
void set_state(void* state);

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.

24
src/api/api_solver.cpp
View file

@ -36,11 +36,17 @@ extern "C" {
static void init_solver_core(Z3_context c, Z3_solver _s) {
ast_manager & m = mk_c(c)->m();
Z3_solver_ref * s = to_solver(_s);
s->m_solver->set_produce_proofs(m.proofs_enabled());
s->m_solver->set_produce_unsat_cores(s->m_params.get_bool(":unsat-core", false));
s->m_solver->set_produce_models(s->m_params.get_bool(":model", true));
s->m_solver->set_front_end_params(mk_c(c)->fparams());
s->m_solver->updt_params(s->m_params);
s->m_solver->set_produce_proofs(mk_c(c)->produce_proofs());
s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", mk_c(c)->produce_unsat_cores()));
s->m_solver->set_produce_models(s->m_params.get_bool("model", mk_c(c)->produce_models()));
if (!mk_c(c)->use_auto_config()) {
params_ref p = s->m_params;
p.set_bool("auto_config", false);
s->m_solver->updt_params(p);
}
else {
s->m_solver->updt_params(s->m_params);
}
s->m_solver->init(m, s->m_logic);
s->m_initialized = true;
}
@ -127,8 +133,8 @@ extern "C" {
LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE();
if (to_solver(s)->m_initialized) {
bool old_model = to_solver(s)->m_params.get_bool(":model", true);
bool new_model = to_param_ref(p).get_bool(":model", true);
bool old_model = to_solver(s)->m_params.get_bool("model", true);
bool new_model = to_param_ref(p).get_bool("model", true);
if (old_model != new_model)
to_solver_ref(s)->set_produce_models(new_model);
to_solver_ref(s)->updt_params(to_param_ref(p));
@ -238,8 +244,8 @@ extern "C" {
}
}
expr * const * _assumptions = to_exprs(assumptions);
unsigned timeout = to_solver(s)->m_params.get_uint(":timeout", UINT_MAX);
bool use_ctrl_c = to_solver(s)->m_params.get_bool(":ctrl-c", false);
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<solver> eh(*to_solver_ref(s));
api::context::set_interruptable(*(mk_c(c)), eh);
lbool result;

4
src/api/api_tactic.cpp
View file

@ -404,8 +404,8 @@ extern "C" {
Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, mk_c(c)->m());
mk_c(c)->save_object(ref);
unsigned timeout = p.get_uint(":timeout", UINT_MAX);
bool use_ctrl_c = p.get_bool(":ctrl-c", false);
unsigned timeout = p.get_uint("timeout", UINT_MAX);
bool use_ctrl_c = p.get_bool("ctrl_c", false);
cancel_eh<tactic> eh(*to_tactic_ref(t));
to_tactic_ref(t)->updt_params(p);

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)
#########################################
#

100
src/api/z3_api.h
View file

@ -1233,25 +1233,88 @@ 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
- timeout (unsigned) default timeout (in milliseconds) used for solvers
- well_sorted_check type checker
- auto_config use heuristics to automatically select solver and configure it
- model model generation for solvers, this parameter can be overwritten when creating a solver
- validate_model validate models produced by solvers
- unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
\sa Z3_set_param_value
\sa Z3_del_config
@ -1271,18 +1334,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 +1426,18 @@ extern "C" {
#endif
/**
\brief Update a mutable configuration parameter.
\brief Set a value of a context parameter.
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
\sa 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 Return the value of a context parameter.
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
\sa Use #Z3_global_param_get
def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
*/

51
src/ast/ast.cpp
View file

@ -1196,13 +1196,36 @@ decl_plugin * user_sort_plugin::mk_fresh() {
//
// -----------------------------------
ast_manager::ast_manager(proof_gen_mode m, std::ostream *trace_stream, bool is_format_manager):
ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_format_manager):
m_alloc("ast_manager"),
m_expr_array_manager(*this, m_alloc),
m_expr_dependency_manager(*this, m_alloc),
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(m),
m_trace_stream(trace_stream) {
m_trace_stream(0),
m_trace_stream_owner(false) {
if (trace_file) {
m_trace_stream = alloc(std::fstream, trace_file, std::ios_base::out);
m_trace_stream_owner = true;
}
if (!is_format_manager)
m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true);
else
m_format_manager = 0;
init();
}
ast_manager::ast_manager(proof_gen_mode m, std::fstream * trace_stream, bool is_format_manager):
m_alloc("ast_manager"),
m_expr_array_manager(*this, m_alloc),
m_expr_dependency_manager(*this, m_alloc),
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(m),
m_trace_stream(trace_stream),
m_trace_stream_owner(false) {
if (!is_format_manager)
m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true);
else
@ -1216,9 +1239,10 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
m_expr_dependency_manager(*this, m_alloc),
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode),
m_trace_stream(src.m_trace_stream) {
m_trace_stream(src.m_trace_stream),
m_trace_stream_owner(false) {
SASSERT(!src.is_format_manager());
m_format_manager = 0;
m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true);
init();
copy_families_plugins(src);
}
@ -1256,6 +1280,7 @@ void ast_manager::init() {
ast_manager::~ast_manager() {
SASSERT(is_format_manager() || !m_family_manager.has_family(symbol("format")));
dec_ref(m_bool_sort);
dec_ref(m_proof_sort);
dec_ref(m_true);
@ -1294,6 +1319,13 @@ ast_manager::~ast_manager() {
#endif
if (m_format_manager != 0)
dealloc(m_format_manager);
if (m_trace_stream_owner) {
std::fstream & tmp = * m_trace_stream;
tmp << "[eof]\n";
tmp.close();
dealloc(m_trace_stream);
m_trace_stream = 0;
}
}
void ast_manager::compact_memory() {
@ -1873,8 +1905,8 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const
new_node = new (mem) app(decl, num_args, args);
r = register_node(new_node);
}
#ifndef SMTCOMP
if (m_trace_stream != NULL && r == new_node) {
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-app] #" << r->get_id() << " ";
if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") {
ast_ll_pp(*m_trace_stream, *this, r);
@ -1887,7 +1919,7 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const
*m_trace_stream << "\n";
}
}
#endif
return r;
}
@ -2064,8 +2096,7 @@ quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort *
num_no_patterns, no_patterns);
quantifier * r = register_node(new_node);
#ifndef SMTCOMP
if (m_trace_stream != NULL && r == new_node) {
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-quant] #" << r->get_id() << " " << qid;
for (unsigned i = 0; i < num_patterns; ++i) {
*m_trace_stream << " #" << patterns[i]->get_id();
@ -2073,7 +2104,7 @@ quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort *
*m_trace_stream << " #" << body->get_id() << "\n";
}
#endif
return r;
}

9
src/ast/ast.h
View file

@ -1350,7 +1350,8 @@ protected:
unsigned m_fresh_id;
bool m_debug_ref_count;
u_map<unsigned> m_debug_free_indices;
std::ostream* m_trace_stream;
std::fstream* m_trace_stream;
bool m_trace_stream_owner;
#ifdef Z3DEBUG
bool slow_not_contains(ast const * n);
#endif
@ -1361,10 +1362,14 @@ protected:
bool coercion_needed(func_decl * decl, unsigned num_args, expr * const * args);
public:
ast_manager(proof_gen_mode = PGM_DISABLED, std::ostream * trace_stream = NULL, bool is_format_manager = false);
ast_manager(proof_gen_mode = PGM_DISABLED, char const * trace_file = 0, bool is_format_manager = false);
ast_manager(proof_gen_mode, std::fstream * trace_stream, bool is_format_manager = false);
ast_manager(ast_manager const & src, bool disable_proofs = false);
~ast_manager();
bool has_trace_stream() const { return m_trace_stream != 0; }
std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
void enable_int_real_coercions(bool f) { m_int_real_coercions = f; }
bool int_real_coercions() const { return m_int_real_coercions; }

2
src/ast/ast_pp.h
View file

@ -24,7 +24,7 @@ Revision History:
#include"ast_smt2_pp.h"
struct mk_pp : public mk_ismt2_pp {
mk_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
}
mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):

8
src/ast/ast_printer.cpp
View file

@ -33,14 +33,14 @@ public:
virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const {
out << f->get_name();
}
virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), get_pp_default_params(), r); }
virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), get_pp_default_params(), r); }
virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), params_ref(), r); }
virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), params_ref(), r); }
virtual void pp(expr * n, format_ns::format_ref & r) const {
sbuffer<symbol> buf;
mk_smt2_format(n, env(), get_pp_default_params(), 0, 0, r, buf);
mk_smt2_format(n, env(), params_ref(), 0, 0, r, buf);
}
virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
mk_smt2_format(n, env(), get_pp_default_params(), num_vars, var_prefix, r, var_names);
mk_smt2_format(n, env(), params_ref(), num_vars, var_prefix, r, var_names);
}
virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
NOT_IMPLEMENTED_YET();

50
src/ast/ast_smt2_pp.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"algebraic_numbers.h"
#include"pp_params.hpp"
using namespace format_ns;
#define ALIAS_PREFIX "a"
@ -376,7 +377,6 @@ typedef app_ref_vector format_ref_vector;
class smt2_printer {
ast_manager & m_manager;
pp_params const & m_params;
smt2_pp_environment & m_env;
shared_occs m_soccs;
@ -421,6 +421,16 @@ class smt2_printer {
string_buffer<> m_next_name_buffer;
// Config
bool m_pp_decimal;
unsigned m_pp_decimal_precision;
bool m_pp_bv_lits;
bool m_pp_bv_neg;
unsigned m_pp_max_depth;
unsigned m_pp_min_alias_size;
bool m_pp_flat_assoc;
symbol next_name(char const * prefix, unsigned & idx) {
while (true) {
m_next_name_buffer.reset();
@ -508,10 +518,10 @@ class smt2_printer {
void pp_const(app * c) {
format * f;
if (m_env.get_autil().is_numeral(c) || m_env.get_autil().is_irrational_algebraic_numeral(c)) {
f = m_env.pp_arith_literal(c, m_params.m_pp_decimal, m_params.m_pp_decimal_precision);
f = m_env.pp_arith_literal(c, m_pp_decimal, m_pp_decimal_precision);
}
else if (m_env.get_bvutil().is_numeral(c)) {
f = m_env.pp_bv_literal(c, m_params.m_pp_bv_lits, m_params.m_pp_bv_neg);
f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg);
}
else if (m_env.get_futil().is_value(c)) {
f = m_env.pp_float_literal(c);
@ -584,8 +594,8 @@ class smt2_printer {
m_format_stack.shrink(fr.m_spos);
m_info_stack.shrink(fr.m_spos);
if (fr.m_use_alias && m_root != t &&
((f_info.m_depth >= m_params.m_pp_max_depth) ||
((f_info.m_weight >= m_params.m_pp_min_alias_size || is_quantifier(t)) && m_soccs.is_shared(t)))) {
((f_info.m_depth >= m_pp_max_depth) ||
((f_info.m_weight >= m_pp_min_alias_size || is_quantifier(t)) && m_soccs.is_shared(t)))) {
symbol a = next_alias();
TRACE("smt2_pp", tout << "a: " << a << " depth: " << f_info.m_depth << ", weight: " << f_info.m_weight
<< ", lvl: " << f_info.m_lvl << " t: #" << t->get_id() << "\n" << mk_ll_pp(t, m())
@ -602,7 +612,7 @@ class smt2_printer {
}
bool flat_assoc(app * t, frame const & fr) {
if (!m_params.m_pp_flat_assoc)
if (!m_pp_flat_assoc)
return false;
func_decl * f = t->get_decl();
if (f->is_associative() && m_frame_stack.size() >= 2 && !m_soccs.is_shared(t)) {
@ -943,9 +953,8 @@ class smt2_printer {
}
public:
smt2_printer(smt2_pp_environment & env, pp_params const & params):
smt2_printer(smt2_pp_environment & env, params_ref const & params):
m_manager(env.get_manager()),
m_params(params),
m_env(env),
m_soccs(m_manager),
m_root(0),
@ -953,6 +962,15 @@ public:
m_next_alias_idx(1),
m_format_stack(fm()) {
init_expr2alias_stack();
pp_params p(params);
m_pp_decimal = p.decimal();
m_pp_decimal_precision = p.decimal_precision();
m_pp_bv_lits = p.bv_literals();
m_pp_bv_neg = p.bv_neg();
m_pp_max_depth = p.max_depth();
m_pp_min_alias_size = p.min_alias_size();
m_pp_flat_assoc = p.flat_assoc();
}
~smt2_printer() {
@ -1003,24 +1021,24 @@ public:
};
void mk_smt2_format(expr * n, smt2_pp_environment & env, pp_params const & p,
void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p,
unsigned num_vars, char const * var_prefix,
format_ref & r, sbuffer<symbol> & var_names) {
smt2_printer pr(env, p);
pr(n, num_vars, var_prefix, r, var_names);
}
void mk_smt2_format(sort * s, smt2_pp_environment & env, pp_params const & p, format_ref & r) {
void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
smt2_printer pr(env, p);
pr(s, r);
}
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, pp_params const & p, format_ref & r) {
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
smt2_printer pr(env, p);
pr(f, r);
}
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, pp_params const & p, unsigned indent,
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p, unsigned indent,
unsigned num_vars, char const * var_prefix) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
@ -1032,7 +1050,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, pp_params const & p, unsigned indent) {
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
sbuffer<symbol> var_names;
@ -1043,7 +1061,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, pp_params const & p, unsigned indent) {
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
sbuffer<symbol> var_names;
@ -1054,7 +1072,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
return out;
}
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
m_ast(t),
m_manager(m),
m_params(p),
@ -1066,7 +1084,7 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num_vars, char const * var_prefix):
m_ast(t),
m_manager(m),
m_params(get_pp_default_params()),
m_params(m_empty),
m_indent(indent),
m_num_vars(num_vars),
m_var_prefix(var_prefix) {

29
src/ast/ast_smt2_pp.h
View file

@ -23,7 +23,7 @@ Revision History:
#define _AST_SMT2_PP_H_
#include"format.h"
#include"pp_params.h"
#include"params.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
@ -82,28 +82,29 @@ public:
virtual bool uses(symbol const & s) const { return false; }
};
void mk_smt2_format(expr * n, smt2_pp_environment & env, pp_params const & p,
void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p,
unsigned num_vars, char const * var_prefix,
format_ns::format_ref & r, sbuffer<symbol> & var_names);
void mk_smt2_format(sort * s, smt2_pp_environment & env, pp_params const & p, format_ns::format_ref & r);
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, pp_params const & p, format_ns::format_ref & r);
void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0,
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0,
unsigned num_vars = 0, char const * var_prefix = 0);
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
/**
\brief Internal wrapper (for debugging purposes only)
*/
struct mk_ismt2_pp {
ast * m_ast;
ast_manager & m_manager;
pp_params const & m_params;
unsigned m_indent;
unsigned m_num_vars;
char const * m_var_prefix;
mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
ast * m_ast;
ast_manager & m_manager;
params_ref m_empty;
params_ref const & m_params;
unsigned m_indent;
unsigned m_num_vars;
char const * m_var_prefix;
mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
};

30
src/ast/float_decl_plugin.cpp
View file

@ -348,13 +348,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
// When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float!
sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1);
symbol name("asFloat");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else {
// .. Otherwise we only know how to convert rationals/reals.
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to asFloat");
if (arity != 2 && arity != 3)
if (arity != 2 && arity != 3)
m_manager->raise_exception("invalid number of arguments to asFloat operator");
if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort)
m_manager->raise_exception("sort mismatch");
@ -373,6 +373,23 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
}
}
func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (!m_bv_plugin)
m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support");
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to asIEEEBV");
if (!is_float_sort(domain[0]))
m_manager->raise_exception("sort mismatch");
// When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector.
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
parameter ps[] = { parameter(float_sz) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
symbol name("asIEEEBV");
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
switch (k) {
@ -420,6 +437,8 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_FUSED_MA:
return mk_fused_ma(k, num_parameters, parameters, arity, domain, range);
case OP_TO_IEEE_BV:
return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
default:
m_manager->raise_exception("unsupported floating point operator");
return 0;
@ -462,7 +481,10 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
if (m_bv_plugin)
op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
}
void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

9
src/ast/float_decl_plugin.h
View file

@ -67,6 +67,7 @@ enum float_op_kind {
OP_FLOAT_IS_SIGN_MINUS,
OP_TO_FLOAT,
OP_TO_IEEE_BV,
LAST_FLOAT_OP
};
@ -118,6 +119,8 @@ class float_decl_plugin : public decl_plugin {
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual void set_manager(ast_manager * m, family_id id);
unsigned mk_id(mpf const & v);
@ -159,7 +162,7 @@ class float_util {
ast_manager & m_manager;
float_decl_plugin * m_plugin;
family_id m_fid;
arith_util m_a_util;
arith_util m_a_util;
public:
float_util(ast_manager & m);
~float_util();
@ -209,7 +212,7 @@ public:
bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_TO_FLOAT); }
app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); }
app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); }
app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); }
app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); }
app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); }
@ -238,6 +241,8 @@ public:
app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }
bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); }
app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); }
};
#endif

524
src/ast/normal_forms/cnf.cpp
View file

@ -1,524 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
cnf.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-23.
Revision History:
--*/
#include"cnf.h"
#include"var_subst.h"
#include"ast_util.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
unsigned cnf_entry::hash() const {
unsigned a = m_node->get_id();
unsigned b = m_polarity;
unsigned c = m_in_q;
mix(a,b,c);
return c;
}
bool cnf_entry::operator==(cnf_entry const & k) const {
return m_node == k.m_node && m_polarity == k.m_polarity && m_in_q == k.m_in_q;
}
cnf_cache::cnf_cache(ast_manager & m):
m_manager(m) {
}
void cnf_cache::insert(cnf_entry const & k, expr * r, proof * pr) {
SASSERT(!m_cache.contains(k));
m_manager.inc_ref(r);
m_manager.inc_ref(pr);
m_cache.insert(k, expr_proof_pair(r, pr));
}
void cnf_cache::reset() {
cache::iterator it = m_cache.begin();
cache::iterator end = m_cache.end();
for (; it != end; ++it) {
expr_proof_pair & pair = (*it).m_value;
m_manager.dec_ref(pair.first);
m_manager.dec_ref(pair.second);
}
m_cache.reset();
}
void cnf::cache_result(expr * e, bool in_q, expr * r, proof * pr) {
SASSERT(r);
TRACE("cnf", tout << "caching result for: " << e->get_id() << " " << r->get_id() << "\n";);
m_cache.insert(cnf_entry(e, true, in_q), r, pr);
}
void cnf::visit(expr * n, bool in_q, bool & visited) {
if (!is_cached(n, in_q)) {
m_todo.push_back(std::make_pair(n, in_q));
visited = false;
}
}
bool cnf::visit_children(expr * n, bool in_q) {
bool visited = true;
switch(n->get_kind()) {
case AST_APP:
if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_label(n)) {
unsigned j = to_app(n)->get_num_args();
while (j > 0) {
--j;
visit(to_app(n)->get_arg(j), in_q, visited);
}
}
break;
case AST_QUANTIFIER:
visit(to_quantifier(n)->get_expr(), true, visited);
break;
default:
break;
}
return visited;
}
void cnf::reduce1(expr * n, bool in_q) {
switch(n->get_kind()) {
case AST_APP:
if (m_manager.is_or(n))
reduce1_or(to_app(n), in_q);
else if (m_manager.is_and(n))
reduce1_and(to_app(n), in_q);
else if (m_manager.is_label(n))
reduce1_label(to_app(n), in_q);
else
cache_result(n, in_q, n, 0);
break;
case AST_QUANTIFIER:
reduce1_quantifier(to_quantifier(n), in_q);
break;
default:
cache_result(n, in_q, n, 0);
break;
}
}
void cnf::get_args(app * n, bool in_q, ptr_buffer<expr> & new_args, ptr_buffer<proof> & new_arg_prs) {
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * new_arg = 0;
proof * new_arg_pr = 0;
get_cached(n->get_arg(i), in_q, new_arg, new_arg_pr);
SASSERT(new_arg);
new_args.push_back(new_arg);
if (new_arg_pr)
new_arg_prs.push_back(new_arg_pr);
}
}
void cnf::flat_args(func_decl * d, ptr_buffer<expr> const & args, ptr_buffer<expr> & flat_args) {
ptr_buffer<expr>::const_iterator it = args.begin();
ptr_buffer<expr>::const_iterator end = args.end();
for (; it != end; ++it) {
expr * arg = *it;
if (is_app_of(arg, d))
flat_args.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
else
flat_args.push_back(arg);
}
}
/**
\brief Return the approximated size of distributing OR over AND on
(OR args[0] .... args[sz-1])
*/
approx_nat cnf::approx_result_size_for_disj(ptr_buffer<expr> const & args) {
approx_nat r(1);
ptr_buffer<expr>::const_iterator it = args.begin();
ptr_buffer<expr>::const_iterator end = args.end();
for (; it != end; ++it) {
expr * arg = *it;
if (m_manager.is_and(arg))
r *= to_app(arg)->get_num_args();
}
return r;
}
/**
\brief Return true if it is too expensive to process the disjunction of args
*/
inline bool cnf::is_too_expensive(approx_nat approx_result_size, ptr_buffer<expr> const & args) {
// (OR A (AND B C)) is always considered cheap.
if (args.size() == 2 && (!m_manager.is_and(args[0]) || !m_manager.is_and(args[1])))
return false;
return !(approx_result_size < m_params.m_cnf_factor);
}
/**
\brief Create a (positive) name for the expressions of the form (AND ...) in args.
Store the result in new_args.
*/
void cnf::name_args(ptr_buffer<expr> const & args, expr_ref_buffer & new_args, proof_ref_buffer & new_arg_prs) {
ptr_buffer<expr>::const_iterator it = args.begin();
ptr_buffer<expr>::const_iterator end = args.end();
for (; it != end; ++it) {
expr * arg = *it;
if (m_manager.is_and(arg)) {
expr_ref new_def(m_manager);
proof_ref new_def_pr(m_manager);
app_ref new_arg(m_manager);
proof_ref new_arg_pr(m_manager);
if (m_defined_names.mk_pos_name(to_app(arg), new_def, new_def_pr, new_arg, new_arg_pr)) {
m_todo_defs.push_back(new_def);
if (m_manager.proofs_enabled())
m_todo_proofs.push_back(new_def_pr);
}
new_args.push_back(new_arg);
if (m_manager.fine_grain_proofs())
new_arg_prs.push_back(new_arg_pr);
else
m_coarse_proofs.push_back(new_arg_pr);
}
else
new_args.push_back(arg);
}
}
void cnf::distribute(app * n, app * & r, proof * & pr) {
SASSERT(m_manager.is_or(n));
buffer<unsigned> sz;
buffer<unsigned> it;
ptr_buffer<expr> new_args;
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = n->get_arg(i);
it.push_back(0);
if (m_manager.is_and(arg))
sz.push_back(to_app(arg)->get_num_args());
else
sz.push_back(1);
}
do {
ptr_buffer<expr> lits;
for (unsigned i = 0; i < num; i++) {
expr * arg = n->get_arg(i);
if (m_manager.is_and(arg)) {
SASSERT(it[i] < to_app(arg)->get_num_args());
lits.push_back(to_app(arg)->get_arg(it[i]));
}
else {
SASSERT(it[i] == 0);
lits.push_back(arg);
}
}
app * n = m_manager.mk_or(lits.size(), lits.c_ptr());
new_args.push_back(n);
}
while (product_iterator_next(sz.size(), sz.c_ptr(), it.c_ptr()));
SASSERT(!new_args.empty());
if (new_args.size() == 1)
r = to_app(new_args[0]);
else
r = m_manager.mk_and(new_args.size(), new_args.c_ptr());
pr = 0;
if (m_manager.fine_grain_proofs() && r != n)
pr = m_manager.mk_iff_oeq(m_manager.mk_distributivity(n, r));
}
void cnf::push_quant(quantifier * q, expr * & r, proof * & pr) {
SASSERT(is_forall(q));
expr * e = q->get_expr();
pr = 0;
if (m_manager.is_and(e)) {
expr_ref_buffer new_args(m_manager);
unsigned num = to_app(e)->get_num_args();
for (unsigned i = 0; i < num; i++) {
quantifier_ref aux(m_manager);
aux = m_manager.update_quantifier(q, 0, 0, 0, 0, to_app(e)->get_arg(i));
expr_ref new_arg(m_manager);
elim_unused_vars(m_manager, aux, new_arg);
new_args.push_back(new_arg);
}
r = m_manager.mk_and(new_args.size(), new_args.c_ptr());
if (m_manager.fine_grain_proofs())
pr = m_manager.mk_iff_oeq(m_manager.mk_push_quant(q, r));
}
else {
r = q;
}
}
void cnf::reduce1_or(app * n, bool in_q) {
ptr_buffer<expr> new_args;
ptr_buffer<proof> new_arg_prs;
get_args(n, in_q, new_args, new_arg_prs);
expr * r;
proof * pr = 0;
if (in_q || m_params.m_cnf_mode == CNF_OPPORTUNISTIC || m_params.m_cnf_mode == CNF_FULL) {
ptr_buffer<expr> f_args;
flat_args(n->get_decl(), new_args, f_args);
TRACE("cnf_or", for (unsigned i = 0; i < f_args.size(); i++) tout << mk_pp(f_args[i], m_manager) << "\n";);
approx_nat result_size = approx_result_size_for_disj(f_args);
TRACE("cnf_or", tout << mk_pp(n, m_manager) << "\napprox. result: " << result_size << "\n";);
if (m_params.m_cnf_mode != CNF_OPPORTUNISTIC || result_size < m_params.m_cnf_factor) {
expr_ref_buffer cheap_args(m_manager);
proof_ref_buffer cheap_args_pr(m_manager);
if (is_too_expensive(result_size, f_args)) {
name_args(f_args, cheap_args, cheap_args_pr);
}
else {
cheap_args.append(f_args.size(), f_args.c_ptr());
}
app_ref r1(m_manager);
r1 = m_manager.mk_or(cheap_args.size(), cheap_args.c_ptr());
// Proof gen support ---------------------------
// r1 is (OR cheap_args) it is only built if proofs are enabled.
// p1 is a proof for (= n r1)
proof * p1 = 0;
if (m_manager.fine_grain_proofs()) {
proof * prs[3];
app * r[2];
r[0] = m_manager.mk_or(new_args.size(), new_args.c_ptr());
prs[0] = n == r[0] ? 0 : m_manager.mk_oeq_congruence(n, r[0], new_arg_prs.size(), new_arg_prs.c_ptr());
r[1] = m_manager.mk_or(f_args.size(), f_args.c_ptr());
prs[1] = r[0] == r[1] ? 0 : m_manager.mk_iff_oeq(m_manager.mk_rewrite(r[0], r[1]));
prs[2] = r[1] == r1 ? 0 : m_manager.mk_oeq_congruence(r[1], r1, cheap_args_pr.size(), cheap_args_pr.c_ptr());
p1 = m_manager.mk_transitivity(3, prs);
}
// --------------------------------------------
expr_ref r2(m_manager);
proof_ref p2(m_manager);
m_pull.pull_quant2(r1, r2, p2);
if (is_quantifier(r2)) {
expr * e = to_quantifier(r2)->get_expr();
SASSERT(m_manager.is_or(e));
app * d_r;
proof * d_pr;
distribute(to_app(e), d_r, d_pr);
quantifier_ref r3(m_manager);
r3 = m_manager.update_quantifier(to_quantifier(r2), d_r);
proof * push_pr;
push_quant(r3, r, push_pr);
if (m_manager.fine_grain_proofs()) {
// p1 is a proof of n == r1
// p2 is a proof of r1 == r2
p2 = p2 == 0 ? 0 : m_manager.mk_iff_oeq(p2);
proof * p3 = r2 == r3 ? 0 : m_manager.mk_oeq_quant_intro(to_quantifier(r2), r3, d_pr);
CTRACE("cnf_or", p1, tout << "p1:\n" << mk_pp(m_manager.get_fact(p1), m_manager) << "\n";);
CTRACE("cnf_or", p2, tout << "p2:\n" << mk_pp(m_manager.get_fact(p2), m_manager) << "\n";);
CTRACE("cnf_or", p3, tout << "p3:\n" << mk_pp(m_manager.get_fact(p3), m_manager) << "\n";);
TRACE("cnf_or", tout << "r2 == r3: " << (r2 == r3) << "\n"
<< mk_pp(r2, m_manager) << "\n" << mk_pp(r3, m_manager) << "\n";);
pr = m_manager.mk_transitivity(p1, p2, p3, push_pr);
}
cache_result(n, in_q, r, pr);
}
else {
SASSERT(p2 == 0);
SASSERT(r1 == r2);
SASSERT(m_manager.is_or(r2));
app * r3;
distribute(to_app(r2), r3, pr);
r = r3;
pr = m_manager.mk_transitivity(p1, pr);
cache_result(n, in_q, r, pr);
}
return;
}
}
r = m_manager.mk_or(new_args.size(), new_args.c_ptr());
if (m_manager.fine_grain_proofs() && n != r)
pr = m_manager.mk_oeq_congruence(n, to_app(r), new_arg_prs.size(), new_arg_prs.c_ptr());
cache_result(n, in_q, r, pr);
}
void cnf::reduce1_and(app * n, bool in_q) {
ptr_buffer<expr> new_args;
ptr_buffer<proof> new_arg_prs;
get_args(n, in_q, new_args, new_arg_prs);
app * r;
proof * pr = 0;
if (in_q || m_params.m_cnf_mode == CNF_OPPORTUNISTIC || m_params.m_cnf_mode == CNF_FULL) {
ptr_buffer<expr> f_args;
flat_args(n->get_decl(), new_args, f_args);
r = m_manager.mk_and(f_args.size(), f_args.c_ptr());
if (m_manager.fine_grain_proofs() && n != r) {
app * r0 = m_manager.mk_and(new_args.size(), new_args.c_ptr());
proof * p0 = r0 == n ? 0 : m_manager.mk_oeq_congruence(n, r0, new_arg_prs.size(), new_arg_prs.c_ptr());
proof * p1 = r0 == r ? 0 : m_manager.mk_iff_oeq(m_manager.mk_rewrite(r0, r));
pr = m_manager.mk_transitivity(p0, p1);
}
}
else {
r = m_manager.mk_and(new_args.size(), new_args.c_ptr());
if (m_manager.fine_grain_proofs() && n != r)
pr = m_manager.mk_oeq_congruence(n, r, new_arg_prs.size(), new_arg_prs.c_ptr());
}
cache_result(n, in_q, r, pr);
}
void cnf::reduce1_label(app * n, bool in_q) {
expr * r;
proof * pr = 0;
expr * new_arg;
proof * new_arg_pr;
get_cached(n->get_arg(0), true, new_arg, new_arg_pr);
if (in_q || m_params.m_cnf_mode == CNF_FULL) {
// TODO: in the current implementation, labels are removed during CNF translation.
// This is satisfactory for Boogie, since it does not use labels inside quantifiers,
// and we only need CNF_QUANT for Superposition Calculus.
r = new_arg;
if (m_manager.fine_grain_proofs()) {
proof * p0 = m_manager.mk_iff_oeq(m_manager.mk_rewrite(n, n->get_arg(0)));
pr = m_manager.mk_transitivity(p0, new_arg_pr);
}
}
else {
r = m_manager.mk_app(n->get_decl(), new_arg);
if (m_manager.fine_grain_proofs() && n != r)
pr = m_manager.mk_oeq_congruence(n, to_app(r), 1, &new_arg_pr);
}
cache_result(n, in_q, r, pr);
}
void cnf::reduce1_quantifier(quantifier * q, bool in_q) {
expr * new_expr;
proof * new_expr_pr;
get_cached(q->get_expr(), true, new_expr, new_expr_pr);
expr_ref r(m_manager);
proof_ref pr(m_manager);
if (m_manager.is_and(new_expr) && q->is_forall()) {
quantifier_ref q1(m_manager);
q1 = m_manager.update_quantifier(q, new_expr);
expr_ref q2(m_manager);
proof_ref p2(m_manager);
m_pull.pull_quant2(q1, q2, p2);
expr * q3;
proof * p3;
push_quant(to_quantifier(q2), q3, p3);
r = q3;
if (m_manager.fine_grain_proofs()) {
proof * p1 = q == q1 ? 0 : m_manager.mk_oeq_quant_intro(q, q1, new_expr_pr);
p2 = p2 == 0 ? 0 : m_manager.mk_iff_oeq(p2);
pr = m_manager.mk_transitivity(p1, p2, p3);
}
}
else if ((m_manager.is_or(new_expr) || is_forall(new_expr)) && q->is_forall()) {
quantifier_ref q1(m_manager);
q1 = m_manager.update_quantifier(q, new_expr);
m_pull.pull_quant2(q1, r, pr);
if (m_manager.fine_grain_proofs()) {
pr = pr == 0 ? 0 : m_manager.mk_iff_oeq(pr);
proof * p1 = q == q1 ? 0 : m_manager.mk_oeq_quant_intro(q, q1, new_expr_pr);
pr = m_manager.mk_transitivity(p1, pr);
}
}
else {
r = m_manager.update_quantifier(q, new_expr);
if (m_manager.fine_grain_proofs() && r != q)
pr = q == r ? 0 : m_manager.mk_oeq_quant_intro(q, to_quantifier(r), new_expr_pr);
}
cache_result(q, in_q, r, pr);
TRACE("cnf_quant", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";);
}
cnf::cnf(ast_manager & m, defined_names & n, cnf_params & params):
m_params(params),
m_manager(m),
m_defined_names(n),
m_pull(m),
m_cache(m),
m_todo_defs(m),
m_todo_proofs(m),
m_coarse_proofs(m) {
}
cnf::~cnf() {
}
void cnf::reduce(expr * n, expr_ref & r, proof_ref & pr) {
m_coarse_proofs.reset();
m_todo.reset();
m_todo.push_back(expr_bool_pair(n, false));
while (!m_todo.empty()) {
expr_bool_pair pair = m_todo.back();
expr * n = pair.first;
bool in_q = pair.second;
if (is_cached(n, in_q)) {
m_todo.pop_back();
}
else if (visit_children(n, in_q)) {
m_todo.pop_back();
reduce1(n, in_q);
}
}
expr * r2;
proof * pr2;
get_cached(n, false, r2, pr2);
r = r2;
switch (m_manager.proof_mode()) {
case PGM_DISABLED:
pr = m_manager.mk_undef_proof();
break;
case PGM_COARSE:
remove_duplicates(m_coarse_proofs);
pr = n == r2 ? m_manager.mk_reflexivity(n) : m_manager.mk_cnf_star(n, r2, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
break;
case PGM_FINE:
pr = pr2 == 0 ? m_manager.mk_reflexivity(n) : pr2;
break;
}
}
void cnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & pr) {
if (m_params.m_cnf_mode == CNF_DISABLED) {
r = n;
pr = m_manager.mk_reflexivity(n);
return;
}
reset();
reduce(n, r, pr);
for (unsigned i = 0; i < m_todo_defs.size(); i++) {
expr_ref dr(m_manager);
proof_ref dpr(m_manager);
reduce(m_todo_defs.get(i), dr, dpr);
m_result_defs.push_back(dr);
if (m_manager.proofs_enabled()) {
proof * new_pr = m_manager.mk_modus_ponens(m_todo_proofs.get(i), dpr);
m_result_def_proofs.push_back(new_pr);
}
else
m_result_def_proofs.push_back(m_manager.mk_undef_proof());
}
std::reverse(m_result_defs.begin(), m_result_defs.end());
new_defs.append(m_result_defs.size(), m_result_defs.c_ptr());
std::reverse(m_result_def_proofs.begin(), m_result_def_proofs.end());
new_def_proofs.append(m_result_def_proofs.size(), m_result_def_proofs.c_ptr());
}
void cnf::reset() {
m_cache.reset();
m_todo.reset();
m_todo_defs.reset();
m_todo_proofs.reset();
m_result_defs.reset();
m_result_def_proofs.reset();
}

121
src/ast/normal_forms/cnf.h
View file

@ -1,121 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
cnf.h
Abstract:
CNF translation
Author:
Leonardo de Moura (leonardo) 2008-01-17.
Revision History:
--*/
#ifndef _CNF_H_
#define _CNF_H_
#include"cnf_params.h"
#include"pull_quant.h"
#include"nnf.h"
#include"approx_nat.h"
/**
\brief Entry into the todo list of the CNF translator. It is also used as the key in the CNF cache.
*/
struct cnf_entry {
expr * m_node;
bool m_polarity:1;
bool m_in_q:1;
cnf_entry():m_node(0), m_polarity(false), m_in_q(false) {}
cnf_entry(expr * n, bool p, bool in_q):m_node(n), m_polarity(p), m_in_q(in_q) {}
unsigned hash() const;
bool operator==(cnf_entry const & k) const;
};
/**
\brief Cache for CNF transformation. It is a mapping from (expr, polarity, in_q) -> (expr, proof)
*/
class cnf_cache {
public:
typedef std::pair<expr *, proof *> expr_proof_pair;
typedef map<cnf_entry, expr_proof_pair, obj_hash<cnf_entry>, default_eq<cnf_entry> > cache;
ast_manager & m_manager;
cache m_cache;
public:
cnf_cache(ast_manager & m);
~cnf_cache() { reset(); }
void insert(cnf_entry const & k, expr * r, proof * pr);
bool contains(cnf_entry const & k) const { return m_cache.contains(k); }
void get(cnf_entry const & k, expr * & r, proof * & pr) const { expr_proof_pair tmp; m_cache.find(k, tmp); r = tmp.first; pr = tmp.second; }
void reset();
};
/**
\brief Functor for converting expressions into CNF. The functor can
optionally process subformulas nested in quantifiers. New names may be
introduced for subformulas that are too expensive to be put into CNF.
NNF translation must be applied before converting to CNF.
- To use CNF_QUANT, we must use at least NNF_QUANT
- To use CNF_OPPORTUNISTIC, we must use at least NNF_QUANT
- To use CNF_FULL, we must use NNF_FULL
*/
class cnf {
typedef std::pair<expr *, bool> expr_bool_pair;
cnf_params & m_params;
ast_manager & m_manager;
defined_names & m_defined_names;
pull_quant m_pull;
cnf_cache m_cache;
svector<expr_bool_pair> m_todo;
expr_ref_vector m_todo_defs;
proof_ref_vector m_todo_proofs;
ptr_vector<expr> m_result_defs;
ptr_vector<proof> m_result_def_proofs;
proof_ref_vector m_coarse_proofs;
void cache_result(expr * e, bool in_q, expr * r, proof * pr);
void get_cached(expr * n, bool in_q, expr * & r, proof * & pr) const { m_cache.get(cnf_entry(n, true, in_q), r, pr); }
bool is_cached(expr * n, bool in_q) const { return m_cache.contains(cnf_entry(n, true, in_q)); }
void visit(expr * n, bool in_q, bool & visited);
bool visit_children(expr * n, bool in_q);
void get_args(app * n, bool in_q, ptr_buffer<expr> & new_args, ptr_buffer<proof> & new_arg_prs);
void flat_args(func_decl * d, ptr_buffer<expr> const & args, ptr_buffer<expr> & flat_args);
approx_nat approx_result_size_for_disj(ptr_buffer<expr> const & args);
bool is_too_expensive(approx_nat approx_result_size, ptr_buffer<expr> const & args);
void name_args(ptr_buffer<expr> const & args, expr_ref_buffer & new_args, proof_ref_buffer & new_arg_prs);
void distribute(app * arg, app * & r, proof * & pr);
void push_quant(quantifier * q, expr * & r, proof * & pr);
void reduce1(expr * n, bool in_q);
void reduce1_or(app * n, bool in_q);
void reduce1_and(app * n, bool in_q);
void reduce1_label(app * n, bool in_q);
void reduce1_quantifier(quantifier * q, bool in_q);
void reduce(expr * n, expr_ref & r, proof_ref & pr);
public:
cnf(ast_manager & m, defined_names & n, cnf_params & params);
~cnf();
void operator()(expr * n, // [IN] expression that should be put into CNF
expr_ref_vector & new_defs, // [OUT] new definitions
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
expr_ref & r, // [OUT] resultant expression
proof_ref & p // [OUT] proof for (~ n r)
);
void reset();
};
#endif /* _CNF_H_ */

101
src/ast/normal_forms/nnf.cpp
View file

@ -18,6 +18,7 @@ Notes:
--*/
#include"nnf.h"
#include"nnf_params.hpp"
#include"warning.h"
#include"used_vars.h"
#include"well_sorted.h"
@ -29,6 +30,40 @@ Notes:
#include"ast_smt2_pp.h"
/**
\brief NNF translation mode. The cheapest mode is NNF_SKOLEM, and
the most expensive is NNF_FULL.
*/
enum nnf_mode {
NNF_SKOLEM, /* A subformula is put into NNF only if it contains
quantifiers or labels. The result of the
transformation will be in skolem normal form.
If a formula is too expensive to be put into NNF,
then nested quantifiers and labels are renamed.
This mode is sufficient when using E-matching.
*/
NNF_QUANT, /* A subformula is put into NNF if it contains
quantifiers, labels, or is in the scope of a
quantifier. The result of the transformation will be
in skolem normal form, and the body of quantifiers
will be in NNF. If a ground formula is too expensive to
be put into NNF, then nested quantifiers and labels
are renamed.
This mode is sufficient when using Superposition
Calculus.
Remark: If the problem does not contain quantifiers,
then NNF_QUANT is identical to NNF_SKOLEM.
*/
NNF_OPPORTUNISTIC, /* Similar to NNF_QUANT, but a subformula is
also put into NNF, if it is
cheap. Otherwise, the nested quantifiers and
labels are renamed. */
NNF_FULL /* Everything is put into NNF. */
};
class skolemizer {
typedef act_cache cache;
@ -113,20 +148,16 @@ class skolemizer {
}
public:
skolemizer(ast_manager & m, params_ref const & p):
skolemizer(ast_manager & m):
m_manager(m),
m_sk_hack("sk_hack"),
m_sk_hack_enabled(false),
m_cache(m),
m_cache_pr(m) {
updt_params(p);
}
void updt_params(params_ref const & p) {
m_sk_hack_enabled = p.get_bool(":nnf-sk-hack", false);
}
static void get_param_descrs(param_descrs & r) {
r.insert(":nnf-sk-hack", CPK_BOOL, "(default: false) hack for VCC");
void set_sk_hack(bool f) {
m_sk_hack_enabled = f;
}
ast_manager & m() const { return m_manager; }
@ -220,8 +251,6 @@ struct nnf::imp {
name_exprs * m_name_nested_formulas;
name_exprs * m_name_quant;
symbol m_skolem;
volatile bool m_cancel;
unsigned long long m_max_memory; // in bytes
@ -231,10 +260,9 @@ struct nnf::imp {
m_todo_defs(m),
m_todo_proofs(m),
m_result_pr_stack(m),
m_skolemizer(m, p),
m_skolem("skolem"),
m_skolemizer(m),
m_cancel(false) {
updt_local_params(p);
updt_params(p);
for (unsigned i = 0; i < 4; i++) {
m_cache[i] = alloc(act_cache, m);
if (m.proofs_enabled())
@ -258,14 +286,10 @@ struct nnf::imp {
del_name_exprs(m_name_quant);
}
void updt_params(params_ref const & p) {
updt_local_params(p);
m_skolemizer.updt_params(p);
}
void updt_local_params(params_ref const & p) {
symbol mode_sym = p.get_sym(":nnf-mode", m_skolem);
if (mode_sym == m_skolem)
void updt_params(params_ref const & _p) {
nnf_params p(_p);
symbol mode_sym = p.mode();
if (mode_sym == "skolem")
m_mode = NNF_SKOLEM;
else if (mode_sym == "full")
m_mode = NNF_FULL;
@ -273,23 +297,17 @@ struct nnf::imp {
m_mode = NNF_QUANT;
else
throw nnf_params_exception("invalid NNF mode");
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";);
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << p << "\n";);
m_ignore_labels = p.get_bool(":nnf-ignore-labels", false);
m_skolemize = p.get_bool(":skolemize", true);
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_ignore_labels = p.ignore_labels();
m_skolemize = p.skolemize();
m_max_memory = megabytes_to_bytes(p.max_memory());
m_skolemizer.set_sk_hack(p.sk_hack());
}
static void get_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert(":nnf-mode", CPK_SYMBOL,
"(default: skolem) NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full");
r.insert(":nnf-ignore-labels", CPK_BOOL,
"(default: false) remove/ignore labels in the input formula, this option is ignored if proofs are enabled");
r.insert(":skolemize", CPK_BOOL,
"(default: true) skolemize (existential force) quantifiers");
skolemizer::get_param_descrs(r);
nnf_params::collect_param_descrs(r);
}
void reset() {
@ -881,21 +899,6 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) {
m_imp = alloc(imp, m, n, p);
}
nnf::nnf(ast_manager & m, defined_names & n, nnf_params & np) {
params_ref p;
if (np.m_nnf_mode == NNF_FULL)
p.set_sym(":nnf-mode", symbol("full"));
else if (np.m_nnf_mode == NNF_QUANT)
p.set_sym(":nnf-mode", symbol("quantifiers"));
if (np.m_nnf_ignore_labels)
p.set_bool(":nnf-ignore-labels", true);
if (np.m_nnf_sk_hack)
p.set_bool(":nnf-sk-hack", true);
m_imp = alloc(imp, m, n, p);
}
nnf::~nnf() {
dealloc(m_imp);
}

5
src/ast/normal_forms/nnf.h
View file

@ -21,7 +21,6 @@ Notes:
#define _NNF_H_
#include"ast.h"
#include"nnf_params.h"
#include"params.h"
#include"defined_names.h"
@ -30,7 +29,6 @@ class nnf {
imp * m_imp;
public:
nnf(ast_manager & m, defined_names & n, params_ref const & p = params_ref());
nnf(ast_manager & m, defined_names & n, nnf_params & params); // for backward compatibility
~nnf();
void operator()(expr * n, // [IN] expression that should be put into NNF
@ -41,6 +39,9 @@ public:
);
void updt_params(params_ref const & p);
/*
REG_MODULE_PARAMS('nnf', 'nnf::get_param_descrs')
*/
static void get_param_descrs(param_descrs & r);
void cancel() { set_cancel(true); }

9
src/ast/normal_forms/nnf_params.pyg Normal file
View file

@ -0,0 +1,9 @@
def_module_params('nnf',
description='negation normal form',
export=True,
params=(max_memory_param(),
('sk_hack', BOOL, False, 'hack for VCC'),
('mode', SYMBOL, 'skolem',
'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full'),
('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled'),
('skolemize', BOOL, True, 'skolemize (existential force) quantifiers')))

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

@ -36,7 +36,6 @@ Notes:
#include"ast_pp.h"
#include"cmd_context.h"
#include"smt2parser.h"
#include"front_end_params.h"
expr_pattern_match::expr_pattern_match(ast_manager & manager):
m_manager(manager), m_precompiled(manager) {
@ -388,8 +387,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();

1
src/ast/pattern/expr_pattern_match.h
View file

@ -22,7 +22,6 @@ Notes:
#include"ast.h"
#include"map.h"
#include"front_end_params.h"
class expr_pattern_match {

32
src/ast/pattern/pattern_inference_params.cpp Normal file
View file

@ -0,0 +1,32 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
pattern_inference_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include"pattern_inference_params.h"
#include"pattern_inference_params_helper.hpp"
void pattern_inference_params::updt_params(params_ref const & _p) {
pattern_inference_params_helper p(_p);
m_pi_max_multi_patterns = p.max_multi_patterns();
m_pi_block_loop_patterns = p.block_loop_patterns();
m_pi_arith = static_cast<arith_pattern_inference_kind>(p.arith());
m_pi_use_database = p.use_database();
m_pi_arith_weight = p.arith_weight();
m_pi_non_nested_arith_weight = p.non_nested_arith_weight();
m_pi_pull_quantifiers = p.pull_quantifiers();
m_pi_warnings = p.warnings();
}

17
src/front_end_params/pattern_inference_params.h → src/ast/pattern/pattern_inference_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef _PATTERN_INFERENCE_PARAMS_H_
#define _PATTERN_INFERENCE_PARAMS_H_
#include"ini_file.h"
#include"params.h"
enum arith_pattern_inference_kind {
AP_NO, // do not infer patterns with arithmetic terms
@ -39,20 +39,13 @@ struct pattern_inference_params {
bool m_pi_avoid_skolems;
bool m_pi_warnings;
pattern_inference_params():
m_pi_max_multi_patterns(0),
m_pi_block_loop_patterns(true),
m_pi_arith(AP_CONSERVATIVE),
m_pi_use_database(false),
m_pi_arith_weight(5),
m_pi_non_nested_arith_weight(10),
m_pi_pull_quantifiers(true),
pattern_inference_params(params_ref const & p = params_ref()):
m_pi_nopat_weight(-1),
m_pi_avoid_skolems(true),
m_pi_warnings(false) {
m_pi_avoid_skolems(true) {
updt_params(p);
}
void register_params(ini_params & p);
void updt_params(params_ref const & _p);
};
#endif /* _PATTERN_INFERENCE_PARAMS_H_ */

12
src/ast/pattern/pattern_inference_params_helper.pyg Normal file
View file

@ -0,0 +1,12 @@
def_module_params(class_name='pattern_inference_params_helper',
module_name='pi',
description='pattern inference (heuristics) for universal formulas (without annotation)',
export=True,
params=(('max_multi_patterns', UINT, 0, 'when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern'),
('block_loop_patterns', BOOL, True, 'block looping patterns during pattern inference'),
('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
('use_database', BOOL, True, 'use pattern database'),
('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
('warnings', BOOL, False, 'enable/disable warning messages in the pattern inference module')))

43
src/ast/pp.cpp
View file

@ -17,22 +17,9 @@ Revision History:
--*/
#include"pp.h"
#include"pp_params.hpp"
using namespace format_ns;
pp_params g_pp_params;
void set_pp_default_params(pp_params const & p) {
g_pp_params = p;
}
void register_pp_params(ini_params & p) {
g_pp_params.register_params(p);
}
pp_params const & get_pp_default_params() {
return g_pp_params;
}
static std::pair<unsigned, bool> space_upto_line_break(ast_manager & m, format * f) {
unsigned r;
SASSERT(f->get_family_id() == fm(m).get_family_id("format"));
@ -69,7 +56,15 @@ inline bool fits(ast_manager & m, format * f, unsigned space_left) {
return s <= space_left;
}
void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p) {
pp_params p(_p);
unsigned max_width = p.max_width();
unsigned max_ribbon = p.max_ribbon();
unsigned max_num_lines = p.max_num_lines();
unsigned max_indent = p.max_indent();
bool bounded = p.bounded();
bool single_line = p.single_line();
unsigned pos = 0;
unsigned ribbon_pos = 0;
unsigned line = 0;
@ -80,7 +75,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
todo.push_back(std::make_pair(f, 0));
app_ref space(mk_string(m, " "), fm(m));
while (!todo.empty()) {
if (line >= p.m_pp_max_num_lines)
if (line >= max_num_lines)
return;
std::pair<format *, unsigned> pair = todo.back();
format * f = pair.first;
@ -89,10 +84,10 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
SASSERT(f->get_family_id() == fm(m).get_family_id("format"));
switch (f->get_decl_kind()) {
case OP_STRING:
if (p.m_pp_bounded && pos > p.m_pp_max_width)
if (bounded && pos > max_width)
break;
len = static_cast<unsigned>(strlen(f->get_decl()->get_parameter(0).get_symbol().bare_str()));
if (p.m_pp_bounded && pos + len > p.m_pp_max_width) {
if (bounded && pos + len > max_width) {
out << "...";
break;
}
@ -103,7 +98,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
case OP_INDENT:
todo.push_back(std::make_pair(to_app(f->get_arg(0)),
std::min(indent + f->get_decl()->get_parameter(0).get_int(),
p.m_pp_max_indent)));
max_indent)));
break;
case OP_COMPOSE:
i = f->get_num_args();
@ -113,7 +108,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
}
break;
case OP_CHOICE:
space_left = std::min(p.m_pp_max_width - pos, p.m_pp_max_ribbon - pos);
space_left = std::min(max_width - pos, max_ribbon - pos);
if (space_left > 0 && fits(m, to_app(f->get_arg(0)), space_left))
todo.push_back(std::make_pair(to_app(f->get_arg(0)), indent));
else
@ -121,14 +116,14 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
break;
case OP_LINE_BREAK:
case OP_LINE_BREAK_EXT:
if (p.m_pp_single_line) {
if (single_line) {
todo.push_back(std::make_pair(space, indent));
break;
}
pos = indent;
ribbon_pos = 0;
line++;
if (line < p.m_pp_max_num_lines) {
if (line < max_num_lines) {
out << "\n";
for (unsigned i = 0; i < indent; i++)
out << " ";
@ -142,7 +137,3 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
}
}
void pp(std::ostream & out, format_ns::format * f, ast_manager & m) {
pp(out, f, m, g_pp_params);
}

10
src/ast/pp.h
View file

@ -20,15 +20,9 @@ Revision History:
#define _PP_H_
#include"format.h"
#include"pp_params.h"
#include"params.h"
void set_pp_default_params(pp_params const & p);
void register_pp_params(ini_params & p);
pp_params const & get_pp_default_params();
void pp(std::ostream & out, format_ns::format * f, ast_manager & m, pp_params const & p);
void pp(std::ostream & out, format_ns::format * f, ast_manager & m);
void pp(std::ostream & out, format_ns::format * f, ast_manager & m, params_ref const & p = params_ref());
#endif /* _PP_H_ */

57
src/ast/pp_params.cpp
View file

@ -1,57 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pp_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-20.
Revision History:
--*/
#include"pp_params.h"
pp_params::pp_params():
m_pp_max_indent(UINT_MAX),
m_pp_max_num_lines(UINT_MAX),
m_pp_max_width(80),
m_pp_max_ribbon(80),
m_pp_max_depth(5),
m_pp_min_alias_size(10),
m_pp_decimal(false),
m_pp_decimal_precision(10),
m_pp_bv_lits(true),
m_pp_bv_neg(false),
m_pp_flat_assoc(true),
m_pp_fixed_indent(false),
m_pp_single_line(false),
m_pp_bounded(false),
m_pp_simplify_implies(false) {
}
void pp_params::register_params(ini_params & p) {
p.register_unsigned_param("PP_MAX_INDENT", m_pp_max_indent, "max. indentation in pretty printer", true);
p.register_unsigned_param("PP_MAX_NUM_LINES", m_pp_max_num_lines, "max. number of lines to be displayed in pretty printer", true);
p.register_unsigned_param("PP_MAX_WIDTH", m_pp_max_width, "max. width in pretty printer", true);
p.register_unsigned_param("PP_MAX_RIBBON", m_pp_max_ribbon, "max. ribbon (width - indentation) in pretty printer", true);
p.register_unsigned_param("PP_MAX_DEPTH", m_pp_max_depth, "max. term depth (when pretty printing SMT2 terms/formulas)", true);
p.register_unsigned_param("PP_MIN_ALIAS_SIZE", m_pp_min_alias_size, "min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)", true);
p.register_bool_param("PP_DECIMAL", m_pp_decimal, "pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a '?' if the value is not precise", true);
p.register_unsigned_param("PP_DECIMAL_PRECISION", m_pp_decimal_precision, "maximum number of decimal places to be used when PP_DECIMAL=true", true);
p.register_bool_param("PP_BV_LITERALS", m_pp_bv_lits, "use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing", true);
p.register_bool_param("PP_BV_NEG", m_pp_bv_neg, "use bvneg when displaying Bit-Vector literals where the most significant bit is 1", true);
p.register_bool_param("PP_FLAT_ASSOC", m_pp_flat_assoc, "flat associative operators (when pretty printing SMT2 terms/formulas)", true);
p.register_bool_param("PP_FIXED_INDENT", m_pp_fixed_indent, "use a fixed indentation for applications", true);
p.register_bool_param("PP_SINGLE_LINE", m_pp_single_line, "ignore line breaks when true", true);
p.register_bool_param("PP_BOUNDED", m_pp_bounded, "ignore characters exceeding max widht", true);
p.register_bool_param("PP_SIMPLIFY_IMPLIES", m_pp_simplify_implies, "simplify nested implications for pretty printing", true);
}

46
src/ast/pp_params.h
View file

@ -1,46 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pp_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-20.
Revision History:
--*/
#ifndef _PP_PARAMS_H_
#define _PP_PARAMS_H_
#include"ini_file.h"
struct pp_params {
unsigned m_pp_max_indent; // max. indentation
unsigned m_pp_max_num_lines; // max. num. lines
unsigned m_pp_max_width; // max. width
unsigned m_pp_max_ribbon; // max. ribbon: width - indentation
unsigned m_pp_max_depth;
unsigned m_pp_min_alias_size;
bool m_pp_decimal; // display reals using decimals
unsigned m_pp_decimal_precision; // max. number of decimal places
bool m_pp_bv_lits;
bool m_pp_bv_neg; // use bvneg to display bit-vector literals which the most significant bit is 1
bool m_pp_flat_assoc;
bool m_pp_fixed_indent;
bool m_pp_single_line; // ignore line breaks if true
bool m_pp_bounded; // ignore characters exceeding max width.
bool m_pp_simplify_implies; // simplify nested implications during pretty printing
pp_params();
void register_params(ini_params & p);
};
#endif /* _PP_PARAMS_H_ */

18
src/ast/pp_params.pyg Normal file
View file

@ -0,0 +1,18 @@
def_module_params('pp',
export=True,
description='pretty printer',
params=(('max_indent', UINT, UINT_MAX, 'max. indentation in pretty printer'),
('max_num_lines', UINT, UINT_MAX, 'max. number of lines to be displayed in pretty printer'),
('max_width', UINT, 80, 'max. width in pretty printer'),
('max_ribbon', UINT, 80, 'max. ribbon (width - indentation) in pretty printer'),
('max_depth', UINT, 5, 'max. term depth (when pretty printing SMT2 terms/formulas)'),
('min_alias_size', UINT, 10, 'min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)'),
('decimal', BOOL, False, 'pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise'),
('decimal_precision', UINT, 10, 'maximum number of decimal places to be used when pp.decimal=true'),
('bv_literals', BOOL, True, 'use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing'),
('bv_neg', BOOL, False, 'use bvneg when displaying Bit-Vector literals where the most significant bit is 1'),
('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'),
('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),
('single_line', BOOL, False, 'ignore line breaks when true'),
('bounded', BOOL, False, 'ignore characters exceeding max widht'),
('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing')))

1
src/ast/proof_checker/proof_checker.cpp
View file

@ -4,7 +4,6 @@
// include "spc_decl_plugin.h"
#include "ast_smt_pp.h"
#include "arith_decl_plugin.h"
#include "front_end_params.h"
#include "th_rewriter.h"
#include "var_subst.h"

48
src/ast/rewriter/arith_rewriter.cpp
View file

@ -22,18 +22,18 @@ Notes:
#include"ast_pp.h"
void arith_rewriter::updt_local_params(params_ref const & p) {
m_arith_lhs = p.get_bool(":arith-lhs", false);
m_gcd_rounding = p.get_bool(":gcd-rounding", false);
m_eq2ineq = p.get_bool(":eq2ineq", false);
m_elim_to_real = p.get_bool(":elim-to-real", false);
m_push_to_real = p.get_bool(":push-to-real", true);
m_anum_simp = p.get_bool(":algebraic-number-evaluator", true);
m_max_degree = p.get_uint(":max-degree", 64);
m_expand_power = p.get_bool(":expand-power", false);
m_mul2power = p.get_bool(":mul-to-power", false);
m_elim_rem = p.get_bool(":elim-rem", false);
m_expand_tan = p.get_bool(":expand-tan", false);
set_sort_sums(p.get_bool(":sort-sums", false)); // set here to avoid collision with bvadd
m_arith_lhs = p.get_bool("arith_lhs", false);
m_gcd_rounding = p.get_bool("gcd_rounding", false);
m_eq2ineq = p.get_bool("eq2ineq", false);
m_elim_to_real = p.get_bool("elim_to_real", false);
m_push_to_real = p.get_bool("push_to_real", true);
m_anum_simp = p.get_bool("algebraic_number_evaluator", true);
m_max_degree = p.get_uint("max_degree", 64);
m_expand_power = p.get_bool("expand_power", false);
m_mul2power = p.get_bool("mul_to_power", false);
m_elim_rem = p.get_bool("elim_rem", false);
m_expand_tan = p.get_bool("expand_tan", false);
set_sort_sums(p.get_bool("sort_sums", false)); // set here to avoid collision with bvadd
}
void arith_rewriter::updt_params(params_ref const & p) {
@ -43,18 +43,18 @@ void arith_rewriter::updt_params(params_ref const & p) {
void arith_rewriter::get_param_descrs(param_descrs & r) {
poly_rewriter<arith_rewriter_core>::get_param_descrs(r);
r.insert(":algebraic-number-evaluator", CPK_BOOL, "(default: true) simplify/evaluate expressions containing (algebraic) irrational numbers.");
r.insert(":mul-to-power", CPK_BOOL, "(default: false) collpase (* t ... t) into (^ t k), it is ignored if :expand-power is true.");
r.insert(":expand-power", CPK_BOOL, "(default: false) expand (^ t k) into (* t ... t) if 1 < k <= :max-degree.");
r.insert(":expand-tan", CPK_BOOL, "(default: false) replace (tan x) with (/ (sin x) (cos x)).");
r.insert(":max-degree", CPK_UINT, "(default: 64) max degree of algebraic numbers (and power operators) processed by simplifier.");
r.insert(":eq2ineq", CPK_BOOL, "(default: false) split arithmetic equalities into two inequalities.");
r.insert(":sort-sums", CPK_BOOL, "(default: false) sort the arguments of + application.");
r.insert(":gcd-rounding", CPK_BOOL, "(default: false) use gcd rounding on integer arithmetic atoms.");
r.insert(":arith-lhs", CPK_BOOL, "(default: false) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant.");
r.insert(":elim-to-real", CPK_BOOL, "(default: false) eliminate to_real from arithmetic predicates that contain only integers.");
r.insert(":push-to-real", CPK_BOOL, "(default: true) distribute to_real over * and +.");
r.insert(":elim-rem", CPK_BOOL, "(default: false) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).");
r.insert("algebraic_number_evaluator", CPK_BOOL, "(default: true) simplify/evaluate expressions containing (algebraic) irrational numbers.");
r.insert("mul_to_power", CPK_BOOL, "(default: false) collpase (* t ... t) into (^ t k), it is ignored if expand_power is true.");
r.insert("expand_power", CPK_BOOL, "(default: false) expand (^ t k) into (* t ... t) if 1 < k <= max_degree.");
r.insert("expand_tan", CPK_BOOL, "(default: false) replace (tan x) with (/ (sin x) (cos x)).");
r.insert("max_degree", CPK_UINT, "(default: 64) max degree of algebraic numbers (and power operators) processed by simplifier.");
r.insert("eq2ineq", CPK_BOOL, "(default: false) split arithmetic equalities into two inequalities.");
r.insert("sort_sums", CPK_BOOL, "(default: false) sort the arguments of + application.");
r.insert("gcd_rounding", CPK_BOOL, "(default: false) use gcd rounding on integer arithmetic atoms.");
r.insert("arith_lhs", CPK_BOOL, "(default: false) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant.");
r.insert("elim_to_real", CPK_BOOL, "(default: false) eliminate to_real from arithmetic predicates that contain only integers.");
r.insert("push_to_real", CPK_BOOL, "(default: true) distribute to_real over * and +.");
r.insert("elim_rem", CPK_BOOL, "(default: false) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).");
}
br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {

8
src/ast/rewriter/array_rewriter.cpp
View file

@ -21,13 +21,13 @@ Notes:
#include"ast_pp.h"
void array_rewriter::updt_params(params_ref const & p) {
m_sort_store = p.get_bool(":sort-store", false);
m_expand_select_store = p.get_bool(":expand-select-store", false);
m_sort_store = p.get_bool("sort_store", false);
m_expand_select_store = p.get_bool("expand_select_store", false);
}
void array_rewriter::get_param_descrs(param_descrs & r) {
r.insert(":expand-select-store", CPK_BOOL, "(default: false) replace a (select (store ...) ...) term by an if-then-else term.");
r.insert(":sort-store", CPK_BOOL, "(default: false) sort nested stores when the indices are known to be different.");
r.insert("expand_select_store", CPK_BOOL, "(default: false) replace a (select (store ...) ...) term by an if-then-else term.");
r.insert("sort_store", CPK_BOOL, "(default: false) sort nested stores when the indices are known to be different.");
}
br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {

8
src/front_end_params/bit_blaster_params.h → src/ast/rewriter/bit_blaster/bit_blaster_params.h
View file

@ -19,8 +19,6 @@ Revision History:
#ifndef _BIT_BLASTER_PARAMS_H_
#define _BIT_BLASTER_PARAMS_H_
#include"ini_file.h"
struct bit_blaster_params {
bool m_bb_ext_gates;
bool m_bb_quantifiers;
@ -28,10 +26,12 @@ struct bit_blaster_params {
m_bb_ext_gates(false),
m_bb_quantifiers(false) {
}
#if 0
void register_params(ini_params & p) {
p.register_bool_param("BB_EXT_GATES", m_bb_ext_gates, "use extended gates during bit-blasting");
p.register_bool_param("BB_QUANTIFIERS", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers");
p.register_bool_param("bb_ext_gates", m_bb_ext_gates, "use extended gates during bit-blasting");
p.register_bool_param("bb_quantifiers", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers");
}
#endif
};
#endif /* _BIT_BLASTER_PARAMS_H_ */

12
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -125,12 +125,12 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_max_steps = p.get_uint(":max-steps", UINT_MAX);
m_blast_add = p.get_bool(":blast-add", true);
m_blast_mul = p.get_bool(":blast-mul", true);
m_blast_full = p.get_bool(":blast-full", false);
m_blast_quant = p.get_bool(":blast-quant", false);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
m_blast_add = p.get_bool("blast_add", true);
m_blast_mul = p.get_bool("blast_mul", true);
m_blast_full = p.get_bool("blast_full", false);
m_blast_quant = p.get_bool("blast_quant", false);
m_blaster.set_max_memory(m_max_memory);
}

25
src/ast/rewriter/bool_rewriter.cpp
View file

@ -20,21 +20,22 @@ Notes:
#include"rewriter_def.h"
void bool_rewriter::updt_params(params_ref const & p) {
m_flat = p.get_bool(":flat", true);
m_elim_and = p.get_bool(":elim-and", false);
m_local_ctx = p.get_bool(":local-ctx", false);
m_local_ctx_limit = p.get_uint(":local-ctx-limit", UINT_MAX);
m_blast_distinct = p.get_bool(":blast-distinct", false);
m_ite_extra_rules = p.get_bool(":ite-extra-rules", false);
m_flat = p.get_bool("flat", true);
m_elim_and = p.get_bool("elim_and", false);
m_local_ctx = p.get_bool("local_ctx", false);
m_local_ctx_limit = p.get_uint("local_ctx_limit", UINT_MAX);
m_blast_distinct = p.get_bool("blast_distinct", false);
m_ite_extra_rules = p.get_bool("ite_extra_rules", false);
}
void bool_rewriter::get_param_descrs(param_descrs & r) {
r.insert(":ite-extra-rules", CPK_BOOL, "(default: false) extra ite simplifications, these additional simplifications may reduce size locally but increase globally.");
r.insert(":flat", CPK_BOOL, "(default: true) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor.");
r.insert(":elim-and", CPK_BOOL, "(default: false) conjunctions are rewritten using negation and disjunctions.");
r.insert(":local-ctx", CPK_BOOL, "(default: false) perform local (i.e., cheap) context simplifications.");
r.insert(":local-ctx-limit", CPK_UINT, "(default: inf) limit for applying local context simplifier.");
r.insert(":blast-distinct", CPK_BOOL, "(default: false) expand a distinct predicate into a quadratic number of disequalities.");
r.insert("ite_extra_rules", CPK_BOOL,
"(default: false) extra ite simplifications, these additional simplifications may reduce size locally but increase globally.");
r.insert("flat", CPK_BOOL, "(default: true) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor.");
r.insert("elim_and", CPK_BOOL, "(default: false) conjunctions are rewritten using negation and disjunctions.");
r.insert("local_ctx", CPK_BOOL, "(default: false) perform local (i.e., cheap) context simplifications.");
r.insert("local_ctx_limit", CPK_UINT, "(default: inf) limit for applying local context simplifier.");
r.insert("blast_distinct", CPK_BOOL, "(default: false) expand a distinct predicate into a quadratic number of disequalities.");
}
br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {

32
src/ast/rewriter/bv_rewriter.cpp
View file

@ -54,14 +54,14 @@ app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
}
void bv_rewriter::updt_local_params(params_ref const & p) {
m_hi_div0 = p.get_bool(":hi-div0", true);
m_elim_sign_ext = p.get_bool(":elim-sign-ext", true);
m_mul2concat = p.get_bool(":mul2concat", false);
m_bit2bool = p.get_bool(":bit2bool", true);
m_blast_eq_value = p.get_bool(":blast-eq-value", false);
m_mkbv2num = p.get_bool(":mkbv2num", false);
m_split_concat_eq = p.get_bool(":split-concat-eq", false);
m_udiv2mul = p.get_bool(":udiv2mul", false);
m_hi_div0 = p.get_bool("hi_div0", true);
m_elim_sign_ext = p.get_bool("elim_sign_ext", true);
m_mul2concat = p.get_bool("mul2concat", false);
m_bit2bool = p.get_bool("bit2bool", true);
m_blast_eq_value = p.get_bool("blast_eq_value", false);
m_mkbv2num = p.get_bool("mkbv2num", false);
m_split_concat_eq = p.get_bool("split_concat_eq", false);
m_udiv2mul = p.get_bool("udiv2mul", false);
}
void bv_rewriter::updt_params(params_ref const & p) {
@ -71,15 +71,15 @@ void bv_rewriter::updt_params(params_ref const & p) {
void bv_rewriter::get_param_descrs(param_descrs & r) {
poly_rewriter<bv_rewriter_core>::get_param_descrs(r);
r.insert(":udiv2mul", CPK_BOOL, "(default: false) convert constant udiv to mul.");
r.insert(":split-concat-eq", CPK_BOOL, "(default: false) split equalities of the form (= (concat t1 t2) t3).");
r.insert(":bit2bool", CPK_BOOL, "(default: true) try to convert bit-vector terms of size 1 into Boolean terms.");
r.insert(":blast-eq-value", CPK_BOOL, "(default: false) blast (some) Bit-vector equalities into bits.");
r.insert(":elim-sign-ext", CPK_BOOL, "(default: true) expand sign-ext operator using concat and extract.");
r.insert(":hi-div0", CPK_BOOL, "(default: true) use the 'hardware interpretation' for division by zero (for bit-vector terms).");
r.insert(":mul2concat", CPK_BOOL, "(default: false) replace multiplication by a power of two into a concatenation.");
r.insert("udiv2mul", CPK_BOOL, "(default: false) convert constant udiv to mul.");
r.insert("split_concat_eq", CPK_BOOL, "(default: false) split equalities of the form (= (concat t1 t2) t3).");
r.insert("bit2bool", CPK_BOOL, "(default: true) try to convert bit-vector terms of size 1 into Boolean terms.");
r.insert("blast_eq_value", CPK_BOOL, "(default: false) blast (some) Bit-vector equalities into bits.");
r.insert("elim_sign_ext", CPK_BOOL, "(default: true) expand sign-ext operator using concat and extract.");
r.insert("hi_div0", CPK_BOOL, "(default: true) use the 'hardware interpretation' for division by zero (for bit-vector terms).");
r.insert("mul2concat", CPK_BOOL, "(default: false) replace multiplication by a power of two into a concatenation.");
#ifndef _EXTERNAL_RELEASE
r.insert(":mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
#endif
}

5
src/ast/rewriter/float_rewriter.cpp
View file

@ -59,6 +59,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
}
return st;
}
@ -439,3 +440,7 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
return BR_FAILED;
}
br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) {
return BR_FAILED;
}

2
src/ast/rewriter/float_rewriter.h
View file

@ -67,6 +67,8 @@ public:
br_status mk_is_nzero(expr * arg1, expr_ref & result);
br_status mk_is_pzero(expr * arg1, expr_ref & result);
br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
};
#endif

18
src/ast/rewriter/poly_rewriter_def.h
View file

@ -27,19 +27,19 @@ char const * poly_rewriter<Config>::g_ste_blowup_msg = "sum of monomials blowup"
template<typename Config>
void poly_rewriter<Config>::updt_params(params_ref const & p) {
m_flat = p.get_bool(":flat", true);
m_som = p.get_bool(":som", false);
m_hoist_mul = p.get_bool(":hoist-mul", false);
m_hoist_cmul = p.get_bool(":hoist-cmul", false);
m_som_blowup = p.get_uint(":som-blowup", UINT_MAX);
m_flat = p.get_bool("flat", true);
m_som = p.get_bool("som", false);
m_hoist_mul = p.get_bool("hoist_mul", false);
m_hoist_cmul = p.get_bool("hoist_cmul", false);
m_som_blowup = p.get_uint("som_blowup", UINT_MAX);
}
template<typename Config>
void poly_rewriter<Config>::get_param_descrs(param_descrs & r) {
r.insert(":som", CPK_BOOL, "(default: false) put polynomials in som-of-monomials form.");
r.insert(":som-blowup", CPK_UINT, "(default: infty) maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form");
r.insert(":hoist-mul", CPK_BOOL, "(default: false) hoist multiplication over summation to minimize number of multiplications");
r.insert(":hoist-cmul", CPK_BOOL, "(default: false) hoist constant multiplication over summation to minimize number of multiplications");
r.insert("som", CPK_BOOL, "(default: false) put polynomials in som-of-monomials form.");
r.insert("som_blowup", CPK_UINT, "(default: infty) maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form");
r.insert("hoist_mul", CPK_BOOL, "(default: false) hoist multiplication over summation to minimize number of multiplications");
r.insert("hoist_cmul", CPK_BOOL, "(default: false) hoist constant multiplication over summation to minimize number of multiplications");
}
template<typename Config>

22
src/ast/rewriter/th_rewriter.cpp
View file

@ -57,13 +57,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m() const { return m_b_rw.m(); }
void updt_local_params(params_ref const & p) {
m_flat = p.get_bool(":flat", true);
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_max_steps = p.get_uint(":max-steps", UINT_MAX);
m_pull_cheap_ite = p.get_bool(":pull-cheap-ite", false);
m_cache_all = p.get_bool(":cache-all", false);
m_push_ite_arith = p.get_bool(":push-ite-arith", false);
m_push_ite_bv = p.get_bool(":push-ite-bv", false);
m_flat = p.get_bool("flat", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
m_pull_cheap_ite = p.get_bool("pull_cheap_ite", false);
m_cache_all = p.get_bool("cache_all", false);
m_push_ite_arith = p.get_bool("push_ite_arith", false);
m_push_ite_bv = p.get_bool("push_ite_bv", false);
}
void updt_params(params_ref const & p) {
@ -695,10 +695,10 @@ void th_rewriter::get_param_descrs(param_descrs & r) {
array_rewriter::get_param_descrs(r);
insert_max_memory(r);
insert_max_steps(r);
r.insert(":push-ite-arith", CPK_BOOL, "(default: false) push if-then-else over arithmetic terms.");
r.insert(":push-ite-bv", CPK_BOOL, "(default: false) push if-then-else over bit-vector terms.");
r.insert(":pull-cheap-ite", CPK_BOOL, "(default: false) pull if-then-else terms when cheap.");
r.insert(":cache-all", CPK_BOOL, "(default: false) cache all intermediate results.");
r.insert("push_ite_arith", CPK_BOOL, "(default: false) push if-then-else over arithmetic terms.");
r.insert("push_ite_bv", CPK_BOOL, "(default: false) push if-then-else over bit-vector terms.");
r.insert("pull_cheap_ite", CPK_BOOL, "(default: false) pull if-then-else terms when cheap.");
r.insert("cache_all", CPK_BOOL, "(default: false) cache all intermediate results.");
}
th_rewriter::~th_rewriter() {

4
src/ast/rewriter/th_rewriter.h
View file

@ -37,7 +37,9 @@ public:
void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
/*
REG_MODULE_PARAMS('simplify', 'th_rewriter::get_param_descrs')
*/
unsigned get_cache_size() const;
unsigned get_num_steps() const;

26
src/ast/simplifier/arith_simplifier_params.cpp Normal file
View file

@ -0,0 +1,26 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
arith_simplifier_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include"arith_simplifier_params.h"
#include"arith_simplifier_params_helper.hpp"
void arith_simplifier_params::updt_params(params_ref const & _p) {
arith_simplifier_params_helper p(_p);
m_arith_expand_eqs = p.arith_expand_eqs();
m_arith_process_all_eqs = p.arith_process_all_eqs();
}

13
src/front_end_params/arith_simplifier_params.h → src/ast/simplifier/arith_simplifier_params.h
View file

@ -19,18 +19,17 @@ Revision History:
#ifndef _ARITH_SIMPLIFIER_PARAMS_H_
#define _ARITH_SIMPLIFIER_PARAMS_H_
#include"ini_file.h"
#include"params.h"
struct arith_simplifier_params {
struct arith_simplifier_params {
bool m_arith_expand_eqs;
bool m_arith_process_all_eqs;
arith_simplifier_params():
m_arith_expand_eqs(false),
m_arith_process_all_eqs(false) {
arith_simplifier_params(params_ref const & p = params_ref()) {
updt_params(p);
}
void register_params(ini_params & p);
void updt_params(params_ref const & _p);
};
#endif /* _ARITH_SIMPLIFIER_PARAMS_H_ */

7
src/ast/simplifier/arith_simplifier_params_helper.pyg Normal file
View file

@ -0,0 +1,7 @@
def_module_params(class_name='arith_simplifier_params_helper',
module_name="old_simplify", # Parameters will be in the old_simplify module
description="old simplification (stack) still used in the smt module",
export=True,
params=(
('arith.expand_eqs', BOOL, False, 'expand equalities into two inequalities'),
('arith.process_all_eqs', BOOL, False, 'put all equations in the form (= t c), where c is a numeral')))

26
src/ast/simplifier/array_simplifier_params.cpp Normal file
View file

@ -0,0 +1,26 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
array_simplifier_params.cpp
Abstract:
This file was created during code reorg.
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include"array_simplifier_params.h"
#include"array_simplifier_params_helper.hpp"
void array_simplifier_params::updt_params(params_ref const & _p) {
array_simplifier_params_helper p(_p);
m_array_canonize_simplify = p.array_canonize();
m_array_simplify = p.array_simplify();
}

36
src/ast/simplifier/array_simplifier_params.h Normal file
View file

@ -0,0 +1,36 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
array_simplifier_params.h
Abstract:
This file was created during code reorg.
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#ifndef _ARRAY_SIMPLIFIER_PARAMS_H_
#define _ARRAY_SIMPLIFIER_PARAMS_H_
#include"params.h"
struct array_simplifier_params {
bool m_array_canonize_simplify;
bool m_array_simplify; // temporary hack for disabling array simplifier plugin.
array_simplifier_params(params_ref const & p = params_ref()) {
updt_params(p);
}
void updt_params(params_ref const & _p);
};
#endif /* _ARITH_SIMPLIFIER_PARAMS_H_ */

6
src/ast/simplifier/array_simplifier_params_helper.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params(class_name='array_simplifier_params_helper',
module_name="old_simplify", # Parameters will be in the old_simplify module
export=True,
params=(
('array.canonize', BOOL, False, 'normalize array terms into normal form during simplification'),
('array.simplify', BOOL, True, 'enable/disable array simplifications')))

2
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -33,7 +33,7 @@ array_simplifier_plugin::array_simplifier_plugin(
ast_manager & m,
basic_simplifier_plugin& s,
simplifier& simp,
theory_array_params const& p) :
array_simplifier_params const& p) :
simplifier_plugin(symbol("array"),m),
m_util(m),
m_simp(s),

6
src/ast/simplifier/array_simplifier_plugin.h
View file

@ -24,7 +24,7 @@ Revision History:
#include"array_decl_plugin.h"
#include"simplifier_plugin.h"
#include"basic_simplifier_plugin.h"
#include"theory_array_params.h"
#include"array_simplifier_params.h"
#include"simplifier.h"
#include"obj_hashtable.h"
#include"lbool.h"
@ -71,7 +71,7 @@ class array_simplifier_plugin : public simplifier_plugin {
array_util m_util;
basic_simplifier_plugin& m_simp;
simplifier& m_simplifier;
theory_array_params const& m_params;
array_simplifier_params const& m_params;
select_cache m_select_cache;
ptr_vector<expr> m_tmp;
ptr_vector<expr> m_tmp2;
@ -100,7 +100,7 @@ class array_simplifier_plugin : public simplifier_plugin {
public:
array_simplifier_plugin(ast_manager & m, basic_simplifier_plugin& s, simplifier& simp, theory_array_params const& p);
array_simplifier_plugin(ast_manager & m, basic_simplifier_plugin& s, simplifier& simp, array_simplifier_params const& p);
virtual ~array_simplifier_plugin();
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);

26
src/ast/simplifier/bv_simplifier_params.cpp Normal file
View file

@ -0,0 +1,26 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
bv_simplifier_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include"bv_simplifier_params.h"
#include"bv_simplifier_params_helper.hpp"
void bv_simplifier_params::updt_params(params_ref const & _p) {
bv_simplifier_params_helper p(_p);
m_hi_div0 = p.bv_hi_div0();
m_bv2int_distribute = p.bv_bv2int_distribute();
}

13
src/front_end_params/bv_simplifier_params.h → src/ast/simplifier/bv_simplifier_params.h
View file

@ -19,20 +19,17 @@ Revision History:
#ifndef _BV_SIMPLIFIER_PARAMS_H_
#define _BV_SIMPLIFIER_PARAMS_H_
#include"ini_file.h"
#include"params.h"
struct bv_simplifier_params {
bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
bool m_bv2int_distribute; //!< if true allows downward propagation of bv2int.
bv_simplifier_params():
m_hi_div0(true),
m_bv2int_distribute(true) {
}
void register_params(ini_params & p) {
p.register_bool_param("HI_DIV0", m_hi_div0, "if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted.");
p.register_bool_param("BV2INT_DISTRIBUTE", m_bv2int_distribute, "if true, then int2bv is distributed over arithmetical operators.");
bv_simplifier_params(params_ref const & p = params_ref()) {
updt_params(p);
}
void updt_params(params_ref const & _p);
};
#endif /* _BV_SIMPLIFIER_PARAMS_H_ */

6
src/ast/simplifier/bv_simplifier_params_helper.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params(class_name='bv_simplifier_params_helper',
module_name="old_simplify", # Parameters will be in the old_simplify module
export=True,
params=(
('bv.hi_div0', BOOL, True, 'if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero; otherwise, these operations are considered uninterpreted'),
('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators')))

4
src/ast/substitution/substitution_tree.cpp
View file

@ -607,8 +607,8 @@ void substitution_tree::display(std::ostream & out, node * n, unsigned delta) co
out << " ";
display(out, n->m_subst);
if (n->m_leaf) {
pp_params p;
p.m_pp_single_line = true;
params_ref p;
p.set_bool("single_line", true);
out << " ==> ";
out << mk_pp(n->m_expr, m_manager, p);
out << "\n";

81
src/cmd_context/basic_cmds.cpp
View file

@ -27,7 +27,9 @@ Notes:
#include"cmd_util.h"
#include"simplify_cmd.h"
#include"eval_cmd.h"
#include"front_end_params.h"
#include"gparams.h"
#include"model_params.hpp"
#include"env_params.h"
class help_cmd : public cmd {
svector<symbol> m_cmds;
@ -103,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;
@ -156,7 +159,7 @@ public:
};
ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
if (ctx.params().m_proof_mode == PGM_DISABLED)
if (!ctx.produce_proofs())
throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
if (!ctx.has_manager() ||
ctx.cs_state() != cmd_context::css_unsat)
@ -219,25 +222,6 @@ UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr
UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << arg << std::endl;);
/**
\brief Convert a keyword into an internal Z3 option name
*/
std::string smt_keyword2opt_name(symbol const & opt) {
std::string r;
SASSERT(opt.bare_str()[0] == ':');
r = opt.bare_str() + 1;
unsigned sz = static_cast<unsigned>(r.size());
for (unsigned i = 0; i < sz; i++) {
char curr = r[i];
if ('a' <= curr && curr <= 'z')
r[i] = 'A' + (curr - 'a');
else if (curr == '-')
r[i] = '_';
}
TRACE("smt2_opt_name", tout << opt << " -> '" << r << "'\n";);
return r;
}
class set_get_option_cmd : public cmd {
protected:
symbol m_true;
@ -259,7 +243,6 @@ protected:
symbol m_numeral_as_real;
symbol m_error_behavior;
symbol m_int_real_coercions;
ini_params m_ini;
bool is_builtin_option(symbol const & s) const {
return
@ -270,7 +253,7 @@ protected:
}
public:
set_get_option_cmd(char const * name, front_end_params & params):
set_get_option_cmd(char const * name):
cmd(name),
m_true("true"),
m_false("false"),
@ -289,10 +272,7 @@ public:
m_global_decls(":global-decls"),
m_numeral_as_real(":numeral-as-real"),
m_error_behavior(":error-behavior"),
m_int_real_coercions(":int-real-coercions"),
m_ini(false) {
params.register_params(m_ini);
register_pp_params(m_ini);
m_int_real_coercions(":int-real-coercions") {
}
virtual ~set_get_option_cmd() {}
@ -324,22 +304,13 @@ class set_option_cmd : public set_get_option_cmd {
}
void set_param(cmd_context & ctx, char const * value) {
m_ini.freeze(ctx.has_manager());
std::string internal_opt = smt_keyword2opt_name(m_option);
try {
std::string old_value;
if (!m_ini.get_param_value(internal_opt.c_str(), old_value)) {
m_unsupported = true;
return;
}
m_ini.set_param_value(internal_opt.c_str(), value);
gparams::set(m_option, value);
env_params::updt_params();
ctx.params().updt_params();
}
catch (set_get_param_exception ex) {
std::string msg = "error setting '";
msg += m_option.str();
msg += "', ";
msg += ex.get_msg();
throw cmd_exception(msg);
catch (gparams::exception ex) {
throw cmd_exception(ex.msg());
}
}
@ -406,8 +377,8 @@ class set_option_cmd : public set_get_option_cmd {
}
public:
set_option_cmd(front_end_params & params):
set_get_option_cmd("set-option", params),
set_option_cmd():
set_get_option_cmd("set-option"),
m_unsupported(false) {
}
@ -485,8 +456,8 @@ class get_option_cmd : public set_get_option_cmd {
}
public:
get_option_cmd(front_end_params & params):
set_get_option_cmd("get-option", params) {
get_option_cmd():
set_get_option_cmd("get-option") {
}
virtual char const * get_usage() const { return "<keyword>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; }
@ -507,13 +478,13 @@ public:
print_bool(ctx, ctx.interactive_mode());
}
else if (opt == m_produce_proofs) {
print_bool(ctx, ctx.params().m_proof_mode != PGM_DISABLED);
print_bool(ctx, ctx.produce_proofs());
}
else if (opt == m_produce_unsat_cores) {
print_bool(ctx, ctx.produce_unsat_cores());
}
else if (opt == m_produce_models) {
print_bool(ctx, ctx.params().m_model);
print_bool(ctx, ctx.produce_models());
}
else if (opt == m_produce_assignments) {
print_bool(ctx, ctx.produce_assignments());
@ -545,12 +516,10 @@ public:
print_bool(ctx, ctx.m().int_real_coercions());
}
else {
std::string iopt = smt_keyword2opt_name(opt);
std::string r;
if (m_ini.get_param_value(iopt.c_str(), r)) {
ctx.regular_stream() << r << std::endl;
try {
std::string val = gparams::get_value(opt);
}
else {
catch (gparams::exception ex) {
ctx.print_unsupported(opt);
}
}
@ -744,8 +713,8 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(get_assertions_cmd));
ctx.insert(alloc(get_proof_cmd));
ctx.insert(alloc(get_unsat_core_cmd));
ctx.insert(alloc(set_option_cmd, ctx.params()));
ctx.insert(alloc(get_option_cmd, ctx.params()));
ctx.insert(alloc(set_option_cmd));
ctx.insert(alloc(get_option_cmd));
ctx.insert(alloc(get_info_cmd));
ctx.insert(alloc(set_info_cmd));
ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));

131
src/cmd_context/cmd_context.cpp
View file

@ -16,7 +16,6 @@ Notes:
--*/
#include<signal.h>
#include"front_end_params.h"
#include"tptr.h"
#include"cmd_context.h"
#include"func_decl_dependencies.h"
@ -39,6 +38,22 @@ Notes:
#include"model_evaluator.h"
#include"for_each_expr.h"
std::string smt2_keyword_to_param(symbol const & opt) {
std::string r;
SASSERT(opt.bare_str()[0] == ':');
r = opt.bare_str() + 1;
unsigned sz = static_cast<unsigned>(r.size());
for (unsigned i = 0; i < sz; i++) {
char curr = r[i];
if ('A' <= curr && curr <= 'Z')
r[i] = curr - 'A' + 'a';
else if (curr == '-')
r[i] = '_';
}
TRACE("smt2_keyword_to_param", tout << opt << " -> '" << r << "'\n";);
return r;
}
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
m.inc_ref(f);
@ -300,10 +315,8 @@ 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_logic(l),
m_interactive_mode(false),
m_global_decls(false), // :global-decls is false by default.
@ -343,39 +356,44 @@ cmd_context::~cmd_context() {
finalize_probes();
m_solver = 0;
m_check_sat_result = 0;
if (m_params_owner) {
dealloc(m_params);
}
}
void cmd_context::set_produce_models(bool f) {
params().m_model = f;
if (m_solver)
m_solver->set_produce_models(f);
m_params.m_model = f;
}
void cmd_context::set_produce_unsat_cores(bool f) {
// can only be set before initialization
SASSERT(!has_manager());
m_produce_unsat_cores = f;
m_params.m_unsat_core = f;
}
void cmd_context::set_produce_proofs(bool f) {
// can only be set before initialization
SASSERT(!has_manager());
params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
}
bool cmd_context::is_smtlib2_compliant() const {
return params().m_smtlib2_compliant;
m_params.m_proof = f;
}
bool cmd_context::produce_models() const {
return params().m_model;
return m_params.m_model;
}
bool cmd_context::produce_proofs() const {
return params().m_proof_mode != PGM_DISABLED;
return m_params.m_proof;
}
bool cmd_context::produce_unsat_cores() const {
return m_params.m_unsat_core;
}
bool cmd_context::well_sorted_check_enabled() const {
return m_params.m_well_sorted_check;
}
bool cmd_context::validate_model_enabled() const {
return m_params.m_validate_model;
}
cmd_context::check_sat_state cmd_context::cs_state() const {
@ -460,6 +478,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "LIA" ||
s == "LRA" ||
s == "QF_FPA" ||
s == "QF_FPABV" ||
s == "HORN";
}
@ -478,6 +497,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
s == "QF_ABV" ||
s == "QF_AUFBV" ||
s == "QF_BVRE" ||
s == "QF_FPABV" ||
s == "HORN";
}
@ -502,7 +522,7 @@ bool cmd_context::logic_has_seq() const {
}
bool cmd_context::logic_has_floats() const {
return !has_logic() || m_logic == "QF_FPA";
return !has_logic() || m_logic == "QF_FPA" || m_logic == "QF_FPABV";
}
bool cmd_context::logic_has_array_core(symbol const & s) const {
@ -568,10 +588,7 @@ void cmd_context::init_manager_core(bool new_manager) {
insert(pm().mk_plist_decl());
}
if (m_solver) {
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_solver->set_produce_models(params().m_model);
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
m_solver->init(m(), m_logic);
init_solver_options(m_solver.get());
}
m_check_logic.set_logic(m(), m_logic);
}
@ -580,11 +597,14 @@ void cmd_context::init_manager() {
SASSERT(m_manager == 0);
SASSERT(m_pmanager == 0);
m_check_sat_result = 0;
m_manager = alloc(ast_manager, params().m_proof_mode, params().m_trace_stream);
m_manager = alloc(ast_manager,
produce_proofs() ? PGM_FINE : PGM_DISABLED,
m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0);
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() {
@ -599,7 +619,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
logic_has_arith_core(s) || logic_has_bv_core(s) ||
logic_has_array_core(s) || logic_has_seq_core(s) ||
logic_has_horn(s) ||
s == "QF_FPA";
s == "QF_FPA" || s == "QF_FPABV";
}
void cmd_context::set_logic(symbol const & s) {
@ -843,7 +863,7 @@ object_ref * cmd_context::find_object_ref(symbol const & s) const {
return r;
}
#define CHECK_SORT(T) if (params().m_well_sorted_check) m().check_sorts_core(T)
#define CHECK_SORT(T) if (well_sorted_check_enabled()) m().check_sorts_core(T)
void cmd_context::mk_const(symbol const & s, expr_ref & result) const {
mk_app(s, 0, 0, 0, 0, 0, result);
@ -883,13 +903,13 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
return;
}
SASSERT(num_args > 0);
TRACE("macro_bug", tout << "m_well_sorted_check: " << params().m_well_sorted_check << "\n";
TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n";
tout << "s: " << s << "\n";
tout << "body:\n" << mk_ismt2_pp(_m.second, m()) << "\n";
tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(m().get_sort(args[i]), m()) << "\n";);
var_subst subst(m());
subst(_m.second, num_args, args, result);
if (params().m_well_sorted_check && !is_well_sorted(m(), result))
if (well_sorted_check_enabled() && !is_well_sorted(m(), result))
throw cmd_exception("invalid macro application, sort mismatch ", s);
return;
}
@ -918,7 +938,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
func_decl * f = fs.find(m(), num_args, args, range);
if (f == 0)
throw cmd_exception("unknown constant ", s);
if (params().m_well_sorted_check)
if (well_sorted_check_enabled())
m().check_sort(f, num_args, args);
result = m().mk_app(f, num_args, args);
return;
@ -1139,7 +1159,7 @@ void cmd_context::assert_expr(expr * t) {
m_check_sat_result = 0;
m().inc_ref(t);
m_assertions.push_back(t);
if (m_produce_unsat_cores)
if (produce_unsat_cores())
m_assertion_names.push_back(0);
if (m_solver)
m_solver->assert_expr(t);
@ -1148,7 +1168,7 @@ void cmd_context::assert_expr(expr * t) {
void cmd_context::assert_expr(symbol const & name, expr * t) {
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
if (!m_produce_unsat_cores || name == symbol::null) {
if (!produce_unsat_cores() || name == symbol::null) {
assert_expr(t);
return;
}
@ -1254,7 +1274,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
SASSERT(old_sz <= m_assertions.size());
SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
restore(m(), m_assertions, old_sz);
if (m_produce_unsat_cores)
if (produce_unsat_cores())
restore(m(), m_assertion_names, old_sz);
if (m_interactive_mode)
m_assertion_strings.shrink(old_sz);
@ -1283,18 +1303,12 @@ void cmd_context::pop(unsigned n) {
void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) {
if (m_ignore_check)
return;
IF_VERBOSE(100, verbose_stream() << "check-sat..." << std::endl;);
IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
TRACE("before_check_sat", dump_assertions(tout););
if (params().m_ignore_checksat) {
m_check_sat_result = 0;
regular_stream() << "unknown" << std::endl;
return;
}
if (!has_manager())
init_manager();
if (m_solver) {
m_check_sat_result = m_solver.get(); // solver itself stores the result.
m_solver->set_front_end_params(params());
m_solver->set_progress_callback(this);
scoped_watch sw(*this);
cancel_eh<solver> eh(*m_solver);
@ -1392,7 +1406,7 @@ struct contains_array_op_proc {
\brief Check if the current model satisfies the quantifier free formulas.
*/
void cmd_context::validate_model() {
if (!params().m_model_validate)
if (!validate_model_enabled())
return;
if (!is_model_available())
return;
@ -1400,9 +1414,9 @@ void cmd_context::validate_model() {
get_check_sat_result()->get_model(md);
SASSERT(md.get() != 0);
params_ref p;
p.set_uint(":max-degree", UINT_MAX); // evaluate algebraic numbers of any degree.
p.set_uint(":sort-store", true);
p.set_bool(":model-completion", true);
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
p.set_uint("sort_store", true);
p.set_bool("model_completion", true);
model_evaluator evaluator(*(md.get()), p);
contains_array_op_proc contains_array(m());
{
@ -1435,15 +1449,23 @@ void cmd_context::validate_model() {
}
}
void cmd_context::init_solver_options(solver * s) {
m_solver->set_produce_unsat_cores(produce_unsat_cores());
m_solver->set_produce_models(produce_models());
m_solver->set_produce_proofs(produce_proofs());
m_solver->init(m(), m_logic);
if (!m_params.m_auto_config) {
params_ref p;
p.set_bool("auto_config", false);
m_solver->updt_params(p);
}
}
void cmd_context::set_solver(solver * s) {
m_check_sat_result = 0;
m_solver = s;
m_solver->set_front_end_params(params());
if (has_manager() && s != 0) {
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_solver->set_produce_models(params().m_model);
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
m_solver->init(m(), m_logic);
init_solver_options(s);
// assert formulas and create scopes in the new solver.
unsigned lim = 0;
svector<scope>::iterator it = m_scopes.begin();
@ -1497,7 +1519,7 @@ void cmd_context::display_assertions() {
}
bool cmd_context::is_model_available() const {
if (params().m_model &&
if (produce_models() &&
has_manager() &&
(cs_state() == css_sat || cs_state() == css_unknown)) {
model_ref md;
@ -1520,8 +1542,7 @@ cmd_context::pp_env & cmd_context::get_pp_env() const {
}
void cmd_context::pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
mk_smt2_format(n, get_pp_env(), get_pp_default_params(),
num_vars, var_prefix, r, var_names);
mk_smt2_format(n, get_pp_env(), params_ref(), num_vars, var_prefix, r, var_names);
}
void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
@ -1530,7 +1551,7 @@ void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
}
void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const {
mk_smt2_format(f, get_pp_env(), get_pp_default_params(), r);
mk_smt2_format(f, get_pp_env(), params_ref(), r);
}
void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
@ -1538,7 +1559,7 @@ void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
f = pp(s);
if (indent > 0)
f = format_ns::mk_indent(m(), indent, f);
::pp(out, f.get(), m(), get_pp_default_params());
::pp(out, f.get(), m());
}
void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
@ -1546,7 +1567,7 @@ void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigne
pp(n, num_vars, var_prefix, f, var_names);
if (indent > 0)
f = format_ns::mk_indent(m(), indent, f);
::pp(out, f.get(), m(), get_pp_default_params());
::pp(out, f.get(), m());
}
void cmd_context::display(std::ostream & out, expr * n, unsigned indent) const {
@ -1559,7 +1580,7 @@ void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) co
pp(d, f);
if (indent > 0)
f = format_ns::mk_indent(m(), indent, f);
::pp(out, f.get(), m(), get_pp_default_params());
::pp(out, f.get(), m());
}
void cmd_context::dump_assertions(std::ostream & out) const {

20
src/cmd_context/cmd_context.h
View file

@ -36,8 +36,12 @@ Notes:
#include"check_logic.h"
#include"progress_callback.h"
#include"scoped_ptr_vector.h"
#include"context_params.h"
struct front_end_params;
/**
\brief Auxiliary function for converting SMT2 keywords into Z3 internal parameter names.
*/
std::string smt2_keyword_to_param(symbol const & k);
class func_decls {
func_decl * m_decls;
@ -132,9 +136,8 @@ public:
};
protected:
context_params m_params;
bool m_main_ctx;
front_end_params * m_params;
bool m_params_owner;
symbol m_logic;
bool m_interactive_mode;
bool m_global_decls;
@ -245,10 +248,12 @@ protected:
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
void init_solver_options(solver * s);
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;
context_params & params() { return m_params; }
void set_logic(symbol const & s);
bool has_logic() const { return m_logic != symbol::null; }
symbol const & get_logic() const { return m_logic; }
@ -270,7 +275,9 @@ public:
void set_random_seed(unsigned s) { m_random_seed = s; }
bool produce_models() const;
bool produce_proofs() const;
bool produce_unsat_cores() const { return m_produce_unsat_cores; }
bool produce_unsat_cores() const;
bool well_sorted_check_enabled() const;
bool validate_model_enabled() const;
void set_produce_models(bool flag);
void set_produce_unsat_cores(bool flag);
void set_produce_proofs(bool flag);
@ -285,7 +292,6 @@ 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; }
void set_solver(solver * s);
solver * get_solver() const { return m_solver.get(); }

114
src/cmd_context/context_params.cpp Normal file
View file

@ -0,0 +1,114 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
context_params.cpp
Abstract:
Goodies for managing context parameters in the cmd_context and
api_context
Author:
Leonardo (leonardo) 2012-12-01
Notes:
--*/
#include"context_params.h"
#include"gparams.h"
#include"params.h"
context_params::context_params() {
updt_params();
}
void context_params::set_bool(bool & opt, char const * param, char const * value) {
if (strcmp(value, "true") == 0) {
opt = true;
}
else if (strcmp(value, "false") == 0) {
opt = false;
}
else {
throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param);
}
}
void context_params::set(char const * param, char const * value) {
std::string p = param;
unsigned n = p.size();
for (unsigned i = 0; i < n; i++) {
if (p[i] >= 'A' && p[i] <= 'Z')
p[i] = p[i] - 'A' + 'a';
else if (p[i] == '-')
p[i] = '_';
}
if (p == "timeout") {
long val = strtol(value, 0, 10);
m_timeout = static_cast<unsigned>(val);
}
else if (p == "type_check" || p == "well_sorted_check") {
set_bool(m_well_sorted_check, param, value);
}
else if (p == "auto_config") {
set_bool(m_auto_config, param, value);
}
else if (p == "proof") {
set_bool(m_proof, param, value);
}
else if (p == "model") {
set_bool(m_model, param, value);
}
else if (p == "validate_model") {
set_bool(m_validate_model, param, value);
}
else if (p == "trace") {
set_bool(m_trace, param, value);
}
else if (p == "trace_file_name") {
m_trace_file_name = value;
}
else if (p == "unsat_core") {
set_bool(m_unsat_core, param, value);
}
else if (p == "debug_ref_count") {
set_bool(m_debug_ref_count, param, value);
}
else {
throw default_exception("unknown parameter '%s'", p.c_str());
}
}
void context_params::updt_params() {
updt_params(gparams::get());
}
void context_params::updt_params(params_ref const & p) {
m_timeout = p.get_uint("timeout", UINT_MAX);
m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
m_auto_config = p.get_bool("auto_config", true);
m_proof = p.get_bool("proof", false);
m_model = p.get_bool("model", true);
m_validate_model = p.get_bool("validate_model", false);
m_trace = p.get_bool("trace", false);
m_trace_file_name = p.get_str("trace_file_name", "z3.log");
m_unsat_core = p.get_bool("unsat_core", false);
m_debug_ref_count = p.get_bool("debug_ref_count", false);
}
void context_params::collect_param_descrs(param_descrs & d) {
d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295");
d.insert("well_sorted_check", CPK_BOOL, "type checker", "true");
d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
d.insert("validate_model", CPK_BOOL, "validate models produced by solvers", "false");
d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
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");
d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
}

51
src/cmd_context/context_params.h Normal file
View file

@ -0,0 +1,51 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
context_params.h
Abstract:
Goodies for managing context parameters in the cmd_context and
api_context
Author:
Leonardo (leonardo) 2012-12-01
Notes:
--*/
#ifndef _CONTEXT_PARAMS_H_
#define _CONTEXT_PARAMS_H_
#include"params.h"
class context_params {
void set_bool(bool & opt, char const * param, char const * value);
public:
bool m_auto_config;
bool m_proof;
bool m_debug_ref_count;
bool m_trace;
std::string m_trace_file_name;
bool m_well_sorted_check;
bool m_model;
bool m_validate_model;
bool m_unsat_core;
unsigned m_timeout;
context_params();
void set(char const * param, char const * value);
void updt_params();
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
/*
REG_PARAMS('context_params::collect_param_descrs')
*/
};
#endif

2
src/cmd_context/eval_cmd.cpp
View file

@ -62,7 +62,7 @@ public:
SASSERT(last_result);
last_result->get_model(md);
expr_ref r(ctx.m());
unsigned timeout = m_params.get_uint(":timeout", UINT_MAX);
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
model_evaluator ev(*(md.get()), m_params);
cancel_eh<model_evaluator> eh(ev);
{

24
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -141,8 +141,8 @@ public:
UNARY_CMD(bool_rewriter_cmd, "dbg-bool-rewriter", "<term>", "apply the Boolean rewriter to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
params_ref p;
p.set_bool(":flat", false);
SASSERT(p.get_bool(":flat", true) == false);
p.set_bool("flat", false);
SASSERT(p.get_bool("flat", true) == false);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
ctx.display(ctx.regular_stream(), t);
@ -153,7 +153,7 @@ UNARY_CMD(bool_frewriter_cmd, "dbg-bool-flat-rewriter", "<term>", "apply the Boo
expr_ref t(ctx.m());
{
params_ref p;
p.set_bool(":flat", true);
p.set_bool("flat", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
@ -165,8 +165,8 @@ UNARY_CMD(elim_and_cmd, "dbg-elim-and", "<term>", "apply the Boolean rewriter (e
expr_ref t(ctx.m());
{
params_ref p;
p.set_bool(":flat", true);
p.set_bool(":elim-and", true);
p.set_bool("flat", true);
p.set_bool("elim_and", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
@ -208,15 +208,15 @@ UNARY_CMD(some_value_cmd, "dbg-some-value", "<sort>", "retrieve some value of th
void tst_params(cmd_context & ctx) {
params_ref p1;
params_ref p2;
p1.set_uint(":val", 100);
p1.set_uint("val", 100);
p2 = p1;
SASSERT(p2.get_uint(":val", 0) == 100);
p2.set_uint(":val", 200);
SASSERT(p2.get_uint(":val", 0) == 200);
SASSERT(p1.get_uint(":val", 0) == 100);
SASSERT(p2.get_uint("val", 0) == 100);
p2.set_uint("val", 200);
SASSERT(p2.get_uint("val", 0) == 200);
SASSERT(p1.get_uint("val", 0) == 100);
p2 = p1;
SASSERT(p2.get_uint(":val", 0) == 100);
SASSERT(p1.get_uint(":val", 0) == 100);
SASSERT(p2.get_uint("val", 0) == 100);
SASSERT(p1.get_uint("val", 0) == 100);
ctx.regular_stream() << "worked" << std::endl;
}

8
src/cmd_context/extra_cmds/polynomial_cmds.cpp
View file

@ -26,10 +26,10 @@ Notes:
#include"parametric_cmd.h"
#include"mpq.h"
#include"algebraic_numbers.h"
#include"pp.h"
#include"pp_params.h"
#include"polynomial_var2value.h"
#include"expr2var.h"
#include"pp.h"
#include"pp_params.hpp"
static void to_poly(cmd_context & ctx, expr * t) {
polynomial::numeral_manager nm;
@ -145,9 +145,11 @@ class poly_isolate_roots_cmd : public cmd {
scoped_anum_vector rs(m_am);
m_am.isolate_roots(m_p, m_x2v, rs);
ctx.regular_stream() << "(roots";
pp_params params;
bool pp_decimal = params.decimal();
for (unsigned i = 0; i < rs.size(); i++) {
ctx.regular_stream() << std::endl;
if (!get_pp_default_params().m_pp_decimal)
if (!pp_decimal)
m_am.display_root_smt2(ctx.regular_stream(), rs[i]);
else
m_am.display_decimal(ctx.regular_stream(), rs[i]);

2
src/cmd_context/extra_cmds/subpaving_cmds.cpp
View file

@ -31,7 +31,7 @@ static void to_subpaving(cmd_context & ctx, expr * t) {
expr2var e2v(m);
expr2subpaving e2s(m, *s, &e2v);
params_ref p;
p.set_bool(":mul-to-power", true);
p.set_bool("mul_to_power", true);
th_rewriter simp(m, p);
expr_ref t_s(m);
simp(t, t_s);

9
src/cmd_context/parametric_cmd.cpp
View file

@ -16,6 +16,7 @@ Notes:
--*/
#include<sstream>
#include"cmd_context.h"
#include"parametric_cmd.h"
char const * parametric_cmd::get_descr(cmd_context & ctx) const {
@ -37,13 +38,15 @@ cmd_arg_kind parametric_cmd::next_arg_kind(cmd_context & ctx) const {
void parametric_cmd::set_next_arg(cmd_context & ctx, symbol const & s) {
if (m_last == symbol::null) {
m_last = s;
m_last = symbol(smt2_keyword_to_param(s).c_str());
if (pdescrs(ctx).get_kind(m_last.bare_str()) == CPK_INVALID)
throw cmd_exception("invalid keyword argument");
return;
}
m_params.set_sym(m_last.bare_str(), s);
m_last = symbol::null;
else {
m_params.set_sym(m_last.bare_str(), s);
m_last = symbol::null;
}
}
param_descrs const & parametric_cmd::pdescrs(cmd_context & ctx) const {

18
src/cmd_context/simplify_cmd.cpp
View file

@ -40,9 +40,9 @@ public:
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
th_rewriter::get_param_descrs(p);
insert_timeout(p);
p.insert(":print", CPK_BOOL, "(default: true) print the simplified term.");
p.insert(":print-proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one.");
p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics.");
p.insert("print", CPK_BOOL, "(default: true) print the simplified term.");
p.insert("print_proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one.");
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
}
virtual ~simplify_cmd() {
@ -67,12 +67,12 @@ public:
throw cmd_exception("invalid simplify command, argument expected");
expr_ref r(ctx.m());
proof_ref pr(ctx.m());
if (m_params.get_bool(":som", false))
m_params.set_bool(":flat", true);
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
unsigned cache_sz;
unsigned num_steps = 0;
unsigned timeout = m_params.get_uint(":timeout", UINT_MAX);
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
bool failed = false;
cancel_eh<th_rewriter> eh(s);
{
@ -94,17 +94,17 @@ public:
num_steps = s.get_num_steps();
s.cleanup();
}
if (m_params.get_bool(":print", true)) {
if (m_params.get_bool("print", true)) {
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;
}
if (!failed && m_params.get_bool(":print-proofs", false)) {
if (!failed && m_params.get_bool("print_proofs", false)) {
ast_smt_pp pp(ctx.m());
pp.set_logic(ctx.get_logic().str().c_str());
pp.display_expr_smt2(ctx.regular_stream(), pr.get());
ctx.regular_stream() << std::endl;
}
if (m_params.get_bool(":print-statistics", false)) {
if (m_params.get_bool("print_statistics", false)) {
shared_occs s1(ctx.m());
if (!failed)
s1(r);

46
src/cmd_context/tactic_cmds.cpp
View file

@ -24,7 +24,6 @@ Notes:
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"model_smt2_pp.h"
#include"params2front_end_params.h"
#include"ast_smt2_pp.h"
#include"tactic.h"
#include"tactical.h"
@ -153,7 +152,7 @@ public:
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
insert_timeout(p);
insert_max_memory(p);
p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics.");
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
}
void display_statistics(cmd_context & ctx, tactic * t) {
@ -180,19 +179,17 @@ public:
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
exec_given_tactic_cmd::init_pdescrs(ctx, p);
p.insert(":print-unsat-core", CPK_BOOL, "(default: false) print unsatisfiable core.");
p.insert(":print-proof", CPK_BOOL, "(default: false) print proof.");
p.insert(":print-model", CPK_BOOL, "(default: false) print model.");
p.insert("print_unsat_core", CPK_BOOL, "(default: false) print unsatisfiable core.");
p.insert("print_proof", CPK_BOOL, "(default: false) print proof.");
p.insert("print_model", CPK_BOOL, "(default: false) print model.");
}
virtual void execute(cmd_context & ctx) {
params_ref p = ps();
front_end_params2params(ctx.params(), p);
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
tref->set_front_end_params(ctx.params());
tref->set_logic(ctx.get_logic());
ast_manager & m = ctx.m();
unsigned timeout = p.get_uint(":timeout", UINT_MAX);
unsigned timeout = p.get_uint("timeout", UINT_MAX);
goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
assert_exprs_from(ctx, *g);
TRACE("check_sat_using", g->display(tout););
@ -241,7 +238,7 @@ public:
ptr_vector<expr> core_elems;
m.linearize(core, core_elems);
result->m_core.append(core_elems.size(), core_elems.c_ptr());
if (p.get_bool(":print-unsat-core", false)) {
if (p.get_bool("print_unsat_core", false)) {
ctx.regular_stream() << "(unsat-core";
ptr_vector<expr>::const_iterator it = core_elems.begin();
ptr_vector<expr>::const_iterator end = core_elems.end();
@ -255,7 +252,7 @@ public:
if (ctx.produce_models() && md) {
result->m_model = md;
if (p.get_bool(":print-model", false)) {
if (p.get_bool("print_model", false)) {
ctx.regular_stream() << "(model " << std::endl;
model_smt2_pp(ctx.regular_stream(), ctx, *md, 2);
ctx.regular_stream() << ")" << std::endl;
@ -266,12 +263,12 @@ public:
if (ctx.produce_proofs() && pr) {
result->m_proof = pr;
if (p.get_bool(":print-proof", false)) {
if (p.get_bool("print_proof", false)) {
ctx.regular_stream() << mk_ismt2_pp(pr, m) << "\n";
}
}
if (p.get_bool(":print-statistics", false))
if (p.get_bool("print_statistics", false))
display_statistics(ctx, tref.get());
}
};
@ -285,21 +282,20 @@ public:
virtual char const * get_main_descr() const { return "apply the given tactic to the current context, and print the resultant set of goals."; }
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
p.insert(":print", CPK_BOOL, "(default: true) print resultant goals.");
p.insert("print", CPK_BOOL, "(default: true) print resultant goals.");
#ifndef _EXTERNAL_RELEASE
p.insert(":print-proof", CPK_BOOL, "(default: false) print proof associated with each assertion.");
p.insert("print_proof", CPK_BOOL, "(default: false) print proof associated with each assertion.");
#endif
p.insert(":print-model-converter", CPK_BOOL, "(default: false) print model converter.");
p.insert(":print-benchmark", CPK_BOOL, "(default: false) display resultant goals as a SMT2 benchmark.");
p.insert("print_model_converter", CPK_BOOL, "(default: false) print model converter.");
p.insert("print_benchmark", CPK_BOOL, "(default: false) display resultant goals as a SMT2 benchmark.");
#ifndef _EXTERNAL_RELEASE
p.insert(":print-dependencies", CPK_BOOL, "(default: false) print dependencies when displaying the resultant set of goals.");
p.insert("print_dependencies", CPK_BOOL, "(default: false) print dependencies when displaying the resultant set of goals.");
#endif
exec_given_tactic_cmd::init_pdescrs(ctx, p);
}
virtual void execute(cmd_context & ctx) {
params_ref p = ps();
front_end_params2params(ctx.params(), p);
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
{
tactic & t = *(tref.get());
@ -307,7 +303,7 @@ public:
goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
assert_exprs_from(ctx, *g);
unsigned timeout = p.get_uint(":timeout", UINT_MAX);
unsigned timeout = p.get_uint("timeout", UINT_MAX);
goal_ref_buffer result_goals;
model_converter_ref mc;
@ -330,8 +326,8 @@ public:
}
}
if (!failed && p.get_bool(":print", true)) {
bool print_dependencies = p.get_bool(":print-dependencies", false);
if (!failed && p.get_bool("print", true)) {
bool print_dependencies = p.get_bool("print_dependencies", false);
ctx.regular_stream() << "(goals\n";
unsigned sz = result_goals.size();
for (unsigned i = 0; i < sz; i++) {
@ -344,12 +340,12 @@ public:
}
#ifndef _EXTERNAL_RELEASE
if (!failed && ctx.produce_proofs() && p.get_bool(":print-proof", false)) {
if (!failed && ctx.produce_proofs() && p.get_bool("print_proof", false)) {
// TODO
}
#endif
if (!failed && p.get_bool(":print-benchmark", false)) {
if (!failed && p.get_bool("print_benchmark", false)) {
unsigned num_goals = result_goals.size();
SASSERT(num_goals > 0);
if (num_goals == 1) {
@ -381,10 +377,10 @@ public:
}
}
if (!failed && mc && p.get_bool(":print-model-converter", false))
if (!failed && mc && p.get_bool("print_model_converter", false))
mc->display(ctx.regular_stream());
if (p.get_bool(":print-statistics", false))
if (p.get_bool("print_statistics", false))
display_statistics(ctx, tref.get());
}
}

26
src/front_end_params/arith_simplifier_params.cpp
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
arith_simplifier_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-05-09.
Revision History:
--*/
#include"arith_simplifier_params.h"
void arith_simplifier_params::register_params(ini_params & p) {
p.register_bool_param("ARITH_EXPAND_EQS", m_arith_expand_eqs);
p.register_bool_param("ARITH_PROCESS_ALL_EQS", m_arith_process_all_eqs);
}

26
src/front_end_params/cnf_params.cpp
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
cnf_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-23.
Revision History:
--*/
#include"cnf_params.h"
void cnf_params::register_params(ini_params & p) {
p.register_unsigned_param("CNF_FACTOR", m_cnf_factor, "the maximum number of clauses that can be created when converting a subformula");
p.register_int_param("CNF_MODE", 0, 3, reinterpret_cast<int&>(m_cnf_mode), "CNF translation mode: 0 - disabled, 1 - quantifiers in CNF, 2 - 0 + opportunistic, 3 - full");
}

56
src/front_end_params/cnf_params.h
View file

@ -1,56 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
cnf_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-23.
Revision History:
--*/
#ifndef _CNF_PARAMS_H_
#define _CNF_PARAMS_H_
#include"ini_file.h"
/**
\brief CNF translation mode. The cheapest mode is CNF_QUANT, and
the most expensive is CNF_FULL.
*/
enum cnf_mode {
CNF_DISABLED, /* CNF translator is disabled.
This mode is sufficient when using E-matching.
*/
CNF_QUANT, /* A subformula is put into CNF if it is inside of a
quantifier.
This mode is sufficient when using Superposition
Calculus.
*/
CNF_OPPORTUNISTIC, /* a subformula is also put in CNF if it is cheap. */
CNF_FULL /* Everything is put into CNF, new names are introduced
if it is too expensive. */
};
struct cnf_params {
cnf_mode m_cnf_mode;
unsigned m_cnf_factor;
cnf_params():
m_cnf_mode(CNF_DISABLED),
m_cnf_factor(4) {
}
void register_params(ini_params & p);
};
#endif /* _CNF_PARAMS_H_ */

102
src/front_end_params/front_end_params.cpp
View file

@ -1,102 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
front_end_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-05-10.
Revision History:
--*/
#include"front_end_params.h"
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,
"check that labels containing '@' are used correctly to only produce unique counter examples");
p.register_bool_param("DEFAULT_QID", m_default_qid, "create a default quantifier id based on its position, the id is used to report profiling information (see QI_PROFILE)");
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
// The non-windows memory manager does not have access to memory sizes.
p.register_unsigned_param("MEMORY_HIGH_WATERMARK", m_memory_high_watermark,
"set high watermark for memory consumption (in megabytes)");
p.register_unsigned_param("MEMORY_MAX_SIZE", m_memory_max_size,
"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););
});
// temporary hack until strategic_solver is ported to new tactic framework
PRIVATE_PARAMS({
p.register_bool_param("NLSAT", m_nlsat);
});
}
void front_end_params::open_trace_file() {
if (m_trace) {
m_trace_stream = alloc(std::fstream, m_trace_file_name.c_str(), std::ios_base::out);
}
}
void front_end_params::close_trace_file() {
if (m_trace_stream != NULL) {
std::fstream &tmp = *m_trace_stream;
m_trace_stream = NULL;
tmp << "[eof]\n";
tmp.close();
// do not delete it, this might be called from a Ctrl-C signal handler
// and there might be someone writing to it
}
}

126
src/front_end_params/front_end_params.h
View file

@ -1,126 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
front_end_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-05-10.
Revision History:
--*/
#ifndef _FRONT_END_PARAMS_H_
#define _FRONT_END_PARAMS_H_
#include"ini_file.h"
#include"ast.h"
#include"preprocessor_params.h"
#include"smt_params.h"
#include"pp_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
{
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;
unsigned m_memory_high_watermark;
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
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),
m_memory_high_watermark(0),
m_memory_max_size(0),
m_proof_mode(PGM_DISABLED),
#if defined(SMTCOMP) || defined(_EXTERNAL_RELEASE)
m_auto_config(true),
#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) {
}
void register_params(ini_params & p);
void open_trace_file();
void close_trace_file();
void copy_params(unsigned idx) {
m_param_vector->copy_params(this, idx);
}
bool has_auto_config(unsigned idx) { return m_auto_config; }
private:
front_end_params& operator=(front_end_params const& other);
};
#endif /* _FRONT_END_PARAMS_H_ */

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_ */

26
src/front_end_params/nnf_params.cpp
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
nnf_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-14.
Revision History:
--*/
#include"nnf_params.h"
void nnf_params::register_params(ini_params & p) {
p.register_unsigned_param("NNF_FACTOR", m_nnf_factor, "the maximum growth factor during NNF translation (auxiliary definitions are introduced if the threshold is reached)");
p.register_int_param("NNF_MODE", 0, 3, reinterpret_cast<int&>(m_nnf_mode), "NNF translation mode: 0 - skolem normal form, 1 - 0 + quantifiers in NNF, 2 - 1 + opportunistic, 3 - full");
p.register_bool_param("NNF_IGNORE_LABELS", m_nnf_ignore_labels, "remove/ignore labels in the input formula, this option is ignored if proofs are enabled");
p.register_bool_param("NNF_SK_HACK", m_nnf_sk_hack, "hack for VCC");
}

74
src/front_end_params/nnf_params.h
View file

@ -1,74 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
nnf_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-14.
Revision History:
--*/
#ifndef _NNF_PARAMS_H_
#define _NNF_PARAMS_H_
#include"ini_file.h"
/**
\brief NNF translation mode. The cheapest mode is NNF_SKOLEM, and
the most expensive is NNF_FULL.
*/
enum nnf_mode {
NNF_SKOLEM, /* A subformula is put into NNF only if it contains
quantifiers or labels. The result of the
transformation will be in skolem normal form.
If a formula is too expensive to be put into NNF,
then nested quantifiers and labels are renamed.
This mode is sufficient when using E-matching.
*/
NNF_QUANT, /* A subformula is put into NNF if it contains
quantifiers, labels, or is in the scope of a
quantifier. The result of the transformation will be
in skolem normal form, and the body of quantifiers
will be in NNF. If a ground formula is too expensive to
be put into NNF, then nested quantifiers and labels
are renamed.
This mode is sufficient when using Superposition
Calculus.
Remark: If the problem does not contain quantifiers,
then NNF_QUANT is identical to NNF_SKOLEM.
*/
NNF_OPPORTUNISTIC, /* Similar to NNF_QUANT, but a subformula is
also put into NNF, if it is
cheap. Otherwise, the nested quantifiers and
labels are renamed. */
NNF_FULL /* Everything is put into NNF. */
};
struct nnf_params {
nnf_mode m_nnf_mode;
unsigned m_nnf_factor;
bool m_nnf_ignore_labels;
bool m_nnf_sk_hack;
nnf_params():
m_nnf_mode(NNF_SKOLEM),
m_nnf_factor(4),
m_nnf_ignore_labels(false),
m_nnf_sk_hack(false) {
}
void register_params(ini_params & p);
};
#endif /* _NNF_PARAMS_H_ */

80
src/front_end_params/params2front_end_params.cpp
View file

@ -1,80 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
params2front_end_params.h
Abstract:
Backward compatibility utilities for parameter setting
Author:
Leonardo de Moura (leonardo) 2011-05-19.
Revision History:
--*/
#include"front_end_params.h"
#include"params.h"
/**
Update front_end_params using s.
Only the most frequently used options are updated.
This function is mainly used to allow smt::context to be used in
the new strategy framework.
*/
void params2front_end_params(params_ref const & s, front_end_params & t) {
t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl);
TRACE("qi_cost", s.display(tout); tout << "\n";);
t.m_qi_cost = s.get_str(":qi-cost", t.m_qi_cost.c_str());
t.m_mbqi = s.get_bool(":mbqi", t.m_mbqi);
t.m_mbqi_max_iterations = s.get_uint(":mbqi-max-iterations", t.m_mbqi_max_iterations);
t.m_random_seed = s.get_uint(":random-seed", t.m_random_seed);
t.m_model = s.get_bool(":produce-models", t.m_model);
if (s.get_bool(":produce-proofs", false))
t.m_proof_mode = PGM_FINE;
t.m_well_sorted_check = s.get_bool(":check-sorts", t.m_well_sorted_check);
t.m_qi_eager_threshold = s.get_double(":qi-eager-threshold", t.m_qi_eager_threshold);
t.m_qi_lazy_threshold = s.get_double(":qi-lazy-threshold", t.m_qi_lazy_threshold);
t.m_preprocess = s.get_bool(":preprocess", t.m_preprocess);
t.m_hi_div0 = s.get_bool(":hi-div0", t.m_hi_div0);
t.m_auto_config = s.get_bool(":auto-config", t.m_auto_config);
t.m_array_simplify = s.get_bool(":array-old-simplifier", t.m_array_simplify);
t.m_arith_branch_cut_ratio = s.get_uint(":arith-branch-cut-ratio", t.m_arith_branch_cut_ratio);
t.m_arith_expand_eqs = s.get_bool(":arith-expand-eqs", t.m_arith_expand_eqs);
if (s.get_bool(":arith-greatest-error-pivot", false))
t.m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
else if (s.get_bool(":arith-least-error-pivot", false))
t.m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
}
/**
\brief Copy parameters (from s) that affect the semantics of Z3 (e.g., HI_DIV0).
It also copies the model construction parameter. Thus, model construction
can be enabled at the command line.
*/
void front_end_params2params(front_end_params const & s, params_ref & t) {
if (s.m_model)
t.set_bool(":produce-models", true);
if (!s.m_hi_div0)
t.set_bool(":hi-div0", false);
}
/**
\brief Bridge for using params_ref with smt::context.
*/
void solver_front_end_params_descrs(param_descrs & r) {
r.insert(":hi-div0", CPK_BOOL, "(default: true) if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted");
r.insert(":relevancy", CPK_UINT, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant");
r.insert(":mbqi", CPK_BOOL, "model based quantifier instantiation (MBQI)");
r.insert(":mbqi-max-iterations", CPK_UINT, "maximum number of rounds of MBQI");
r.insert(":random-seed", CPK_UINT, "random seed for smt solver");
r.insert(":qi-eager-threshold", CPK_DOUBLE, "threshold for eager quantifier instantiation");
r.insert(":qi-lazy-threshold", CPK_DOUBLE, "threshold for lazy quantifier instantiation");
r.insert(":auto_config", CPK_BOOL, "use heuristics to automatically configure smt solver");
r.insert(":arith-branch-cut-ratio", CPK_UINT, "branch&bound / gomory cut ratio");
}

31
src/front_end_params/params2front_end_params.h
View file

@ -1,31 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
params2front_end_params.h
Abstract:
Backward compatibility utilities for parameter setting
Author:
Leonardo de Moura (leonardo) 2011-05-19.
Revision History:
--*/
#ifndef _PARAMS2FRONT_END_PARAMS_H_
#define _PARAMS2FRONT_END_PARAMS_H_
class params_ref;
struct front_end_params;
void params2front_end_params(params_ref const & s, front_end_params & t);
void front_end_params2params(front_end_params const & s, params_ref & t);
void solver_front_end_params_descrs(param_descrs & r);
#endif

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_ */

37
src/front_end_params/pattern_inference_params.cpp
View file

@ -1,37 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pattern_inference_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-03-24.
Revision History:
--*/
#include"pattern_inference_params.h"
void pattern_inference_params::register_params(ini_params & p) {
p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns,
"when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
p.register_bool_param("PI_BLOCK_LOOP_PATTERNS", m_pi_block_loop_patterns,
"block looping patterns during pattern inference");
p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith),
"0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");
p.register_bool_param("PI_USE_DATABASE", m_pi_use_database);
p.register_unsigned_param("PI_ARITH_WEIGHT", m_pi_arith_weight, "default weight for quantifiers where the only available pattern has nested arithmetic terms.");
p.register_unsigned_param("PI_NON_NESTED_ARITH_WEIGHT", m_pi_non_nested_arith_weight, "default weight for quantifiers where the only available pattern has non nested arithmetic terms.");
p.register_bool_param("PI_PULL_QUANTIFIERS", m_pi_pull_quantifiers, "pull nested quantifiers, if no pattern was found.");
p.register_int_param("PI_NOPAT_WEIGHT", m_pi_nopat_weight, "set weight of quantifiers without patterns, if negative the weight is not changed.");
p.register_bool_param("PI_AVOID_SKOLEMS", m_pi_avoid_skolems);
p.register_bool_param("PI_WARNINGS", m_pi_warnings, "enable/disable warning messages in the pattern inference module.");
}

109
src/front_end_params/preprocessor_params.h
View file

@ -1,109 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
preprocessor_params.h
Abstract:
Preprocess AST before adding them to the logical context
Author:
Leonardo de Moura (leonardo) 2008-01-17.
Revision History:
--*/
#ifndef _PREPROCESSOR_PARAMS_H_
#define _PREPROCESSOR_PARAMS_H_
#include"nnf_params.h"
#include"cnf_params.h"
#include"pattern_inference_params.h"
#include"bit_blaster_params.h"
#include"bv_simplifier_params.h"
enum lift_ite_kind {
LI_NONE,
LI_CONSERVATIVE,
LI_FULL
};
struct preprocessor_params : public nnf_params, public cnf_params, public pattern_inference_params,
public bit_blaster_params, public bv_simplifier_params {
lift_ite_kind m_lift_ite;
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
bool m_pull_cheap_ite_trees;
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
bool m_macro_finder;
bool m_propagate_values;
bool m_propagate_booleans;
bool m_refine_inj_axiom;
bool m_eliminate_bounds;
bool m_simplify_bit2int;
bool m_nnf_cnf;
bool m_distribute_forall;
bool m_reduce_args;
bool m_quasi_macros;
bool m_restricted_quasi_macros;
bool m_max_bv_sharing;
bool m_pre_simplifier;
bool m_nlquant_elim;
public:
preprocessor_params():
m_lift_ite(LI_NONE),
m_ng_lift_ite(LI_NONE),
m_pull_cheap_ite_trees(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),
m_eliminate_and(true),
m_macro_finder(false),
m_propagate_values(true),
m_propagate_booleans(false), // TODO << check peformance
m_refine_inj_axiom(true),
m_eliminate_bounds(false),
m_simplify_bit2int(false),
m_nnf_cnf(true),
m_distribute_forall(false),
m_reduce_args(false),
m_quasi_macros(false),
m_restricted_quasi_macros(false),
m_max_bv_sharing(true),
m_pre_simplifier(true),
m_nlquant_elim(false) {
}
void register_params(ini_params & p) {
nnf_params::register_params(p);
cnf_params::register_params(p);
pattern_inference_params::register_params(p);
bit_blaster_params::register_params(p);
bv_simplifier_params::register_params(p);
p.register_int_param("LIFT_ITE", 0, 2, reinterpret_cast<int&>(m_lift_ite), "ite term lifting: 0 - no lifting, 1 - conservative, 2 - full");
p.register_int_param("NG_LIFT_ITE", 0, 2, reinterpret_cast<int&>(m_ng_lift_ite), "ite (non-ground) term lifting: 0 - no lifting, 1 - conservative, 2 - full");
p.register_bool_param("ELIM_TERM_ITE", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor");
p.register_bool_param("ELIM_AND", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))");
p.register_bool_param("MACRO_FINDER", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros");
p.register_bool_param("PROPAGATE_VALUES", m_propagate_values, "propagate values during preprocessing step");
p.register_bool_param("PROPAGATE_BOOLEANS", m_propagate_booleans, "propagate boolean values during preprocessing step");
p.register_bool_param("PULL_CHEAP_ITE_TREES", m_pull_cheap_ite_trees);
p.register_bool_param("PULL_NESTED_QUANTIFIERS", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF");
p.register_bool_param("REFINE_INJ_AXIOM", m_refine_inj_axiom);
p.register_bool_param("ELIM_BOUNDS", m_eliminate_bounds, "cheap Fourier-Motzkin");
p.register_bool_param("BIT2INT", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions");
p.register_bool_param("DISTRIBUTE_FORALL", m_distribute_forall);
p.register_bool_param("REDUCE_ARGS", m_reduce_args);
p.register_bool_param("QUASI_MACROS", m_quasi_macros);
p.register_bool_param("RESTRICTED_QUASI_MACROS", m_restricted_quasi_macros);
p.register_bool_param("BV_MAX_SHARING", m_max_bv_sharing);
p.register_bool_param("PRE_SIMPLIFIER", m_pre_simplifier);
}
};
#endif /* _PREPROCESSOR_PARAMS_H_ */

108
src/front_end_params/smt_params.cpp
View file

@ -1,108 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-02-20.
Revision History:
--*/
#include"smt_params.h"
#include"trace.h"
void smt_params::register_params(ini_params & p) {
dyn_ack_params::register_params(p);
qi_params::register_params(p);
theory_arith_params::register_params(p);
theory_array_params::register_params(p);
theory_bv_params::register_params(p);
theory_datatype_params::register_params(p);
p.register_bool_param("CHECK_PROOF", m_check_proof);
p.register_bool_param("DISPLAY_PROOF", m_display_proof);
p.register_bool_param("DISPLAY_DOT_PROOF", m_display_dot_proof);
p.register_bool_param("DISPLAY_UNSAT_CORE", m_display_unsat_core);
p.register_bool_param("INTERNALIZER_NNF", m_internalizer_nnf);
p.register_bool_param("EQ_PROPAGATION", m_eq_propagation);
p.register_bool_param("BIN_CLAUSES", m_binary_clause_opt);
p.register_unsigned_param("RELEVANCY", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true);
p.register_bool_param("RELEVANCY_LEMMA", m_relevancy_lemma, "true if lemmas are used to propagate relevancy");
p.register_unsigned_param("RANDOM_SEED", m_random_seed, "random seed for Z3");
p.register_percentage_param("RANDOM_CASE_SPLIT_FREQ", m_random_var_freq, "frequency of random case splits");
p.register_int_param("PHASE_SELECTION", 0, 6, reinterpret_cast<int&>(m_phase_selection), "phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences");
p.register_bool_param("MINIMIZE_LEMMAS", m_minimize_lemmas, "enable/disable lemma minimization algorithm");
p.register_unsigned_param("MAX_CONFLICTS", m_max_conflicts, "maximum number of conflicts");
p.register_unsigned_param("RECENT_LEMMA_THRESHOLD", m_recent_lemmas_size);
p.register_unsigned_param("TICK", m_tick);
PRIVATE_PARAMS({
p.register_bool_param("THEORY_RESOLVE", m_theory_resolve, "Apply theory resolution to produce auxiliary conflict clauses", true);
});
p.register_int_param("RESTART_STRATEGY", 0, 4, reinterpret_cast<int&>(m_restart_strategy), "0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic");
p.register_unsigned_param("RESTART_INITIAL", m_restart_initial,
"inital restart frequency in number of conflicts, it is also the unit for the luby sequence");
p.register_double_param("RESTART_FACTOR", m_restart_factor, "when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold");
p.register_bool_param("RESTART_ADAPTIVE", m_restart_adaptive, "disable restarts based on the search 'agility'");
p.register_percentage_param("RESTART_AGILITY_THRESHOLD", m_restart_agility_threshold);
p.register_int_param("LEMMA_GC_STRATEGY", 0, 2, reinterpret_cast<int&>(m_lemma_gc_strategy), "0 - fixed, 1 - geometric, 2 - at every restart");
p.register_bool_param("LEMMA_GC_HALF", m_lemma_gc_half, "true for simple gc algorithm (delete approx. half of the clauses)");
p.register_unsigned_param("LEMMA_GC_INITIAL", m_lemma_gc_initial, "lemma initial gc frequency (in number of conflicts), used by fixed or geometric strategies");
p.register_double_param("LEMMA_GC_FACTOR", m_lemma_gc_factor, "used by geometric strategy");
p.register_unsigned_param("LEMMA_GC_NEW_OLD_RATIO", m_new_old_ratio);
p.register_unsigned_param("LEMMA_GC_NEW_CLAUSE_ACTIVITY", m_new_clause_activity);
p.register_unsigned_param("LEMMA_GC_OLD_CLAUSE_ACTIVITY", m_old_clause_activity);
p.register_unsigned_param("LEMMA_GC_NEW_CLAUSE_RELEVANCY", m_new_clause_relevancy);
p.register_unsigned_param("LEMMA_GC_OLD_CLAUSE_RELEVANCY", m_old_clause_activity);
p.register_bool_param("SIMPLIFY_CLAUSES", m_simplify_clauses);
p.register_int_param("RANDOM_INITIAL_ACTIVITY", 0, 2, reinterpret_cast<int&>(m_random_initial_activity));
PRIVATE_PARAMS({
p.register_double_param("INV_DECAY", m_inv_decay);
p.register_unsigned_param("PHASE_CACHING_ON_DURATION", m_phase_caching_on);
p.register_unsigned_param("PHASE_CACHING_OFF_DURATION", m_phase_caching_off);
});
p.register_bool_param("SMTLIB_DUMP_LEMMAS", m_smtlib_dump_lemmas);
p.register_string_param("SMTLIB_LOGIC", m_smtlib_logic, "Name used for the :logic field when generating SMT-LIB benchmarks");
p.register_bool_param("DISPLAY_FEATURES", m_display_features);
p.register_bool_param("NEW_CORE2TH_EQ", m_new_core2th_eq);
p.register_bool_param("EMATCHING", m_ematching, "E-Matching based quantifier instantiation");
p.register_bool_param("PROFILE_RES_SUB", m_profile_res_sub);
#ifndef _EXTERNAL_RELEASE
p.register_bool_param("DISPLAY_BOOL_VAR2EXPR", m_display_bool_var2expr);
p.register_bool_param("DISPLAY_LL_BOOL_VAR2EXPR", m_display_ll_bool_var2expr);
p.register_bool_param("ABORT_AFTER_PREPROC", m_abort_after_preproc, "abort after preprocessing step, this flag is only useful for debugging purposes");
p.register_bool_param("DISPLAY_INSTALLED_THEORIES", m_display_installed_theories, "display theories installed at smt::context", true);
#endif
p.register_int_param("CASE_SPLIT", 0, 5, reinterpret_cast<int&>(m_case_split_strategy), "0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal");
p.register_unsigned_param("REL_CASE_SPLIT_ORDER", 0, 2, m_rel_case_split_order, "structural (relevancy) splitting order: 0 - left-to-right (default), 1 - random, 2 - right-to-left");
p.register_bool_param("LOOKAHEAD_DISEQ", m_lookahead_diseq);
p.register_bool_param("DELAY_UNITS", m_delay_units);
p.register_unsigned_param("DELAY_UNITS_THRESHOLD", m_delay_units_threshold);
p.register_bool_param("MODEL", m_model, "enable/disable model construction", true);
p.register_bool_param("MODEL_VALIDATE", m_model_validate, "validate the model", true);
p.register_bool_param("MODEL_ON_TIMEOUT", m_model_on_timeout, "after hitting soft-timeout or memory high watermark, generate a candidate model", true);
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");
}

76
src/front_end_params/theory_arith_params.cpp
View file

@ -1,76 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
theory_arith_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-05-06.
Revision History:
--*/
#include"theory_arith_params.h"
void theory_arith_params::register_params(ini_params & p) {
#ifdef _EXTERNAL_RELEASE
p.register_int_param("ARITH_SOLVER", 0, 3, reinterpret_cast<int&>(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination");
#else
p.register_int_param("ARITH_SOLVER", 0, 4, reinterpret_cast<int&>(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination, 4 - model guided arith_solver");
#endif
p.register_bool_param("ARITH_FORCE_SIMPLEX", m_arith_auto_config_simplex, "force Z3 to use simplex solver.");
p.register_unsigned_param("ARITH_BLANDS_RULE_THRESHOLD", m_arith_blands_rule_threshold);
p.register_bool_param("ARITH_PROPAGATE_EQS", m_arith_propagate_eqs);
p.register_int_param("ARITH_PROPAGATION_MODE", 0, 2, reinterpret_cast<int&>(m_arith_bound_prop));
p.register_bool_param("ARITH_STRONGER_LEMMAS", m_arith_stronger_lemmas);
p.register_bool_param("ARITH_SKIP_BIG_COEFFS", m_arith_skip_rows_with_big_coeffs);
p.register_unsigned_param("ARITH_MAX_LEMMA_SIZE", m_arith_max_lemma_size);
p.register_unsigned_param("ARITH_SMALL_LEMMA_SIZE", m_arith_small_lemma_size);
p.register_bool_param("ARITH_REFLECT", m_arith_reflect);
p.register_bool_param("ARITH_IGNORE_INT", m_arith_ignore_int);
p.register_unsigned_param("ARITH_LAZY_PIVOTING", m_arith_lazy_pivoting_lvl);
p.register_unsigned_param("ARITH_RANDOM_SEED", m_arith_random_seed);
p.register_bool_param("ARITH_RANDOM_INITIAL_VALUE", m_arith_random_initial_value);
p.register_int_param("ARITH_RANDOM_LOWER", m_arith_random_lower);
p.register_int_param("ARITH_RANDOM_UPPER", m_arith_random_upper);
p.register_bool_param("ARITH_ADAPTIVE", m_arith_adaptive);
p.register_double_param("ARITH_ADAPTIVE_ASSERTION_THRESHOLD", m_arith_adaptive_assertion_threshold, "Delay arithmetic atoms if the num-arith-conflicts/total-conflicts < threshold");
p.register_double_param("ARITH_ADAPTIVE_PROPAGATION_THRESHOLD", m_arith_adaptive_propagation_threshold, "Disable arithmetic theory propagation if the num-arith-conflicts/total-conflicts < threshold");
p.register_bool_param("ARITH_DUMP_LEMMAS", m_arith_dump_lemmas);
p.register_bool_param("ARITH_EAGER_EQ_AXIOMS", m_arith_eager_eq_axioms);
p.register_unsigned_param("ARITH_BRANCH_CUT_RATIO", m_arith_branch_cut_ratio);
p.register_bool_param("ARITH_ADD_BINARY_BOUNDS", m_arith_add_binary_bounds);
p.register_unsigned_param("ARITH_PROP_STRATEGY", 0, 1, reinterpret_cast<unsigned&>(m_arith_propagation_strategy), "Propagation strategy: 0 - use agility measures based on ration of theory conflicts, 1 - propagate proportional to ratio of theory conflicts (default)");
p.register_bool_param("ARITH_EQ_BOUNDS", m_arith_eq_bounds);
p.register_bool_param("ARITH_LAZY_ADAPTER", m_arith_lazy_adapter);
p.register_bool_param("ARITH_GCD_TEST", m_arith_gcd_test);
p.register_bool_param("ARITH_EAGER_GCD", m_arith_eager_gcd);
p.register_bool_param("ARITH_ADAPTIVE_GCD", m_arith_adaptive_gcd);
p.register_unsigned_param("ARITH_PROPAGATION_THRESHOLD", m_arith_propagation_threshold);
p.register_bool_param("NL_ARITH", m_nl_arith, "enable/disable non linear arithmetic support. This option is ignored when ARITH_SOLVER != 2.");
p.register_bool_param("NL_ARITH_GB", m_nl_arith_gb, "enable/disable Grobner Basis computation. This option is ignored when NL_ARITH=false");
p.register_bool_param("NL_ARITH_GB_EQS", m_nl_arith_gb_eqs, "enable/disable equations in the Grobner Basis to be copied to the Simplex tableau.");
p.register_bool_param("NL_ARITH_GB_PERTURBATE", m_nl_arith_gb_perturbate, "enable/disable perturbation of the variable order in GB when searching for new polynomials.");
p.register_unsigned_param("NL_ARITH_GB_THRESHOLD", m_nl_arith_gb_threshold, "Grobner basis computation can be very expensive. This is a threshold on the number of new equalities that can be generated.");
p.register_bool_param("NL_ARITH_BRANCHING", m_nl_arith_branching, "enable/disable branching on integer variables in non linear clusters");
p.register_unsigned_param("NL_ARITH_ROUNDS", m_nl_arith_rounds, "threshold for number of (nested) final checks for non linear arithmetic.");
p.register_unsigned_param("NL_ARITH_MAX_DEGREE", m_nl_arith_max_degree, "max degree for internalizing new monomials.");
PRIVATE_PARAMS({
p.register_bool_param("ARITH_FIXNUM", m_arith_fixnum);
p.register_bool_param("ARITH_INT_ONLY", m_arith_int_only);
p.register_bool_param("ARITH_ENUM_CONST_MOD", m_arith_enum_const_mod, "Create axioms for the finite set of equalities for (mod x k) where k is a positive numeral constant");
p.register_bool_param("ARITH_INT_EQ_BRANCHING", m_arith_int_eq_branching, "Determine branch predicates based on integer equation solving");
});
p.register_bool_param("ARITH_EUCLIDEAN_SOLVER", m_arith_euclidean_solver, "");
}

55
src/front_end_params/theory_bv_params.h
View file

@ -1,55 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
theory_bv_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-06.
Revision History:
--*/
#ifndef _THEORY_BV_PARAMS_H_
#define _THEORY_BV_PARAMS_H_
#include"ini_file.h"
enum bv_solver_id {
BS_NO_BV,
BS_BLASTER
};
struct theory_bv_params {
bv_solver_id m_bv_mode;
bool m_bv_reflect;
bool m_bv_lazy_le;
bool m_bv_cc;
unsigned m_bv_blast_max_size;
bool m_bv_enable_int2bv2int;
theory_bv_params():
m_bv_mode(BS_BLASTER),
m_bv_reflect(true),
m_bv_lazy_le(false),
m_bv_cc(false),
m_bv_blast_max_size(INT_MAX),
m_bv_enable_int2bv2int(false) {}
void register_params(ini_params & p) {
p.register_int_param("BV_SOLVER", 0, 2, reinterpret_cast<int&>(m_bv_mode), "0 - no bv, 1 - simple");
p.register_unsigned_param("BV_BLAST_MAX_SIZE", m_bv_blast_max_size, "Maximal size for bit-vectors to blast");
p.register_bool_param("BV_REFLECT", m_bv_reflect);
p.register_bool_param("BV_LAZY_LE", m_bv_lazy_le);
p.register_bool_param("BV_CC", m_bv_cc, "enable congruence closure for BV operators");
p.register_bool_param("BV_ENABLE_INT2BV_PROPAGATION", m_bv_enable_int2bv2int,
"enable full (potentially expensive) propagation for int2bv and bv2int");
}
};
#endif /* _THEORY_BV_PARAMS_H_ */

10
src/math/polynomial/algebraic.pyg Normal file
View file

@ -0,0 +1,10 @@
def_module_params('algebraic',
description='real algebraic number package',
export=True,
params=(('zero_accuracy', UINT, 0, 'one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)'),
('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'),
('factor', BOOL, True, 'use polynomial factorization to simplify polynomials representing algebraic numbers'),
('factor_max_prime', UINT, 31, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step'),
('factor_num_primes', UINT, 1, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)\'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching'),
('factor_search_size', UINT, 5000, 'parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space')))

23
src/math/polynomial/algebraic_numbers.cpp
View file

@ -25,6 +25,7 @@ Notes:
#include"scoped_ptr_vector.h"
#include"mpbqi.h"
#include"timeit.h"
#include"algebraic_params.hpp"
namespace algebraic_numbers {
@ -57,12 +58,7 @@ namespace algebraic_numbers {
typedef upolynomial::factors factors;
void manager::get_param_descrs(param_descrs & r) {
r.insert(":algebraic-zero-accuracy", CPK_UINT, "(default: 0) one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k).");
r.insert(":algebraic-min-mag", CPK_UINT, "(default: 16) Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16");
r.insert(":algebraic-factor", CPK_BOOL, "(default: true) use polynomial factorization to simplify polynomials representing algebraic numbers.");
r.insert(":algebraic-factor-max-prime", CPK_UINT, "(default: 31), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step.");
r.insert(":algebraic-factor-num-primes", CPK_UINT, "(default: 1), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching.");
r.insert(":algebraic-factor-search-size", CPK_UINT, "(default: 5000), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.");
algebraic_params::collect_param_descrs(r);
}
struct manager::imp {
@ -156,13 +152,14 @@ namespace algebraic_numbers {
#endif
}
void updt_params(params_ref const & p) {
m_min_magnitude = -static_cast<int>(p.get_uint(":algebraic-min-mag", 16));
m_factor = p.get_bool(":algebraic-factor", true); // use polynomial factorization
m_factor_params.m_max_p = p.get_uint(":algebraic-factor-max-prime", 31);
m_factor_params.m_p_trials = p.get_uint(":algebraic-factor-num-primes", 1);
m_factor_params.m_max_search_size = p.get_uint(":algebraic-factor-max-search-size", 5000);
m_zero_accuracy = -static_cast<int>(p.get_uint(":algebraic-zero-accuracy", 0));
void updt_params(params_ref const & _p) {
algebraic_params p(_p);
m_min_magnitude = -static_cast<int>(p.min_mag());
m_factor = p.factor();
m_factor_params.m_max_p = p.factor_max_prime();
m_factor_params.m_p_trials = p.factor_num_primes();
m_factor_params.m_max_search_size = p.factor_search_size();
m_zero_accuracy = -static_cast<int>(p.zero_accuracy());
}
unsynch_mpq_manager & qm() {

12
src/math/polynomial/polynomial.cpp
View file

@ -50,15 +50,15 @@ namespace polynomial {
}
void factor_params::updt_params(params_ref const & p) {
m_max_p = p.get_uint(":factor-max-prime", UINT_MAX);
m_p_trials = p.get_uint(":factor-num-primes", 1);
m_max_search_size = p.get_uint(":factor-max-search-size", UINT_MAX);
m_max_p = p.get_uint("max_prime", UINT_MAX);
m_p_trials = p.get_uint("num_primes", 1);
m_max_search_size = p.get_uint("max_search_size", UINT_MAX);
}
void factor_params::get_param_descrs(param_descrs & r) {
r.insert(":factor-max-search-size", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.");
r.insert(":factor-max-prime", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step.");
r.insert(":factor-num-primes", CPK_UINT, "(default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching.");
r.insert("max_search_size", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.");
r.insert("max_prime", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step.");
r.insert("num_primes", CPK_UINT, "(default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching.");
}
typedef ptr_vector<monomial> monomial_vector;

3
src/math/polynomial/polynomial.h
View file

@ -90,6 +90,9 @@ namespace polynomial {
factor_params();
factor_params(unsigned max_p, unsigned p_trials, unsigned max_search_size);
void updt_params(params_ref const & p);
/*
REG_MODULE_PARAMS('factor', polynomial::factor_params::get_param_descrs')
*/
static void get_param_descrs(param_descrs & r);
};

32
src/math/subpaving/subpaving_t_def.h
View file

@ -474,7 +474,7 @@ void context_t<C>::del(interval & a) {
template<typename C>
void context_t<C>::updt_params(params_ref const & p) {
unsigned epsilon = p.get_uint(":epsilon", 20);
unsigned epsilon = p.get_uint("epsilon", 20);
if (epsilon != 0) {
nm().set(m_epsilon, static_cast<int>(epsilon));
nm().inv(m_epsilon);
@ -485,18 +485,18 @@ void context_t<C>::updt_params(params_ref const & p) {
m_zero_epsilon = true;
}
unsigned max_power = p.get_uint(":max-bound", 10);
unsigned max_power = p.get_uint("max_bound", 10);
nm().set(m_max_bound, 10);
nm().power(m_max_bound, max_power, m_max_bound);
nm().set(m_minus_max_bound, m_max_bound);
nm().neg(m_minus_max_bound);
m_max_depth = p.get_uint(":max-depth", 128);
m_max_nodes = p.get_uint(":max-nodes", 8192);
m_max_depth = p.get_uint("max_depth", 128);
m_max_nodes = p.get_uint("max_nodes", 8192);
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
unsigned prec = p.get_uint(":nth-root-precision", 8192);
unsigned prec = p.get_uint("nth_root_precision", 8192);
if (prec == 0)
prec = 1;
nm().set(m_nth_root_prec, static_cast<int>(prec));
@ -505,20 +505,20 @@ void context_t<C>::updt_params(params_ref const & p) {
template<typename C>
void context_t<C>::collect_param_descrs(param_descrs & d) {
d.insert(":max-nodes", CPK_UINT, "(default: 8192) maximum number of nodes in the subpaving tree.");
d.insert(":max-depth", CPK_UINT, "(default: 128) maximum depth of the subpaving tree.");
d.insert(":epsilon", CPK_UINT, "(default: 20) value k s.t. a new lower (upper) bound for x is propagated only new-lower(x) > lower(k) + 1/k * max(min(upper(x) - lower(x), |lower|), 1) (new-upper(x) < upper(x) - 1/k * max(min(upper(x) - lower(x), |lower|), 1)). If k = 0, then this restriction is ignored.");
d.insert(":max-bound", CPK_UINT, "(default 10) value k s.t. a new upper (lower) bound for x is propagated only if upper(x) > -10^k or lower(x) = -oo (lower(x) < 10^k or upper(x) = oo)");
d.insert(":nth-root-precision", CPK_UINT, "(default 8192) value k s.t. 1/k is the precision for computing the nth root in the subpaving module.");
d.insert("max_nodes", CPK_UINT, "(default: 8192) maximum number of nodes in the subpaving tree.");
d.insert("max_depth", CPK_UINT, "(default: 128) maximum depth of the subpaving tree.");
d.insert("epsilon", CPK_UINT, "(default: 20) value k s.t. a new lower (upper) bound for x is propagated only new-lower(x) > lower(k) + 1/k * max(min(upper(x) - lower(x), |lower|), 1) (new-upper(x) < upper(x) - 1/k * max(min(upper(x) - lower(x), |lower|), 1)). If k = 0, then this restriction is ignored.");
d.insert("max_bound", CPK_UINT, "(default 10) value k s.t. a new upper (lower) bound for x is propagated only if upper(x) > -10^k or lower(x) = -oo (lower(x) < 10^k or upper(x) = oo)");
d.insert("nth_root_precision", CPK_UINT, "(default 8192) value k s.t. 1/k is the precision for computing the nth root in the subpaving module.");
}
template<typename C>
void context_t<C>::display_params(std::ostream & out) const {
out << ":max-nodes " << m_max_nodes << "\n";
out << ":max-depth " << m_max_depth << "\n";
out << ":epsilon " << nm().to_rational_string(m_epsilon) << "\n";
out << ":max-bound " << nm().to_rational_string(m_max_bound) << "\n";
out << ":max-memory " << m_max_memory << "\n";
out << "max_nodes " << m_max_nodes << "\n";
out << "max_depth " << m_max_depth << "\n";
out << "epsilon " << nm().to_rational_string(m_epsilon) << "\n";
out << "max_bound " << nm().to_rational_string(m_max_bound) << "\n";
out << "max_memory " << m_max_memory << "\n";
}
template<typename C>

24
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -81,14 +81,14 @@ class subpaving_tactic : public tactic {
void collect_param_descrs(param_descrs & r) {
m_ctx->collect_param_descrs(r);
// #ifndef _EXTERNAL_RELEASE
r.insert(":numeral", CPK_SYMBOL, "(default: mpq) options: mpq, mpf, hwf, mpff, mpfx.");
r.insert(":print-nodes", CPK_BOOL, "(default: false) display subpaving tree leaves.");
r.insert("numeral", CPK_SYMBOL, "(default: mpq) options: mpq, mpf, hwf, mpff, mpfx.");
r.insert("print_nodes", CPK_BOOL, "(default: false) display subpaving tree leaves.");
// #endif
}
void updt_params(params_ref const & p) {
m_display = p.get_bool(":print-nodes", false);
symbol engine = p.get_sym(":numeral", symbol("mpq"));
m_display = p.get_bool("print_nodes", false);
symbol engine = p.get_sym("numeral", symbol("mpq"));
engine_kind new_kind;
if (engine == "mpq")
new_kind = MPQ;
@ -293,16 +293,16 @@ tactic * mk_subpaving_tactic_core(ast_manager & m, params_ref const & p) {
tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool(":arith-lhs", true);
simp_p.set_bool(":expand-power", true);
simp_p.set_uint(":max-power", UINT_MAX);
simp_p.set_bool(":som", true);
simp_p.set_bool(":eq2ineq", true);
simp_p.set_bool(":elim-and", true);
simp_p.set_bool(":blast-distinct", true);
simp_p.set_bool("arith_lhs", true);
simp_p.set_bool("expand_power", true);
simp_p.set_uint("max_power", UINT_MAX);
simp_p.set_bool("som", true);
simp_p.set_bool("eq2ineq", true);
simp_p.set_bool("elim_and", true);
simp_p.set_bool("blast_distinct", true);
params_ref simp2_p = p;
simp2_p.set_bool(":mul-to-power", true);
simp2_p.set_bool("mul_to_power", true);
return and_then(using_params(mk_simplify_tactic(m, p),
simp_p),

12
src/model/model_evaluator.cpp
View file

@ -60,10 +60,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_max_steps = p.get_uint(":max-steps", UINT_MAX);
m_model_completion = p.get_bool(":model-completion", false);
m_cache = p.get_bool(":cache", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
m_model_completion = p.get_bool("model_completion", false);
m_cache = p.get_bool("cache", true);
}
ast_manager & m() const { return m_model.get_manager(); }
@ -232,8 +232,8 @@ void model_evaluator::updt_params(params_ref const & p) {
void model_evaluator::get_param_descrs(param_descrs & r) {
insert_max_memory(r);
insert_max_steps(r);
r.insert(":model-completion", CPK_BOOL, "(default: false) assigns an interpretation to symbols that are not intepreted by the model.");
r.insert(":cache", CPK_BOOL, "(default: true) cache intermediate results.");
r.insert("model_completion", CPK_BOOL, "(default: false) assigns an interpretation to symbols that are not intepreted by the model.");
r.insert("cache", CPK_BOOL, "(default: true) cache intermediate results.");
}
void model_evaluator::set_model_completion(bool f) {

8
src/model/model_params.pyg Normal file
View file

@ -0,0 +1,8 @@
def_module_params('model',
export=True,
params=(('partial', BOOL, False, 'enable/disable partial function interpretations'),
('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model')))

3
src/model/model_pp.cpp
View file

@ -85,8 +85,7 @@ static void display_functions(std::ostream & out, model_core const & md) {
if (fi->is_partial())
out << " #unspecified";
else {
pp_params const & params = get_pp_default_params();
out << " " << mk_ismt2_pp(fi->get_else(), m, params, 5, arity, "x");
out << " " << mk_ismt2_pp(fi->get_else(), m, params_ref(), 5, arity, "x");
}
for (unsigned j = 0; j < num_entries; j++)
out << ")";

4
src/model/model_smt2_pp.cpp
View file

@ -128,7 +128,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
format_ref f_card(fm(m));
f_card = mk_indent(m, indent, mk_seq1<format**, f2f>(m, f_args, f_args+2, f2f(), "forall"));
pp_indent(out, indent);
pp(out, f_card, m, get_pp_default_params());
pp(out, f_card, m);
out << "\n";
pp_indent(out, indent);
out << ";; -----------\n";
@ -284,7 +284,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
body.get(),
mk_string(m, ")")))));
pp_indent(out, indent);
pp(out, def.get(), m, get_pp_default_params());
pp(out, def.get(), m);
out << "\n";
}
}

Some files were not shown because too many files have changed in this diff Show more