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

change default behavior of solver pretty printer to include declarations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-06 18:57:11 +02:00
parent 6780784bcf
commit a3c43c34fb
6 changed files with 110 additions and 97 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

81
src/ast/ast_pp_util.h Normal file
View file

@ -0,0 +1,81 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
ast_pp_util.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2015-8-6.
Revision History:
--*/
#ifndef AST_PP_UTIL_H_
#define AST_PP_UTIL_H_
#include "decl_collector.h"
#include "ast_smt2_pp.h"
#include "ast_smt_pp.h"
class ast_pp_util {
ast_manager& m;
public:
decl_collector coll;
ast_pp_util(ast_manager& m): m(m), coll(m, false) {}
void collect(expr* e) {
coll.visit(e);
}
void collect(unsigned n, expr* const* es) {
for (unsigned i = 0; i < n; ++i) {
coll.visit(es[i]);
}
}
void collect(expr_ref_vector const& es) {
collect(es.size(), es.c_ptr());
}
void display_decls(std::ostream& out) {
smt2_pp_environment_dbg env(m);
unsigned n = coll.get_num_sorts();
for (unsigned i = 0; i < n; ++i) {
ast_smt2_pp(out, coll.get_sorts()[i], env);
}
n = coll.get_num_decls();
for (unsigned i = 0; i < n; ++i) {
ast_smt2_pp(out, coll.get_func_decls()[i], env);
out << "\n";
}
}
void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true) {
if (neat) {
smt2_pp_environment_dbg env(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
out << "(assert ";
ast_smt2_pp(out, fmls[i], env);
out << ")\n";
}
}
else {
ast_smt_pp ll_smt2_pp(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
out << "(assert ";
ll_smt2_pp.display_expr_smt2(out, fmls[i]);
out << ")\n";
}
}
}
};
#endif /* AST_PP_UTIL_H_ */

2
src/ast/decl_collector.h
View file

@ -43,6 +43,8 @@ public:
ast_manager & m() { return m_manager; }
void visit(ast * n);
void visit(unsigned n, expr* const* es);
void visit(expr_ref_vector const& es);
unsigned get_num_sorts() const { return m_sorts.size(); }
unsigned get_num_decls() const { return m_decls.size(); }

56
src/muz/base/dl_context.cpp
View file

@ -28,6 +28,7 @@ Revision History:
#include"datatype_decl_plugin.h"
#include"scoped_proof.h"
#include"fixedpoint_params.hpp"
#include"ast_pp_util.h"
namespace datalog {
@ -957,31 +958,13 @@ namespace datalog {
}
// NB: algebraic data-types declarations will not be printed.
class free_func_visitor {
ast_manager& m;
func_decl_set m_funcs;
obj_hashtable<sort> m_sorts;
public:
free_func_visitor(ast_manager& m): m(m) {}
void operator()(var * n) { }
void operator()(app * n) {
m_funcs.insert(n->get_decl());
sort* s = m.get_sort(n);
if (s->get_family_id() == null_family_id) {
m_sorts.insert(s);
}
}
void operator()(quantifier * n) { }
func_decl_set& funcs() { return m_funcs; }
obj_hashtable<sort>& sorts() { return m_sorts; }
};
static void collect_free_funcs(unsigned sz, expr* const* exprs,
expr_mark& visited, free_func_visitor& v,
ast_pp_util& v,
mk_fresh_name& fresh_names) {
v.collect(sz, exprs);
for (unsigned i = 0; i < sz; ++i) {
expr* e = exprs[i];
for_each_expr(v, visited, e);
while (is_quantifier(e)) {
e = to_quantifier(e)->get_expr();
}
@ -1051,8 +1034,7 @@ namespace datalog {
void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
ast_manager& m = get_manager();
free_func_visitor visitor(m);
expr_mark visited;
ast_pp_util visitor(m);
func_decl_set rels;
unsigned num_axioms = m_background.size();
expr* const* axioms = m_background.c_ptr();
@ -1070,14 +1052,13 @@ namespace datalog {
smt2_pp_environment_dbg env(m);
mk_fresh_name fresh_names;
collect_free_funcs(num_axioms, axioms, visited, visitor, fresh_names);
collect_free_funcs(rules.size(), rules.c_ptr(), visited, visitor, fresh_names);
collect_free_funcs(queries.size(), queries.c_ptr(), visited, visitor, fresh_names);
collect_free_funcs(num_axioms, axioms, visitor, fresh_names);
collect_free_funcs(rules.size(), rules.c_ptr(), visitor, fresh_names);
collect_free_funcs(queries.size(), queries.c_ptr(), visitor, fresh_names);
func_decl_set funcs;
func_decl_set::iterator it = visitor.funcs().begin();
func_decl_set::iterator end = visitor.funcs().end();
for (; it != end; ++it) {
func_decl* f = *it;
unsigned sz = visitor.coll.get_num_decls();
for (unsigned i = 0; i < sz; ++i) {
func_decl* f = visitor.coll.get_func_decls()[i];
if (f->get_family_id() != null_family_id) {
//
}
@ -1092,20 +1073,9 @@ namespace datalog {
if (!use_fixedpoint_extensions) {
out << "(set-logic HORN)\n";
}
it = funcs.begin(), end = funcs.end();
obj_hashtable<sort>& sorts = visitor.sorts();
obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
for (; sit != send; ++sit) {
PP(*sit);
}
for (; it != end; ++it) {
func_decl* f = *it;
PP(f);
out << "\n";
}
it = rels.begin(); end = rels.end();
visitor.display_decls(out);
func_decl_set::iterator it = rels.begin(), end = rels.end();
for (; it != end; ++it) {
func_decl* f = *it;
out << "(declare-rel " << f->get_name() << " (";

60
src/opt/opt_context.cpp
View file

@ -40,6 +40,7 @@ Notes:
#include "pb_decl_plugin.h"
#include "ast_smt_pp.h"
#include "filter_model_converter.h"
#include "ast_pp_util.h"
namespace opt {
@ -1255,44 +1256,13 @@ namespace opt {
m_pp_neat = _p.pp_neat();
}
typedef obj_hashtable<func_decl> func_decl_set;
struct context::free_func_visitor {
ast_manager& m;
func_decl_set m_funcs;
obj_hashtable<sort> m_sorts;
expr_mark m_visited;
public:
free_func_visitor(ast_manager& m): m(m) {}
void operator()(var * n) { }
void operator()(app * n) {
if (n->get_family_id() == null_family_id) {
m_funcs.insert(n->get_decl());
}
sort* s = m.get_sort(n);
if (s->get_family_id() == null_family_id) {
m_sorts.insert(s);
}
}
void operator()(quantifier * n) { }
func_decl_set& funcs() { return m_funcs; }
obj_hashtable<sort>& sorts() { return m_sorts; }
void collect(expr* e) {
for_each_expr(*this, m_visited, e);
}
};
std::string context::to_string() const {
smt2_pp_environment_dbg env(m);
ast_smt_pp ll_smt2_pp(m);
free_func_visitor visitor(m);
ast_pp_util visitor(m);
std::ostringstream out;
#define PP(_e_) ast_smt2_pp(out, _e_, env);
#define PPE(_e_) if (m_pp_neat) ast_smt2_pp(out, _e_, env); else ll_smt2_pp.display_expr_smt2(out, _e_);
for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
visitor.collect(m_scoped_state.m_hard[i]);
}
visitor.collect(m_scoped_state.m_hard);
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_scoped_state.m_objectives[i];
switch(obj.m_type) {
@ -1301,9 +1271,7 @@ namespace opt {
visitor.collect(obj.m_term);
break;
case O_MAXSMT:
for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
visitor.collect(obj.m_terms[j]);
}
visitor.collect(obj.m_terms);
break;
default:
UNREACHABLE();
@ -1311,22 +1279,8 @@ namespace opt {
}
}
obj_hashtable<sort>::iterator sit = visitor.sorts().begin();
obj_hashtable<sort>::iterator send = visitor.sorts().end();
for (; sit != send; ++sit) {
PP(*sit);
}
func_decl_set::iterator it = visitor.funcs().begin();
func_decl_set::iterator end = visitor.funcs().end();
for (; it != end; ++it) {
PP(*it);
out << "\n";
}
for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
out << "(assert ";
PPE(m_scoped_state.m_hard[i]);
out << ")\n";
}
visitor.display_decls(out);
visitor.display_asserts(out, m_scoped_state.m_hard, m_pp_neat);
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_scoped_state.m_objectives[i];
switch(obj.m_type) {

1
src/opt/opt_context.h
View file

@ -68,7 +68,6 @@ namespace opt {
public opt_wrapper,
public pareto_callback,
public maxsat_context {
struct free_func_visitor;
typedef map<symbol, maxsmt*, symbol_hash_proc, symbol_eq_proc> map_t;
typedef map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> map_id;
typedef vector<std::pair<inf_eps, inf_eps> > bounds_t;

7
src/solver/tactic2solver.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include"solver_na2as.h"
#include"tactic.h"
#include"ast_smt2_pp.h"
#include"ast_pp_util.h"
/**
\brief Simulates the incremental solver interface using a tactic.
@ -221,6 +222,11 @@ expr * tactic2solver::get_assertion(unsigned idx) const {
}
void tactic2solver::display(std::ostream & out) const {
ast_pp_util visitor(m_assertions.m());
visitor.collect(m_assertions);
visitor.display_decls(out);
visitor.display_asserts(out, m_assertions, true);
#if 0
ast_manager & m = m_assertions.m();
unsigned num = m_assertions.size();
out << "(solver";
@ -228,6 +234,7 @@ void tactic2solver::display(std::ostream & out) const {
out << "\n " << mk_ismt2_pp(m_assertions.get(i), m, 2);
}
out << ")";
#endif
}
solver * mk_tactic2solver(ast_manager & m,