mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05: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-11 20:49:49 -08:00
commit 89ddb5eac4
105 changed files with 4992 additions and 2748 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/smt/mam.cpp
View file

@ -142,6 +142,14 @@ namespace smt {
}
};
struct initn : public instruction {
// We need that because starting at Z3 3.0, some associative
// operators (e.g., + and *) are represented using n-ary
// applications.
// We do not need the extra field for INIT1, ..., INIT6.
unsigned m_num_args;
};
struct compare : public instruction {
unsigned m_reg1;
unsigned m_reg2;
@ -608,7 +616,18 @@ namespace smt {
instruction * mk_init(unsigned n) {
SASSERT(n >= 1);
opcode op = n <= 6 ? static_cast<opcode>(INIT1 + n - 1) : INITN;
return mk_instr<instruction>(op, sizeof(instruction));
if (op == INITN) {
// We store the actual number of arguments for INITN.
// Starting at Z3 3.0, some associative operators
// (e.g., + and *) are represented using n-ary
// applications.
initn * r = mk_instr<initn>(op, sizeof(initn));
r->m_num_args = n;
return r;
}
else {
return mk_instr<instruction>(op, sizeof(instruction));
}
}
public:
@ -2345,6 +2364,8 @@ namespace smt {
case INITN:
m_app = m_registers[0];
m_num_args = m_app->get_num_args();
if (m_num_args != static_cast<const initn *>(m_pc)->m_num_args)
goto backtrack;
for (unsigned i = 0; i < m_num_args; i++)
m_registers[i+1] = m_app->get_arg(i);
m_pc = m_pc->m_next;
@ -3982,3 +4003,8 @@ namespace smt {
}
};
#ifdef Z3DEBUG
void pp(smt::code_tree * c) {
c->display(std::cout);
}
#endif

3
src/smt/params/preprocessor_params.cpp
View file

@ -21,7 +21,8 @@ Revision History:
void preprocessor_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_macro_finder = p.macro_finder();
m_macro_finder = p.macro_finder();
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
}
void preprocessor_params::updt_params(params_ref const & p) {

2
src/smt/params/smt_params.cpp
View file

@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
m_soft_timeout = p.soft_timeout();
if (_p.get_bool("arith.greatest_error_pivot", false))
m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
else if (_p.get_bool("arith.least_error_pivot", false))
@ -48,7 +49,6 @@ void smt_params::updt_params(params_ref const & p) {
void smt_params::updt_params(context_params const & p) {
m_auto_config = p.m_auto_config;
m_soft_timeout = p.m_timeout;
m_model = p.m_model;
m_model_validate = p.m_model_validate;
}

4
src/smt/params/smt_params_helper.pyg
View file

@ -7,12 +7,14 @@ def_module_params(module_name='smt',
('relevancy', UINT, 2, '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'),
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
('phase_selection', UINT, 4, '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'),
('phase_selection', UINT, 3, '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'),
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
('case_split', UINT, 1, '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'),
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),

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

@ -155,7 +155,7 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(fi.m().get_basic_family_id()));
for (unsigned k = 0; k < fi.num_entries(); k++) {
func_entry const * curr = fi.get_entry(k);
SASSERT(!curr->eq_args(fi.get_arity(), args));
SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args));
if (!actuals_are_values || !curr->args_are_values()) {
expr_ref_buffer eqs(fi.m());
unsigned i = fi.get_arity();

32
src/smt/smt_implied_equalities.cpp
View file

@ -21,23 +21,21 @@ Revision History:
#include "smt_implied_equalities.h"
#include "union_find.h"
#include "cmd_context.h"
#include "parametric_cmd.h"
#include "ast_pp.h"
#include "arith_decl_plugin.h"
#include "datatype_decl_plugin.h"
#include "array_decl_plugin.h"
#include "uint_set.h"
#include "model_v2_pp.h"
#include "smt_value_sort.h"
#include "model_smt2_pp.h"
#include "stopwatch.h"
#include "model.h"
#include "solver.h"
namespace smt {
class get_implied_equalities_impl {
ast_manager& m;
smt::kernel& m_solver;
solver& m_solver;
union_find_default_ctx m_df;
union_find<union_find_default_ctx> m_uf;
array_util m_array_util;
@ -98,7 +96,7 @@ namespace smt {
++m_stats_calls;
m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(s, t)));
bool is_eq = l_false == m_solver.check();
bool is_eq = l_false == m_solver.check_sat(0,0);
m_solver.pop(1);
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";);
if (is_eq) {
@ -125,7 +123,7 @@ namespace smt {
m_stats_timer.start();
m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(s, t)));
bool is_eq = l_false == m_solver.check();
bool is_eq = l_false == m_solver.check_sat(0,0);
m_solver.pop(1);
m_stats_timer.stop();
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";);
@ -168,7 +166,7 @@ namespace smt {
terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr());
}
assert_relevant(terms);
lbool is_sat = m_solver.check();
lbool is_sat = m_solver.check_sat(0,0);
model_ref model1;
m_solver.get_model(model1);
SASSERT(model1.get());
@ -218,7 +216,7 @@ namespace smt {
expr* s = terms[vec[j]].term;
m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(t, s)));
lbool is_sat = m_solver.check();
lbool is_sat = m_solver.check_sat(0,0);
m_solver.pop(1);
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << is_sat << "\n";);
if (is_sat == l_false) {
@ -237,7 +235,7 @@ namespace smt {
if (!non_values.empty()) {
TRACE("get_implied_equalities", model_v2_pp(tout, *model, true););
TRACE("get_implied_equalities", model_smt2_pp(tout, m, *model, 0););
get_implied_equalities_filter_basic(non_values, terms);
//get_implied_equalities_basic(terms);
}
@ -321,7 +319,7 @@ namespace smt {
public:
get_implied_equalities_impl(smt::kernel& s) : m(s.m()), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {}
get_implied_equalities_impl(ast_manager& m, solver& s) : m(m), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {}
lbool operator()(unsigned num_terms, expr* const* terms, unsigned* class_ids) {
params_ref p;
@ -338,7 +336,7 @@ namespace smt {
m_solver.push();
assert_relevant(num_terms, terms);
lbool is_sat = m_solver.check();
lbool is_sat = m_solver.check_sat(0,0);
if (is_sat != l_false) {
model_ref model;
@ -374,8 +372,8 @@ namespace smt {
stopwatch get_implied_equalities_impl::s_timer;
stopwatch get_implied_equalities_impl::s_stats_val_eq_timer;
lbool implied_equalities(smt::kernel& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) {
get_implied_equalities_impl gi(solver);
lbool implied_equalities(ast_manager& m, solver& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) {
get_implied_equalities_impl gi(m, solver);
return gi(num_terms, terms, class_ids);
}
};
@ -552,7 +550,7 @@ namespace smt {
m_solver.assert_expr(m.mk_implies(eq_lit, eq));
}
m_solver.assert_expr(m.mk_not(m.mk_and(eqs.size(), eqs.c_ptr())));
lbool is_sat = m_solver.check();
lbool is_sat = m_solver.check_sat(0,0);
switch(is_sat) {
case l_false:
for (unsigned i = 0; i + 1 < terms.size(); ++i) {

7
src/smt/smt_implied_equalities.h
View file

@ -23,13 +23,16 @@ Revision History:
#ifndef __SMT_IMPLIED_EQUALITIES_H__
#define __SMT_IMPLIED_EQUALITIES_H__
#include"smt_kernel.h"
#include"smt_solver.h"
#include"lbool.h"
#include"ast.h"
namespace smt {
lbool implied_equalities(
kernel & solver,
ast_manager & m,
solver & solver,
unsigned num_terms, expr* const* terms,
unsigned* class_ids);

2
src/smt/smt_internalizer.cpp
View file

@ -907,7 +907,7 @@ namespace smt {
}
enode * e = enode::mk(m_manager, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
if (n->get_num_args() == 0 && m_manager.is_value(n))
if (n->get_num_args() == 0 && m_manager.is_unique_value(n))
e->mark_as_interpreted();
TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);

138
src/smt/smt_solver.cpp
View file

@ -25,166 +25,114 @@ namespace smt {
class solver : public solver_na2as {
smt_params m_params;
smt::kernel * m_context;
smt::kernel m_context;
progress_callback * m_callback;
symbol m_logic;
public:
solver():m_context(0), m_callback(0) {}
solver(ast_manager & m, params_ref const & p, symbol const & l):
solver_na2as(m),
m_params(p),
m_context(m, m_params) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
}
virtual ~solver() {
if (m_context != 0)
dealloc(m_context);
}
virtual void updt_params(params_ref const & p) {
m_params.updt_params(p);
if (m_context == 0)
return;
m_context->updt_params(p);
m_context.updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
if (m_context == 0) {
ast_manager m;
reg_decl_plugins(m);
smt::kernel s(m, m_params);
s.collect_param_descrs(r);
}
else {
m_context->collect_param_descrs(r);
}
}
virtual void init_core(ast_manager & m, symbol const & logic) {
reset();
// We can throw exceptions when creating a smt::kernel object
// So, we should create the smt::kernel outside of the criticial section
// block. OMP does not allow exceptions to cross critical section boundaries.
smt::kernel * new_kernel = alloc(smt::kernel, m, m_params);
#pragma omp critical (solver)
{
m_context = new_kernel;
if (m_callback)
m_context->set_progress_callback(m_callback);
}
if (logic != symbol::null)
m_context->set_logic(logic);
m_context.collect_param_descrs(r);
}
virtual void collect_statistics(statistics & st) const {
if (m_context == 0) {
return;
}
else {
m_context->collect_statistics(st);
}
}
virtual void reset_core() {
if (m_context != 0) {
#pragma omp critical (solver)
{
dealloc(m_context);
m_context = 0;
}
}
}
// An exception may be thrown when creating a smt::kernel.
// So, there is no guarantee that m_context != 0 when
// using smt_solver from the SMT 2.0 command line frontend.
void check_context() const {
if (m_context == 0)
throw default_exception("Z3 failed to create solver, check previous error messages");
m_context.collect_statistics(st);
}
virtual void assert_expr(expr * t) {
check_context();
m_context->assert_expr(t);
m_context.assert_expr(t);
}
virtual void push_core() {
check_context();
m_context->push();
m_context.push();
}
virtual void pop_core(unsigned n) {
check_context();
m_context->pop(n);
m_context.pop(n);
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
check_context();
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
return m_context->check(num_assumptions, assumptions);
return m_context.check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
check_context();
unsigned sz = m_context->get_unsat_core_size();
unsigned sz = m_context.get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(m_context->get_unsat_core_expr(i));
r.push_back(m_context.get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) {
check_context();
m_context->get_model(m);
m_context.get_model(m);
}
virtual proof * get_proof() {
check_context();
return m_context->get_proof();
return m_context.get_proof();
}
virtual std::string reason_unknown() const {
check_context();
return m_context->last_failure_as_string();
return m_context.last_failure_as_string();
}
virtual void get_labels(svector<symbol> & r) {
check_context();
buffer<symbol> tmp;
m_context->get_relevant_labels(0, tmp);
m_context.get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());
}
virtual void set_cancel(bool f) {
#pragma omp critical (solver)
{
if (m_context)
m_context->set_cancel(f);
}
m_context.set_cancel(f);
}
virtual void set_progress_callback(progress_callback * callback) {
m_callback = callback;
if (m_context)
m_context->set_progress_callback(callback);
m_context.set_progress_callback(callback);
}
virtual unsigned get_num_assertions() const {
if (m_context)
return m_context->size();
else
return 0;
return m_context.size();
}
virtual expr * get_assertion(unsigned idx) const {
SASSERT(m_context);
SASSERT(idx < get_num_assertions());
return m_context->get_formulas()[idx];
return m_context.get_formulas()[idx];
}
virtual void display(std::ostream & out) const {
if (m_context)
m_context->display(out);
else
out << "(solver)";
m_context.display(out);
}
};
};
solver * mk_smt_solver() {
return alloc(smt::solver);
solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic) {
return alloc(smt::solver, m, p, logic);
}
class smt_solver_factory : public solver_factory {
public:
virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) {
return mk_smt_solver(m, p, logic);
}
};
solver_factory * mk_smt_solver_factory() {
return alloc(smt_solver_factory);
}

9
src/smt/smt_solver.h
View file

@ -21,8 +21,13 @@ Notes:
#ifndef _SMT_SOLVER_H_
#define _SMT_SOLVER_H_
class solver;
#include"ast.h"
#include"params.h"
solver * mk_smt_solver();
class solver;
class solver_factory;
solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic);
solver_factory * mk_smt_solver_factory();
#endif

1
src/smt/tactic/smt_tactic.cpp
View file

@ -139,6 +139,7 @@ public:
ast_manager & m = in->m();
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
<< " PREPROCESS: " << fparams().m_preprocess << "\n";
tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n";
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
tout << "params_ref: " << m_params_ref << "\n";);
TRACE("smt_tactic_detail", in->display(tout););

2
src/smt/user_plugin/user_decl_plugin.h
View file

@ -49,6 +49,8 @@ public:
virtual bool is_value(app*) const;
virtual bool is_unique_value(app * a) const { return is_value(a); }
bool is_value(func_decl *) const;
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);