mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

follow logic annotation/enable diff logic when configured

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-07 11:52:14 -07:00
parent 18b491eee0
commit c1580fb85a
11 changed files with 71 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_model.cpp
View file

@ -60,6 +60,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0);
}
@ -263,6 +264,7 @@ extern "C" {
RESET_ERROR_CODE();
CHECK_NON_NULL(f, 0);
expr * e = to_func_interp_ref(f)->get_else();
mk_c(c)->save_ast_trail(e);
RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(0);
}
@ -301,6 +303,7 @@ extern "C" {
LOG_Z3_func_entry_get_value(c, e);
RESET_ERROR_CODE();
expr * v = to_func_entry_ref(e)->get_result();
mk_c(c)->save_ast_trail(v);
RETURN_Z3(of_expr(v));
Z3_CATCH_RETURN(0);
}

1
src/cmd_context/cmd_context.cpp
View file

@ -362,6 +362,7 @@ void cmd_context::set_opt(opt_wrapper* opt) {
for (unsigned i = 0; i < m_scopes.size(); ++i) {
m_opt->push();
}
m_opt->set_logic(m_logic);
}
void cmd_context::global_params_updated() {

1
src/cmd_context/cmd_context.h
View file

@ -123,6 +123,7 @@ public:
virtual void set_hard_constraints(ptr_vector<expr> & hard) = 0;
virtual void display_assignment(std::ostream& out) = 0;
virtual bool is_pareto() = 0;
virtual void set_logic(symbol const& s) = 0;
};
class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {

29
src/muz/pdr/pdr_context.cpp
View file

@ -49,6 +49,7 @@ Notes:
#include "scoped_proof.h"
#include "blast_term_ite_tactic.h"
#include "model_implicant.h"
#include "expr_safe_replace.h"
namespace pdr {
@ -1073,10 +1074,7 @@ namespace pdr {
predicates.pop_back();
for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
dctx.get_rewriter()(tmp);
if (!m.is_true(tmp)) {
constraints.push_back(tmp);
}
constraints.push_back(tmp);
}
for (unsigned i = 0; i < constraints.size(); ++i) {
max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
@ -1099,7 +1097,27 @@ namespace pdr {
children.append(n->children());
}
return pm.mk_and(constraints);
expr_safe_replace repl(m);
for (unsigned i = 0; i < constraints.size(); ++i) {
expr* e = constraints[i].get(), *e1, *e2;
if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) {
repl.insert(e1, e2);
}
else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) {
repl.insert(e2, e1);
}
}
expr_ref_vector result(m);
for (unsigned i = 0; i < constraints.size(); ++i) {
expr_ref tmp(m);
tmp = constraints[i].get();
repl(tmp);
dctx.get_rewriter()(tmp);
if (!m.is_true(tmp)) {
result.push_back(tmp);
}
}
return pm.mk_and(result);
}
proof_ref model_search::get_proof_trace(context const& ctx) {
@ -1232,6 +1250,7 @@ namespace pdr {
remove_node(*m_root, false);
dealloc(m_root);
m_root = 0;
m_cache.reset();
}
}

4
src/opt/opt_context.cpp
View file

@ -284,6 +284,7 @@ namespace opt {
lbool context::execute_lex() {
lbool r = l_true;
IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
bool is_last = i + 1 == m_objectives.size();
r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last);
@ -435,7 +436,8 @@ namespace opt {
void context::init_solver() {
#pragma omp critical (opt_context)
{
m_opt_solver = alloc(opt_solver, m, m_params, m_fm, symbol());
m_opt_solver = alloc(opt_solver, m, m_params, m_fm);
m_opt_solver->set_logic(m_logic);
m_solver = m_opt_solver.get();
}
}

2
src/opt/opt_context.h
View file

@ -128,6 +128,7 @@ namespace opt {
bool m_enable_sat;
bool m_enable_sls;
symbol m_maxsat_engine;
symbol m_logic;
public:
context(ast_manager& m);
virtual ~context();
@ -153,6 +154,7 @@ namespace opt {
virtual void display_assignment(std::ostream& out);
virtual bool is_pareto() { return m_pareto.get() != 0; }
virtual void set_logic(symbol const& s) { m_logic = s; }
void display(std::ostream& out);
static void collect_param_descrs(param_descrs & r);

22
src/opt/opt_solver.cpp
View file

@ -36,17 +36,14 @@ Notes:
namespace opt {
opt_solver::opt_solver(ast_manager & mgr, params_ref const & p,
filter_model_converter& fm, symbol const & l):
filter_model_converter& fm):
solver_na2as(mgr),
m_params(p),
m_context(mgr, m_params),
m(mgr),
m_dump_benchmarks(false),
m_fm(fm) {
m_logic = l;
if (m_logic != symbol::null) {
m_context.set_logic(m_logic);
}
m_fm(fm),
m_first(true) {
m_params.updt_params(p);
m_params.m_relevancy_lvl = 0;
}
@ -83,6 +80,10 @@ namespace opt {
m_context.pop(n);
}
void opt_solver::set_logic(symbol const& logic) {
m_context.set_logic(logic);
}
smt::theory_opt& opt_solver::get_optimizer() {
smt::context& ctx = m_context.get_context();
smt::theory_id arith_id = m_context.m().get_family_id("arith");
@ -143,7 +144,14 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(created benchmark: " << file_name.str() << "...";
verbose_stream().flush(););
}
lbool r = m_context.check(num_assumptions, assumptions);
lbool r;
if (m_first && num_assumptions == 0 && m_context.get_scope_level() == 0) {
r = m_context.setup_and_check();
}
else {
r = m_context.check(num_assumptions, assumptions);
}
m_first = false;
if (dump_benchmarks()) {
w.stop();
IF_VERBOSE(1, verbose_stream() << ".. " << r << " " << std::fixed << w.get_seconds() << ")\n";);

6
src/opt/opt_solver.h
View file

@ -51,8 +51,9 @@ namespace opt {
bool m_dump_benchmarks;
static unsigned m_dump_count;
statistics m_stats;
bool m_first;
public:
opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm, symbol const & l);
opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
virtual ~opt_solver();
virtual void updt_params(params_ref & p);
@ -61,7 +62,7 @@ namespace opt {
virtual void assert_expr(expr * t);
virtual void push_core();
virtual void pop_core(unsigned n);
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
virtual void get_unsat_core(ptr_vector<expr> & r);
virtual void get_model(model_ref & m);
virtual proof * get_proof();
@ -72,6 +73,7 @@ namespace opt {
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
virtual void display(std::ostream & out) const;
void set_logic(symbol const& logic);
smt::theory_var add_objective(app* term);
void reset_objectives();

1
src/opt/optsmt.cpp
View file

@ -235,7 +235,6 @@ namespace opt {
}
lbool optsmt::lex(unsigned obj_index) {
IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
TRACE("opt", tout << "optsmt:lex\n";);
solver::scoped_push _push(*m_s);
SASSERT(obj_index < m_vars.size());

10
src/smt/smt_setup.cpp
View file

@ -301,7 +301,7 @@ namespace smt {
}
void setup::setup_QF_IDL() {
TRACE("setup", tout << "setup_QF_IDL(st)\n";);
TRACE("setup", tout << "setup_QF_IDL()\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_reflect = false;
@ -351,16 +351,15 @@ namespace smt {
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
TRACE("setup", tout << "using dense diff logic...\n";);
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE;
#if 0
m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));
#else
if (st.m_arith_k_sum < rational(INT_MAX / 8))
m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params));
#endif
}
else if (!m_params.m_arith_auto_config_simplex && !is_dense(st)) {
m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));
}
else {
// if (st.m_arith_k_sum < rational(INT_MAX / 8)) {
// TRACE("setup", tout << "using small integer simplex...\n";);
@ -379,6 +378,7 @@ namespace smt {
m_params.m_arith_reflect = false;
m_params.m_nnf_cnf = false;
m_params.m_arith_eq_bounds = true;
m_params.m_arith_expand_eqs = true;
m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5;

22
src/smt/theory_diff_logic_def.h
View file

@ -81,8 +81,10 @@ template<typename Ext>
bool theory_diff_logic<Ext>::internalize_term(app * term) {
bool result = null_theory_var != mk_term(term);
CTRACE("arith", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
TRACE("non_diff_logic", tout << "Terms may not be internalized\n";);
found_non_diff_logic_expr(term);
if (!result) {
TRACE("non_diff_logic", tout << "Terms may not be internalized\n";);
found_non_diff_logic_expr(term);
}
return result;
}
@ -273,6 +275,8 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
template<typename Ext>
void theory_diff_logic<Ext>::internalize_eq_eh(app * atom, bool_var v) {
context & ctx = get_context();
ast_manager& m = get_manager();
TRACE("arith", tout << mk_pp(atom, m) << "\n";);
app * lhs = to_app(atom->get_arg(0));
app * rhs = to_app(atom->get_arg(1));
app * s;
@ -1070,13 +1074,13 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
ast_manager& m = get_manager();
objective_term const& objective = m_objectives[v];
IF_VERBOSE(1,
for (unsigned i = 0; i < objective.size(); ++i) {
verbose_stream() << "Coefficient " << objective[i].second
<< " of theory_var " << objective[i].first << "\n";
}
verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";);
TRACE("arith",
for (unsigned i = 0; i < objective.size(); ++i) {
tout << "Coefficient " << objective[i].second
<< " of theory_var " << objective[i].first << "\n";
}
tout << "Free coefficient " << m_objective_consts[v] << "\n";
);
unsigned num_nodes = m_graph.get_num_nodes();
unsigned num_edges = m_graph.get_num_edges();
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();