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

Whitespace, typo.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-06-20 14:36:40 +01:00
parent 02161f2ff7
commit 7b97688302
1 changed files with 53 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

106
src/cmd_context/basic_cmds.cpp
View file

@ -39,7 +39,7 @@ class help_cmd : public cmd {
ctx.regular_stream() << " (" << s; ctx.regular_stream() << " (" << s;
if (usage) if (usage)
ctx.regular_stream() << " " << escaped(usage, true) << ")\n"; ctx.regular_stream() << " " << escaped(usage, true) << ")\n";
else else
ctx.regular_stream() << ")\n"; ctx.regular_stream() << ")\n";
if (descr) { if (descr) {
ctx.regular_stream() << " " << escaped(descr, true, 4) << "\n"; ctx.regular_stream() << " " << escaped(descr, true, 4) << "\n";
@ -62,7 +62,7 @@ public:
} }
m_cmds.push_back(s); m_cmds.push_back(s);
} }
typedef std::pair<symbol, cmd*> named_cmd; typedef std::pair<symbol, cmd*> named_cmd;
struct named_cmd_lt { struct named_cmd_lt {
bool operator()(named_cmd const & c1, named_cmd const & c2) const { return c1.first.str() < c2.first.str(); } bool operator()(named_cmd const & c1, named_cmd const & c2) const { return c1.first.str() < c2.first.str(); }
@ -104,14 +104,14 @@ class get_model_cmd : public cmd {
unsigned m_index; unsigned m_index;
public: public:
get_model_cmd(): cmd("get-model"), m_index(0) {} get_model_cmd(): cmd("get-model"), m_index(0) {}
virtual char const * get_usage() const { return "[<index of box objective>]"; } virtual char const * get_usage() const { return "[<index of box objective>]"; }
virtual char const * get_descr(cmd_context & ctx) const { virtual char const * get_descr(cmd_context & ctx) const {
return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective";
} }
virtual unsigned get_arity() const { return VAR_ARITY; } virtual unsigned get_arity() const { return VAR_ARITY; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; }
virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }
virtual void execute(cmd_context & ctx) { virtual void execute(cmd_context & ctx) {
if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
throw cmd_exception("model is not available"); throw cmd_exception("model is not available");
model_ref m; model_ref m;
@ -122,7 +122,7 @@ public:
ctx.get_check_sat_result()->get_model(m); ctx.get_check_sat_result()->get_model(m);
} }
ctx.display_model(m); ctx.display_model(m);
} }
virtual void reset(cmd_context& ctx) { virtual void reset(cmd_context& ctx) {
m_index = 0; m_index = 0;
} }
@ -167,11 +167,11 @@ class cmd_is_declared : public ast_smt_pp::is_declared {
cmd_context& m_ctx; cmd_context& m_ctx;
public: public:
cmd_is_declared(cmd_context& ctx): m_ctx(ctx) {} cmd_is_declared(cmd_context& ctx): m_ctx(ctx) {}
virtual bool operator()(func_decl* d) const { virtual bool operator()(func_decl* d) const {
return m_ctx.is_func_decl(d->get_name()); return m_ctx.is_func_decl(d->get_name());
} }
virtual bool operator()(sort* s) const { virtual bool operator()(sort* s) const {
return m_ctx.is_sort_decl(s->get_name()); return m_ctx.is_sort_decl(s->get_name());
} }
}; };
@ -189,13 +189,13 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) { if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
throw cmd_exception("proof is not well sorted"); throw cmd_exception("proof is not well sorted");
} }
pp_params params; pp_params params;
if (params.pretty_proof()) { if (params.pretty_proof()) {
ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl; ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl;
} }
else { else {
// TODO: reimplement a new SMT2 pretty printer // TODO: reimplement a new SMT2 pretty printer
ast_smt_pp pp(ctx.m()); ast_smt_pp pp(ctx.m());
cmd_is_declared isd(ctx); cmd_is_declared isd(ctx);
pp.set_is_declared(&isd); pp.set_is_declared(&isd);
@ -206,19 +206,19 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
}); });
static void print_core(cmd_context& ctx) { static void print_core(cmd_context& ctx) {
ptr_vector<expr> core; ptr_vector<expr> core;
ctx.get_check_sat_result()->get_unsat_core(core); ctx.get_check_sat_result()->get_unsat_core(core);
ctx.regular_stream() << "("; ctx.regular_stream() << "(";
ptr_vector<expr>::const_iterator it = core.begin(); ptr_vector<expr>::const_iterator it = core.begin();
ptr_vector<expr>::const_iterator end = core.end(); ptr_vector<expr>::const_iterator end = core.end();
for (bool first = true; it != end; ++it) { for (bool first = true; it != end; ++it) {
if (first) if (first)
first = false; first = false;
else else
ctx.regular_stream() << " "; ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m());
} }
ctx.regular_stream() << ")" << std::endl; ctx.regular_stream() << ")" << std::endl;
} }
ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
@ -260,7 +260,7 @@ ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when i
ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(); ctx.print_success();); ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(); ctx.print_success(););
UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &, UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &,
if (ctx.set_logic(arg)) if (ctx.set_logic(arg))
ctx.print_success(); ctx.print_success();
else { else {
@ -269,9 +269,9 @@ UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", C
} }
); );
UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, { UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, {
ctx.display(ctx.regular_stream(), arg); ctx.display(ctx.regular_stream(), arg);
ctx.regular_stream() << std::endl; ctx.regular_stream() << std::endl;
}); });
UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;); UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;);
@ -305,18 +305,18 @@ protected:
symbol m_reproducible_resource_limit; symbol m_reproducible_resource_limit;
bool is_builtin_option(symbol const & s) const { bool is_builtin_option(symbol const & s) const {
return return
s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_print_success || s == m_print_warning || s == m_expand_definitions ||
s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions ||
s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants ||
s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_regular_output_channel || s == m_diagnostic_output_channel ||
s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations || s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
s == m_produce_assertions || s == m_reproducible_resource_limit; s == m_produce_assertions || s == m_reproducible_resource_limit;
} }
public: public:
set_get_option_cmd(char const * name): set_get_option_cmd(char const * name):
cmd(name), cmd(name),
m_true("true"), m_true("true"),
m_false("false"), m_false("false"),
m_print_success(":print-success"), m_print_success(":print-success"),
@ -348,7 +348,7 @@ public:
class set_option_cmd : public set_get_option_cmd { class set_option_cmd : public set_get_option_cmd {
bool m_unsupported; bool m_unsupported;
symbol m_option; symbol m_option;
bool to_bool(symbol const & value) const { bool to_bool(symbol const & value) const {
if (value != m_true && value != m_false) if (value != m_true && value != m_false)
throw cmd_exception("invalid option value, true/false expected"); throw cmd_exception("invalid option value, true/false expected");
@ -369,7 +369,7 @@ class set_option_cmd : public set_get_option_cmd {
throw cmd_exception(msg); throw cmd_exception(msg);
} }
} }
void set_param(cmd_context & ctx, char const * value) { void set_param(cmd_context & ctx, char const * value) {
try { try {
gparams::set(m_option, value); gparams::set(m_option, value);
@ -466,11 +466,11 @@ public:
virtual void prepare(cmd_context & ctx) { m_unsupported = false; m_option = symbol::null; } virtual void prepare(cmd_context & ctx) { m_unsupported = false; m_option = symbol::null; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
return m_option == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; return m_option == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE;
} }
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
if (m_option == symbol::null) { if (m_option == symbol::null) {
m_option = opt; m_option = opt;
} }
@ -525,7 +525,7 @@ class get_option_cmd : public set_get_option_cmd {
static void print_bool(cmd_context & ctx, bool b) { static void print_bool(cmd_context & ctx, bool b) {
ctx.regular_stream() << (b ? "true" : "false") << std::endl; ctx.regular_stream() << (b ? "true" : "false") << std::endl;
} }
static void print_unsigned(cmd_context & ctx, unsigned v) { static void print_unsigned(cmd_context & ctx, unsigned v) {
ctx.regular_stream() << v << std::endl; ctx.regular_stream() << v << std::endl;
} }
@ -542,11 +542,11 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; } virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; }
virtual unsigned get_arity() const { return 1; } virtual unsigned get_arity() const { return 1; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; }
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
if (opt == m_print_success) { if (opt == m_print_success) {
print_bool(ctx, ctx.print_success_enabled()); print_bool(ctx, ctx.print_success_enabled());
} }
// TODO: // TODO:
// else if (opt == m_print_warning) { // else if (opt == m_print_warning) {
// print_bool(ctx, ); // print_bool(ctx, );
// } // }
@ -636,7 +636,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "get information."; } virtual char const * get_descr(cmd_context & ctx) const { return "get information."; }
virtual unsigned get_arity() const { return 1; } virtual unsigned get_arity() const { return 1; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; }
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
if (opt == m_error_behavior) { if (opt == m_error_behavior) {
if (ctx.exit_on_error()) if (ctx.exit_on_error())
ctx.regular_stream() << "(:error-behavior immediate-exit)" << std::endl; ctx.regular_stream() << "(:error-behavior immediate-exit)" << std::endl;
@ -692,12 +692,12 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "set information."; } virtual char const * get_descr(cmd_context & ctx) const { return "set information."; }
virtual unsigned get_arity() const { return 2; } virtual unsigned get_arity() const { return 2; }
virtual void prepare(cmd_context & ctx) { m_info = symbol::null; } virtual void prepare(cmd_context & ctx) { m_info = symbol::null; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE;
} }
virtual void set_next_arg(cmd_context & ctx, rational const & val) {} virtual void set_next_arg(cmd_context & ctx, rational const & val) {}
virtual void set_next_arg(cmd_context & ctx, char const * val) {} virtual void set_next_arg(cmd_context & ctx, char const * val) {}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) { virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
if (m_info == symbol::null) { if (m_info == symbol::null) {
m_info = s; m_info = s;
} }
@ -745,7 +745,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; } virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
virtual unsigned get_arity() const { return 3; } virtual unsigned get_arity() const { return 3; }
virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); } virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_name == symbol::null) return CPK_SYMBOL; if (m_name == symbol::null) return CPK_SYMBOL;
if (m_domain.empty()) return CPK_SORT_LIST; if (m_domain.empty()) return CPK_SORT_LIST;
return CPK_FUNC_DECL; return CPK_FUNC_DECL;
@ -756,10 +756,10 @@ public:
throw cmd_exception("invalid map declaration, empty sort list"); throw cmd_exception("invalid map declaration, empty sort list");
m_domain.append(num, slist); m_domain.append(num, slist);
} }
virtual void set_next_arg(cmd_context & ctx, func_decl * f) { virtual void set_next_arg(cmd_context & ctx, func_decl * f) {
m_f = f; m_f = f;
if (m_f->get_arity() == 0) if (m_f->get_arity() == 0)
throw cmd_exception("invalid map declaration, function declaration must have arity > 0"); throw cmd_exception("invalid map declaration, function declaration must have arity > 0");
} }
virtual void reset(cmd_context & ctx) { virtual void reset(cmd_context & ctx) {
m_array_fid = null_family_id; m_array_fid = null_family_id;
@ -798,7 +798,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "retrieve consequences that fix values for supplied variables"; } virtual char const * get_descr(cmd_context & ctx) const { return "retrieve consequences that fix values for supplied variables"; }
virtual unsigned get_arity() const { return 2; } virtual unsigned get_arity() const { return 2; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR_LIST; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR_LIST; }
virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) {
if (m_count == 0) { if (m_count == 0) {
m_assumptions.append(num, tlist); m_assumptions.append(num, tlist);
++m_count; ++m_count;
@ -858,7 +858,7 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(builtin_cmd, "declare-fun", "<symbol> (<sort>*) <sort>", "declare a new function/constant.")); ctx.insert(alloc(builtin_cmd, "declare-fun", "<symbol> (<sort>*) <sort>", "declare a new function/constant."));
ctx.insert(alloc(builtin_cmd, "declare-const", "<symbol> <sort>", "declare a new constant.")); ctx.insert(alloc(builtin_cmd, "declare-const", "<symbol> <sort>", "declare a new constant."));
ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))")); ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))"));
ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals")); ctx.insert(alloc(builtin_cmd, "check-sat-assuming", "( hprop_literali* )", "check sat assuming a collection of literals"));
ctx.insert(alloc(get_unsat_assumptions_cmd)); ctx.insert(alloc(get_unsat_assumptions_cmd));
ctx.insert(alloc(reset_assertions_cmd)); ctx.insert(alloc(reset_assertions_cmd));