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

updates to printer to get instantiations, take 1

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-25 10:47:33 -07:00
parent f0eee41ab9
commit a628e4c4e5
10 changed files with 82 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/ast/ast_pp_util.cpp
View file

@ -139,11 +139,18 @@ void ast_pp_util::pop(unsigned n) {
m_sorts.pop(n);
unsigned old_sz = m_defined_lim[m_defined_lim.size() - n];
for (unsigned i = m_defined.size(); i-- > old_sz; )
m_is_defined.mark(m_defined[i], false);
m_is_defined.mark(m_defined.get(i), false);
m_defined.shrink(old_sz);
m_defined_lim.shrink(m_defined_lim.size() - n);
}
std::ostream& ast_pp_util::display_expr_def(std::ostream& out, expr* n) {
if (is_app(n) && to_app(n)->get_num_args() == 0)
return out << mk_pp(n, m);
else
return out << "$" << n->get_id();
}
std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) {
ptr_buffer<expr> visit;
visit.push_back(n);
@ -166,13 +173,11 @@ std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) {
m_defined.push_back(n);
m_is_defined.mark(n, true);
visit.pop_back();
if (to_app(n)->get_num_args() == 0)
out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " " << mk_pp(n, m) << "\n";
else {
if (to_app(n)->get_num_args() > 0) {
out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " (";
out << to_app(n)->get_name(); // fixme
for (auto* e : *to_app(n))
out << " $" << e->get_id();
display_expr_def(out << " ", e);
out << ")\n";
}
continue;

8
src/ast/ast_pp_util.h
View file

@ -31,14 +31,14 @@ class ast_pp_util {
stacked_value<unsigned> m_decls;
stacked_value<unsigned> m_sorts;
expr_mark m_is_defined;
ptr_vector<expr> m_defined;
expr_ref_vector m_defined;
unsigned_vector m_defined_lim;
public:
decl_collector coll;
ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m) {}
ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m), m_defined(m) {}
void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u);
m_is_defined.reset(); m_defined.reset(); m_defined_lim.reset(); }
@ -65,6 +65,8 @@ class ast_pp_util {
std::ostream& define_expr(std::ostream& out, expr* f);
std::ostream& display_expr_def(std::ostream& out, expr* f);
void push();
void pop(unsigned n);

1
src/params/solver_params.pyg
View file

@ -6,6 +6,7 @@ def_module_params('solver',
('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"),
('lemmas2console', BOOL, False, 'print lemmas during search'),
('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'),
('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'),
))

52
src/sat/smt/euf_proof.cpp
View file

@ -199,27 +199,51 @@ namespace euf {
return;
if (!st.is_redundant() && !st.is_asserted())
return;
if (!visit_clause(n, lits))
return;
std::function<symbol(int)> ppth = [&](int th) {
return m.get_family_name(th);
};
expr_ref_vector clause(m);
for (unsigned i = 0; i < n; ++i) {
expr_ref e = literal2expr(lits[i]);
if (!e)
return;
clause.push_back(e);
m_clause_visitor.collect(e);
}
m_clause_visitor.display_skolem_decls(std::cout);
for (expr* e : clause)
m_clause_visitor.define_expr(std::cout, e);
if (!st.is_sat())
std::cout << "; " << sat::status_pp(st, ppth) << "\n";
display_clause(n, lits);
}
bool solver::visit_clause(unsigned n, literal const* lits) {
for (unsigned i = 0; i < n; ++i) {
expr* e = bool_var2expr(lits[i].var());
if (!e)
return false;
visit_expr(e);
}
return true;
}
void solver::display_clause(unsigned n, literal const* lits) {
std::cout << "(assert (or";
for (expr* e : clause)
std::cout << " $" << e->get_id();
for (unsigned i = 0; i < n; ++i) {
expr* e = bool_var2expr(lits[i].var());
if (lits[i].sign())
m_clause_visitor.display_expr_def(std::cout << " (not ", e) << ")";
else
m_clause_visitor.display_expr_def(std::cout << " ", e);
}
std::cout << "))\n";
}
void solver::visit_expr(expr* e) {
m_clause_visitor.collect(e);
m_clause_visitor.display_skolem_decls(std::cout);
m_clause_visitor.define_expr(std::cout, e);
}
void solver::display_expr(expr* e) {
m_clause_visitor.display_expr_def(std::cout, e);
}
}

5
src/sat/smt/euf_solver.h
View file

@ -185,6 +185,7 @@ namespace euf {
ast_pp_util m_clause_visitor;
void log_clause(unsigned n, literal const* lits, sat::status st);
// relevancy
//bool_vector m_relevant_expr_ids;
//bool_vector m_relevant_visited;
@ -348,6 +349,10 @@ namespace euf {
void drat_bool_def(sat::bool_var v, expr* n);
void drat_eq_def(sat::literal lit, expr* eq);
void drat_log_expr(expr* n);
bool visit_clause(unsigned n, literal const* lits);
void display_clause(unsigned n, literal const* lits);
void visit_expr(expr* e);
void display_expr(expr* e);
// decompile
bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,

2
src/sat/smt/q_ematch.cpp
View file

@ -382,7 +382,7 @@ namespace q {
lits.push_back(~j.m_clause.m_literal);
for (unsigned i = 0; i < j.m_clause.size(); ++i)
lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i]));
m_qs.log_instantiation(lits);
m_qs.log_instantiation(lits, &j);
m_qs.add_clause(lits);
}

18
src/sat/smt/q_solver.cpp
View file

@ -24,6 +24,7 @@ Author:
#include "sat/smt/euf_solver.h"
#include "sat/smt/sat_th.h"
#include "qe/lite/qe_lite.h"
#include <iostream>
namespace q {
@ -356,7 +357,22 @@ namespace q {
m_ematch.get_antecedents(l, idx, r, probing);
}
void solver::log_instantiation(unsigned n, sat::literal const* lits) {
void solver::log_instantiation(unsigned n, sat::literal const* lits, justification* j) {
TRACE("q", for (unsigned i = 0; i < n; ++i) tout << literal2expr(lits[i]) << "\n";);
if (get_config().m_instantiations2console) {
ctx.visit_clause(n, lits);
if (j) {
for (unsigned i = 0; i < j->m_clause.num_decls(); ++i)
ctx.visit_expr(j->m_binding[i]->get_expr());
std::cout << "; (instantiation";
for (unsigned i = 0; i < j->m_clause.num_decls(); ++i) {
std::cout << " ";
ctx.display_expr(j->m_binding[i]->get_expr());
}
std::cout << ")\n";
}
ctx.display_clause(n, lits);
}
}
}

6
src/sat/smt/q_solver.h
View file

@ -88,9 +88,9 @@ namespace q {
sat::literal_vector const& universal() const { return m_universal; }
quantifier* flatten(quantifier* q);
void log_instantiation(sat::literal q, sat::literal i) { sat::literal lits[2] = { q, i }; log_instantiation(2, lits); }
void log_instantiation(sat::literal_vector const& lits) { log_instantiation(lits.size(), lits.data()); }
void log_instantiation(unsigned n, sat::literal const* lits);
void log_instantiation(sat::literal q, sat::literal i, justification* j = nullptr) { sat::literal lits[2] = { q, i }; log_instantiation(2, lits, j); }
void log_instantiation(sat::literal_vector const& lits, justification* j) { log_instantiation(lits.size(), lits.data(), j); }
void log_instantiation(unsigned n, sat::literal const* lits, justification* j);
};
}

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

@ -63,6 +63,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
solver_params sp(_p);
m_axioms2files = sp.axioms2files();
m_lemmas2console = sp.lemmas2console();
m_instantiations2console = sp.instantiations2console();
}
void smt_params::updt_params(params_ref const & p) {

1
src/smt/params/smt_params.h
View file

@ -175,6 +175,7 @@ struct smt_params : public preprocessor_params,
// -----------------------------------
bool m_axioms2files = false;
bool m_lemmas2console = false;
bool m_instantiations2console = false;
symbol m_logic = symbol::null;
// -----------------------------------