mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
Trailing whitespace removed.
This commit is contained in:
Christoph M. Wintersteiger
parent
11b6676e8f
commit
949ad4d2fc
2 changed files with 61 additions and 63 deletions
|
|
@ -131,11 +131,11 @@ bool func_decls::clash(func_decl * f) const {
|
|||
func_decl * g = *it;
|
||||
if (g == f)
|
||||
continue;
|
||||
if (g->get_arity() != f->get_arity())
|
||||
if (g->get_arity() != f->get_arity())
|
||||
continue;
|
||||
unsigned num = g->get_arity();
|
||||
unsigned i;
|
||||
for (i = 0; i < num; i++)
|
||||
for (i = 0; i < num; i++)
|
||||
if (g->get_domain(i) != f->get_domain(i))
|
||||
break;
|
||||
if (i == num)
|
||||
|
|
@ -273,12 +273,12 @@ public:
|
|||
virtual array_util & get_arutil() { return m_arutil; }
|
||||
virtual fpa_util & get_futil() { return m_futil; }
|
||||
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
|
||||
virtual bool uses(symbol const & s) const {
|
||||
return
|
||||
virtual bool uses(symbol const & s) const {
|
||||
return
|
||||
m_owner.m_builtin_decls.contains(s) ||
|
||||
m_owner.m_func_decls.contains(s);
|
||||
}
|
||||
virtual format_ns::format * pp_sort(sort * s) {
|
||||
virtual format_ns::format * pp_sort(sort * s) {
|
||||
return m_owner.pp(s);
|
||||
}
|
||||
virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len) {
|
||||
|
|
@ -309,7 +309,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
|
|||
m_main_ctx(main_ctx),
|
||||
m_logic(l),
|
||||
m_interactive_mode(false),
|
||||
m_global_decls(false),
|
||||
m_global_decls(false),
|
||||
m_print_success(m_params.m_smtlib2_compliant),
|
||||
m_random_seed(0),
|
||||
m_produce_unsat_cores(false),
|
||||
|
|
@ -318,7 +318,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
|
|||
m_numeral_as_real(false),
|
||||
m_ignore_check(false),
|
||||
m_exit_on_error(false),
|
||||
m_manager(m),
|
||||
m_manager(m),
|
||||
m_own_manager(m == 0),
|
||||
m_manager_initialized(false),
|
||||
m_pmanager(0),
|
||||
|
|
@ -331,7 +331,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
|
|||
install_core_tactic_cmds(*this);
|
||||
install_interpolant_cmds(*this);
|
||||
SASSERT(m != 0 || !has_manager());
|
||||
if (m_main_ctx) {
|
||||
if (m_main_ctx) {
|
||||
set_verbose_stream(diagnostic_stream());
|
||||
}
|
||||
}
|
||||
|
|
@ -343,7 +343,7 @@ cmd_context::~cmd_context() {
|
|||
finalize_cmds();
|
||||
finalize_tactic_cmds();
|
||||
finalize_probes();
|
||||
reset(true);
|
||||
reset(true);
|
||||
m_solver = 0;
|
||||
m_check_sat_result = 0;
|
||||
}
|
||||
|
|
@ -351,7 +351,7 @@ cmd_context::~cmd_context() {
|
|||
void cmd_context::set_cancel(bool f) {
|
||||
if (m_solver) {
|
||||
if (f) {
|
||||
m_solver->cancel();
|
||||
m_solver->cancel();
|
||||
}
|
||||
else {
|
||||
m_solver->reset_cancel();
|
||||
|
|
@ -412,20 +412,20 @@ void cmd_context::set_produce_interpolants(bool f) {
|
|||
// set_solver_factory(mk_smt_solver_factory());
|
||||
}
|
||||
|
||||
bool cmd_context::produce_models() const {
|
||||
bool cmd_context::produce_models() const {
|
||||
return m_params.m_model;
|
||||
}
|
||||
|
||||
bool cmd_context::produce_proofs() const {
|
||||
bool cmd_context::produce_proofs() const {
|
||||
return m_params.m_proof;
|
||||
}
|
||||
|
||||
bool cmd_context::produce_interpolants() const {
|
||||
bool cmd_context::produce_interpolants() const {
|
||||
// FIXME currently synonym for produce_proofs
|
||||
return m_params.m_proof;
|
||||
}
|
||||
|
||||
bool cmd_context::produce_unsat_cores() const {
|
||||
bool cmd_context::produce_unsat_cores() const {
|
||||
return m_params.m_unsat_core;
|
||||
}
|
||||
|
||||
|
|
@ -497,7 +497,7 @@ void cmd_context::load_plugin(symbol const & name, bool install, svector<family_
|
|||
}
|
||||
|
||||
bool cmd_context::logic_has_arith_core(symbol const & s) const {
|
||||
return
|
||||
return
|
||||
s == "QF_LRA" ||
|
||||
s == "QF_LIA" ||
|
||||
s == "QF_RDL" ||
|
||||
|
|
@ -527,8 +527,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
|
|||
s == "UFNRA" ||
|
||||
s == "UFNIRA" ||
|
||||
s == "UFNIA" ||
|
||||
s == "LIA" ||
|
||||
s == "LRA" ||
|
||||
s == "LIA" ||
|
||||
s == "LRA" ||
|
||||
s == "QF_FP" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "QF_BVFP" ||
|
||||
|
|
@ -568,7 +568,7 @@ bool cmd_context::logic_has_seq_core(symbol const& s) const {
|
|||
}
|
||||
|
||||
bool cmd_context::logic_has_seq() const {
|
||||
return !has_logic() || logic_has_seq_core(m_logic);
|
||||
return !has_logic() || logic_has_seq_core(m_logic);
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_fpa_core(symbol const& s) const {
|
||||
|
|
@ -580,7 +580,7 @@ bool cmd_context::logic_has_fpa() const {
|
|||
}
|
||||
|
||||
bool cmd_context::logic_has_array_core(symbol const & s) const {
|
||||
return
|
||||
return
|
||||
s == "QF_AX" ||
|
||||
s == "QF_AUFLIA" ||
|
||||
s == "QF_ALIA" ||
|
||||
|
|
@ -591,8 +591,8 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
|
|||
s == "AUFLIRA" ||
|
||||
s == "AUFNIA" ||
|
||||
s == "AUFNIRA" ||
|
||||
s == "AUFBV" ||
|
||||
s == "ABV" ||
|
||||
s == "AUFBV" ||
|
||||
s == "ABV" ||
|
||||
s == "QF_ABV" ||
|
||||
s == "QF_AUFBV" ||
|
||||
s == "HORN";
|
||||
|
|
@ -637,7 +637,7 @@ void cmd_context::init_manager_core(bool new_manager) {
|
|||
load_plugin(symbol("datatype"), logic_has_datatype(), fids);
|
||||
load_plugin(symbol("seq"), logic_has_seq(), fids);
|
||||
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
|
||||
|
||||
|
||||
svector<family_id>::iterator it = fids.begin();
|
||||
svector<family_id>::iterator end = fids.end();
|
||||
for (; it != end; ++it) {
|
||||
|
|
@ -686,8 +686,8 @@ void cmd_context::init_external_manager() {
|
|||
}
|
||||
|
||||
bool cmd_context::supported_logic(symbol const & s) const {
|
||||
return s == "QF_UF" || s == "UF" ||
|
||||
logic_has_arith_core(s) || logic_has_bv_core(s) ||
|
||||
return s == "QF_UF" || s == "UF" ||
|
||||
logic_has_arith_core(s) || logic_has_bv_core(s) ||
|
||||
logic_has_array_core(s) || logic_has_seq_core(s) ||
|
||||
logic_has_horn(s) || logic_has_fpa_core(s);
|
||||
}
|
||||
|
|
@ -695,11 +695,11 @@ bool cmd_context::supported_logic(symbol const & s) const {
|
|||
bool cmd_context::set_logic(symbol const & s) {
|
||||
if (has_logic())
|
||||
throw cmd_exception("the logic has already been set");
|
||||
if (has_manager() && m_main_ctx)
|
||||
throw cmd_exception("logic must be set before initialization");
|
||||
if (has_manager() && m_main_ctx)
|
||||
throw cmd_exception("logic must be set before initialization");
|
||||
if (!supported_logic(s)) {
|
||||
if (m_params.m_smtlib2_compliant) {
|
||||
return false;
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
warning_msg("unknown logic, ignoring set-logic command");
|
||||
|
|
@ -719,10 +719,10 @@ bool cmd_context::set_logic(symbol const & s) {
|
|||
return true;
|
||||
}
|
||||
|
||||
std::string cmd_context::reason_unknown() const {
|
||||
std::string cmd_context::reason_unknown() const {
|
||||
if (m_check_sat_result.get() == 0)
|
||||
throw cmd_exception("state of the most recent check-sat command is not unknown");
|
||||
return m_check_sat_result->reason_unknown();
|
||||
return m_check_sat_result->reason_unknown();
|
||||
}
|
||||
|
||||
bool cmd_context::is_func_decl(symbol const & s) const {
|
||||
|
|
@ -865,7 +865,7 @@ static builtin_decl const & peek_builtin_decl(builtin_decl const & first, family
|
|||
return first;
|
||||
}
|
||||
|
||||
func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
|
||||
func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
|
||||
unsigned arity, sort * const * domain, sort * range) const {
|
||||
builtin_decl d;
|
||||
if (m_builtin_decls.find(s, d)) {
|
||||
|
|
@ -891,7 +891,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
|
|||
throw cmd_exception("invalid function declaration reference, invalid builtin reference ", s);
|
||||
return f;
|
||||
}
|
||||
|
||||
|
||||
if (m_macros.contains(s))
|
||||
throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
|
||||
|
||||
|
|
@ -907,7 +907,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
|
|||
throw cmd_exception("invalid function declaration reference, unknown function ", s);
|
||||
return f;
|
||||
}
|
||||
|
||||
|
||||
psort_decl * cmd_context::find_psort_decl(symbol const & s) const {
|
||||
psort_decl * p = 0;
|
||||
m_psort_decls.find(s, p);
|
||||
|
|
@ -1222,7 +1222,7 @@ void cmd_context::reset(bool finalize) {
|
|||
// reinit cmd_context if this is not a finalization step
|
||||
if (!finalize)
|
||||
init_external_manager();
|
||||
else
|
||||
else
|
||||
m_manager_initialized = false;
|
||||
}
|
||||
}
|
||||
|
|
@ -1272,14 +1272,14 @@ void cmd_context::push() {
|
|||
s.m_macros_stack_lim = m_macros_stack.size();
|
||||
s.m_aux_pdecls_lim = m_aux_pdecls.size();
|
||||
s.m_assertions_lim = m_assertions.size();
|
||||
if (m_solver)
|
||||
if (m_solver)
|
||||
m_solver->push();
|
||||
if (m_opt)
|
||||
if (m_opt)
|
||||
m_opt->push();
|
||||
}
|
||||
|
||||
void cmd_context::push(unsigned n) {
|
||||
for (unsigned i = 0; i < n; i++)
|
||||
for (unsigned i = 0; i < n; i++)
|
||||
push();
|
||||
}
|
||||
|
||||
|
|
@ -1371,7 +1371,7 @@ void cmd_context::pop(unsigned n) {
|
|||
if (m_solver) {
|
||||
m_solver->pop(n);
|
||||
}
|
||||
if (m_opt)
|
||||
if (m_opt)
|
||||
m_opt->pop(n);
|
||||
unsigned new_lvl = lvl - n;
|
||||
scope & s = m_scopes[new_lvl];
|
||||
|
|
@ -1523,8 +1523,8 @@ void cmd_context::validate_check_sat_result(lbool r) {
|
|||
}
|
||||
}
|
||||
|
||||
void cmd_context::set_diagnostic_stream(char const * name) {
|
||||
m_diagnostic.set(name);
|
||||
void cmd_context::set_diagnostic_stream(char const * name) {
|
||||
m_diagnostic.set(name);
|
||||
if (m_main_ctx) {
|
||||
set_warning_stream(&(*m_diagnostic));
|
||||
set_verbose_stream(diagnostic_stream());
|
||||
|
|
@ -1536,15 +1536,15 @@ struct contains_array_op_proc {
|
|||
family_id m_array_fid;
|
||||
contains_array_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")) {}
|
||||
void operator()(var * n) {}
|
||||
void operator()(app * n) {
|
||||
void operator()(app * n) {
|
||||
if (n->get_family_id() != m_array_fid)
|
||||
return;
|
||||
decl_kind k = n->get_decl_kind();
|
||||
if (k == OP_AS_ARRAY ||
|
||||
k == OP_STORE ||
|
||||
k == OP_ARRAY_MAP ||
|
||||
if (k == OP_AS_ARRAY ||
|
||||
k == OP_STORE ||
|
||||
k == OP_ARRAY_MAP ||
|
||||
k == OP_CONST_ARRAY)
|
||||
throw found();
|
||||
throw found();
|
||||
}
|
||||
void operator()(quantifier * n) {}
|
||||
};
|
||||
|
|
@ -1553,7 +1553,7 @@ struct contains_array_op_proc {
|
|||
\brief Check if the current model satisfies the quantifier free formulas.
|
||||
*/
|
||||
void cmd_context::validate_model() {
|
||||
if (!validate_model_enabled())
|
||||
if (!validate_model_enabled())
|
||||
return;
|
||||
if (!is_model_available())
|
||||
return;
|
||||
|
|
@ -1562,8 +1562,8 @@ void cmd_context::validate_model() {
|
|||
SASSERT(md.get() != 0);
|
||||
params_ref p;
|
||||
p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
|
||||
p.set_uint("sort_store", true);
|
||||
p.set_bool("completion", true);
|
||||
p.set_uint("sort_store", true);
|
||||
p.set_bool("completion", true);
|
||||
model_evaluator evaluator(*(md.get()), p);
|
||||
contains_array_op_proc contains_array(m());
|
||||
{
|
||||
|
|
@ -1612,8 +1612,6 @@ void cmd_context::mk_solver() {
|
|||
m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
|
||||
}
|
||||
|
||||
|
||||
|
||||
void cmd_context::set_interpolating_solver_factory(solver_factory * f) {
|
||||
SASSERT(!has_manager());
|
||||
m_interpolating_solver_factory = f;
|
||||
|
|
@ -1718,7 +1716,7 @@ void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const {
|
|||
void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
|
||||
format_ns::format_ref f(format_ns::fm(m()));
|
||||
f = pp(s);
|
||||
if (indent > 0)
|
||||
if (indent > 0)
|
||||
f = format_ns::mk_indent(m(), indent, f);
|
||||
::pp(out, f.get(), m());
|
||||
}
|
||||
|
|
@ -1726,7 +1724,7 @@ void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
|
|||
void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
|
||||
format_ns::format_ref f(format_ns::fm(m()));
|
||||
pp(n, num_vars, var_prefix, f, var_names);
|
||||
if (indent > 0)
|
||||
if (indent > 0)
|
||||
f = format_ns::mk_indent(m(), indent, f);
|
||||
::pp(out, f.get(), m());
|
||||
}
|
||||
|
|
@ -1739,7 +1737,7 @@ void cmd_context::display(std::ostream & out, expr * n, unsigned indent) const {
|
|||
void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) const {
|
||||
format_ns::format_ref f(format_ns::fm(m()));
|
||||
pp(d, f);
|
||||
if (indent > 0)
|
||||
if (indent > 0)
|
||||
f = format_ns::mk_indent(m(), indent, f);
|
||||
::pp(out, f.get(), m());
|
||||
}
|
||||
|
|
@ -1763,7 +1761,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr
|
|||
}
|
||||
|
||||
// TODO: display uninterpreted sort decls, and datatype decls.
|
||||
|
||||
|
||||
unsigned num_decls = decls.get_num_decls();
|
||||
func_decl * const * fs = decls.get_func_decls();
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
|
|
@ -1779,7 +1777,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr
|
|||
out << "(check-sat)" << std::endl;
|
||||
}
|
||||
|
||||
void cmd_context::slow_progress_sample() {
|
||||
void cmd_context::slow_progress_sample() {
|
||||
SASSERT(m_solver);
|
||||
statistics st;
|
||||
regular_stream() << "(progress\n";
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ static void display_statistics() {
|
|||
}
|
||||
|
||||
static void on_timeout() {
|
||||
#pragma omp critical (g_display_stats)
|
||||
#pragma omp critical (g_display_stats)
|
||||
{
|
||||
display_statistics();
|
||||
exit(0);
|
||||
|
|
@ -65,7 +65,7 @@ static void on_timeout() {
|
|||
|
||||
static void on_ctrl_c(int) {
|
||||
signal (SIGINT, SIG_DFL);
|
||||
#pragma omp critical (g_display_stats)
|
||||
#pragma omp critical (g_display_stats)
|
||||
{
|
||||
display_statistics();
|
||||
}
|
||||
|
|
@ -78,9 +78,9 @@ unsigned read_smtlib_file(char const * benchmark_file) {
|
|||
signal(SIGINT, on_ctrl_c);
|
||||
smtlib::solver solver;
|
||||
g_solver = &solver;
|
||||
|
||||
|
||||
bool ok = true;
|
||||
|
||||
|
||||
ok = solver.solve_smt(benchmark_file);
|
||||
if (!ok) {
|
||||
if (benchmark_file) {
|
||||
|
|
@ -90,8 +90,8 @@ unsigned read_smtlib_file(char const * benchmark_file) {
|
|||
std::cerr << "ERROR: solving input stream.\n";
|
||||
}
|
||||
}
|
||||
|
||||
#pragma omp critical (g_display_stats)
|
||||
|
||||
#pragma omp critical (g_display_stats)
|
||||
{
|
||||
display_statistics();
|
||||
register_on_timeout_proc(0);
|
||||
|
|
@ -117,7 +117,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
|
|||
|
||||
g_cmd_context = &ctx;
|
||||
signal(SIGINT, on_ctrl_c);
|
||||
|
||||
|
||||
bool result = true;
|
||||
if (file_name) {
|
||||
std::ifstream in(file_name);
|
||||
|
|
@ -130,9 +130,9 @@ unsigned read_smtlib2_commands(char const * file_name) {
|
|||
else {
|
||||
result = parse_smt2_commands(ctx, std::cin, true);
|
||||
}
|
||||
|
||||
|
||||
#pragma omp critical (g_display_stats)
|
||||
|
||||
#pragma omp critical (g_display_stats)
|
||||
{
|
||||
display_statistics();
|
||||
g_cmd_context = 0;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue