mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'opt' of https://git00.codeplex.com/z3 into opt
Conflicts: src/smt/theory_card.cpp
This commit is contained in:
commit
41efa8a75d
57
src/api/api_pb.cpp
Normal file
57
src/api/api_pb.cpp
Normal file
|
@ -0,0 +1,57 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
api_pb.cpp
|
||||
|
||||
Abstract:
|
||||
API for pb theory
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-11-13.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#include"z3.h"
|
||||
#include"api_log_macros.h"
|
||||
#include"api_context.h"
|
||||
#include"api_util.h"
|
||||
#include"card_decl_plugin.h"
|
||||
|
||||
extern "C" {
|
||||
|
||||
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
|
||||
Z3_ast const args[], unsigned k) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_atmost(c, num_args, args, k);
|
||||
RESET_ERROR_CODE();
|
||||
parameter param(k);
|
||||
card_util util(mk_c(c)->m());
|
||||
ast* a = util.mk_at_most_k(num_args, to_exprs(args), k);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
check_sorts(c, a);
|
||||
RETURN_Z3(of_ast(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
|
||||
Z3_ast const args[], int coeffs[],
|
||||
int k) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_pble(c, num_args, args, coeffs, k);
|
||||
RESET_ERROR_CODE();
|
||||
card_util util(mk_c(c)->m());
|
||||
ast* a = util.mk_le(num_args, coeffs, to_exprs(args), k);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
check_sorts(c, a);
|
||||
RETURN_Z3(of_ast(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
};
|
|
@ -1054,7 +1054,8 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u
|
|||
|
||||
void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
||||
ptr_vector<quantifier> ql;
|
||||
decl_collector decls(m_manager);
|
||||
ast_manager& m = m_manager;
|
||||
decl_collector decls(m);
|
||||
smt_renaming rn;
|
||||
|
||||
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
|
||||
|
@ -1065,7 +1066,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
|||
}
|
||||
decls.visit(n);
|
||||
|
||||
if (m_manager.is_proof(n)) {
|
||||
if (m.is_proof(n)) {
|
||||
strm << "(";
|
||||
}
|
||||
if (m_benchmark_name != symbol::null) {
|
||||
|
@ -1074,7 +1075,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
|||
if (m_source_info != symbol::null && m_source_info != symbol("")) {
|
||||
strm << "; :source { " << m_source_info << " }\n";
|
||||
}
|
||||
if (m_manager.is_bool(n)) {
|
||||
if (m.is_bool(n)) {
|
||||
strm << "(set-info :status " << m_status << ")\n";
|
||||
}
|
||||
if (m_category != symbol::null && m_category != symbol("")) {
|
||||
|
@ -1091,7 +1092,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
|||
for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
|
||||
sort* s = decls.get_sorts()[i];
|
||||
if (!(*m_is_declared)(s)) {
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
|
||||
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
|
||||
p.pp_sort_decl(sort_mark, s);
|
||||
}
|
||||
}
|
||||
|
@ -1099,7 +1100,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
|||
for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
|
||||
func_decl* d = decls.get_func_decls()[i];
|
||||
if (!(*m_is_declared)(d)) {
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
|
||||
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
|
||||
p(d);
|
||||
strm << "\n";
|
||||
}
|
||||
|
@ -1108,34 +1109,36 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
|||
for (unsigned i = 0; i < decls.get_num_preds(); ++i) {
|
||||
func_decl* d = decls.get_pred_decls()[i];
|
||||
if (!(*m_is_declared)(d)) {
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
|
||||
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
|
||||
p(d);
|
||||
strm << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
|
||||
strm << "(assert\n";
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
|
||||
p(m_assumptions[i].get());
|
||||
strm << ")\n";
|
||||
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
|
||||
strm << "(assert\n ";
|
||||
p(m_assumptions[i].get());
|
||||
strm << ")\n";
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
|
||||
strm << "(assert\n";
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
|
||||
p(m_assumptions_star[i].get());
|
||||
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
|
||||
strm << "(assert\n ";
|
||||
p(m_assumptions_star[i].get());
|
||||
strm << ")\n";
|
||||
}
|
||||
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
|
||||
if (m_manager.is_bool(n)) {
|
||||
strm << "(assert\n";
|
||||
p(n);
|
||||
strm << ")\n";
|
||||
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0);
|
||||
if (m.is_bool(n)) {
|
||||
if (!m.is_true(n)) {
|
||||
strm << "(assert\n ";
|
||||
p(n);
|
||||
strm << ")\n";
|
||||
}
|
||||
strm << "(check-sat)\n";
|
||||
}
|
||||
else if (m_manager.is_proof(n)) {
|
||||
else if (m.is_proof(n)) {
|
||||
strm << "(proof\n";
|
||||
p(n);
|
||||
strm << "))\n";
|
||||
|
|
|
@ -65,7 +65,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < ans.size(); ++i) {
|
||||
tout << mk_pp(ans[i].get(), m) << "\n";
|
||||
});
|
||||
IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat: " << ans.size() << "\n";);
|
||||
IF_VERBOSE(0, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";);
|
||||
if (ans.size() > m_answer.size()) {
|
||||
m_answer.reset();
|
||||
m_answer.append(ans);
|
||||
|
@ -92,7 +92,7 @@ namespace opt {
|
|||
core_vars.insert(get_not(core[i]));
|
||||
block_vars.remove(core[i]);
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
|
||||
IF_VERBOSE(0, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
|
||||
if (core.empty()) {
|
||||
m_upper = m_answer.size();
|
||||
return l_true;
|
||||
|
|
|
@ -18,6 +18,11 @@ Notes:
|
|||
--*/
|
||||
|
||||
#include "fu_malik.h"
|
||||
#include "smtlogics/qfbv_tactic.h"
|
||||
#include "tactic2solver.h"
|
||||
#include "goal.h"
|
||||
#include "probe.h"
|
||||
#include "smt_context.h"
|
||||
|
||||
/**
|
||||
\brief Fu & Malik procedure for MaxSAT. This procedure is based on
|
||||
|
@ -37,25 +42,30 @@ namespace opt {
|
|||
|
||||
struct fu_malik::imp {
|
||||
ast_manager& m;
|
||||
solver& s;
|
||||
ref<solver> m_s;
|
||||
expr_ref_vector m_soft;
|
||||
expr_ref_vector m_orig_soft;
|
||||
expr_ref_vector m_aux;
|
||||
expr_ref_vector m_assignment;
|
||||
unsigned m_upper_size;
|
||||
|
||||
solver & m_original_solver;
|
||||
bool m_use_new_bv_solver;
|
||||
|
||||
imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
|
||||
m(m),
|
||||
s(s),
|
||||
m_s(&s),
|
||||
m_soft(soft),
|
||||
m_orig_soft(soft),
|
||||
m_aux(m),
|
||||
m_assignment(m)
|
||||
m_assignment(m),
|
||||
m_original_solver(s),
|
||||
m_use_new_bv_solver(false)
|
||||
{
|
||||
m_upper_size = m_soft.size() + 1;
|
||||
}
|
||||
|
||||
solver& s() { return *m_s; }
|
||||
|
||||
/**
|
||||
\brief One step of the Fu&Malik algorithm.
|
||||
|
@ -73,18 +83,30 @@ namespace opt {
|
|||
*/
|
||||
|
||||
lbool step() {
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step)\n";); // add some count, add some information of # of soft constraints still possibly sat.
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
|
||||
expr_ref_vector assumptions(m), block_vars(m);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
assumptions.push_back(m.mk_not(m_aux[i].get()));
|
||||
}
|
||||
lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr());
|
||||
lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr());
|
||||
if (is_sat != l_false) {
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
ptr_vector<expr> core;
|
||||
s.get_unsat_core(core);
|
||||
if (m_use_new_bv_solver) {
|
||||
unsigned i = 0;
|
||||
while (s().check_sat(core.size(), core.c_ptr()) != l_false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
core.push_back(assumptions[i].get());
|
||||
++i;
|
||||
}
|
||||
}
|
||||
else {
|
||||
s().get_unsat_core(core);
|
||||
}
|
||||
|
||||
SASSERT(!core.empty());
|
||||
|
||||
// Update soft-constraints and aux_vars
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
|
@ -101,9 +123,11 @@ namespace opt {
|
|||
m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
|
||||
m_soft[i] = m.mk_or(m_soft[i].get(), block_var);
|
||||
block_vars.push_back(block_var);
|
||||
s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
|
||||
s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
|
||||
}
|
||||
SASSERT (!block_vars.empty());
|
||||
assert_at_most_one(block_vars);
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
|
||||
return l_false;
|
||||
}
|
||||
|
||||
|
@ -111,7 +135,7 @@ namespace opt {
|
|||
expr_ref has_one(m), has_zero(m), at_most_one(m);
|
||||
mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero);
|
||||
at_most_one = m.mk_or(has_one, has_zero);
|
||||
s.assert_expr(at_most_one);
|
||||
s().assert_expr(at_most_one);
|
||||
}
|
||||
|
||||
void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& has_zero) {
|
||||
|
@ -129,15 +153,40 @@ namespace opt {
|
|||
has_zero = m.mk_and(has_zero1, has_zero2);
|
||||
}
|
||||
}
|
||||
|
||||
void set_solver() {
|
||||
solver& current_solver = s();
|
||||
goal g(m, true, false);
|
||||
unsigned num_assertions = current_solver.get_num_assertions();
|
||||
for (unsigned i = 0; i < num_assertions; ++i) {
|
||||
g.assert_expr(current_solver.get_assertion(i));
|
||||
}
|
||||
probe *p = mk_is_qfbv_probe();
|
||||
bool all_bv = (*p)(g).is_true();
|
||||
if (all_bv) {
|
||||
opt_solver & os = opt_solver::to_opt(m_original_solver);
|
||||
smt::context & ctx = os.get_context();
|
||||
tactic* t = mk_qfbv_tactic(m, ctx.get_params());
|
||||
// The new SAT solver hasn't supported unsat core yet
|
||||
m_s = mk_tactic2solver(m, t);
|
||||
SASSERT(m_s != &m_original_solver);
|
||||
for (unsigned i = 0; i < num_assertions; ++i) {
|
||||
m_s->assert_expr(current_solver.get_assertion(i));
|
||||
}
|
||||
m_use_new_bv_solver = true;
|
||||
IF_VERBOSE(0, verbose_stream() << "Force to use the new BV solver." << std::endl;);
|
||||
}
|
||||
}
|
||||
|
||||
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
|
||||
lbool operator()() {
|
||||
lbool is_sat = s.check_sat(0,0);
|
||||
set_solver();
|
||||
lbool is_sat = s().check_sat(0,0);
|
||||
if (!m_soft.empty() && is_sat == l_true) {
|
||||
solver::scoped_push _sp(s);
|
||||
solver::scoped_push _sp(s());
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
|
||||
s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
|
||||
s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
|
||||
}
|
||||
|
||||
lbool is_sat = l_true;
|
||||
|
@ -150,7 +199,7 @@ namespace opt {
|
|||
if (is_sat == l_true) {
|
||||
// Get a list of satisfying m_soft
|
||||
model_ref model;
|
||||
s.get_model(model);
|
||||
s().get_model(model);
|
||||
|
||||
m_assignment.reset();
|
||||
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
|
||||
|
|
|
@ -109,9 +109,11 @@ namespace opt {
|
|||
|
||||
lbool r = m_context.check(num_assumptions, assumptions);
|
||||
if (m_is_dump) {
|
||||
std::stringstream buffer;
|
||||
buffer << "opt_solver" << ++g_checksat_count << ".smt2";
|
||||
to_smt2_benchmark(buffer.str().c_str(), "benchmark", "QF_BV");
|
||||
std::stringstream file_name;
|
||||
file_name << "opt_solver" << ++g_checksat_count << ".smt2";
|
||||
std::ofstream buffer(file_name.str().c_str());
|
||||
to_smt2_benchmark(buffer, "opt_solver", "QF_BV");
|
||||
buffer.close();
|
||||
}
|
||||
if (r == l_true && m_objective_enabled) {
|
||||
m_objective_values.reset();
|
||||
|
@ -212,9 +214,8 @@ namespace opt {
|
|||
return dynamic_cast<opt_solver&>(s);
|
||||
}
|
||||
|
||||
void opt_solver::to_smt2_benchmark(char const * file_name, char const * name, char const * logic,
|
||||
char const * status, char const * attributes) {
|
||||
std::ofstream buffer(file_name);
|
||||
void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic,
|
||||
char const * status, char const * attributes) {
|
||||
ast_smt_pp pp(m);
|
||||
pp.set_benchmark_name(name);
|
||||
pp.set_logic(logic);
|
||||
|
@ -225,8 +226,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < get_num_assertions(); ++i) {
|
||||
pp.add_assumption(to_expr(get_assertion(i)));
|
||||
}
|
||||
pp.display_smt2(buffer, to_expr(m.mk_true()));
|
||||
buffer.close();
|
||||
pp.display_smt2(buffer, to_expr(m.mk_true()));
|
||||
}
|
||||
|
||||
opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) {
|
||||
|
|
|
@ -90,8 +90,8 @@ namespace opt {
|
|||
|
||||
smt::theory_opt& get_optimizer();
|
||||
|
||||
void to_smt2_benchmark(char const * file_name, char const * name = "benchmarks",
|
||||
char const * logic = "", char const * status = "unknown", char const * attributes = "");
|
||||
void to_smt2_benchmark(std::ofstream & buffer, char const * name = "benchmarks",
|
||||
char const * logic = "", char const * status = "unknown", char const * attributes = "");
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
@ -137,9 +137,10 @@ namespace smt {
|
|||
}
|
||||
|
||||
static unsigned gcd(unsigned a, unsigned b) {
|
||||
if (a == 0) return b;
|
||||
if (b == 0) return a;
|
||||
while (a != b) {
|
||||
if (a == 0) return b;
|
||||
if (b == 0) return a;
|
||||
SASSERT(a != 0 && b != 0);
|
||||
if (a < b) {
|
||||
b %= a;
|
||||
}
|
||||
|
@ -175,7 +176,7 @@ namespace smt {
|
|||
if (!args.empty()) {
|
||||
unsigned g = abs(args[0].second);
|
||||
for (unsigned i = 1; g > 1 && i < args.size(); ++i) {
|
||||
g = gcd(g, args[i].second);
|
||||
g = gcd(g, abs(args[i].second));
|
||||
}
|
||||
if (g > 1) {
|
||||
int k = c->m_k;
|
||||
|
@ -187,7 +188,7 @@ namespace smt {
|
|||
k = abs(k);
|
||||
k += (k % g);
|
||||
k /= g;
|
||||
k = -k;
|
||||
c->m_k = -k;
|
||||
}
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
args[i].second /= g;
|
||||
|
@ -217,6 +218,7 @@ namespace smt {
|
|||
|
||||
void theory_card::collect_statistics(::statistics& st) const {
|
||||
st.update("pb axioms", m_stats.m_num_axioms);
|
||||
st.update("pb propagations", m_stats.m_num_propagations);
|
||||
st.update("pb predicates", m_stats.m_num_predicates);
|
||||
st.update("pb compilations", m_stats.m_num_compiles);
|
||||
}
|
||||
|
@ -320,6 +322,21 @@ namespace smt {
|
|||
return curr_min;
|
||||
}
|
||||
|
||||
int theory_card::get_max_delta(card& c) {
|
||||
if (m_util.is_at_most_k(c.m_app)) {
|
||||
return 1;
|
||||
}
|
||||
int max = 0;
|
||||
context& ctx = get_context();
|
||||
for (unsigned i = 0; i < c.m_args.size(); ++i) {
|
||||
if (c.m_args[i].second > max && ctx.get_assignment(c.m_args[i].first) == l_undef) {
|
||||
max = c.m_args[i].second;
|
||||
}
|
||||
}
|
||||
return max;
|
||||
}
|
||||
|
||||
|
||||
int theory_card::accumulate_max(literal_vector& lits, card& c) {
|
||||
context& ctx = get_context();
|
||||
arg_t const& args = c.m_args;
|
||||
|
@ -368,20 +385,17 @@ namespace smt {
|
|||
lbool aval = ctx.get_assignment(abv);
|
||||
if (min > k && aval != l_false) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~literal(abv));
|
||||
int curr_min = accumulate_min(lits, c);
|
||||
SASSERT(curr_min > k);
|
||||
add_clause(c, lits);
|
||||
add_assign(c, lits, ~literal(abv));
|
||||
}
|
||||
else if (max <= k && aval != l_true) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(literal(abv));
|
||||
int curr_max = accumulate_max(lits, c);
|
||||
SASSERT(curr_max <= k);
|
||||
add_clause(c, lits);
|
||||
add_assign(c, lits, literal(abv));
|
||||
}
|
||||
// min + min_increment > k
|
||||
else if (min == k && aval == l_true) {
|
||||
else if (min <= k && k < min + get_max_delta(c) && aval == l_true) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~literal(abv));
|
||||
int curr_min = accumulate_min(lits, c);
|
||||
|
@ -389,39 +403,70 @@ namespace smt {
|
|||
add_clause(c, lits);
|
||||
}
|
||||
else {
|
||||
// curr_min + min_increment > k
|
||||
SASSERT(curr_min == k);
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
literal_vector lits_save(lits); // add_clause has a side-effect on literals.
|
||||
lits_save.push_back(literal(bv, inc > 0)); // avoid incrementing min.
|
||||
add_clause(c, lits_save);
|
||||
if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
add_assign(c, lits, literal(bv, inc > 0));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
// k < max && ... ?
|
||||
else if (max == k + 1 && aval == l_false) {
|
||||
else if (max - get_max_delta(c) <= k && k < max && aval == l_false) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(literal(abv));
|
||||
int curr_max = accumulate_max(lits, c);
|
||||
if (curr_max <= k) {
|
||||
add_clause(c, lits);
|
||||
}
|
||||
else if (curr_max == k + 1) {
|
||||
else {
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
literal_vector lits_save(lits); // add_clause has a side-effect on literals.
|
||||
lits_save.push_back(literal(bv, inc < 0)); // avoid decrementing max.
|
||||
add_clause(c, lits_save);
|
||||
if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
add_assign(c, lits, literal(bv, inc < 0));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
#if 0
|
||||
else if (aval == l_true) {
|
||||
SASSERT(min < k);
|
||||
literal_vector& lits = get_lits();
|
||||
int curr_min = accumulate_min(lits, c);
|
||||
bool all_inc = curr_min == k;
|
||||
unsigned num_incs = 0;
|
||||
for (unsigned i = 0; all_inc && i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
all_inc = inc + min > k;
|
||||
num_incs++;
|
||||
}
|
||||
}
|
||||
if (num_incs > 0) {
|
||||
std::cout << "missed T propgations " << num_incs << "\n";
|
||||
}
|
||||
}
|
||||
else if (aval == l_false) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(literal(abv));
|
||||
int curr_max = accumulate_max(lits, c);
|
||||
bool all_dec = curr_max > k;
|
||||
unsigned num_decs = 0;
|
||||
for (unsigned i = 0; all_dec && i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
all_dec = inc + max <= k;
|
||||
num_decs++;
|
||||
}
|
||||
}
|
||||
if (num_decs > 0) {
|
||||
std::cout << "missed F propgations " << num_decs << "\n";
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
void theory_card::assign_eh(bool_var v, bool is_true) {
|
||||
|
@ -616,10 +661,14 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool theory_card::should_compile(card& c) {
|
||||
#if 1
|
||||
return false;
|
||||
#else
|
||||
if (!m_util.is_at_most_k(c.m_app)) {
|
||||
return false;
|
||||
}
|
||||
return c.m_num_propagations >= c.m_compilation_threshold;
|
||||
#endif
|
||||
}
|
||||
|
||||
void theory_card::compile_at_most(card& c) {
|
||||
|
@ -630,7 +679,7 @@ namespace smt {
|
|||
SASSERT(m_util.is_at_most_k(a));
|
||||
literal atmostk;
|
||||
int k = m_util.get_k(a);
|
||||
unsigned num_args = ca.m_args.size();
|
||||
unsigned num_args = c.m_args.size();
|
||||
|
||||
sort_expr se(*this);
|
||||
if (k >= static_cast<int>(num_args)) {
|
||||
|
@ -694,6 +743,19 @@ namespace smt {
|
|||
return m_literals;
|
||||
}
|
||||
|
||||
void theory_card::add_assign(card& c, literal_vector const& lits, literal l) {
|
||||
literal_vector ls;
|
||||
++c.m_num_propagations;
|
||||
m_stats.m_num_propagations++;
|
||||
context& ctx = get_context();
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
ls.push_back(~lits[i]);
|
||||
}
|
||||
ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l)));
|
||||
}
|
||||
|
||||
|
||||
|
||||
void theory_card::add_clause(card& c, literal_vector const& lits) {
|
||||
++c.m_num_propagations;
|
||||
m_stats.m_num_axioms++;
|
||||
|
@ -701,7 +763,8 @@ namespace smt {
|
|||
TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
justification* js = 0;
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
|
||||
IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr());
|
||||
IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(),
|
||||
lits.size(), lits.c_ptr());
|
||||
verbose_stream() << "\n";);
|
||||
// ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
}
|
||||
|
|
|
@ -32,6 +32,7 @@ namespace smt {
|
|||
|
||||
struct stats {
|
||||
unsigned m_num_axioms;
|
||||
unsigned m_num_propagations;
|
||||
unsigned m_num_predicates;
|
||||
unsigned m_num_compiles;
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
|
@ -75,10 +76,12 @@ namespace smt {
|
|||
void add_card(card* c);
|
||||
|
||||
void add_clause(card& c, literal_vector const& lits);
|
||||
void add_assign(card& c, literal_vector const& lits, literal l);
|
||||
literal_vector& get_lits();
|
||||
|
||||
int find_inc(bool_var bv, svector<std::pair<bool_var, int> >const& vars);
|
||||
void propagate_assignment(card& c);
|
||||
int get_max_delta(card& c);
|
||||
int accumulate_max(literal_vector& lits, card& c);
|
||||
int accumulate_min(literal_vector& lits, card& c);
|
||||
lbool dec_max(int inc, lbool val);
|
||||
|
|
|
@ -31,6 +31,15 @@ Notes:
|
|||
|
||||
#define MEMLIMIT 300
|
||||
|
||||
tactic * mk_new_sat_tactic(ast_manager & m) {
|
||||
IF_VERBOSE(0, verbose_stream() << "Try to use the new SAT solver." << std::endl;);
|
||||
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
return new_sat;
|
||||
}
|
||||
|
||||
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
|
@ -85,10 +94,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
tactic * new_sat = and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic());
|
||||
#else
|
||||
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
tactic * new_sat = mk_new_sat_tactic(m);
|
||||
#endif
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
|
|
|
@ -53,6 +53,7 @@ public:
|
|||
m_scopes.push_back(m_chuncks.size());
|
||||
}
|
||||
|
||||
|
||||
void pop_scope() {
|
||||
unsigned old_size = m_scopes.back();
|
||||
m_scopes.pop_back();
|
||||
|
|
Loading…
Reference in a new issue