mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 12:25:51 +00:00
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
e47eea2c61
commit
ed7e0e11a8
8 changed files with 142 additions and 55 deletions
|
|
@ -355,6 +355,10 @@ extern "C" {
|
|||
init_solver(c, s);
|
||||
Z3_stats_ref * st = alloc(Z3_stats_ref);
|
||||
to_solver_ref(s)->collect_statistics(st->m_stats);
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
st->m_stats.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
|
||||
st->m_stats.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
|
||||
mk_c(c)->save_object(st);
|
||||
Z3_stats r = of_stats(st);
|
||||
RETURN_Z3(r);
|
||||
|
|
|
|||
|
|
@ -945,6 +945,10 @@ namespace datalog {
|
|||
if (m_engine) {
|
||||
m_engine->collect_statistics(st);
|
||||
}
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
st.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
|
||||
st.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -323,12 +323,8 @@ private:
|
|||
|
||||
void display_statistics(cmd_context& ctx) {
|
||||
statistics stats;
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
stats.update("time", ctx.get_seconds());
|
||||
stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
|
||||
stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
|
||||
get_opt(ctx).collect_statistics(stats);
|
||||
stats.update("time", ctx.get_seconds());
|
||||
stats.display_smt2(ctx.regular_stream());
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -1179,6 +1179,10 @@ namespace opt {
|
|||
for (; it != end; ++it) {
|
||||
it->m_value->collect_statistics(stats);
|
||||
}
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
|
||||
stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
|
||||
}
|
||||
|
||||
void context::collect_param_descrs(param_descrs & r) {
|
||||
|
|
|
|||
131
src/qe/qsat.cpp
131
src/qe/qsat.cpp
|
|
@ -21,10 +21,12 @@ Revision History:
|
|||
#include "qsat.h"
|
||||
#include "smt_kernel.h"
|
||||
#include "qe_mbp.h"
|
||||
#include "smt_params.h"
|
||||
#include "ast_util.h"
|
||||
|
||||
namespace qe;
|
||||
using namespace qe;
|
||||
|
||||
sturct qdef_t {
|
||||
struct qdef_t {
|
||||
expr_ref m_pred;
|
||||
expr_ref m_expr;
|
||||
expr_ref_vector m_vars;
|
||||
|
|
@ -41,15 +43,25 @@ typedef vector<qdef_t> qdefs_t;
|
|||
struct pdef_t {
|
||||
expr_ref m_pred;
|
||||
expr_ref m_atom;
|
||||
pdef_t(expr_ref& p, expr_ref& a):
|
||||
m_pred(p),
|
||||
m_atom(a)
|
||||
pdef_t(expr_ref& p, expr* a):
|
||||
m_pred(p),
|
||||
m_atom(a, p.get_manager())
|
||||
{}
|
||||
};
|
||||
|
||||
class qsat::impl {
|
||||
ast_manager& m;
|
||||
mbp mbp;
|
||||
ast_manager& m;
|
||||
qe::mbp mbp;
|
||||
smt_params m_smtp;
|
||||
smt::kernel m_kernel;
|
||||
expr_ref m_fml_pred; // predicate that encodes top-level formula
|
||||
expr_ref_vector m_atoms; // predicates that encode atomic subformulas
|
||||
|
||||
|
||||
lbool check_sat() {
|
||||
// TBD main procedure goes here.
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate.
|
||||
|
|
@ -63,11 +75,12 @@ class qsat::impl {
|
|||
propositional variables, and adding definitions for each propositional formula on the side.
|
||||
Assumption is that the formula is quantifier-free.
|
||||
*/
|
||||
void mk_abstract(expr_ref_vector& fmls, vector<pdef_t>& pdefs) {
|
||||
expr_ref_vector todo(fmls), trail(m);
|
||||
void mk_abstract(expr_ref& fml, vector<pdef_t>& pdefs) {
|
||||
expr_ref_vector todo(m), trail(m);
|
||||
obj_map<expr,expr*> cache;
|
||||
ptr_vector<expr> args;
|
||||
expr_ref r(m);
|
||||
todo.push_back(fml);
|
||||
while (!todo.empty()) {
|
||||
expr* e = todo.back();
|
||||
if (cache.contains(e)) {
|
||||
|
|
@ -87,47 +100,114 @@ class qsat::impl {
|
|||
else {
|
||||
todo.push_back(f);
|
||||
}
|
||||
}
|
||||
}
|
||||
if (args.size() == sz) {
|
||||
r = m.mk_app(a->get_decl(), sz, args.c_ptr());
|
||||
cache.insert(e, r);
|
||||
trail.push_back(r);
|
||||
todo.pop_back(e);
|
||||
todo.pop_back();
|
||||
}
|
||||
}
|
||||
else if (is_uninterpreted_const(a)) {
|
||||
else if (is_uninterp_const(a)) {
|
||||
cache.insert(e, e);
|
||||
}
|
||||
else {
|
||||
// TBD: nested Booleans.
|
||||
// TBD: nested Booleans.
|
||||
|
||||
r = m.mk_fresh_const("p",m.mk_bool_sort());
|
||||
trail.push_back(r);
|
||||
cache.insert(e, r);
|
||||
pdefs.push_back(pdef_t(e, r));
|
||||
pdefs.push_back(pdef_t(r, e));
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
fmls[i] = cache.find(fmls[i].get());
|
||||
}
|
||||
fml = cache.find(fml);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief use dual propagation to minimize model.
|
||||
*/
|
||||
void minimize_assignment(app_ref_vector& assignment) {
|
||||
|
||||
bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) {
|
||||
bool result = false;
|
||||
assignment.push_back(not_fml);
|
||||
lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
|
||||
switch (res) {
|
||||
case l_true:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
case l_undef:
|
||||
break;
|
||||
case l_false:
|
||||
result = true;
|
||||
get_core(assignment, not_fml);
|
||||
break;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
lbool check_sat(expr_ref_vector& assignment, expr* fml) {
|
||||
assignment.push_back(fml);
|
||||
lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
|
||||
switch (res) {
|
||||
case l_true: {
|
||||
model_ref mdl;
|
||||
expr_ref tmp(m);
|
||||
assignment.reset();
|
||||
m_kernel.get_model(mdl);
|
||||
for (unsigned i = 0; i < m_atoms.size(); ++i) {
|
||||
expr* p = m_atoms[i].get();
|
||||
if (mdl->eval(p, tmp)) {
|
||||
if (m.is_true(tmp)) {
|
||||
assignment.push_back(p);
|
||||
}
|
||||
else if (m.is_false(tmp)) {
|
||||
assignment.push_back(m.mk_not(p));
|
||||
}
|
||||
}
|
||||
}
|
||||
expr_ref not_fml = mk_not(fml);
|
||||
if (!minimize_assignment(assignment, not_fml)) {
|
||||
res = l_undef;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_undef:
|
||||
break;
|
||||
case l_false:
|
||||
get_core(assignment, fml);
|
||||
break;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
void get_core(expr_ref_vector& core, expr* exclude) {
|
||||
unsigned sz = m_kernel.get_unsat_core_size();
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr* e = m_kernel.get_unsat_core_expr(i);
|
||||
if (e != exclude) {
|
||||
core.push_back(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref mk_not(expr* e) {
|
||||
return expr_ref(::mk_not(m, e), m);
|
||||
}
|
||||
|
||||
public:
|
||||
impl(ast_manager& m):
|
||||
m(m),
|
||||
mbp(m) {}
|
||||
|
||||
mbp(m),
|
||||
m_kernel(m, m_smtp),
|
||||
m_fml_pred(m),
|
||||
m_atoms(m) {}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) {
|
||||
}
|
||||
|
||||
void operator()(/* in */ goal_ref const & in,
|
||||
/* out */ goal_ref_buffer & result,
|
||||
/* out */ model_converter_ref & mc,
|
||||
|
|
@ -141,12 +221,16 @@ public:
|
|||
}
|
||||
void reset_statistics() {
|
||||
}
|
||||
|
||||
void cleanup() {
|
||||
}
|
||||
|
||||
void set_logic(symbol const & l) {
|
||||
}
|
||||
|
||||
void set_progress_callback(progress_callback * callback) {
|
||||
}
|
||||
|
||||
tactic * translate(ast_manager & m) {
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -195,6 +279,3 @@ tactic * qsat::translate(ast_manager & m) {
|
|||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -18,8 +18,8 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#ifndef __QE_MBP_H__
|
||||
#define __QE_MBP_H__
|
||||
#ifndef __QE_QSAT_H__
|
||||
#define __QE_QSAT_H__
|
||||
|
||||
#include "tactic.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -208,6 +208,8 @@ namespace smt {
|
|||
theory_array::reset_eh();
|
||||
std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
|
||||
m_var_data_full.reset();
|
||||
m_eqs.reset();
|
||||
m_eqsv.reset();
|
||||
}
|
||||
|
||||
void theory_array_full::display_var(std::ostream & out, theory_var v) const {
|
||||
|
|
@ -223,7 +225,6 @@ namespace smt {
|
|||
}
|
||||
|
||||
theory_var theory_array_full::mk_var(enode * n) {
|
||||
|
||||
theory_var r = theory_array::mk_var(n);
|
||||
SASSERT(r == static_cast<int>(m_var_data_full.size()));
|
||||
m_var_data_full.push_back(alloc(var_data_full));
|
||||
|
|
@ -512,7 +513,7 @@ namespace smt {
|
|||
|
||||
TRACE("array_map_bug",
|
||||
tout << "select-map axiom\n" << mk_ismt2_pp(sel1, m) << "\n=\n" << mk_ismt2_pp(sel2,m) << "\n";);
|
||||
|
||||
|
||||
return try_assign_eq(sel1, sel2);
|
||||
}
|
||||
|
||||
|
|
@ -760,36 +761,30 @@ namespace smt {
|
|||
r = FC_CONTINUE;
|
||||
}
|
||||
}
|
||||
while (!m_eqsv.empty()) {
|
||||
literal eq = m_eqsv.back();
|
||||
m_eqsv.pop_back();
|
||||
get_context().mark_as_relevant(eq);
|
||||
assert_axiom(eq);
|
||||
r = FC_CONTINUE;
|
||||
}
|
||||
if (r == FC_DONE && m_found_unsupported_op)
|
||||
r = FC_GIVEUP;
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
|
||||
context& ctx = get_context();
|
||||
enode* n1 = ctx.get_enode(v1);
|
||||
enode* n2 = ctx.get_enode(v2);
|
||||
if (n1->get_root() == n2->get_root()) {
|
||||
if (m_eqs.contains(v1, v2)) {
|
||||
return false;
|
||||
}
|
||||
m_eqs.insert(v1, v2, true);
|
||||
TRACE("array",
|
||||
tout << mk_bounded_pp(v1, get_manager()) << "\n==\n"
|
||||
<< mk_bounded_pp(v2, get_manager()) << "\n";);
|
||||
|
||||
#if 0
|
||||
if (m.proofs_enabled()) {
|
||||
#endif
|
||||
literal eq(mk_eq(v1,v2,true));
|
||||
ctx.mark_as_relevant(eq);
|
||||
assert_axiom(eq);
|
||||
#if 0
|
||||
}
|
||||
else {
|
||||
ctx.mark_as_relevant(n1);
|
||||
ctx.mark_as_relevant(n2);
|
||||
ctx.assign_eq(n1, n2, eq_justification::mk_axiom());
|
||||
}
|
||||
#endif
|
||||
literal eq(mk_eq(v1, v2, true));
|
||||
m_eqsv.push_back(eq);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -798,6 +793,8 @@ namespace smt {
|
|||
theory_array::pop_scope_eh(num_scopes);
|
||||
std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc<var_data_full>());
|
||||
m_var_data_full.shrink(num_old_vars);
|
||||
m_eqs.reset();
|
||||
m_eqsv.reset();
|
||||
}
|
||||
|
||||
void theory_array_full::collect_statistics(::statistics & st) const {
|
||||
|
|
|
|||
|
|
@ -38,12 +38,12 @@ namespace smt {
|
|||
|
||||
ast2ast_trailmap<sort,app> m_sort2epsilon;
|
||||
simplifier* m_simp;
|
||||
obj_pair_map<expr,expr,bool> m_eqs;
|
||||
svector<literal> m_eqsv;
|
||||
|
||||
protected:
|
||||
|
||||
#if 0
|
||||
virtual final_check_status final_check_eh();
|
||||
#endif
|
||||
//virtual final_check_status final_check_eh();
|
||||
virtual void reset_eh();
|
||||
|
||||
virtual void set_prop_upward(theory_var v);
|
||||
|
|
@ -84,6 +84,7 @@ namespace smt {
|
|||
|
||||
|
||||
bool try_assign_eq(expr* n1, expr* n2);
|
||||
void assign_eqs();
|
||||
|
||||
|
||||
public:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue