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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-09 09:19:37 -07:00
commit efe440839e
22 changed files with 215 additions and 85 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_polynomial.cpp
View file

@ -26,17 +26,6 @@ Notes:
#include "util/scoped_timer.h" #include "util/scoped_timer.h"
#include "ast/expr2var.h" #include "ast/expr2var.h"
namespace api {
pmanager::pmanager(reslimit& lim):
m_pm(lim, m_nm) {
}
pmanager::~pmanager() {
}
};
extern "C" { extern "C" {
Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) { Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) {

6
src/api/api_polynomial.h
View file

@ -23,13 +23,13 @@ Notes:
namespace api { namespace api {
class pmanager { class pmanager final {
unsynch_mpz_manager m_nm; unsynch_mpz_manager m_nm;
polynomial::manager m_pm; polynomial::manager m_pm;
// TODO: add support for caching expressions -> polynomial and back // TODO: add support for caching expressions -> polynomial and back
public: public:
pmanager(reslimit& limx); pmanager(reslimit& lim) : m_pm(lim, m_nm) {}
virtual ~pmanager(); ~pmanager() {}
polynomial::manager & pm() { return m_pm; } polynomial::manager & pm() { return m_pm; }
}; };

18
src/ast/ast.cpp
View file

@ -1057,7 +1057,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
} }
std::ostringstream buffer; std::ostringstream buffer;
buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible"; buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
throw ast_exception(buffer.str().c_str()); throw ast_exception(buffer.str());
} }
@ -1086,7 +1086,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
if (domain[i] != domain[0]) { if (domain[i] != domain[0]) {
std::ostringstream buffer; std::ostringstream buffer;
buffer << "Sort mismatch between first argument and argument " << (i+1); buffer << "Sort mismatch between first argument and argument " << (i+1);
throw ast_exception(buffer.str().c_str()); throw ast_exception(buffer.str());
} }
} }
return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info); return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);
@ -1701,9 +1701,9 @@ ast * ast_manager::register_node_core(ast * n) {
SASSERT(m_ast_table.contains(n)); SASSERT(m_ast_table.contains(n));
if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) { if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {
std::ostringstream buffer; std::ostringstream buffer;
buffer << "Recycling of declaration for the same name '" << to_func_decl(r)->get_name().str().c_str() << "'" buffer << "Recycling of declaration for the same name '" << to_func_decl(r)->get_name().str()
<< " and domain, but different range type is not permitted"; << "' and domain, but different range type is not permitted";
throw ast_exception(buffer.str().c_str()); throw ast_exception(buffer.str());
} }
deallocate_node(n, ::get_node_size(n)); deallocate_node(n, ::get_node_size(n));
return r; return r;
@ -1992,7 +1992,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
buff << "invalid function application for " << decl->get_name() << ", "; buff << "invalid function application for " << decl->get_name() << ", ";
buff << "sort mismatch on argument at position " << (i+1) << ", "; buff << "sort mismatch on argument at position " << (i+1) << ", ";
buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str()); throw ast_exception(buff.str());
} }
} }
} }
@ -2008,7 +2008,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
buff << "invalid function application for " << decl->get_name() << ", "; buff << "invalid function application for " << decl->get_name() << ", ";
buff << "sort mismatch on argument at position " << (i+1) << ", "; buff << "sort mismatch on argument at position " << (i+1) << ", ";
buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str()); throw ast_exception(buff.str());
} }
} }
} }
@ -2170,7 +2170,7 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
<< " for function " << mk_pp(f,*this) << " for function " << mk_pp(f,*this)
<< " supplied sort is " << " supplied sort is "
<< mk_pp(actual_sort, *this); << mk_pp(actual_sort, *this);
throw ast_exception(buffer.str().c_str()); throw ast_exception(buffer.str());
} }
} }
} }
@ -2194,7 +2194,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
std::ostringstream buffer; std::ostringstream buffer;
buffer << "Wrong number of arguments (" << num_args buffer << "Wrong number of arguments (" << num_args
<< ") passed to function " << mk_pp(decl, *this); << ") passed to function " << mk_pp(decl, *this);
throw ast_exception(buffer.str().c_str()); throw ast_exception(buffer.str());
} }
app * r = nullptr; app * r = nullptr;
if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) { if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {

2
src/ast/ast.h
View file

@ -69,7 +69,7 @@ class ast_manager;
*/ */
class ast_exception : public default_exception { class ast_exception : public default_exception {
public: public:
ast_exception(char const * msg):default_exception(msg) {} ast_exception(std::string && msg) : default_exception(std::move(msg)) {}
}; };
typedef int family_id; typedef int family_id;

11
src/ast/proofs/proof_checker.cpp
View file

@ -389,14 +389,14 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
match_fact(p, fact) && match_fact(p, fact) &&
match_fact(p1, fml) && match_fact(p1, fml) &&
match_and(fml, terms)) { match_and(fml, terms)) {
for (expr* t : terms) for (expr* t : terms)
if (t == fact) return true; if (t == fact) return true;
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
} }
case PR_NOT_OR_ELIM: { case PR_NOT_OR_ELIM: {
if (match_proof(p, p1) && if (match_proof(p, p1) &&
match_fact(p, fact) && match_fact(p, fact) &&
match_fact(p1, fml) && match_fact(p1, fml) &&
@ -605,6 +605,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
bool found = false; bool found = false;
for (expr* term2 : terms2) { for (expr* term2 : terms2) {
found = term1 == term2; found = term1 == term2;
if (found) break;
} }
if (!found) { if (!found) {
IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";); IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
@ -738,9 +739,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
} }
if (is_quantifier(e)) { if (is_quantifier(e)) {
SASSERT(!is_lambda(e)); SASSERT(!is_lambda(e));
q = to_quantifier(e); q = to_quantifier(e);
// TBD check that quantifier is properly instantiated // TBD check that quantifier is properly instantiated
return is_forall == ::is_forall(q); return is_forall == ::is_forall(q);
} }
} }
UNREACHABLE(); UNREACHABLE();
@ -1004,7 +1005,7 @@ bool proof_checker::match_op(expr const* e, decl_kind k, ptr_vector<expr>& terms
if (e->get_kind() == AST_APP && if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k) { to_app(e)->get_decl_kind() == k) {
for (expr* arg : *to_app(e)) for (expr* arg : *to_app(e))
terms.push_back(arg); terms.push_back(arg);
return true; return true;
} }

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

@ -2629,17 +2629,15 @@ namespace algebraic_numbers {
} }
else if (a.is_basic()) { else if (a.is_basic()) {
mpq const & v = basic_value(a); mpq const & v = basic_value(a);
scoped_mpz neg_n(qm()); mpz neg_n;
qm().set(neg_n, v.numerator()); qm().set(neg_n, v.numerator());
qm().neg(neg_n); qm().neg(neg_n);
unsynch_mpz_manager zmgr; mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
// FIXME: remove these copies
mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
out << "("; out << "(";
upm().display(out, 2, coeffs, "#"); upm().display(out, 2, coeffs, "#");
out << ", 1)"; // first root of the polynomial d*# - n out << ", 1)"; // first root of the polynomial d*# - n
zmgr.del(coeffs[0]); qm().del(coeffs[0]);
zmgr.del(coeffs[1]); qm().del(coeffs[1]);
} }
else { else {
algebraic_cell * c = a.to_algebraic(); algebraic_cell * c = a.to_algebraic();
@ -2679,17 +2677,15 @@ namespace algebraic_numbers {
} }
else if (a.is_basic()) { else if (a.is_basic()) {
mpq const & v = basic_value(a); mpq const & v = basic_value(a);
scoped_mpz neg_n(qm()); mpz neg_n;
qm().set(neg_n, v.numerator()); qm().set(neg_n, v.numerator());
qm().neg(neg_n); qm().neg(neg_n);
unsynch_mpz_manager zmgr; mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
// FIXME: remove these copies
mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
out << "(root-obj "; out << "(root-obj ";
upm().display_smt2(out, 2, coeffs, "x"); upm().display_smt2(out, 2, coeffs, "x");
out << " 1)"; // first root of the polynomial d*# - n out << " 1)"; // first root of the polynomial d*# - n
zmgr.del(coeffs[0]); qm().del(coeffs[0]);
zmgr.del(coeffs[1]); qm().del(coeffs[1]);
} }
else { else {
algebraic_cell * c = a.to_algebraic(); algebraic_cell * c = a.to_algebraic();

2
src/sat/sat_allocator.h
View file

@ -23,7 +23,7 @@ Revision History:
#include "util/machine.h" #include "util/machine.h"
class sat_allocator { class sat_allocator {
static const unsigned CHUNK_SIZE = (1 << 16); static const unsigned CHUNK_SIZE = (1 << 16) - sizeof(char*);
static const unsigned SMALL_OBJ_SIZE = 512; static const unsigned SMALL_OBJ_SIZE = 512;
static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1); static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1);
static const unsigned NUM_FREE = 1 + (SMALL_OBJ_SIZE >> PTR_ALIGNMENT); static const unsigned NUM_FREE = 1 + (SMALL_OBJ_SIZE >> PTR_ALIGNMENT);

31
src/smt/mam.cpp
View file

@ -1847,7 +1847,10 @@ namespace smt {
enode * m_n2; enode * m_n2;
enode * m_app; enode * m_app;
const bind * m_b; const bind * m_b;
ptr_vector<enode> m_used_enodes;
// equalities used for pattern match. The first element of the tuple gives the argument (or null) of some term that was matched against some higher level
// structure of the trigger, the second element gives the term that argument is replaced with in order to match the trigger. Used for logging purposes only.
vector<std::tuple<enode *, enode *>> m_used_enodes;
unsigned m_curr_used_enodes_size; unsigned m_curr_used_enodes_size;
ptr_vector<enode> m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation ptr_vector<enode> m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
unsigned_vector m_min_top_generation, m_max_top_generation; unsigned_vector m_min_top_generation, m_max_top_generation;
@ -1864,11 +1867,11 @@ namespace smt {
m_pool.recycle(v); m_pool.recycle(v);
} }
void update_max_generation(enode * n) { void update_max_generation(enode * n, enode * prev) {
m_max_generation = std::max(m_max_generation, n->get_generation()); m_max_generation = std::max(m_max_generation, n->get_generation());
if (m_ast_manager.has_trace_stream()) if (m_ast_manager.has_trace_stream())
m_used_enodes.push_back(n); m_used_enodes.push_back(std::make_tuple(prev, n));
} }
// We have to provide the number of expected arguments because we have flat-assoc applications such as +. // We have to provide the number of expected arguments because we have flat-assoc applications such as +.
@ -1877,7 +1880,7 @@ namespace smt {
enode * first = curr; enode * first = curr;
do { do {
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) { if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
update_max_generation(curr); update_max_generation(curr, first);
return curr; return curr;
} }
curr = curr->get_next(); curr = curr->get_next();
@ -1890,7 +1893,7 @@ namespace smt {
curr = curr->get_next(); curr = curr->get_next();
while (curr != first) { while (curr != first) {
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) { if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
update_max_generation(curr); update_max_generation(curr, first);
return curr; return curr;
} }
curr = curr->get_next(); curr = curr->get_next();
@ -1914,7 +1917,7 @@ namespace smt {
do { do {
if (n->get_decl() == f && if (n->get_decl() == f &&
n->get_arg(0)->get_root() == m_args[0]) { n->get_arg(0)->get_root() == m_args[0]) {
update_max_generation(n); update_max_generation(n, first);
return true; return true;
} }
n = n->get_next(); n = n->get_next();
@ -1929,7 +1932,7 @@ namespace smt {
if (n->get_decl() == f && if (n->get_decl() == f &&
n->get_arg(0)->get_root() == m_args[0] && n->get_arg(0)->get_root() == m_args[0] &&
n->get_arg(1)->get_root() == m_args[1]) { n->get_arg(1)->get_root() == m_args[1]) {
update_max_generation(n); update_max_generation(n, first);
return true; return true;
} }
n = n->get_next(); n = n->get_next();
@ -1949,7 +1952,7 @@ namespace smt {
break; break;
} }
if (i == num_args) { if (i == num_args) {
update_max_generation(n); update_max_generation(n, first);
return true; return true;
} }
} }
@ -2196,7 +2199,7 @@ namespace smt {
if (bp.m_it == bp.m_end) if (bp.m_it == bp.m_end)
return nullptr; return nullptr;
m_top++; m_top++;
update_max_generation(*(bp.m_it)); update_max_generation(*(bp.m_it), nullptr);
return *(bp.m_it); return *(bp.m_it);
} }
@ -2277,7 +2280,7 @@ namespace smt {
if (m_ast_manager.has_trace_stream()) { if (m_ast_manager.has_trace_stream()) {
m_used_enodes.reset(); m_used_enodes.reset();
m_used_enodes.push_back(n); m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
} }
m_pc = t->get_root(); m_pc = t->get_root();
@ -2382,6 +2385,10 @@ namespace smt {
SASSERT(m_n2 != 0); SASSERT(m_n2 != 0);
if (m_n1->get_root() != m_n2->get_root()) if (m_n1->get_root() != m_n2->get_root())
goto backtrack; goto backtrack;
// we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
m_pc = m_pc->m_next; m_pc = m_pc->m_next;
goto main_loop; goto main_loop;
@ -2776,7 +2783,7 @@ namespace smt {
m_pattern_instances.pop_back(); m_pattern_instances.pop_back();
m_pattern_instances.push_back(m_app); m_pattern_instances.push_back(m_app);
// continue succeeded // continue succeeded
update_max_generation(m_app); update_max_generation(m_app, nullptr); // null indicates a top-level match
TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
m_num_args = c->m_num_args; m_num_args = c->m_num_args;
m_oreg = c->m_oreg; m_oreg = c->m_oreg;
@ -3878,7 +3885,7 @@ namespace smt {
} }
#endif #endif
void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) override { void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) override {
TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";); TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
#ifdef Z3DEBUG #ifdef Z3DEBUG
if (m_check_missing_instances) { if (m_check_missing_instances) {

3
src/smt/mam.h
View file

@ -21,6 +21,7 @@ Revision History:
#include "ast/ast.h" #include "ast/ast.h"
#include "smt/smt_types.h" #include "smt/smt_types.h"
#include <tuple>
namespace smt { namespace smt {
/** /**
@ -57,7 +58,7 @@ namespace smt {
virtual void display(std::ostream& out) = 0; virtual void display(std::ostream& out) = 0;
virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) = 0; virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) = 0;
virtual bool is_shared(enode * n) const = 0; virtual bool is_shared(enode * n) const = 0;

6
src/smt/smt_context.cpp
View file

@ -562,6 +562,7 @@ namespace smt {
invert_trans(n1); invert_trans(n1);
n1->m_trans.m_target = n2; n1->m_trans.m_target = n2;
n1->m_trans.m_justification = js; n1->m_trans.m_justification = js;
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
SASSERT(r1->trans_reaches(n1)); SASSERT(r1->trans_reaches(n1));
// --------------- // ---------------
// r1 -> .. -> n1 -> n2 -> ... -> r2 // r1 -> .. -> n1 -> n2 -> ... -> r2
@ -741,12 +742,14 @@ namespace smt {
eq_justification js = n->m_trans.m_justification; eq_justification js = n->m_trans.m_justification;
prev->m_trans.m_target = nullptr; prev->m_trans.m_target = nullptr;
prev->m_trans.m_justification = null_eq_justification; prev->m_trans.m_justification = null_eq_justification;
prev->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
while (curr != nullptr) { while (curr != nullptr) {
SASSERT(prev->trans_reaches(n)); SASSERT(prev->trans_reaches(n));
enode * new_curr = curr->m_trans.m_target; enode * new_curr = curr->m_trans.m_target;
eq_justification new_js = curr->m_trans.m_justification; eq_justification new_js = curr->m_trans.m_justification;
curr->m_trans.m_target = prev; curr->m_trans.m_target = prev;
curr->m_trans.m_justification = js; curr->m_trans.m_justification = js;
curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
prev = curr; prev = curr;
js = new_js; js = new_js;
curr = new_curr; curr = new_curr;
@ -1040,6 +1043,7 @@ namespace smt {
SASSERT(r1->trans_reaches(n1)); SASSERT(r1->trans_reaches(n1));
n1->m_trans.m_target = nullptr; n1->m_trans.m_target = nullptr;
n1->m_trans.m_justification = null_eq_justification; n1->m_trans.m_justification = null_eq_justification;
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
invert_trans(r1); invert_trans(r1);
// --------------- // ---------------
// n1 -> ... -> r1 // n1 -> ... -> r1
@ -1786,7 +1790,7 @@ namespace smt {
} }
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation, bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes) { unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes); return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
} }

3
src/smt/smt_context.h
View file

@ -49,6 +49,7 @@ Revision History:
#include "util/timer.h" #include "util/timer.h"
#include "util/statistics.h" #include "util/statistics.h"
#include "solver/progress_callback.h" #include "solver/progress_callback.h"
#include <tuple>
// there is a significant space overhead with allocating 1000+ contexts in // there is a significant space overhead with allocating 1000+ contexts in
// the case that each context only references a few expressions. // the case that each context only references a few expressions.
@ -970,7 +971,7 @@ namespace smt {
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings); bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation, bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes); unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
void set_global_generation(unsigned generation) { m_generation = generation; } void set_global_generation(unsigned generation) { m_generation = generation; }

4
src/smt/smt_context_pp.cpp
View file

@ -577,7 +577,7 @@ namespace smt {
case b_justification::BIN_CLAUSE: { case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal(); literal l2 = j.get_literal();
out << "bin-clause "; out << "bin-clause ";
display_literal_verbose(out, l2); display_literal(out, l2);
break; break;
} }
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
@ -590,7 +590,7 @@ namespace smt {
out << "justification " << j.get_justification()->get_from_theory() << ": "; out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits; literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits); const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals_verbose(out, lits); display_literals(out, lits);
break; break;
} }
default: default:

1
src/smt/smt_enode.cpp
View file

@ -47,6 +47,7 @@ namespace smt {
n->m_cgc_enabled = cgc_enabled; n->m_cgc_enabled = cgc_enabled;
n->m_iscope_lvl = iscope_lvl; n->m_iscope_lvl = iscope_lvl;
n->m_lbl_hash = -1; n->m_lbl_hash = -1;
n->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
enode * arg = app2enode[owner->get_arg(i)->get_id()]; enode * arg = app2enode[owner->get_arg(i)->get_id()];

15
src/smt/smt_enode.h
View file

@ -38,6 +38,15 @@ namespace smt {
} }
}; };
/**
\brief Indicates whether the proof for membership in an equivalence class is already logged.
*/
enum logged_status {
NOT_LOGGED, //!< Proof is not logged or logged information is not up-to-date.
BEING_LOGGED, //!< We are currently in the process of logging all relevant information. This is used to prevent looping when logging congruence steps.
LOGGED //!< Proof is logged and logged information is still up-to-date.
};
/** \ brief Use sparse maps in SMT solver. /** \ brief Use sparse maps in SMT solver.
Define this to use hash maps rather than vectors over ast Define this to use hash maps rather than vectors over ast
@ -105,6 +114,7 @@ namespace smt {
enode_vector m_parents; //!< Parent enodes of the equivalence class. enode_vector m_parents; //!< Parent enodes of the equivalence class.
theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode. theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode.
trans_justification m_trans; //!< A justification for the enode being equal to its root. trans_justification m_trans; //!< A justification for the enode being equal to its root.
logged_status m_proof_logged_status; //!< Indicates that the proof for the enode being equal to its root is in the log.
signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern
approx_set m_lbls; approx_set m_lbls;
approx_set m_plbls; approx_set m_plbls;
@ -113,6 +123,7 @@ namespace smt {
friend class context; friend class context;
friend class euf_manager; friend class euf_manager;
friend class conflict_resolution; friend class conflict_resolution;
friend class quantifier_manager;
theory_var_list * get_th_var_list() { theory_var_list * get_th_var_list() {
@ -361,6 +372,10 @@ namespace smt {
theory_var get_th_var(theory_id th_id) const; theory_var get_th_var(theory_id th_id) const;
trans_justification get_trans_justification() {
return m_trans;
}
unsigned get_generation() const { unsigned get_generation() const {
return m_generation; return m_generation;
} }

3
src/smt/smt_model_checker.cpp
View file

@ -33,6 +33,7 @@ Revision History:
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "smt/smt_model_finder.h" #include "smt/smt_model_finder.h"
#include "model/model_pp.h" #include "model/model_pp.h"
#include <tuple>
namespace smt { namespace smt {
@ -518,7 +519,7 @@ namespace smt {
void model_checker::assert_new_instances() { void model_checker::assert_new_instances() {
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";); TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
ptr_buffer<enode> bindings; ptr_buffer<enode> bindings;
ptr_vector<enode> dummy; vector<std::tuple<enode *, enode *>> dummy;
for (instance const& inst : m_new_instances) { for (instance const& inst : m_new_instances) {
quantifier * q = inst.m_q; quantifier * q = inst.m_q;
if (m_context->b_internalized(q)) { if (m_context->b_internalized(q)) {

120
src/smt/smt_quantifier.cpp
View file

@ -104,6 +104,90 @@ namespace smt {
return m_plugin->is_shared(n); return m_plugin->is_shared(n);
} }
/**
\brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
equivalence class are in the log and up-to-date.
*/
void log_justification_to_root(std::ostream & log, enode *en) {
enode *root = en->get_root();
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
log_single_justification(log, it);
it->m_proof_logged_status = smt::logged_status::LOGGED;
} else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
// When the justification of an argument changes m_proof_logged_status is not reset => We need to check if the proofs of all arguments are logged.
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
const unsigned num_args = it->get_num_args();
enode *target = it->get_trans_justification().m_target;
for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(log, it->get_arg(i));
log_justification_to_root(log, target->get_arg(i));
}
it->m_proof_logged_status = smt::logged_status::LOGGED;
}
}
if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
log << "[eq-expl] #" << root->get_owner_id() << " root\n";
root->m_proof_logged_status = smt::logged_status::LOGGED;
}
}
/**
\brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
equalities needed by the step (e.g. argument equalities for congruence steps).
*/
void log_single_justification(std::ostream & out, enode *en) {
smt::literal lit;
unsigned num_args;
enode *target = en->get_trans_justification().m_target;
theory_id th_id;
switch (en->get_trans_justification().m_justification.get_kind()) {
case smt::eq_justification::kind::EQUATION:
lit = en->get_trans_justification().m_justification.get_literal();
out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
break;
case smt::eq_justification::kind::AXIOM:
out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
break;
case smt::eq_justification::kind::CONGRUENCE:
if (!en->get_trans_justification().m_justification.used_commutativity()) {
num_args = en->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(out, en->get_arg(i));
log_justification_to_root(out, target->get_arg(i));
}
out << "[eq-expl] #" << en->get_owner_id() << " cg";
for (unsigned i = 0; i < num_args; ++i) {
out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
}
out << " ; #" << target->get_owner_id() << "\n";
break;
} else {
out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
break;
}
case smt::eq_justification::kind::JUSTIFICATION:
th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
if (th_id != null_theory_id) {
symbol const theory = m().get_family_name(th_id);
out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
} else {
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
}
break;
default:
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
break;
}
}
bool add_instance(quantifier * q, app * pat, bool add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
@ -111,7 +195,7 @@ namespace smt {
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
ptr_vector<enode> & used_enodes) { vector<std::tuple<enode *, enode *>> & used_enodes) {
max_generation = std::max(max_generation, get_generation(q)); max_generation = std::max(max_generation, get_generation(q));
if (m_num_instances > m_params.m_qi_max_instances) { if (m_num_instances > m_params.m_qi_max_instances) {
return false; return false;
@ -121,15 +205,39 @@ namespace smt {
if (f) { if (f) {
if (has_trace_stream()) { if (has_trace_stream()) {
std::ostream & out = trace_stream(); std::ostream & out = trace_stream();
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id();
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
// is used. We need to make sure that all of these equalities appear in the log.
for (unsigned i = 0; i < num_bindings; ++i) {
log_justification_to_root(out, bindings[i]);
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
if (orig != nullptr) {
log_justification_to_root(out, orig);
log_justification_to_root(out, substituted);
}
}
// At this point all relevant equalities for the match are logged.
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
for (unsigned i = 0; i < num_bindings; i++) { for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing. // I don't want to use mk_pp because it creates expressions for pretty printing.
// This nasty side-effect may change the behavior of Z3. // This nasty side-effect may change the behavior of Z3.
out << " #" << bindings[i]->get_owner_id(); out << " #" << bindings[i]->get_owner_id();
} }
out << " ;"; out << " ;";
for (enode* n : used_enodes) for (auto n : used_enodes) {
out << " #" << n->get_owner_id(); enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
if (orig == nullptr)
out << " #" << substituted->get_owner_id();
else {
out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
}
}
out << "\n"; out << "\n";
} }
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
@ -296,12 +404,12 @@ namespace smt {
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
ptr_vector<enode> & used_enodes) { vector<std::tuple<enode *, enode *>> & used_enodes) {
return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes); return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes);
} }
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) { bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {
ptr_vector<enode> tmp; vector<std::tuple<enode *, enode *>> tmp;
return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp); return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp);
} }

3
src/smt/smt_quantifier.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/statistics.h" #include "util/statistics.h"
#include "util/params.h" #include "util/params.h"
#include "smt/smt_types.h" #include "smt/smt_types.h"
#include <tuple>
class proto_model; class proto_model;
struct smt_params; struct smt_params;
@ -58,7 +59,7 @@ namespace smt {
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
ptr_vector<enode> & used_enodes); vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0); bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0);
void init_search_eh(); void init_search_eh();

3
src/smt/smt_quick_checker.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "smt/smt_quick_checker.h" #include "smt/smt_quick_checker.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include <tuple>
namespace smt { namespace smt {
@ -197,7 +198,7 @@ namespace smt {
} }
bool quick_checker::process_candidates(quantifier * q, bool unsat) { bool quick_checker::process_candidates(quantifier * q, bool unsat) {
ptr_vector<enode> empty_used_enodes; vector<std::tuple<enode *, enode *>> empty_used_enodes;
buffer<unsigned> szs; buffer<unsigned> szs;
buffer<unsigned> it; buffer<unsigned> it;
for (unsigned i = 0; i < m_num_bindings; i++) { for (unsigned i = 0; i < m_num_bindings; i++) {

8
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -89,14 +89,6 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
params_ref solver_p; params_ref solver_p;
solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
params_ref no_flat_p;
no_flat_p.set_bool("flat", false);
params_ref ctx_simp_p;
ctx_simp_p.set_uint("max_depth", 32);
ctx_simp_p.set_uint("max_steps", 50000000);
params_ref big_aig_p; params_ref big_aig_p;
big_aig_p.set_bool("aig_per_assertion", false); big_aig_p.set_bool("aig_per_assertion", false);

6
src/util/mpq.h
View file

@ -714,6 +714,12 @@ public:
return temp; return temp;
} }
mpz dup(const mpz & source) {
mpz temp;
set(temp, source);
return temp;
}
void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); } void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
void swap(mpq & a, mpq & b) { void swap(mpq & a, mpq & b) {

7
src/util/trace.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#ifdef _TRACE #ifdef _TRACE
std::ofstream tout(".z3-trace"); std::ofstream tout(".z3-trace");
#endif
static bool g_enable_all_trace_tags = false; static bool g_enable_all_trace_tags = false;
static str_hashtable* g_enabled_trace_tags = nullptr; static str_hashtable* g_enabled_trace_tags = nullptr;
@ -56,13 +55,11 @@ bool is_trace_enabled(const char * tag) {
} }
void close_trace() { void close_trace() {
#ifdef _TRACE
tout.close(); tout.close();
#endif
} }
void open_trace() { void open_trace() {
#ifdef _TRACE
tout.open(".z3-trace"); tout.open(".z3-trace");
#endif
} }
#endif

17
src/util/trace.h
View file

@ -33,9 +33,6 @@ Revision History:
#ifdef _TRACE #ifdef _TRACE
extern std::ofstream tout; extern std::ofstream tout;
#define TRACE_CODE(CODE) { CODE } ((void) 0 ) #define TRACE_CODE(CODE) { CODE } ((void) 0 )
#else
#define TRACE_CODE(CODE) ((void) 0)
#endif
void enable_trace(const char * tag); void enable_trace(const char * tag);
void enable_all_trace(bool flag); void enable_all_trace(bool flag);
@ -48,6 +45,19 @@ void finalize_trace();
ADD_FINALIZER('finalize_trace();') ADD_FINALIZER('finalize_trace();')
*/ */
#else
#define TRACE_CODE(CODE) ((void) 0)
static inline void enable_trace(const char * tag) {}
static inline void enable_all_trace(bool flag) {}
static inline void disable_trace(const char * tag) {}
// On a default Visual C++ build on Windows, a non-void function either needs to return a value, or we have to add: #pragma warning(default:4716)
static inline bool is_trace_enabled(const char * tag) { return false; }
static inline void close_trace() {}
static inline void open_trace() {}
static inline void finalize_trace() {}
#endif
#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); }) #define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
#define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); }) #define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); })
@ -55,4 +65,3 @@ void finalize_trace();
#define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); }) #define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
#endif /* TRACE_H_ */ #endif /* TRACE_H_ */