mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

preparing to split framework

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-21 17:31:45 -07:00
parent c4711ac472
commit ffaf88798d
8 changed files with 42 additions and 137 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_make.py
View file

@ -8,7 +8,7 @@
############################################
from mk_util import *
set_build_dir('build-test')
set_build_dir('build')
set_src_dir('src')
set_modes(['Debug', 'Release'])
set_platforms(['Win32', 'x64'])

1
src/framework/cmd_context.cpp
View file

@ -1601,3 +1601,4 @@ std::ostream & operator<<(std::ostream & out, cmd_context::status st) {
}
return out;
}

15
src/framework/cmd_context.h
View file

@ -23,6 +23,7 @@ Notes:
#include<sstream>
#include"ast.h"
#include"ast_printer.h"
#include"pdecl.h"
#include"dictionary.h"
#include"solver.h"
@ -111,7 +112,7 @@ struct builtin_decl {
builtin_decl(family_id fid, decl_kind k, builtin_decl * n = 0):m_fid(fid), m_decl(k), m_next(n) {}
};
class cmd_context : public progress_callback, public tactic_manager {
class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
public:
enum status {
UNSAT, SAT, UNKNOWN
@ -329,8 +330,8 @@ public:
void reset_user_tactics();
void set_regular_stream(char const * name) { m_regular.set(name); }
void set_diagnostic_stream(char const * name);
std::ostream & regular_stream() { return *m_regular; }
std::ostream & diagnostic_stream() { return *m_diagnostic; }
virtual std::ostream & regular_stream() { return *m_regular; }
virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }
char const * get_regular_stream_name() const { return m_regular.name(); }
char const * get_diagnostic_stream_name() const { return m_diagnostic.name(); }
typedef dictionary<cmd*>::iterator cmd_iterator;
@ -385,10 +386,10 @@ public:
void pp(func_decl * f, format_ns::format_ref & r) const;
void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const;
void pp(expr * n, format_ns::format_ref & r) const;
void display(std::ostream & out, sort * s, unsigned indent = 0) const;
void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const;
void display(std::ostream & out, expr * n, unsigned indent = 0) const;
void display(std::ostream & out, func_decl * f, unsigned indent = 0) const;
virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const;
virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const;
virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const;
virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const;
// dump assertions in out using the pretty printer.
void dump_assertions(std::ostream & out) const;

41
src/framework/goal.cpp
View file

@ -17,7 +17,6 @@ Revision History:
--*/
#include"goal.h"
#include"cmd_context.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
#include"for_each_expr.h"
@ -235,17 +234,17 @@ void goal::reset() {
m_inconsistent = false;
}
void goal::display(cmd_context & ctx, std::ostream & out) const {
void goal::display(ast_printer & prn, std::ostream & out) const {
out << "(goal";
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
out << "\n ";
ctx.display(out, form(i), 2);
prn.display(out, form(i), 2);
}
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
}
void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) const {
void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) const {
ptr_vector<expr> deps;
obj_hashtable<expr> to_pp;
out << "(goal";
@ -267,7 +266,7 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons
}
}
out << "\n ";
ctx.display(out, form(i), 2);
prn.display(out, form(i), 2);
}
if (!to_pp.empty()) {
out << "\n :dependencies-definitions (";
@ -276,7 +275,7 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons
for (; it != end; ++it) {
expr * d = *it;
out << "\n (#" << d->get_id() << "\n ";
ctx.display(out, d, 2);
prn.display(out, d, 2);
out << ")";
}
out << ")";
@ -308,11 +307,11 @@ void goal::display_with_dependencies(std::ostream & out) const {
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
}
void goal::display(cmd_context & ctx) const {
void goal::display(ast_printer_context & ctx) const {
display(ctx, ctx.regular_stream());
}
void goal::display_with_dependencies(cmd_context & ctx) const {
void goal::display_with_dependencies(ast_printer_context & ctx) const {
display_with_dependencies(ctx, ctx.regular_stream());
}
@ -546,32 +545,6 @@ bool goal::is_well_sorted() const {
return true;
}
/**
\brief Assert expressions from ctx into t.
*/
void assert_exprs_from(cmd_context const & ctx, goal & t) {
if (ctx.produce_proofs() && ctx.produce_unsat_cores())
throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores");
ast_manager & m = t.m();
bool proofs_enabled = t.proofs_enabled();
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0);
}
if (ctx.produce_unsat_cores()) {
SASSERT(!ctx.produce_proofs());
it = ctx.begin_assumptions();
end = ctx.end_assumptions();
for (; it != end; ++it) {
t.assert_expr(*it, 0, m.mk_leaf(*it));
}
}
else {
SASSERT(ctx.begin_assumptions() == ctx.end_assumptions());
}
}
/**
\brief Translate the assertion set to a new one that uses a different ast_manager.
*/

13
src/framework/goal.h
View file

@ -30,13 +30,12 @@ Revision History:
#include"ast.h"
#include"ast_translation.h"
#include"ast_printer.h"
#include"for_each_expr.h"
#include"ref.h"
#include"ref_vector.h"
#include"ref_buffer.h"
class cmd_context;
class goal {
public:
enum precision {
@ -172,14 +171,14 @@ public:
void elim_true();
void elim_redundancies();
void display(cmd_context & ctx, std::ostream & out) const;
void display(cmd_context & ctx) const;
void display(ast_printer & prn, std::ostream & out) const;
void display(ast_printer_context & ctx) const;
void display(std::ostream & out) const;
void display_ll(std::ostream & out) const;
void display_as_and(std::ostream & out) const;
void display_dimacs(std::ostream & out) const;
void display_with_dependencies(cmd_context & ctx, std::ostream & out) const;
void display_with_dependencies(cmd_context & ctx) const;
void display_with_dependencies(ast_printer & prn, std::ostream & out) const;
void display_with_dependencies(ast_printer_context & ctx) const;
void display_with_dependencies(std::ostream & out) const;
bool sat_preserved() const {
@ -220,8 +219,6 @@ inline bool is_decided_sat(GoalCollection const & c) { return c.size() == 1 && c
template<typename GoalCollection>
inline bool is_decided_unsat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_unsat(); }
void assert_exprs_from(cmd_context const & ctx, goal & t);
template<typename ForEachProc>
void for_each_expr_at(ForEachProc& proc, goal const & s) {
expr_mark visited;

93
src/framework/tactic.cpp
View file

@ -81,25 +81,17 @@ void report_tactic_progress(char const * id, unsigned val) {
}
}
class skip_tactic : public tactic {
public:
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
result.reset();
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
}
virtual void cleanup() {}
virtual tactic * translate(ast_manager & m) { return this; }
};
void skip_tactic::operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
result.reset();
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
}
tactic * mk_skip_tactic() {
return alloc(skip_tactic);
@ -163,69 +155,6 @@ tactic * mk_trace_tactic(char const * tag) {
return alloc(trace_tactic, tag);
}
class echo_tactic : public skip_tactic {
cmd_context & m_ctx;
char const * m_msg;
bool m_newline;
public:
echo_tactic(cmd_context & ctx, char const * msg, bool newline):m_ctx(ctx), m_msg(msg), m_newline(newline) {}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
#pragma omp critical (echo_tactic)
{
m_ctx.diagnostic_stream() << m_msg;
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
}
};
tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline) {
return alloc(echo_tactic, ctx, msg, newline);
}
class probe_value_tactic : public skip_tactic {
cmd_context & m_ctx;
char const * m_msg;
probe * m_p;
bool m_newline;
public:
probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline):m_ctx(ctx), m_msg(msg), m_p(p), m_newline(newline) {
SASSERT(m_p);
m_p->inc_ref();
}
~probe_value_tactic() {
m_p->dec_ref();
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
double val = (*m_p)(*(in.get())).get_value();
#pragma omp critical (probe_value_tactic)
{
if (m_msg)
m_ctx.diagnostic_stream() << m_msg << " ";
m_ctx.diagnostic_stream() << val;
if (m_newline)
m_ctx.diagnostic_stream() << std::endl;
}
skip_tactic::operator()(in, result, mc, pc, core);
}
};
tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline) {
return alloc(probe_value_tactic, ctx, msg, p, newline);
}
class fail_if_undecided_tactic : public skip_tactic {
public:
fail_if_undecided_tactic() {}

12
src/framework/tactic.h
View file

@ -117,17 +117,19 @@ public:
void report_tactic_progress(char const * id, unsigned val);
class skip_tactic : public tactic {
public:
virtual void operator()(goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
virtual void cleanup() {}
virtual tactic * translate(ast_manager & m) { return this; }
};
tactic * mk_skip_tactic();
tactic * mk_fail_tactic();
tactic * mk_fail_if_undecided_tactic();
tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl);
tactic * mk_trace_tactic(char const * tag);
tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline = true);
// Display the value returned by p in the diagnostic_stream
class probe;
tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline = true);
class tactic_factory {
public:

2
src/framework/tactic_cmds.cpp
View file

@ -30,6 +30,8 @@ Notes:
#include"tactical.h"
#include"probe.h"
#include"check_sat_result.h"
#include"cmd_context_to_goal.h"
#include"echo_tactic.h"
tactic_cmd::~tactic_cmd() {
dealloc(m_factory);