checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/cmd_context/README

@@ -0,0 +1,2 @@
+Command context provides the infrastructure for executing commands in front-ends such as SMT-LIB 2.0.
+It is also provides the solver abstraction to plugin solvers in this kind of front-end.

src/cmd_context/basic_cmds.cpp

@@ -0,0 +1,772 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    basic_cmds.cpp
+
+Abstract:
+    Basic commands for SMT2 front end.
+
+Author:
+
+    Leonardo (leonardo) 2011-03-30
+
+Notes:
+
+--*/
+#include"cmd_context.h"
+#include"version.h"
+#include"ast_smt_pp.h"
+#include"ast_smt2_pp.h"
+#include"ast_pp.h"
+#include"model_smt2_pp.h"
+#include"model_v2_pp.h"
+#include"array_decl_plugin.h"
+#include"pp.h"
+#include"cmd_util.h"
+#include"simplify_cmd.h"
+#include"eval_cmd.h"
+
+class help_cmd : public cmd {
+    svector<symbol> m_cmds;
+    void display_cmd(cmd_context & ctx, symbol const & s, cmd * c) {
+        char const * usage = c->get_usage();
+        char const * descr = c->get_descr(ctx);
+        ctx.regular_stream() << " (" << s;
+        if (usage)
+            ctx.regular_stream() << " " << escaped(usage, true) << ")\n";
+        else 
+            ctx.regular_stream() << ")\n";
+        if (descr) {
+            ctx.regular_stream() << "    " << escaped(descr, true, 4) << "\n";
+        }
+    }
+
+public:
+    help_cmd():cmd("help") {}
+    virtual char const * get_usage() const { return "<symbol>*"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "print this help."; }
+    virtual unsigned get_arity() const { return VAR_ARITY; }
+    virtual void prepare(cmd_context & ctx) { m_cmds.reset(); }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_SYMBOL; }
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
+        cmd * c = ctx.find_cmd(s);
+        if (c == 0) {
+            std::string err_msg("unknown command '");
+            err_msg = err_msg + s.bare_str() + "'";
+            throw cmd_exception(err_msg);
+        }
+        m_cmds.push_back(s);
+    }
+    
+    typedef std::pair<symbol, cmd*> named_cmd;
+    struct named_cmd_lt {
+        bool operator()(named_cmd const & c1, named_cmd const & c2) const { return c1.first.str() < c2.first.str(); }
+    };
+
+    virtual void execute(cmd_context & ctx) {
+        ctx.regular_stream() << "\"";
+        if (m_cmds.empty()) {
+            vector<named_cmd> cmds;
+            cmd_context::cmd_iterator it  = ctx.begin_cmds();
+            cmd_context::cmd_iterator end = ctx.end_cmds();
+            for (; it != end; ++it) {
+                cmds.push_back(named_cmd((*it).m_key, (*it).m_value));
+            }
+            // named_cmd_lt is not a total order for commands, but this is irrelevant for Linux x Windows behavior
+            std::sort(cmds.begin(), cmds.end(), named_cmd_lt());
+            vector<named_cmd>::const_iterator it2  = cmds.begin();
+            vector<named_cmd>::const_iterator end2 = cmds.end();
+            for (; it2 != end2; ++it2) {
+                display_cmd(ctx, it2->first, it2->second);
+            }
+        }
+        else {
+            svector<symbol>::const_iterator it  = m_cmds.begin();
+            svector<symbol>::const_iterator end = m_cmds.end();
+            for (; it != end; ++it) {
+                cmd * c = ctx.find_cmd(*it);
+                SASSERT(c);
+                display_cmd(ctx, *it, c);
+            }
+        }
+        ctx.regular_stream() << "\"\n";
+    }
+};
+
+ATOMIC_CMD(exit_cmd, "exit", "exit.", ctx.print_success(); throw stop_parser_exception(););
+
+ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat command", {
+    if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
+        throw cmd_exception("model is not available");
+    model_ref m;
+    ctx.get_check_sat_result()->get_model(m);
+    if (ctx.params().m_model_v1_pp || ctx.params().m_model_v2_pp) {
+        std::ostringstream buffer;
+        model_v2_pp(buffer, *m, ctx.params().m_model_partial);
+        ctx.regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl;
+    } else {
+        ctx.regular_stream() << "(model " << std::endl;
+        model_smt2_pp(ctx.regular_stream(), ctx, *(m.get()), 2);
+        // m->display(ctx.regular_stream());
+        ctx.regular_stream() << ")" << std::endl;
+    }
+});
+
+ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
+    if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
+        throw cmd_exception("model is not available");
+    model_ref m;
+    ctx.get_check_sat_result()->get_model(m);
+    ctx.regular_stream() << "(";
+    dictionary<cmd_context::macro> const & macros = ctx.get_macros();
+    dictionary<cmd_context::macro>::iterator it  = macros.begin();
+    dictionary<cmd_context::macro>::iterator end = macros.end();
+    for (bool first = true; it != end; ++it) {
+        symbol const & name = (*it).m_key;
+        cmd_context::macro const & _m    = (*it).m_value;
+        if (_m.first == 0 && ctx.m().is_bool(_m.second)) {
+            expr_ref val(ctx.m());
+            m->eval(_m.second, val, true);
+            if (ctx.m().is_true(val) || ctx.m().is_false(val)) {
+                if (first)
+                    first = false;
+                else
+                    ctx.regular_stream() << " ";
+                ctx.regular_stream() << "(" << name << " " << (ctx.m().is_true(val) ? "true" : "false") << ")";
+            }
+        }
+    }
+    ctx.regular_stream() << ")" << std::endl;
+});
+
+class cmd_is_declared : public ast_smt_pp::is_declared {
+    cmd_context& m_ctx;
+public:
+    cmd_is_declared(cmd_context& ctx): m_ctx(ctx) {}
+    
+    virtual bool operator()(func_decl* d) const { 
+        return m_ctx.is_func_decl(d->get_name());
+    }
+    virtual bool operator()(sort* s) const { 
+        return m_ctx.is_sort_decl(s->get_name());
+    }
+};
+
+ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
+    if (ctx.params().m_proof_mode == PGM_DISABLED)
+        throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
+    if (!ctx.has_manager() ||
+        ctx.cs_state() != cmd_context::css_unsat)
+        throw cmd_exception("proof is not available");
+    expr_ref pr(ctx.m());
+    pr = ctx.get_check_sat_result()->get_proof();
+    if (pr == 0)
+        throw cmd_exception("proof is not available");
+    // TODO: reimplement a new SMT2 pretty printer 
+    ast_smt_pp pp(ctx.m());
+    cmd_is_declared isd(ctx);
+    pp.set_is_declared(&isd);
+    pp.set_logic(ctx.get_logic().str().c_str());
+    pp.display_smt2(ctx.regular_stream(), pr);
+    ctx.regular_stream() << std::endl;
+});
+
+ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
+    if (!ctx.produce_unsat_cores())
+        throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)");
+    if (!ctx.has_manager() ||
+        ctx.cs_state() != cmd_context::css_unsat)
+        throw cmd_exception("unsat core is not available");
+    ptr_vector<expr> core;
+    ctx.get_check_sat_result()->get_unsat_core(core);
+    ctx.regular_stream() << "(";
+    ptr_vector<expr>::const_iterator it  = core.begin();
+    ptr_vector<expr>::const_iterator end = core.end();
+    for (bool first = true; it != end; ++it) {
+        if (first)
+            first = false;
+        else
+            ctx.regular_stream() << " ";
+        ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m());
+    }
+    ctx.regular_stream() << ")" << std::endl;
+});
+
+ATOMIC_CMD(labels_cmd, "labels", "retrieve Simplify-like labels", {
+    if (!ctx.has_manager() ||
+        (ctx.cs_state() != cmd_context::css_sat && ctx.cs_state() != cmd_context::css_unknown))
+        throw cmd_exception("labels are not available");
+    svector<symbol> labels;
+    ctx.get_check_sat_result()->get_labels(labels);
+    ctx.regular_stream() << "(labels";
+    for (unsigned i = 0; i < labels.size(); i++) {
+        ctx.regular_stream() << " " << labels[i];
+    }
+    ctx.regular_stream() << ")" << std::endl;
+});
+
+ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when in interactive mode", ctx.display_assertions(););
+
+UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &, ctx.set_logic(arg); ctx.print_success(););
+
+UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, { 
+    ctx.display(ctx.regular_stream(), arg);
+    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;);
+
+/**
+   \brief Convert a keyword into an internal Z3 option name
+*/
+std::string smt_keyword2opt_name(symbol const & opt) {
+    std::string r;
+    SASSERT(opt.bare_str()[0] == ':');
+    r = opt.bare_str() + 1;
+    unsigned sz = static_cast<unsigned>(r.size());
+    for (unsigned i = 0; i < sz; i++) {
+        char curr = r[i];
+        if ('a' <= curr && curr <= 'z')
+            r[i] = 'A' + (curr - 'a');
+        else if (curr == '-')
+            r[i] = '_';
+    }
+    TRACE("smt2_opt_name", tout << opt << " -> '" << r << "'\n";);
+    return r;
+}
+
+class set_get_option_cmd : public cmd {
+protected:
+    symbol      m_true;
+    symbol      m_false;
+
+    symbol      m_print_success;
+    symbol      m_print_warning;
+    symbol      m_expand_definitions;
+    symbol      m_interactive_mode;
+    symbol      m_produce_proofs;
+    symbol      m_produce_unsat_cores;
+    symbol      m_produce_models;
+    symbol      m_produce_assignments;
+    symbol      m_regular_output_channel;
+    symbol      m_diagnostic_output_channel;
+    symbol      m_random_seed;
+    symbol      m_verbosity;
+    symbol      m_global_decls;
+    symbol      m_numeral_as_real;
+    symbol      m_error_behavior;
+    symbol      m_int_real_coercions;
+    ini_params  m_ini;
+
+    bool is_builtin_option(symbol const & s) const {
+        return 
+            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_models || s == m_produce_assignments || s == m_regular_output_channel || s == m_diagnostic_output_channel || 
+            s == m_random_seed || s == m_verbosity || s == m_global_decls;
+    }
+
+public:
+    set_get_option_cmd(char const * name, front_end_params & params):
+        cmd(name), 
+        m_true("true"),
+        m_false("false"),
+        m_print_success(":print-success"),
+        m_print_warning(":print-warning"),
+        m_expand_definitions(":expand-definitions"),
+        m_interactive_mode(":interactive-mode"),
+        m_produce_proofs(":produce-proofs"),
+        m_produce_unsat_cores(":produce-unsat-cores"),
+        m_produce_models(":produce-models"),
+        m_produce_assignments(":produce-assignments"),
+        m_regular_output_channel(":regular-output-channel"),
+        m_diagnostic_output_channel(":diagnostic-output-channel"),
+        m_random_seed(":random-seed"),
+        m_verbosity(":verbosity"),
+        m_global_decls(":global-decls"),
+        m_numeral_as_real(":numeral-as-real"),
+        m_error_behavior(":error-behavior"),
+        m_int_real_coercions(":int-real-coercions"),
+        m_ini(false) {
+        params.register_params(m_ini);
+        register_pp_params(m_ini);
+    }
+    virtual ~set_get_option_cmd() {}
+
+};
+
+class set_option_cmd : public set_get_option_cmd {
+    bool        m_unsupported;
+    symbol      m_option;
+    
+    bool to_bool(symbol const & value) const {
+        if (value != m_true && value != m_false)
+            throw cmd_exception("invalid option value, true/false expected");
+        return value == m_true;
+    }
+
+    static unsigned to_unsigned(rational const & val) {
+        if (!val.is_unsigned())
+            throw cmd_exception("option value is too big to fit in a machine integer.");
+        return val.get_unsigned();
+    }
+
+    static void check_not_initialized(cmd_context & ctx, symbol const & opt_name) {
+        if (ctx.has_manager()) {
+            std::string msg = "error setting '";
+            msg += opt_name.str();
+            msg += "', option value cannot be modified after initialization";
+            throw cmd_exception(msg);
+        }
+    }
+    
+    void set_param(cmd_context & ctx, char const * value) {
+        m_ini.freeze(ctx.has_manager());
+        std::string internal_opt = smt_keyword2opt_name(m_option);
+        try {
+            std::string old_value;
+            if (!m_ini.get_param_value(internal_opt.c_str(), old_value)) {
+                m_unsupported = true;
+                return;
+            }
+            m_ini.set_param_value(internal_opt.c_str(), value);
+        }
+        catch (set_get_param_exception ex) {
+            std::string msg = "error setting '";
+            msg += m_option.str();
+            msg += "', ";
+            msg += ex.get_msg();
+            throw cmd_exception(msg);
+        }
+    }
+
+    void set_symbol(cmd_context & ctx, symbol const & value) {
+        if (m_option == m_print_success) {
+            ctx.set_print_success(to_bool(value));
+        }
+        else if (m_option == m_print_warning) {
+            enable_warning_messages(to_bool(value));
+        }
+        else if (m_option == m_expand_definitions) {
+            m_unsupported = true;
+        }
+        else if (m_option == m_interactive_mode) {
+            check_not_initialized(ctx, m_interactive_mode);
+            ctx.set_interactive_mode(to_bool(value));
+        }
+        else if (m_option == m_produce_proofs) {
+            check_not_initialized(ctx, m_produce_proofs);
+            ctx.params().m_proof_mode = to_bool(value) ? PGM_FINE : PGM_DISABLED;
+        }
+        else if (m_option == m_produce_unsat_cores) {
+            check_not_initialized(ctx, m_produce_unsat_cores);
+            ctx.set_produce_unsat_cores(to_bool(value));
+        }
+        else if (m_option == m_produce_models) {
+            ctx.params().m_model = to_bool(value);
+        }
+        else if (m_option == m_produce_assignments) {
+            ctx.set_produce_assignments(to_bool(value));
+        }
+        else if (m_option == m_global_decls) {
+            check_not_initialized(ctx, m_global_decls);
+            ctx.set_global_decls(to_bool(value));
+        }
+        else if (m_option == m_numeral_as_real) {
+            ctx.set_numeral_as_real(to_bool(value));
+        }
+        else if (m_option == m_int_real_coercions) {
+            ctx.m().enable_int_real_coercions(to_bool(value));
+        }
+#ifdef Z3DEBUG
+        else if (m_option == ":enable-assertions") {
+            enable_assertions(to_bool(value));
+        }
+#endif
+        else if (m_option == m_error_behavior) {
+            if (value == "immediate-exit") {
+                ctx.set_exit_on_error(true);
+            }
+            else if (value == "continued-execution") {
+                ctx.set_exit_on_error(false);
+            }
+            else {
+                throw cmd_exception("error setting :error-behavior, 'immediate-execution' or 'continued-execution' expected");
+            }
+        }
+        else if (is_builtin_option(m_option)) {
+            throw cmd_exception("option value is not a symbol");
+        }
+        else {
+            set_param(ctx, value.bare_str());
+        }
+    }
+
+public:
+    set_option_cmd(front_end_params & params):
+        set_get_option_cmd("set-option", params),
+        m_unsupported(false) {
+    }
+
+    virtual char const * get_usage() const { return "<keyword> <value>"; }
+
+    virtual char const * get_descr(cmd_context & ctx) const { return "set configuration option."; }
+
+    virtual unsigned get_arity() const { return 2; }
+
+    virtual void prepare(cmd_context & ctx) { m_unsupported = false; m_option = symbol::null; }
+
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
+        return m_option == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE;
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { 
+        if (m_option == symbol::null) {
+            m_option = opt;
+        }
+        else {
+            set_symbol(ctx, opt);
+        }
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, rational const & val) {
+        if (m_option == m_random_seed) {
+            ctx.set_random_seed(to_unsigned(val));
+        }
+        else if (m_option == m_verbosity) {
+            set_verbosity_level(to_unsigned(val));
+        }
+        else if (is_builtin_option(m_option)) {
+            throw cmd_exception("option value is not a numeral");
+        }
+        else {
+            std::string str = val.to_string();
+            set_param(ctx, str.c_str());
+        }
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, char const * value) {
+        if (m_option == m_regular_output_channel) {
+            ctx.set_regular_stream(value);
+        }
+        else if (m_option == m_diagnostic_output_channel) {
+            ctx.set_diagnostic_stream(value);
+        }
+        else if (is_builtin_option(m_option)) {
+            throw cmd_exception("option value is not a string");
+        }
+        else {
+            set_param(ctx, value);
+        }
+    }
+
+    virtual void execute(cmd_context & ctx) {
+        if (m_unsupported)
+            ctx.print_unsupported(m_option);
+        else
+            ctx.print_success();
+    }
+};
+
+class get_option_cmd : public set_get_option_cmd {
+    static void print_bool(cmd_context & ctx, bool b) {
+        ctx.regular_stream() << (b ? "true" : "false") << std::endl;
+    }
+    
+    static void print_unsigned(cmd_context & ctx, unsigned v) {
+        ctx.regular_stream() << v << std::endl;
+    }
+
+    static void print_string(cmd_context & ctx, char const * str) {
+        ctx.regular_stream() << str << std::endl;
+    }
+
+public:
+    get_option_cmd(front_end_params & params):
+        set_get_option_cmd("get-option", params) {
+    }
+    virtual char const * get_usage() const { return "<keyword>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; }
+    virtual unsigned get_arity() const { return 1; }
+    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) { 
+        if (opt == m_print_success) {
+            print_bool(ctx, ctx.print_success_enabled()); 
+        }
+        // TODO: 
+        // else if (opt == m_print_warning) {
+        // print_bool(ctx, );
+        // }
+        else if (opt == m_expand_definitions) {
+            ctx.print_unsupported(m_expand_definitions);
+        }
+        else if (opt == m_interactive_mode) {
+            print_bool(ctx, ctx.interactive_mode());
+        }
+        else if (opt == m_produce_proofs) {
+            print_bool(ctx, ctx.params().m_proof_mode != PGM_DISABLED);
+        }
+        else if (opt == m_produce_unsat_cores) {
+            print_bool(ctx, ctx.produce_unsat_cores());
+        }
+        else if (opt == m_produce_models) {
+            print_bool(ctx, ctx.params().m_model);
+        }
+        else if (opt == m_produce_assignments) {
+            print_bool(ctx, ctx.produce_assignments());
+        }
+        else if (opt == m_global_decls) {
+            print_bool(ctx, ctx.global_decls());
+        }
+        else if (opt == m_random_seed) {
+            print_unsigned(ctx, ctx.random_seed());
+        }
+        else if (opt == m_verbosity) {
+            print_unsigned(ctx, get_verbosity_level());
+        }
+        else if (opt == m_regular_output_channel) {
+            print_string(ctx, ctx.get_regular_stream_name());
+        }
+        else if (opt == m_diagnostic_output_channel) {
+            print_string(ctx, ctx.get_diagnostic_stream_name());
+        }
+        else if (opt == m_error_behavior) {
+            if (ctx.exit_on_error()) {
+                print_string(ctx, "immediate-exit");
+            }
+            else {
+                print_string(ctx, "continued-execution");
+            }
+        }
+        else if (opt == m_int_real_coercions) {
+            print_bool(ctx, ctx.m().int_real_coercions());
+        }
+        else {
+            std::string iopt = smt_keyword2opt_name(opt);
+            std::string r;
+            if (m_ini.get_param_value(iopt.c_str(), r)) {
+                ctx.regular_stream() << r << std::endl;
+            }
+            else {
+                ctx.print_unsupported(opt);
+            }
+        }
+    }
+};
+
+class get_info_cmd : public cmd {
+    symbol   m_error_behavior;
+    symbol   m_name;
+    symbol   m_authors;
+    symbol   m_version;
+    symbol   m_status;
+    symbol   m_reason_unknown;
+    symbol   m_all_statistics;
+public:
+    get_info_cmd():
+        cmd("get-info"),
+        m_error_behavior(":error-behavior"),
+        m_name(":name"),
+        m_authors(":authors"),
+        m_version(":version"),
+        m_status(":status"),
+        m_reason_unknown(":reason-unknown"),
+        m_all_statistics(":all-statistics") {
+    }
+    virtual char const * get_usage() const { return "<keyword>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "get information."; }
+    virtual unsigned get_arity() const { return 1; }
+    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) { 
+        if (opt == m_error_behavior) {
+            if (ctx.exit_on_error())
+                ctx.regular_stream() << "(:error-behavior immediate-exit)" << std::endl;
+            else
+                ctx.regular_stream() << "(:error-behavior continued-execution)" << std::endl;
+        }
+        else if (opt == m_name) {
+            ctx.regular_stream() << "(:name \"Z3\")" << std::endl;
+        }
+        else if (opt == m_authors) {
+            ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl;
+        }
+        else if (opt == m_version) {
+            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "\")" << std::endl;
+        }
+        else if (opt == m_status) {
+            ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;
+        }
+        else if (opt == m_reason_unknown) {
+            ctx.regular_stream() << "(:reason-unknown " << ctx.reason_unknown() << ")" << std::endl;
+        }
+        else if (opt == m_all_statistics) {
+            ctx.display_statistics();
+        }
+        else {
+            ctx.print_unsupported(opt);
+        }
+    }
+};
+
+class set_info_cmd : public cmd {
+    symbol   m_info;
+    symbol   m_status;
+    symbol   m_unsat;
+    symbol   m_sat;
+    symbol   m_unknown;
+public:
+    set_info_cmd():
+        cmd("set-info"),
+        m_status(":status"),
+        m_unsat("unsat"),
+        m_sat("sat"),
+        m_unknown("unknown") {
+    }
+    virtual char const * get_usage() const { return "<keyword> <value>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "set information."; }
+    virtual unsigned get_arity() const { return 2; }
+    virtual void prepare(cmd_context & ctx) { m_info = symbol::null; }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
+        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, char const * val) {}
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s) { 
+        if (m_info == symbol::null) {
+            m_info = s;
+        }
+        else {
+            if (m_info == m_status) {
+                if (s == m_unsat) {
+                    ctx.set_status(cmd_context::UNSAT);
+                }
+                else if (s == m_sat) {
+                    ctx.set_status(cmd_context::SAT);
+                }
+                else if (s == m_unknown) {
+                    ctx.set_status(cmd_context::UNKNOWN);
+                }
+                else {
+                    throw cmd_exception("invalid ':status' attribute");
+                }
+            }
+        }
+    }
+    virtual void execute(cmd_context & ctx) {
+        ctx.print_success();
+    }
+};
+
+class declare_map_cmd : public cmd {
+    symbol           m_array_sort;
+    symbol           m_name;
+    ptr_vector<sort> m_domain;
+    func_decl *      m_f;
+    family_id        m_array_fid;
+public:
+    declare_map_cmd():
+        cmd("declare-map"),
+        m_array_sort("Array"),
+        m_array_fid(null_family_id) {}
+
+    family_id get_array_fid(cmd_context & ctx) {
+        if (m_array_fid == null_family_id) {
+            m_array_fid = ctx.m().get_family_id("array");
+        }
+        return m_array_fid;
+    }
+    virtual char const * get_usage() const { return "<symbol> (<sort>+) <func-decl-ref>"; }
+    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 void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
+        if (m_name == symbol::null) return CPK_SYMBOL;
+        if (m_domain.empty()) return CPK_SORT_LIST;
+        return CPK_FUNC_DECL;
+    }
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_name = s; }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, sort * const * slist) {
+        if (num == 0)
+            throw cmd_exception("invalid map declaration, empty sort list");
+        m_domain.append(num, slist);
+    }
+    virtual void set_next_arg(cmd_context & ctx, func_decl * f) { 
+        m_f = f; 
+        if (m_f->get_arity() == 0) 
+            throw cmd_exception("invalid map declaration, function declaration must have arity > 0"); 
+    }
+    virtual void reset(cmd_context & ctx) {
+        m_array_fid = null_family_id;
+    }
+    virtual void execute(cmd_context & ctx) {
+        psort_decl * array_sort = ctx.find_psort_decl(m_array_sort);
+        if (array_sort == 0)
+            throw cmd_exception("Array sort is not available");
+        ptr_vector<sort> & array_sort_args = m_domain;
+        sort_ref_buffer domain(ctx.m());
+        unsigned arity = m_f->get_arity();
+        for (unsigned i = 0; i < arity; i++) {
+            array_sort_args.push_back(m_f->get_domain(i));
+            domain.push_back(array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.c_ptr()));
+            array_sort_args.pop_back();
+        }
+        sort_ref range(ctx.m());
+        array_sort_args.push_back(m_f->get_range());
+        range = array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.c_ptr());
+        parameter p[1] = { parameter(m_f) };
+        func_decl_ref new_map(ctx.m());
+        new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, p, domain.size(), domain.c_ptr(), range.get());
+        if (new_map == 0)
+            throw cmd_exception("invalid array map operator");
+        ctx.insert(m_name, new_map);
+    }
+};
+
+// provides "help" for builtin cmds
+class builtin_cmd : public cmd {
+    char const * m_usage;
+    char const * m_descr;
+public:
+    builtin_cmd(char const * name, char const * usage, char const * descr):
+        cmd(name), m_usage(usage), m_descr(descr) {}
+    virtual char const * get_usage() const { return m_usage; }
+    virtual char const * get_descr(cmd_context & ctx) const { return m_descr; }
+};
+
+
+void install_basic_cmds(cmd_context & ctx) {
+    ctx.insert(alloc(set_logic_cmd));
+    ctx.insert(alloc(exit_cmd));
+    ctx.insert(alloc(get_assignment_cmd));
+    ctx.insert(alloc(get_assertions_cmd));
+    ctx.insert(alloc(get_proof_cmd));
+    ctx.insert(alloc(get_unsat_core_cmd));
+    ctx.insert(alloc(set_option_cmd, ctx.params()));
+    ctx.insert(alloc(get_option_cmd, ctx.params()));
+    ctx.insert(alloc(get_info_cmd));
+    ctx.insert(alloc(set_info_cmd));
+    ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
+    ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));
+    ctx.insert(alloc(builtin_cmd, "push", "<number>?", "push 1 (or <number>) scopes."));
+    ctx.insert(alloc(builtin_cmd, "pop", "<number>?", "pop 1 (or <number>) scopes."));
+    ctx.insert(alloc(builtin_cmd, "get-value", "(<term>+)", "evaluate the given terms in the current model."));
+    ctx.insert(alloc(builtin_cmd, "declare-sort", "<symbol> <numeral>?", "declare a new uninterpreted sort of arity <numeral>, if arity is not provided, then it is assumed to be 0."));
+    ctx.insert(alloc(builtin_cmd, "define-sort", "<symbol> (<symbol>*) <sort>", "define a new sort."));
+    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-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)))))"));
+}
+
+void install_ext_basic_cmds(cmd_context & ctx) {
+    ctx.insert(alloc(help_cmd));
+    ctx.insert(alloc(pp_cmd));
+    ctx.insert(alloc(get_model_cmd));
+    ctx.insert(alloc(echo_cmd));
+    ctx.insert(alloc(labels_cmd));
+    ctx.insert(alloc(declare_map_cmd));
+    ctx.insert(alloc(builtin_cmd, "reset", 0, "reset the shell (all declarations and assertions will be erased)"));
+    install_simplify_cmd(ctx);
+    install_eval_cmd(ctx);
+}

src/cmd_context/basic_cmds.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    basic_cmds.h
+
+Abstract:
+    Basic commands for SMT2 front end.
+
+Author:
+
+    Leonardo (leonardo) 2011-03-30
+
+Notes:
+
+--*/
+#ifndef _BASIC_CMDS_H_
+#define _BASIC_CMDS_H_
+
+class cmd_context;
+
+void install_basic_cmds(cmd_context & ctx);
+void install_ext_basic_cmds(cmd_context & ctx);
+
+#endif

src/cmd_context/check_logic.cpp

@@ -0,0 +1,496 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    check_logic.cpp
+
+Abstract:
+
+    Check whether a given assertion is in the correct logic or not
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-08-11.
+
+Revision History:
+
+--*/
+#include"check_logic.h"
+#include"arith_decl_plugin.h"
+#include"array_decl_plugin.h"
+#include"bv_decl_plugin.h"
+#include"ast_pp.h"
+#include"for_each_expr.h"
+
+struct check_logic::imp {
+    ast_manager & m;
+    symbol        m_logic;
+    arith_util    m_a_util;
+    bv_util       m_bv_util;
+    array_util    m_ar_util;
+    bool          m_uf;        // true if the logic supports uninterpreted functions
+    bool          m_arrays;    // true if the logic supports arbitrary arrays
+    bool          m_bv_arrays; // true if the logic supports only bv arrays
+    bool          m_reals;     // true if the logic supports reals
+    bool          m_ints;      // true if the logic supports integers
+    bool          m_diff;      // true if the logic supports difference logic only
+    bool          m_nonlinear; // true if the logic supports nonlinear arithmetic
+    bool          m_bvs;       // true if the logic supports bit-vectors
+    bool          m_quantifiers; // true if the logic supports quantifiers
+    bool          m_unknown_logic;
+
+    imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m) {
+        reset();
+    }
+
+    void reset() {
+        m_uf          = false;
+        m_arrays      = false;
+        m_bv_arrays   = false;
+        m_reals       = false;
+        m_ints        = false;
+        m_diff        = false;
+        m_nonlinear   = false;
+        m_bvs         = false;
+        m_quantifiers = false;
+        m_unknown_logic = true;
+    }
+
+    void set_logic(symbol const & logic) {
+        reset();
+        m_unknown_logic = false;
+        if (logic == "AUFLIA") {
+            m_uf     = true;
+            m_arrays = true;
+            m_ints   = true;
+            m_quantifiers = true;
+        }
+        else if (logic == "AUFLIRA") {
+            m_uf     = true;
+            m_arrays = true;
+            m_reals  = true;
+            m_ints   = true;
+            m_quantifiers = true;
+        }
+        else if (logic == "AUFNIRA") {
+            m_uf     = true;
+            m_arrays = true;
+            m_reals  = true;
+            m_ints   = true;
+            m_nonlinear   = true;
+            m_quantifiers = true;
+        }
+        else if (logic == "LRA") {
+            m_reals       = true;
+            m_quantifiers = true;
+        }
+        else if (logic == "QF_ABV") {
+            m_bv_arrays = true;
+            m_bvs       = true;
+        }
+        else if (logic == "QF_AUFBV") {
+            m_uf        = true;
+            m_bv_arrays = true;
+            m_bvs       = true;
+        }
+        else if (logic == "QF_UFBV") {
+            m_uf        = true;
+            m_bvs       = true;
+        }
+        else if (logic == "QF_AUFLIA") {
+            m_uf     = true;
+            m_arrays = true;
+            m_ints   = true;
+        }
+        else if (logic == "QF_AX") {
+            m_arrays = true;
+        }
+        else if (logic == "QF_BV") {
+            m_bvs    = true;
+        }
+        else if (logic == "QF_IDL") {
+            m_ints   = true;
+            m_diff   = true;
+        }
+        else if (logic == "QF_RDL") {
+            m_reals  = true;
+            m_diff   = true;
+        }
+        else if (logic == "QF_LIA") {
+            m_ints   = true;
+        }
+        else if (logic == "QF_LRA") {
+            m_reals   = true;
+        }
+        else if (logic == "QF_NIA") {
+            m_ints   = true;
+            m_nonlinear = true;
+        }
+        else if (logic == "QF_NRA") {
+            m_reals     = true;
+            m_nonlinear = true;
+        }
+        else if (logic == "QF_UF") {
+            m_uf = true;
+        }
+        else if (logic == "QF_UFIDL") {
+            m_uf     = true;
+            m_ints   = true;
+            m_diff   = true;
+        }
+        else if (logic == "QF_UFLIA") {
+            m_uf     = true;
+            m_ints   = true;
+        }
+        else if (logic == "QF_UFLRA") {
+            m_uf     = true;
+            m_reals  = true;
+        }
+        else if (logic == "QF_UFNRA") {
+            m_uf        = true;
+            m_reals     = true;
+            m_nonlinear = true;
+        }
+        else if (logic == "UFLRA") {
+            m_uf          = true;
+            m_reals       = true;
+            m_quantifiers = true;
+        }
+        else if (logic == "UFNIA") {
+            m_uf          = true;
+            m_ints        = true;
+            m_quantifiers = true;
+            m_nonlinear   = true;
+        }
+        else if (logic == "UFBV") {
+            m_uf          = true;
+            m_bvs         = true;
+            m_quantifiers = true;
+        }
+        else {
+            m_unknown_logic = true;
+        }
+        
+        m_logic = logic;
+    }
+
+    struct failed {};
+    std::string m_last_error;
+
+    void fail(char const * msg) {
+        m_last_error = msg;
+        throw failed();
+    }
+
+    void check_sort(sort * s) {
+        if (s->get_family_id() == null_family_id) {
+            if (!m_uf)
+                fail("logic does not support uninterpreted sorts");
+        }
+        else if (m.is_bool(s)) {
+            return;
+        }
+        else if (m_a_util.is_int(s)) {
+            if (!m_ints)
+                fail("logic does not support integers");
+        }
+        else if (m_a_util.is_real(s)) {
+            if (!m_reals)
+                fail("logic does not support reals");
+        }
+        else if (m_bv_util.is_bv_sort(s)) {
+            if (!m_bvs)
+                fail("logic does not support bitvectors");
+        }
+        else if (m_ar_util.is_array(s)) {
+            if (m_arrays) {
+                return;
+            }
+            else if (m_bv_arrays) {
+                if (get_array_arity(s) != 1)
+                    fail("logic supports only unidimensional arrays");
+                if (!m_bv_util.is_bv_sort(get_array_range(s)) || !m_bv_util.is_bv_sort(get_array_domain(s, 0)))
+                    fail("logic supports only arrays from bitvectors to bitvectors");
+            }
+            else {
+                fail("logic does not support arrays");
+            }
+        }
+    }
+
+    void operator()(var * n) { 
+        if (!m_quantifiers)
+            fail("logic does not support quantifiers");
+        check_sort(m.get_sort(n));
+    }
+
+    bool is_int(expr * t) {
+        if (m_a_util.is_uminus(t))
+            t = to_app(t)->get_arg(0);
+        return m_a_util.is_numeral(t);
+    }
+
+    bool is_numeral(expr * t) {
+        if (m_a_util.is_uminus(t))
+            t = to_app(t)->get_arg(0);
+        // c
+        if (is_int(t))
+            return true;
+        // c1/c2
+        if (m_a_util.is_div(t) && is_int(to_app(t)->get_arg(0)) && is_int(to_app(t)->get_arg(1)))
+            return true;
+        return false;
+    }
+
+    // check if n has at most one argument that is not numeral.
+    void check_mul(app * n) {
+        if (m_nonlinear)
+            return; // nothing to check
+        unsigned num_args = n->get_num_args();
+        bool found_non_numeral = false;
+        for (unsigned i = 0; i < num_args; i++) {
+            if (!is_numeral(n->get_arg(i))) {
+                if (found_non_numeral)
+                    fail("logic does not support nonlinear arithmetic");
+                else
+                    found_non_numeral = true;
+            }
+        }
+    }
+    
+    // check if the divisor is a numeral
+    void check_div(app * n) {
+        SASSERT(n->get_num_args() == 2);
+        if (!m_nonlinear && !is_numeral(n->get_arg(1)))
+            fail("logic does not support nonlinear arithmetic");
+    }
+
+    bool is_diff_var(expr * t) const {
+        if (is_app(t) && to_app(t)->get_decl()->get_family_id() == null_family_id)
+            return true;
+        if (m.is_ite(t))
+            return true;
+        return false;
+    }
+
+    void fail_non_diff(expr * t) {
+        TRACE("check_logic", tout << mk_pp(t, m) << "\n";);
+        fail("logic only supports difference arithmetic");
+    }
+
+    bool same_args(app * t) {
+        unsigned num_args = t->get_num_args();
+        if (num_args == 0)
+            return false;
+        expr * arg = t->get_arg(0);
+        for (unsigned i = 1; i < num_args; i++) {
+            if (t->get_arg(i) != arg)
+                return false;
+        }
+        return true;
+    }
+
+    bool is_arith(expr * t) const {
+        return m.get_sort(t)->get_family_id() == m_a_util.get_family_id();
+    }
+
+    bool is_offset(app * t) {
+        while (true) {
+            expr * non_numeral = 0;
+            unsigned num_args = t->get_num_args();
+            for (unsigned i = 0; i < num_args; i++) {
+                expr * arg = t->get_arg(i);
+                if (is_numeral(arg))
+                    continue;
+                if (non_numeral != 0)
+                    return false;
+                non_numeral = arg;
+            }
+            if (is_diff_var(non_numeral))
+                return true;
+            if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))
+                return false;
+            t = to_app(non_numeral);
+        }
+        return true;
+    }
+    
+    bool is_diff_arg(expr * t) {
+        if (is_diff_var(t))
+            return true; 
+        if (is_numeral(t))
+            return true;
+        if (m_a_util.is_add(t) || m_a_util.is_sub(t))
+            return is_offset(to_app(t));
+        return false;
+    }
+
+    // Check if n is a diff logic predicate
+    void check_diff_predicate(app * n) {
+        expr * lhs = n->get_arg(0);
+        expr * rhs = n->get_arg(1);
+        if (!is_arith(lhs))
+            return; // formula is not in arithmetic
+        if (is_diff_arg(lhs) && is_diff_arg(rhs))
+            return;
+        if (is_numeral(lhs))
+            std::swap(lhs, rhs);
+        if (!is_numeral(rhs))
+            fail_non_diff(n);
+        if (!m_a_util.is_sub(lhs) || to_app(lhs)->get_num_args() != 2)
+            fail_non_diff(n);
+        expr * t1 = to_app(lhs)->get_arg(0);
+        expr * t2 = to_app(lhs)->get_arg(1);
+        if (is_diff_var(t1) && is_diff_var(t2))
+            return; 
+        if (m_a_util.is_add(t1) && m_a_util.is_add(t2)) {
+            // QF_RDL supports (<= (- (+ x ... x) (+ y ... y)) c)
+            if (to_app(t1)->get_num_args() != to_app(t2)->get_num_args())
+                fail_non_diff(n);
+            if (!same_args(to_app(t1)) || !same_args(to_app(t2)))
+                fail_non_diff(n);
+            return;
+        }
+        fail_non_diff(n);
+    }
+
+    void check_diff_arg(expr * t) {
+        if (!is_diff_arg(t))
+            fail_non_diff(t);
+    }
+
+    // Check if the arith args of n are of the form (t + k) where k is a numeral.
+    void check_diff_args(app * n) {
+        unsigned num_args = n->get_num_args();
+        for (unsigned i = 0; i < num_args; i++) {
+            if (is_arith(n))
+                check_diff_arg(n);
+        }
+    }
+    
+    void operator()(app * n) {
+        sort * s = m.get_sort(n);
+        check_sort(s);
+        func_decl * f = n->get_decl();
+        family_id fid = f->get_family_id();
+        if (fid == null_family_id) {
+            if (!m_uf && f->get_arity() > 0)
+                fail("logic does not support uninterpreted functions");
+            if (m_diff)
+                check_diff_args(n);
+        }
+        else if (fid == m_a_util.get_family_id()) {
+            if (m_a_util.is_mul(n))
+                check_mul(n);
+            else if (m_a_util.is_div(n) || m_a_util.is_idiv(n) || m_a_util.is_rem(n) || m_a_util.is_mod(n))
+                check_div(n);
+            if (m_diff) {
+                if (m_a_util.is_le(n) || m_a_util.is_lt(n) || m_a_util.is_ge(n) || m_a_util.is_gt(n))
+                    check_diff_predicate(n);
+            }
+            if (!m_ints || !m_reals) {
+                if (m_a_util.is_to_real(n) || m_a_util.is_to_int(n))
+                    fail("logic does not support casting operators");
+            }                
+        }
+        else if (fid == m_bv_util.get_family_id()) {
+            // nothing to check... 
+        }
+        else if (fid == m_ar_util.get_family_id()) {
+            // nothing to check... 
+            if (m_diff)
+                check_diff_args(n);
+        }
+        else if (fid == m.get_basic_family_id()) {
+            // nothing to check... 
+            if (m_diff) {
+                if (m.is_eq(n))
+                    check_diff_predicate(n);
+                else if (m.is_distinct(n) || m.is_ite(n))
+                    check_diff_args(n);
+            }
+        }
+        else if (m.is_builtin_family_id(fid)) {
+            // nothing to check
+        }
+        else {
+            fail("logic does not support theory");
+        }
+    }
+    
+    void operator()(quantifier * n) { 
+        if (!m_quantifiers)
+            fail("logic does not support quantifiers");
+    }
+
+    bool operator()(expr * n) {
+        if (m_unknown_logic)
+            return true;
+        try {
+            quick_for_each_expr(*this, n);
+            return true;
+        }
+        catch (failed) {
+            return false;
+        }
+    }
+
+    bool operator()(func_decl * f) {
+        if (m_unknown_logic)
+            return true;
+        try {
+            unsigned arity = f->get_arity();
+            if (arity > 0) {
+                if (!m_uf)
+                    fail("logic does not support uninterpreted functions");
+                for (unsigned i = 0; i < arity; i++)
+                    check_sort(f->get_domain(i));
+            }
+            check_sort(f->get_range());
+            return true;
+        }
+        catch (failed) {
+            return false;
+        }
+    }
+};
+
+check_logic::check_logic() {
+    m_imp = 0;
+}
+   
+check_logic::~check_logic() {
+    if (m_imp)
+        dealloc(m_imp);
+}
+
+void check_logic::reset() {
+    if (m_imp)
+        dealloc(m_imp);
+    m_imp = 0;
+}
+
+void check_logic::set_logic(ast_manager & m, symbol const & logic) {
+    reset();
+    m_imp = alloc(imp, m);
+    m_imp->set_logic(logic);
+}
+
+bool check_logic::operator()(expr * n) {
+    if (m_imp)
+        return m_imp->operator()(n);
+    return true;
+}
+
+bool check_logic::operator()(func_decl * f) {
+    if (m_imp)
+        return m_imp->operator()(f);
+    return true;
+}
+
+char const * check_logic::get_last_error() const {
+    if (m_imp)
+        return m_imp->m_last_error.c_str();
+    return "";
+}

src/cmd_context/check_logic.h

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    check_logic.h
+
+Abstract:
+
+    Check whether a given assertion is in the correct logic or not
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-08-11.
+
+Revision History:
+
+--*/
+#ifndef _CHECK_LOGIC_H_
+#define _CHECK_LOGIC_H_
+
+#include"ast.h"
+
+class check_logic {
+    struct imp;
+    imp * m_imp;
+public:
+    check_logic();
+    ~check_logic();
+    void reset();
+    void set_logic(ast_manager & m, symbol const & logic);
+    bool operator()(expr * n);
+    bool operator()(func_decl * f);
+    char const * get_last_error() const;
+};
+
+#endif

src/cmd_context/check_sat_result.h

@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    check_sat_result.h
+
+Abstract:
+    Abstract interface for storing the result produced by 
+    a check_sat like command
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#ifndef _CHECK_SAT_RESULT_H_
+#define _CHECK_SAT_RESULT_H_
+
+#include"model.h"
+#include"lbool.h"
+#include"statistics.h"
+
+class check_sat_result {
+protected:
+    unsigned    m_ref_count;
+    lbool       m_status; 
+public:
+    check_sat_result():m_ref_count(0), m_status(l_undef) {}
+    virtual ~check_sat_result() {}
+    void inc_ref() { m_ref_count++; }
+    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+    void set_status(lbool r) { m_status = r; }
+    lbool status() const { return m_status; }
+    virtual void collect_statistics(statistics & st) const = 0;
+    virtual void get_unsat_core(ptr_vector<expr> & r) = 0;
+    virtual void get_model(model_ref & m) = 0;
+    virtual proof * get_proof() = 0;
+    virtual std::string reason_unknown() const = 0;
+    virtual void get_labels(svector<symbol> & r) = 0;
+};
+
+struct simple_check_sat_result : public check_sat_result {
+    statistics      m_stats;
+    model_ref       m_model;
+    expr_ref_vector m_core;
+    proof_ref       m_proof;
+    std::string     m_unknown;
+
+    simple_check_sat_result(ast_manager & m):
+        m_core(m),
+        m_proof(m) {
+    }
+    virtual ~simple_check_sat_result() {}
+    virtual void collect_statistics(statistics & st) const { st.copy(m_stats); }
+    virtual void get_unsat_core(ptr_vector<expr> & r) { if (m_status == l_false) r.append(m_core.size(), m_core.c_ptr()); }
+    virtual void get_model(model_ref & m) { 
+        if (m_status != l_false) m = m_model; else m = 0; 
+    }
+    virtual proof * get_proof() { return m_status == l_false ? m_proof.get() : 0; }
+    virtual std::string reason_unknown() const { 
+        return m_unknown; 
+    }
+    virtual void get_labels(svector<symbol> & r) {}
+};
+
+#endif

src/cmd_context/cmd_context.h

@@ -0,0 +1,409 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cmd_context.h
+
+Abstract:
+    Ultra-light command context.
+    It provides a generic command pluging infrastructure.
+    A command context also provides names (aka symbols) to Z3 objects. 
+    These names are used to reference Z3 objects in commands.
+
+Author:
+
+    Leonardo (leonardo) 2011-03-01
+
+Notes:
+
+--*/
+#ifndef _CMD_CONTEXT_H_
+#define _CMD_CONTEXT_H_
+
+#include<sstream>
+#include"ast.h"
+#include"ast_printer.h"
+#include"pdecl.h"
+#include"dictionary.h"
+#include"solver.h"
+#include"datatype_decl_plugin.h"
+#include"stopwatch.h"
+#include"cmd_context_types.h"
+#include"event_handler.h"
+#include"sexpr.h"
+#include"tactic_manager.h"
+#include"check_logic.h"
+#include"progress_callback.h"
+#include"scoped_ptr_vector.h"
+
+struct front_end_params;
+
+class func_decls {
+    func_decl * m_decls;
+public:
+    func_decls():m_decls(0) {}
+    func_decls(ast_manager & m, func_decl * f);
+    void finalize(ast_manager & m);
+    bool contains(func_decl * f) const;
+    bool insert(ast_manager & m, func_decl * f);
+    void erase(ast_manager & m, func_decl * f);
+    bool more_than_one() const;
+    bool clash(func_decl * f) const;
+    bool empty() const { return m_decls == 0; }
+    func_decl * first() const;
+    func_decl * find(unsigned arity, sort * const * domain, sort * range) const;
+    func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const;
+};
+
+/**
+   \brief Generic wrapper.
+*/
+class object_ref {
+    unsigned m_ref_count;
+public:
+    object_ref():m_ref_count(0) {}
+    virtual ~object_ref() {}
+    virtual void finalize(cmd_context & ctx) = 0;
+    void inc_ref(cmd_context & ctx) {
+        m_ref_count++;
+    }
+    void dec_ref(cmd_context & ctx) {
+        SASSERT(m_ref_count > 0);
+        m_ref_count--;
+        if (m_ref_count == 0) {
+            finalize(ctx);
+            dealloc(this);
+        }
+    }
+    virtual char const * kind() const = 0;
+};
+
+class ast_object_ref : public object_ref {
+    ast * m_ast;
+public:
+    ast_object_ref(cmd_context & ctx, ast * a);
+    virtual void finalize(cmd_context & ctx);
+    ast * get_ast() const { return m_ast; }
+    static char const * cls_kind() { return "AST"; }
+    virtual char const * kind() const { return cls_kind(); }
+};
+
+class stream_ref {
+    std::string    m_default_name;
+    std::ostream & m_default;
+    std::string    m_name;
+    std::ostream * m_stream;
+    bool           m_owner;
+public:
+    stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
+    ~stream_ref() { reset(); }
+    void set(char const * name);
+    void reset();
+    std::ostream & operator*() { return *m_stream; }
+    char const * name() const { return m_name.c_str(); }
+};
+
+struct builtin_decl {
+    family_id      m_fid;
+    decl_kind      m_decl;
+    builtin_decl * m_next;
+    builtin_decl():m_fid(null_family_id), m_decl(0), m_next(0) {}
+    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, public ast_printer_context {
+public:
+    enum status {
+        UNSAT, SAT, UNKNOWN
+    };
+    
+    enum check_sat_state {
+        css_unsat, css_sat, css_unknown, css_clear
+    };
+    
+    typedef std::pair<unsigned, expr*> macro;
+
+    struct scoped_watch {
+        cmd_context &   m_ctx;
+    public:
+        scoped_watch(cmd_context & ctx):m_ctx(ctx) { m_ctx.m_watch.reset(); m_ctx.m_watch.start(); }
+        ~scoped_watch() { m_ctx.m_watch.stop(); }
+    };
+
+protected:
+    bool                         m_main_ctx;
+    front_end_params &           m_params;
+    symbol                       m_logic;
+    bool                         m_interactive_mode;
+    bool                         m_global_decls;
+    bool                         m_print_success;
+    unsigned                     m_random_seed;
+    bool                         m_produce_unsat_cores;
+    bool                         m_produce_assignments;
+    status                       m_status;
+    bool                         m_numeral_as_real;
+    bool                         m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
+    bool                         m_exit_on_error;
+    
+    static std::ostringstream    g_error_stream;
+
+    ast_manager *                m_manager;
+    bool                         m_own_manager;
+    pdecl_manager *              m_pmanager;
+    sexpr_manager *              m_sexpr_manager;
+    check_logic                  m_check_logic;
+    stream_ref                   m_regular;
+    stream_ref                   m_diagnostic;
+    dictionary<cmd*>             m_cmds;    
+    dictionary<builtin_decl>     m_builtin_decls;
+    scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
+    dictionary<object_ref*>      m_object_refs; // anything that can be named.
+    dictionary<sexpr*>           m_user_tactic_decls;
+
+    dictionary<func_decls>       m_func_decls;
+    obj_map<func_decl, symbol>   m_func_decl2alias;
+    dictionary<psort_decl*>      m_psort_decls;
+    dictionary<macro>            m_macros;
+    // the following fields m_func_decls_stack, m_psort_decls_stack and m_exprs_stack are used when m_global_decls == false
+    typedef std::pair<symbol, func_decl *> sf_pair;
+    svector<sf_pair>             m_func_decls_stack;
+    svector<symbol>              m_psort_decls_stack;
+    svector<symbol>              m_macros_stack;
+    // 
+    ptr_vector<pdecl>            m_aux_pdecls;
+    ptr_vector<expr>             m_assertions;
+    vector<std::string>          m_assertion_strings;
+    ptr_vector<expr>             m_assumptions; // for unsat-core extraction
+
+    struct scope {
+        unsigned m_func_decls_stack_lim;
+        unsigned m_psort_decls_stack_lim;
+        unsigned m_macros_stack_lim;
+        unsigned m_aux_pdecls_lim;
+        // only m_assertions_lim and m_assumptions_lim are relevant when m_global_decls = true
+        unsigned m_assertions_lim;
+        unsigned m_assumptions_lim;
+    };
+
+    svector<scope>               m_scopes;
+    ref<solver>                  m_solver;
+    ref<check_sat_result>        m_check_sat_result;
+
+    stopwatch                    m_watch;
+
+    class dt_eh : public new_datatype_eh {
+        cmd_context &             m_owner;
+        datatype_util             m_dt_util;
+    public:
+        dt_eh(cmd_context & owner);
+        virtual ~dt_eh();
+        virtual void operator()(sort * dt);
+    };
+
+    friend class dt_eh;
+    scoped_ptr<dt_eh>             m_dt_eh;
+
+    class pp_env;
+    friend class pp_env;
+
+    scoped_ptr<pp_env>            m_pp_env;
+    pp_env & get_pp_env() const;
+
+    void register_builtin_sorts(decl_plugin * p);
+    void register_builtin_ops(decl_plugin * p);
+    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
+    void init_manager_core(bool new_manager);
+    void init_manager();
+    void init_external_manager();
+    void reset_cmds();
+    void finalize_cmds();
+
+    void restore_func_decls(unsigned old_sz);
+    void restore_psort_decls(unsigned old_sz);
+    void restore_macros(unsigned old_sz);
+    void restore_aux_pdecls(unsigned old_sz);
+    void restore_assertions(unsigned old_sz);
+    void restore_assumptions(unsigned old_sz);
+
+    void erase_func_decl_core(symbol const & s, func_decl * f);
+    void erase_psort_decl_core(symbol const & s);
+    void erase_macro_core(symbol const & s);
+
+    bool logic_has_arith_core(symbol const & s) const;
+    bool logic_has_bv_core(symbol const & s) const;
+    bool logic_has_array_core(symbol const & s) const;
+    bool logic_has_seq_core(symbol const & s) const;
+    bool logic_has_arith() const;
+    bool logic_has_bv() const;
+    bool logic_has_seq() const;
+    bool logic_has_array() const;
+    bool logic_has_datatype() const;
+    bool logic_has_floats() const;
+    bool supported_logic(symbol const & s) const;
+
+    void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
+    void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
+
+public:
+    cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
+    ~cmd_context(); 
+    bool is_smtlib2_compliant() const { return m_params.m_smtlib2_compliant; }
+    void set_logic(symbol const & s);
+    bool has_logic() const { return m_logic != symbol::null; }
+    symbol const & get_logic() const { return m_logic; }
+    bool is_logic(char const * l_name) const { return has_logic() && strcmp(m_logic.bare_str(), l_name) == 0; }
+    bool numeral_as_real() const { return m_numeral_as_real; }
+    void set_numeral_as_real(bool f) { m_numeral_as_real = f; }
+    void set_interactive_mode(bool flag) { m_interactive_mode = flag; }
+    void set_ignore_check(bool flag) { m_ignore_check = flag; }
+    void set_exit_on_error(bool flag) { m_exit_on_error = flag; }
+    bool exit_on_error() const { return m_exit_on_error; }
+    bool interactive_mode() const { return m_interactive_mode; }
+    void set_print_success(bool flag) { m_print_success = flag; }
+    bool print_success_enabled() const { return m_print_success; }
+    void print_success() { if (print_success_enabled())  regular_stream() << "success" << std::endl; }
+    void print_unsupported(symbol const & s) { print_unsupported_msg(); print_unsupported_info(s); }
+    bool global_decls() const { return m_global_decls; }
+    void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; }
+    unsigned random_seed() const { return m_random_seed; }
+    void set_random_seed(unsigned s) { m_random_seed = s; }
+    bool produce_models() const { return m_params.m_model; }
+    bool produce_proofs() const { return m_params.m_proof_mode != PGM_DISABLED; }
+    bool produce_unsat_cores() const { return m_produce_unsat_cores; }
+    void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; }
+    bool produce_assignments() const { return m_produce_assignments; }
+    void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
+    void set_status(status st) { m_status = st; }
+    status get_status() const { return m_status; }
+    std::string reason_unknown() const;
+
+    bool has_manager() const { return m_manager != 0; }
+    ast_manager & m() const { if (!m_manager) const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
+    virtual ast_manager & get_ast_manager() { return m(); }
+    pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
+    sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
+    front_end_params & params() const { return m_params; }
+ 
+    void set_solver(solver * s);
+    solver * get_solver() const { return m_solver.get(); }
+    void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
+    check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
+    check_sat_state cs_state() const;
+    void validate_model();
+    
+    bool is_func_decl(symbol const & s) const;
+    bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); }
+    void insert(cmd * c);
+    void insert(symbol const & s, func_decl * f); 
+    void insert(func_decl * f) { insert(f->get_name(), f); }
+    void insert(symbol const & s, psort_decl * p);
+    void insert(psort_decl * p) { insert(p->get_name(), p); }
+    void insert(symbol const & s, unsigned arity, expr * t);
+    void insert(symbol const & s, object_ref *);
+    void insert(tactic_cmd * c) { tactic_manager::insert(c); }
+    void insert(probe_info * p) { tactic_manager::insert(p); } 
+    void insert_user_tactic(symbol const & s, sexpr * d); 
+    void insert_aux_pdecl(pdecl * p);
+    func_decl * find_func_decl(symbol const & s) const;
+    func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, 
+                               unsigned arity, sort * const * domain, sort * range) const;
+    psort_decl * find_psort_decl(symbol const & s) const;
+    macro find_macro(symbol const & s) const;
+    cmd * find_cmd(symbol const & s) const;
+    sexpr * find_user_tactic(symbol const & s) const;
+    object_ref * find_object_ref(symbol const & s) const;
+    void mk_const(symbol const & s, expr_ref & result) const;
+    void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, 
+                expr_ref & r) const;
+    void erase_cmd(symbol const & s);
+    void erase_func_decl(symbol const & s);
+    void erase_func_decl(symbol const & s, func_decl * f);
+    void erase_func_decl(func_decl * f) { erase_func_decl(f->get_name(), f); }
+    void erase_psort_decl(symbol const & s);
+    void erase_macro(symbol const & s);
+    void erase_object_ref(symbol const & s);
+    void erase_user_tactic(symbol const & s);
+    void reset_func_decls();
+    void reset_psort_decls();
+    void reset_macros();
+    void reset_object_refs();
+    void reset_user_tactics();
+    void set_regular_stream(char const * name) { m_regular.set(name); }
+    void set_diagnostic_stream(char const * name); 
+    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;
+    cmd_iterator begin_cmds() const { return m_cmds.begin(); }
+    cmd_iterator end_cmds() const { return m_cmds.end(); }
+
+    typedef dictionary<sexpr*>::iterator user_tactic_iterator;
+    user_tactic_iterator begin_user_tactics() const { return m_user_tactic_decls.begin(); }
+    user_tactic_iterator end_user_tactics() const { return m_user_tactic_decls.end(); }
+
+    void display_assertions();
+    void display_statistics(bool show_total_time = false, double total_time = 0.0);
+    void reset(bool finalize = false);
+    void assert_expr(expr * t);
+    void assert_expr(symbol const & name, expr * t);
+    void push_assert_string(std::string const & s) { SASSERT(m_interactive_mode); m_assertion_strings.push_back(s); }
+    void push();
+    void push(unsigned n);
+    void pop(unsigned n);
+    void check_sat(unsigned num_assumptions, expr * const * assumptions);
+    // display the result produced by a check-sat or check-sat-using commands in the regular stream
+    void display_sat_result(lbool r);
+    // check if result produced by check-sat or check-sat-using matches the known status
+    void validate_check_sat_result(lbool r); 
+    unsigned num_scopes() const { return m_scopes.size(); }
+
+    dictionary<macro> const & get_macros() const { return m_macros; }
+
+    bool is_model_available() const;
+
+    double get_seconds() const { return m_watch.get_seconds(); }
+
+    ptr_vector<expr>::const_iterator begin_assertions() const { return m_assertions.begin(); }
+    ptr_vector<expr>::const_iterator end_assertions() const { return m_assertions.end(); }
+
+    ptr_vector<expr>::const_iterator begin_assumptions() const { return m_assumptions.begin(); }
+    ptr_vector<expr>::const_iterator end_assumptions() const { return m_assumptions.end(); }
+
+    /**
+       \brief Hack: consume assertions if there are no scopes.
+       This method is useful for reducing memory consumption in huge benchmarks were incrementality is not an issue.
+    */
+    bool consume_assertions() {
+        if (num_scopes() > 0)
+            return false;
+        restore_assertions(0);
+        restore_assumptions(0);
+        return true;
+    }
+
+    format_ns::format * pp(sort * s) const;
+    virtual void pp(sort * s, format_ns::format_ref & r) const { r = pp(s); }
+    virtual void pp(func_decl * f, format_ns::format_ref & r) const;
+    virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const;
+    virtual void pp(expr * n, format_ns::format_ref & r) 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;
+
+    // display assertions as a SMT2 benchmark.
+    void display_smt2_benchmark(std::ostream & out, unsigned num, expr * const * assertions, symbol const & logic = symbol::null) const;
+
+
+    virtual void slow_progress_sample();
+    virtual void fast_progress_sample();
+};
+
+std::ostream & operator<<(std::ostream & out, cmd_context::status st);
+
+#endif

src/cmd_context/cmd_context_to_goal.cpp

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    cmd_context_to_goal.cpp
+
+Abstract:
+    Procedure for copying the assertions in the
+    command context to a goal object.
+
+Author:
+
+    Leonardo (leonardo) 2012-10-21
+
+Notes:
+
+--*/
+#include"cmd_context.h"
+#include"goal.h"
+
+/**
+   \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());
+    }
+}

src/cmd_context/cmd_context_to_goal.h

@@ -0,0 +1,24 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    cmd_context_to_goal.h
+
+Abstract:
+    Procedure for copying the assertions in the
+    command context to a goal object.
+
+Author:
+
+    Leonardo (leonardo) 2012-10-21
+
+Notes:
+
+--*/
+#ifndef _CMD_CONTEXT_TO_GOAL_H_
+#define _CMD_CONTEXT_TO_GOAL_H_
+
+void assert_exprs_from(cmd_context const & ctx, goal & t);
+
+#endif

src/cmd_context/cmd_util.cpp

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cmd_util.cpp
+
+Abstract:
+    Macros for definining new SMT2 front-end cmds.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-01
+
+Notes:
+
+--*/
+#include"cmd_context.h"
+
+ast * get_ast_ref(cmd_context & ctx, symbol const & v) {
+    object_ref * r = ctx.find_object_ref(v);
+    SASSERT(r != 0);
+    if (r->kind() != ast_object_ref::cls_kind()) 
+        throw cmd_exception("global variable does not reference an AST");
+    return static_cast<ast_object_ref*>(r)->get_ast();
+}
+
+expr * get_expr_ref(cmd_context & ctx, symbol const & v) {
+    ast * r = get_ast_ref(ctx, v);
+    if (!is_expr(r))
+        throw cmd_exception("global variable does not reference a term");
+    return to_expr(r);
+}
+
+void store_expr_ref(cmd_context & ctx, symbol const & v, expr * t) {
+    ctx.insert(v, alloc(ast_object_ref, ctx, t));
+}
+

src/cmd_context/cmd_util.h

@@ -0,0 +1,80 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cmd_util.h
+
+Abstract:
+    Macros for definining new SMT2 front-end cmds.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-01
+
+Notes:
+
+--*/
+#ifndef _CMD_UTIL_H_
+#define _CMD_UTIL_H_
+
+#define ATOMIC_CMD(CLS_NAME, NAME, DESCR, ACTION)                               \
+class CLS_NAME : public cmd {                                                   \
+public:                                                                         \
+    CLS_NAME():cmd(NAME) {}                                                     \
+    virtual char const * get_usage() const { return 0; }                        \
+    virtual char const * get_descr(cmd_context & ctx) const { return DESCR; }   \
+    virtual unsigned get_arity() const { return 0; }                            \
+    virtual void execute(cmd_context & ctx) { ACTION }                          \
+};
+
+#define UNARY_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION)             \
+class CLS_NAME : public cmd {                                                           \
+public:                                                                                 \
+    CLS_NAME():cmd(NAME) {}                                                             \
+    virtual char const * get_usage() const { return USAGE; }                            \
+    virtual char const * get_descr(cmd_context & ctx) const { return DESCR; }           \
+    virtual unsigned get_arity() const { return 1; }                                    \
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return ARG_KIND; }    \
+    virtual void set_next_arg(cmd_context & ctx, ARG_TYPE arg) { ACTION }               \
+}
+
+// Macro for creating commands where the first argument is a symbol
+// The second argument cannot be a symbol
+#define BINARY_SYM_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION)        \
+class CLS_NAME : public cmd {                                                           \
+    symbol m_sym;                                                                       \
+public:                                                                                 \
+    CLS_NAME():cmd(NAME) {}                                                             \
+    virtual char const * get_usage() const { return USAGE; }                            \
+    virtual char const * get_descr(cmd_context & ctx) const { return DESCR; }           \
+    virtual unsigned get_arity() const { return 2; }                                    \
+    virtual void prepare(cmd_context & ctx) { m_sym = symbol::null; }                   \
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {                       \
+        return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND;                           \
+    }                                                                                   \
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_sym = s; }       \
+    virtual void set_next_arg(cmd_context & ctx, ARG_TYPE arg) { ACTION }               \
+};    
+   
+
+class ast;
+class expr;
+class symbol;
+class cmd_context;
+
+/**
+   \brief Return the AST that is referenced by the global variable v in the given command context.
+*/
+ast * get_ast_ref(cmd_context & ctx, symbol const & v);
+/**
+   \brief Return the expression that is referenced by the global variable v in the given command context.
+*/
+expr * get_expr_ref(cmd_context & ctx, symbol const & v);
+
+/**
+   \brief Store t in the global variable v.
+*/
+void store_expr_ref(cmd_context & ctx, symbol const & v, expr * t);
+
+#endif

src/cmd_context/echo_tactic.cpp

@@ -0,0 +1,84 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    echo_tactic.h
+
+Abstract:
+
+    Tactic and probe for dumping data.
+
+Author:
+
+    Leonardo (leonardo) 2012-10-20
+
+Notes:
+
+--*/
+#include"tactic.h"
+#include"probe.h"
+#include"cmd_context.h"
+
+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);
+}

src/cmd_context/echo_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    echo_tactic.h
+
+Abstract:
+
+    Tactic and probe for dumping data.
+
+Author:
+
+    Leonardo (leonardo) 2012-10-20
+
+Notes:
+
+--*/
+#ifndef _ECHO_TACTICS_H_
+#define _ECHO_TACTICS_H_
+
+class cmd_context;
+class tactic;
+class probe;
+
+tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline = true);
+// Display the value returned by p in the diagnostic_stream
+tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline = true);
+
+#endif

src/cmd_context/eval_cmd.cpp

@@ -0,0 +1,87 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    eval_cmd.cpp
+
+Abstract:
+
+    eval_cmd
+
+Author:
+
+    Leonardo (leonardo) 2011-04-30
+
+Notes:
+
+--*/
+#include"cmd_context.h"
+#include"model_evaluator.h"
+#include"parametric_cmd.h"
+#include"scoped_timer.h"
+#include"scoped_ctrl_c.h"
+#include"cancel_eh.h"
+
+class eval_cmd : public parametric_cmd {
+    expr *                   m_target;
+    symbol                   m_last; 
+public:
+    eval_cmd():parametric_cmd("eval") {}
+
+    virtual char const * get_usage() const { return "<term> (<keyword> <value>)*"; }
+    
+    virtual char const * get_main_descr() const { 
+        return "evaluate the given term in the current model.";
+    }
+
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
+        model_evaluator::get_param_descrs(p);
+        insert_timeout(p);
+    }
+
+    virtual void prepare(cmd_context & ctx) { 
+        parametric_cmd::prepare(ctx);
+        m_target = 0; 
+    }
+
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+        if (m_target == 0) return CPK_EXPR;
+        return parametric_cmd::next_arg_kind(ctx);
+    }
+
+    virtual void set_next_arg(cmd_context & ctx, expr * arg) {
+        m_target = arg;
+    }
+
+    virtual void execute(cmd_context & ctx) {
+        if (!ctx.is_model_available())
+            throw cmd_exception("model is not available");
+        model_ref md;
+        check_sat_result * last_result = ctx.get_check_sat_result();
+        SASSERT(last_result);
+        last_result->get_model(md);
+        expr_ref r(ctx.m());
+        unsigned timeout = m_params.get_uint(":timeout", UINT_MAX);
+        model_evaluator ev(*(md.get()), m_params);
+        cancel_eh<model_evaluator> eh(ev);
+        { 
+            scoped_ctrl_c ctrlc(eh);
+            scoped_timer timer(timeout, &eh);
+            cmd_context::scoped_watch sw(ctx);
+            try {
+                ev(m_target, r);
+            }
+            catch (model_evaluator_exception & ex) {
+                ctx.regular_stream() << "(error \"evaluator failed: " << ex.msg() << "\")" << std::endl;
+                return;
+            }
+        }
+        ctx.display(ctx.regular_stream(), r.get());
+        ctx.regular_stream() << std::endl;
+    }
+};
+
+void install_eval_cmd(cmd_context & ctx) {
+    ctx.insert(alloc(eval_cmd));
+}

src/cmd_context/eval_cmd.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    eval_cmd.h
+
+Abstract:
+
+    eval_cmd
+
+Author:
+
+    Leonardo (leonardo) 2011-04-30
+
+Notes:
+
+--*/
+#ifndef _EVAL_CMD_H_
+#define _EVAL_CMD_H_
+
+class cmd_context;
+
+void install_eval_cmd(cmd_context & ctx);
+
+#endif

src/cmd_context/parametric_cmd.cpp

@@ -0,0 +1,64 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    parametric_cmd.h
+
+Abstract:
+    A generic parametric cmd.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-22
+
+Notes:
+
+--*/
+#include<sstream>
+#include"parametric_cmd.h"
+
+char const * parametric_cmd::get_descr(cmd_context & ctx) const { 
+    if (m_descr == 0) {
+        const_cast<parametric_cmd*>(this)->m_descr = alloc(string_buffer<>);
+        m_descr->append(get_main_descr());
+        m_descr->append("\nThe following options are available:\n");
+        std::ostringstream buf;
+        pdescrs(ctx).display(buf, 2);
+        m_descr->append(buf.str().c_str());
+    }
+    return m_descr->c_str();
+}
+
+cmd_arg_kind parametric_cmd::next_arg_kind(cmd_context & ctx) const {
+    if (m_last == symbol::null) return CPK_KEYWORD;
+    return pdescrs(ctx).get_kind(m_last);
+}
+
+void parametric_cmd::set_next_arg(cmd_context & ctx, symbol const & s) { 
+    if (m_last == symbol::null) {
+        m_last = s;
+        if (pdescrs(ctx).get_kind(m_last.bare_str()) == CPK_INVALID)
+            throw cmd_exception("invalid keyword argument");
+        return;
+    }
+    m_params.set_sym(m_last.bare_str(), s);
+    m_last = symbol::null;
+}
+
+param_descrs const & parametric_cmd::pdescrs(cmd_context & ctx) const {
+    if (!m_pdescrs) {
+        parametric_cmd * _this = const_cast<parametric_cmd*>(this);
+        _this->m_pdescrs = alloc(param_descrs);
+        _this->init_pdescrs(ctx, *(_this->m_pdescrs));
+    }
+    return *m_pdescrs;
+}
+
+
+
+
+
+
+
+

src/cmd_context/parametric_cmd.h

@@ -0,0 +1,79 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    parametric_cmd.h
+
+Abstract:
+    A generic parametric cmd.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-22
+
+Notes:
+
+--*/
+#ifndef _PARAMETRIC_CMD_H_
+#define _PARAMETRIC_CMD_H_
+
+#include"params.h"
+#include"symbol.h"
+#include"string_buffer.h"
+#include"cmd_context_types.h"
+
+class parametric_cmd : public cmd {
+public:
+    symbol                   m_last; 
+    string_buffer<> *        m_descr;
+    params_ref               m_params;
+    scoped_ptr<param_descrs> m_pdescrs;
+public:
+    parametric_cmd(char const * name):cmd(name), m_descr(0) {}
+    virtual ~parametric_cmd() { if (m_descr) dealloc(m_descr); }
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & d) = 0;
+    param_descrs const & pdescrs(cmd_context & ctx) const;
+    params_ref const & ps() const { return m_params; }
+    virtual char const * get_main_descr() const = 0;
+    virtual char const * get_descr(cmd_context & ctx) const;
+    virtual unsigned get_arity() const { return VAR_ARITY; }
+    virtual void prepare(cmd_context & ctx) { m_last = symbol::null; m_params.reset(); }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const;
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s);
+    virtual void set_next_arg(cmd_context & ctx, unsigned val) { 
+        m_params.set_uint(m_last, val); 
+        m_last = symbol::null; 
+    }
+    virtual void set_next_arg(cmd_context & ctx, bool val) { 
+        m_params.set_bool(m_last, val); 
+        m_last = symbol::null; 
+    }
+    virtual void set_next_arg(cmd_context & ctx, rational const & val) { 
+        m_params.set_rat(m_last, val); 
+        m_last = symbol::null; 
+    }
+    virtual void set_next_arg(cmd_context & ctx, char const * val) { 
+        m_params.set_str(m_last, val); 
+        m_last = symbol::null; 
+    }
+    virtual void set_next_arg(cmd_context & ctx, sort * s) { 
+        NOT_IMPLEMENTED_YET();
+        // m_params.set_sort(m_last, s); 
+        // m_last = symbol::null; 
+    }
+    virtual void set_next_arg(cmd_context & ctx, expr * t) { 
+        NOT_IMPLEMENTED_YET();
+        // m_params.set_expr(m_last, t); 
+        // m_last = symbol::null; 
+    }
+    virtual void set_next_arg(cmd_context & ctx, func_decl * f) { 
+        NOT_IMPLEMENTED_YET();
+        // m_params.set_func_decl(m_last, f); 
+        // m_last = symbol::null; 
+    }
+};
+
+#endif
+
+

src/cmd_context/pdecl.cpp

@@ -0,0 +1,958 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdecl.cpp
+
+Abstract:
+
+    Parametric declarations for SMT-LIB 2.0 + inductive data-types.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-03-02.
+
+Revision History:
+
+--*/
+#include"pdecl.h"
+#include"datatype_decl_plugin.h"
+using namespace format_ns;
+
+class psort_inst_cache {
+    unsigned              m_num_params;
+    sort *                m_const;
+    obj_map<sort, void *> m_map; // if m_num_params == 1 value is a sort, otherwise it is a reference to another inst_cache
+public:
+    psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) { 
+    }
+
+    ~psort_inst_cache() { SASSERT(m_map.empty()); SASSERT(m_const == 0); }
+    
+    void finalize(pdecl_manager & m) {
+        if (m_num_params == 0) {
+            SASSERT(m_map.empty());
+            if (m_const)
+                m.m().dec_ref(m_const);
+            m_const = 0;
+        }
+        else {
+            SASSERT(m_const == 0);
+            obj_map<sort, void *>::iterator it  = m_map.begin();
+            obj_map<sort, void *>::iterator end = m_map.end();
+            for (; it != end; ++it) {
+                m.m().dec_ref((*it).m_key);
+                if (m_num_params == 1) {
+                    m.m().dec_ref(static_cast<sort*>((*it).m_value));
+                }
+                else {
+                    psort_inst_cache * child = static_cast<psort_inst_cache*>((*it).m_value);
+                    child->finalize(m);
+                    child->~psort_inst_cache();
+                    m.a().deallocate(sizeof(psort_inst_cache), child);
+                }
+            }
+            m_map.reset();
+        }
+    }
+
+    void insert(pdecl_manager & m, sort * const * s, sort * r) {
+        if (m_num_params == 0) {
+            SASSERT(m_const == 0);
+            m.m().inc_ref(r);
+            m_const = r;
+            return;
+        }
+        psort_inst_cache * curr = this;
+        while (true) {
+            if (curr->m_num_params == 1) {
+                SASSERT(!curr->m_map.contains(*s));
+                curr->m_map.insert(*s, r);
+                m.m().inc_ref(*s);
+                m.m().inc_ref(r);
+                return;
+            }
+            void * next = 0;
+            if (!curr->m_map.find(*s, next)) {
+                next = new (m.a().allocate(sizeof(psort_inst_cache))) psort_inst_cache(curr->m_num_params-1);
+                curr->m_map.insert(*s, next);
+                m.m().inc_ref(*s);
+            }
+            SASSERT(next != 0);
+            SASSERT(curr->m_num_params == static_cast<psort_inst_cache*>(next)->m_num_params + 1);
+            s++;
+            curr = static_cast<psort_inst_cache*>(next);
+        }
+    }
+    
+    sort * find(sort * const * s) const {
+        if (m_num_params == 0)
+            return m_const;
+        psort_inst_cache const * curr = this;
+        while (true) {
+            if (curr->m_num_params == 1) {
+                void * r = 0;
+                curr->m_map.find(*s, r);
+                return static_cast<sort*>(r);
+            }
+            else {
+                void * next = 0;
+                curr->m_map.find(*s, next);
+                if (next == 0)
+                    return 0;
+                s++;
+                curr = static_cast<psort_inst_cache*>(next);
+            }
+        }
+    }
+
+    bool empty() const { return m_num_params == 0 ? m_const == 0 : m_map.empty(); }
+};
+
+void psort::cache(pdecl_manager & m, sort * const * s, sort * r) {
+    if (!m_inst_cache)
+        m_inst_cache = m.mk_inst_cache(m_num_params);
+    m_inst_cache->insert(m, s, r);
+}
+
+sort * psort::find(sort * const * s) const {
+    if (!m_inst_cache)
+        return 0;
+    return m_inst_cache->find(s);
+}
+
+void psort::finalize(pdecl_manager & m) {
+    m.del_inst_cache(m_inst_cache);
+    m_inst_cache = 0;
+}
+
+/**
+   \brief wrapper for sorts.
+*/
+class psort_sort : public psort {
+    friend class pdecl_manager;
+    sort * m_sort;
+    psort_sort(unsigned id, pdecl_manager & m, sort * s):psort(id, 0), m_sort(s) { m.m().inc_ref(m_sort); }
+    virtual void finalize(pdecl_manager & m) { 
+        m.m().dec_ref(m_sort); 
+        psort::finalize(m);
+    }
+    virtual bool check_num_params(pdecl * other) const { return true; }
+    virtual size_t obj_size() const { return sizeof(psort_sort); }
+    sort * get_sort() const { return m_sort; }
+    virtual sort * instantiate(pdecl_manager & m, sort * const * s) { return m_sort; }
+public:
+    virtual ~psort_sort() {}
+    virtual bool is_sort_wrapper() const { return true; }
+    virtual char const * hcons_kind() const { return "psort_sort"; }
+    virtual unsigned hcons_hash() const { return m_sort->get_id(); }
+    virtual bool hcons_eq(psort const * other) const {
+        if (other->hcons_kind() != hcons_kind()) 
+            return false;
+        return m_sort == static_cast<psort_sort const *>(other)->m_sort;
+    }
+    virtual void display(std::ostream & out) const {
+        out << m_sort->get_name();
+    }
+};
+
+class psort_var : public psort {
+    friend class pdecl_manager;
+    unsigned m_idx;
+    psort_var(unsigned id, unsigned num_params, unsigned idx):psort(id, num_params), m_idx(idx) { SASSERT(idx < num_params); }
+    virtual sort * instantiate(pdecl_manager & m, sort * const * s) { return s[m_idx]; }
+    virtual size_t obj_size() const { return sizeof(psort_var); }
+public:
+    virtual ~psort_var() {}
+    virtual char const * hcons_kind() const { return "psort_var"; }
+    virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); }
+    virtual bool hcons_eq(psort const * other) const {
+        if (other->hcons_kind() != hcons_kind()) 
+            return false;
+        return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx;
+    }
+    virtual void display(std::ostream & out) const {
+        out << "s_" << m_idx;
+    }
+};
+
+class psort_app : public psort {
+    friend class pdecl_manager;
+    psort_decl *  m_decl;
+    ptr_vector<psort> m_args;
+
+    psort_app(unsigned id, unsigned num_params, pdecl_manager & m, psort_decl * d, unsigned num_args, psort * const * args):
+        psort(id, num_params),
+        m_decl(d),
+        m_args(num_args, args) {
+        m.inc_ref(d);
+        m.inc_ref(num_args, args);
+        SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params());
+        DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this););
+    }
+
+    virtual void finalize(pdecl_manager & m) { 
+        m.lazy_dec_ref(m_decl);
+        m.lazy_dec_ref(m_args.size(), m_args.c_ptr());
+        psort::finalize(m);
+    }
+
+    virtual size_t obj_size() const { return sizeof(psort_app); }
+
+    struct khasher {
+        unsigned operator()(psort_app const * d) const { return d->m_decl->hash(); }
+    };
+    
+    struct chasher {
+        unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); }
+    };
+
+    virtual sort * instantiate(pdecl_manager & m, sort * const * s) { 
+        sort * r = find(s);
+        if (r) 
+            return r;
+        sort_ref_buffer args_i(m.m());
+        unsigned sz = m_args.size();
+        for (unsigned i = 0; i < sz; i++) {
+            sort * a = m_args[i]->instantiate(m, s);
+            args_i.push_back(a);
+        }
+        r = m_decl->instantiate(m, args_i.size(), args_i.c_ptr());
+        cache(m, s, r);
+        return r;
+    }
+
+public:
+    virtual ~psort_app() {}
+    virtual char const * hcons_kind() const { return "psort_app"; }
+    virtual unsigned hcons_hash() const { 
+        return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size());
+    }
+    virtual bool hcons_eq(psort const * other) const {
+        if (other->hcons_kind() != hcons_kind()) 
+            return false;
+        if (get_num_params() != other->get_num_params())
+            return false;
+        psort_app const * _other = static_cast<psort_app const *>(other);
+        if (m_decl != _other->m_decl)
+            return false;
+        SASSERT(m_args.size() == _other->m_args.size());
+        unsigned sz = m_args.size();
+        for (unsigned i = 0; i < sz; i++) {
+            if (m_args[i] != _other->m_args[i])
+                return false;
+        }
+        return true;
+    }
+    virtual void display(std::ostream & out) const {
+        if (m_args.empty()) {
+            out << m_decl->get_name();
+        }
+        else {
+            out << "(" << m_decl->get_name();
+            unsigned sz = m_args.size();
+            for (unsigned i = 0; i < sz; i++) {
+                out << " ";
+                m_args[i]->display(out);
+            }
+            out << ")";
+        }
+    }
+};
+
+psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n):
+    pdecl(id, num_params),
+    m_name(n),
+    m_inst_cache(0) {
+}
+
+void psort_decl::finalize(pdecl_manager & m) {
+    m.del_inst_cache(m_inst_cache);
+    m_inst_cache = 0;
+}
+
+void psort_decl::cache(pdecl_manager & m, sort * const * s, sort * r) {
+    if (!m_inst_cache)
+        m_inst_cache = m.mk_inst_cache(m_num_params);
+    m_inst_cache->insert(m, s, r);
+}
+
+sort * psort_decl::find(sort * const * s) {
+    if (!m_inst_cache)
+        return 0;
+    return m_inst_cache->find(s);
+}
+
+psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p):
+    psort_decl(id, num_params, m, n),
+    m_def(p) {
+    m.inc_ref(p);
+    SASSERT(p == 0 || num_params == p->get_num_params());
+}
+
+void psort_user_decl::finalize(pdecl_manager & m) {
+    m.dec_ref(m_def);
+    m_def = 0;
+    psort_decl::finalize(m);
+}
+
+sort * psort_user_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
+    SASSERT(n == m_num_params);
+    sort * r = find(s);
+    if (r)
+        return r;
+    if (m_def == 0) {
+        user_sort_plugin * plugin = m.m().get_user_sort_plugin();
+        buffer<parameter> ps;
+        for (unsigned i = 0; i < n; i++)
+            ps.push_back(parameter(s[i]));
+        decl_kind kind = plugin->register_name(m_name);
+        r  = plugin->mk_sort(kind, ps.size(), ps.c_ptr());
+    }
+    else {
+        r = m_def->instantiate(m, s);
+    }
+    cache(m, s, r);
+    m.save_info(r, this, n, s);
+    return r;
+}
+
+void display_sort_args(std::ostream & out, unsigned num_params) {
+    if (num_params > 0)
+        out << " (";
+    for (unsigned i = 0; i < num_params; i++) {
+        if (i > 0) out << " ";
+        out << "s_" << i;
+    }
+    if (num_params > 0)
+        out << ") ";
+}
+
+void psort_user_decl::display(std::ostream & out) const {
+    out << "(declare-sort " << m_name;
+    display_sort_args(out, m_num_params);
+    if (m_def)
+        m_def->display(out);
+    out << ")";
+}
+
+psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k):
+    psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n),
+    m_fid(fid),
+    m_kind(k) {
+}
+
+sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
+    if (n == 0) {
+        sort * r = m.m().mk_sort(m_fid, m_kind);
+        m.save_info(r, this, 0, s);
+        return r;
+    }
+    else {
+        buffer<parameter> params;
+        for (unsigned i = 0; i < n; i++)
+            params.push_back(parameter(s[i]));
+        sort * r = m.m().mk_sort(m_fid, m_kind, n, params.c_ptr());
+        m.save_info(r, this, n, s);
+        return r;
+    }
+}
+
+sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, unsigned const * s) {
+    if (n == 0) {
+        sort * r = m.m().mk_sort(m_fid, m_kind);
+        m.save_info(r, this, 0, s);
+        return r;
+    }
+    else {
+        buffer<parameter> params;
+        for (unsigned i = 0; i < n; i++)
+            params.push_back(parameter(s[i]));
+        sort * r = m.m().mk_sort(m_fid, m_kind, n, params.c_ptr());
+        m.save_info(r, this, n, s);
+        return r;
+    }
+}
+
+void psort_builtin_decl::display(std::ostream & out) const {
+    out << "(declare-builtin-sort " << m_name << ")";
+}
+
+void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const {
+    switch (kind()) {
+    case PTR_PSORT:        get_psort()->display(out); break;
+    case PTR_REC_REF:      out << dts[get_idx()]->get_name(); break;
+    case PTR_MISSING_REF:  out << get_missing_ref(); break;
+    }
+}
+
+paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r):
+    pdecl(id, num_params),
+    m_name(n), 
+    m_type(r) {
+    if (m_type.kind() == PTR_PSORT) 
+        m.inc_ref(r.get_psort());
+}
+
+void paccessor_decl::finalize(pdecl_manager & m) { 
+    if (m_type.kind() == PTR_PSORT) 
+        m.lazy_dec_ref(m_type.get_psort()); 
+}
+
+bool paccessor_decl::has_missing_refs(symbol & missing) const {
+    if (m_type.kind() == PTR_MISSING_REF) {
+        missing = m_type.get_missing_ref();
+        return true;
+    }
+    return false;
+}
+
+bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
+    TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n"; 
+          if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";);
+    if (m_type.kind() != PTR_MISSING_REF)
+        return true;
+    int idx;
+    if (symbol2idx.find(m_type.get_missing_ref(), idx)) {
+        m_type = ptype(idx);
+        SASSERT(m_type.kind() == PTR_REC_REF);
+        return true;
+    }
+    missing = m_type.get_missing_ref();
+    return false;
+}
+
+accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) {
+    switch (m_type.kind()) {
+    case PTR_REC_REF: return mk_accessor_decl(m_name, type_ref(m_type.get_idx()));
+    case PTR_PSORT:   return mk_accessor_decl(m_name, type_ref(m_type.get_psort()->instantiate(m, s)));
+    default:
+        // missing refs must have been eliminated.
+        UNREACHABLE();
+        return 0;
+    }
+}
+
+void paccessor_decl::display(std::ostream & out, pdatatype_decl const * const * dts) const {
+    out << "(" << m_name << " ";
+    m_type.display(out, dts);
+    out << ")";
+}
+
+pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+                                     symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors):
+    pdecl(id, num_params),
+    m_name(n),
+    m_recogniser_name(r),
+    m_accessors(num_accessors, accessors) {
+    m.inc_ref(num_accessors, accessors);
+    TRACE("pconstructor_decl", tout << "name: " << n << ", recognizer: " << r << "\n";);
+}
+
+void pconstructor_decl::finalize(pdecl_manager & m) {
+    m.lazy_dec_ref(m_accessors.size(), m_accessors.c_ptr());
+}
+
+bool pconstructor_decl::has_missing_refs(symbol & missing) const {
+    ptr_vector<paccessor_decl>::const_iterator it  = m_accessors.begin();
+    ptr_vector<paccessor_decl>::const_iterator end = m_accessors.end();
+    for (; it != end; ++it) {
+        if ((*it)->has_missing_refs(missing))
+            return true;
+    }
+    return false;
+}
+
+bool pconstructor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
+    ptr_vector<paccessor_decl>::iterator it  = m_accessors.begin();
+    ptr_vector<paccessor_decl>::iterator end = m_accessors.end();
+    for (; it != end; ++it) {
+        if (!(*it)->fix_missing_refs(symbol2idx, missing))
+            return false;
+    }
+    return true;
+}
+
+constructor_decl * pconstructor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) {
+    ptr_buffer<accessor_decl> as;
+    ptr_vector<paccessor_decl>::iterator it  = m_accessors.begin();
+    ptr_vector<paccessor_decl>::iterator end = m_accessors.end();
+    for (; it != end; ++it) 
+        as.push_back((*it)->instantiate_decl(m, s));
+    return mk_constructor_decl(m_name, m_recogniser_name, as.size(), as.c_ptr());
+}
+
+void pconstructor_decl::display(std::ostream & out, pdatatype_decl const * const * dts) const {
+    out << "(" << m_name;
+    ptr_vector<paccessor_decl>::const_iterator it  = m_accessors.begin();
+    ptr_vector<paccessor_decl>::const_iterator end = m_accessors.end();
+    for (; it != end; ++it) {
+        out << " ";
+        (*it)->display(out, dts);
+    }
+    out << ")";
+}
+
+pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+                               symbol const & n, unsigned num_constructors, pconstructor_decl * const * constructors):
+    psort_decl(id, num_params, m, n),
+    m_constructors(num_constructors, constructors),
+    m_parent(0) {
+    m.inc_ref(num_constructors, constructors);
+}
+
+void pdatatype_decl::finalize(pdecl_manager & m) {
+    m.lazy_dec_ref(m_constructors.size(), m_constructors.c_ptr());
+    psort_decl::finalize(m);
+}
+
+bool pdatatype_decl::has_missing_refs(symbol & missing) const {
+    ptr_vector<pconstructor_decl>::const_iterator it  = m_constructors.begin();
+    ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
+    for (; it != end; ++it) {
+        if ((*it)->has_missing_refs(missing))
+            return true;
+    }
+    return false;
+}
+
+bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
+    ptr_vector<pconstructor_decl>::iterator it  = m_constructors.begin();
+    ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();
+    for (; it != end; ++it) {
+        if (!(*it)->fix_missing_refs(symbol2idx, missing))
+            return false;
+    }
+    return true;
+}
+
+datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, sort * const * s) {
+    ptr_buffer<constructor_decl> cs;
+    ptr_vector<pconstructor_decl>::iterator it  = m_constructors.begin();
+    ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();
+    for (; it != end; ++it) {
+        cs.push_back((*it)->instantiate_decl(m, s));
+    }
+    return mk_datatype_decl(m_name, cs.size(), cs.c_ptr());
+}
+
+struct datatype_decl_buffer {
+    ptr_buffer<datatype_decl> m_buffer;
+    ~datatype_decl_buffer() { del_datatype_decls(m_buffer.size(), m_buffer.c_ptr()); }
+};
+
+sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
+    SASSERT(m_num_params == n);
+    sort * r = find(s);
+    if (r)
+        return r;
+    if (m_parent != 0) {
+        if (m_parent->instantiate(m, s)) {
+            r = find(s);
+            SASSERT(r);
+            return r;
+        }
+    }
+    else {
+        datatype_decl_buffer dts;
+        dts.m_buffer.push_back(instantiate_decl(m, s));
+        datatype_decl * d_ptr = dts.m_buffer[0];
+        sort_ref_vector sorts(m.m());
+        bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, sorts);
+        TRACE("pdatatype_decl", tout << "instantiating " << m_name << " is_ok: " << is_ok << "\n";);
+        if (is_ok) {
+            r = sorts.get(0);
+            cache(m, s, r);
+            m.save_info(r, this, n, s);
+            m.notify_new_dt(r);
+            return r;
+        }
+    }
+    return 0;
+}
+
+void pdatatype_decl::display(std::ostream & out) const {
+    out << "(declare-datatype " << m_name;
+    display_sort_args(out, m_num_params);
+    ptr_vector<pconstructor_decl>::const_iterator it  = m_constructors.begin();
+    ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
+    for (bool first = true; it != end; ++it) {
+        if (!first)
+            out << " ";
+        if (m_parent) {
+            (*it)->display(out, m_parent->children());
+        }
+        else {
+            pdatatype_decl const * dts[1] = { this };
+            (*it)->display(out, dts);
+        }
+        first = false;
+    }
+    out << ")";
+}
+
+pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+                                 unsigned num_datatypes, pdatatype_decl * const * dts):
+    pdecl(id, num_params),
+    m_datatypes(num_datatypes, dts) {
+    m.inc_ref(num_datatypes, dts);
+
+    ptr_vector<pdatatype_decl>::iterator it  = m_datatypes.begin();
+    ptr_vector<pdatatype_decl>::iterator end = m_datatypes.end();
+    for (; it != end; ++it) {
+        SASSERT((*it)->m_parent == 0);
+        (*it)->m_parent = this;
+    }
+}
+
+void pdatatypes_decl::finalize(pdecl_manager & m) {
+    m.lazy_dec_ref(m_datatypes.size(), m_datatypes.c_ptr());
+}
+
+bool pdatatypes_decl::fix_missing_refs(symbol & missing) {
+    TRACE("fix_missing_refs", tout << "pdatatypes_decl::fix_missing_refs\n";);
+    dictionary<int> symbol2idx;
+    ptr_vector<pdatatype_decl>::iterator it  = m_datatypes.begin();
+    ptr_vector<pdatatype_decl>::iterator end = m_datatypes.end();
+    for (unsigned idx = 0; it != end; ++it, ++idx)
+        symbol2idx.insert((*it)->get_name(), idx);
+
+    it  = m_datatypes.begin();
+    for (unsigned idx = 0; it != end; ++it, ++idx) {
+        if (!(*it)->fix_missing_refs(symbol2idx, missing))
+            return false;
+    }
+    return true;
+}
+
+bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
+    datatype_decl_buffer dts;
+    ptr_vector<pdatatype_decl>::iterator it  = m_datatypes.begin();
+    ptr_vector<pdatatype_decl>::iterator end = m_datatypes.end();
+    for (; it != end; ++it) {
+        dts.m_buffer.push_back((*it)->instantiate_decl(m, s));
+    }
+    sort_ref_vector sorts(m.m());
+    bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), sorts);
+    if (!is_ok)
+        return false;
+    it  = m_datatypes.begin();
+    for (unsigned i = 0; it != end; ++it, ++i) {
+        sort * new_dt = sorts.get(i);
+        (*it)->cache(m, s, new_dt);
+        m.save_info(new_dt, *it, m_num_params, s);
+        m.notify_new_dt(new_dt);
+    }
+    return true;
+}
+
+struct pdecl_manager::sort_info {
+    psort_decl * m_decl;
+
+    sort_info(pdecl_manager & m, psort_decl * d):
+        m_decl(d) {
+        m.inc_ref(d);
+    }
+    virtual ~sort_info() {}
+    virtual unsigned obj_size() const { return sizeof(sort_info); }
+    virtual void finalize(pdecl_manager & m) {
+        m.dec_ref(m_decl);
+    }
+    virtual void display(std::ostream & out, pdecl_manager const & m) const = 0;
+    virtual format * pp(pdecl_manager const & m) const = 0;
+};
+
+struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
+    ptr_vector<sort> m_args;
+    
+    app_sort_info(pdecl_manager & m, psort_decl * d, unsigned n, sort * const * s):
+        sort_info(m, d),
+        m_args(n, s) {
+        m.m().inc_array_ref(n, s);
+    }
+    
+    virtual ~app_sort_info() {}
+    
+    virtual unsigned obj_size() const { return sizeof(app_sort_info); }
+    
+    virtual void finalize(pdecl_manager & m) {
+        sort_info::finalize(m);
+        m.m().dec_array_ref(m_args.size(), m_args.c_ptr());
+    }
+    
+    virtual void display(std::ostream & out, pdecl_manager const & m) const {
+        if (m_args.empty()) {
+            out << m_decl->get_name();
+        }
+        else {
+            out << "(" << m_decl->get_name();
+            for (unsigned i = 0; i < m_args.size(); i++) {
+                out << " ";
+                m.display(out, m_args[i]);
+            }
+            out << ")";
+        }
+    }
+    
+    virtual format * pp(pdecl_manager const & m) const {
+        if (m_args.empty()) {
+            return mk_string(m.m(), m_decl->get_name().str().c_str());
+        }
+        else {
+            ptr_buffer<format> b;
+            for (unsigned i = 0; i < m_args.size(); i++)
+                b.push_back(m.pp(m_args[i]));
+            return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str());
+        }
+    }
+}; 
+
+struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
+    svector<unsigned> m_indices;
+
+    indexed_sort_info(pdecl_manager & m, psort_decl * d, unsigned n, unsigned const * s):
+        sort_info(m, d),
+        m_indices(n, s) {
+    }
+
+    virtual ~indexed_sort_info() {}
+
+    virtual unsigned obj_size() const { return sizeof(indexed_sort_info); }
+
+    virtual void display(std::ostream & out, pdecl_manager const & m) const {
+        if (m_indices.empty()) {
+            out << m_decl->get_name();
+        }
+        else {
+            out << "(_ " << m_decl->get_name();
+            for (unsigned i = 0; i < m_indices.size(); i++) {
+                out << " " << m_indices[i];
+            }
+            out << ")";
+        }
+    }
+    
+    virtual format * pp(pdecl_manager const & m) const {
+        if (m_indices.empty()) {
+            return mk_string(m.m(), m_decl->get_name().str().c_str());
+        }
+        else {
+            ptr_buffer<format> b;
+            b.push_back(mk_string(m.m(), m_decl->get_name().str().c_str()));
+            for (unsigned i = 0; i < m_indices.size(); i++)
+                b.push_back(mk_unsigned(m.m(), m_indices[i]));
+            return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_");
+        }
+    }
+};
+
+void pdecl_manager::init_list() {
+    SASSERT(m_list == 0);
+    psort * v   = mk_psort_var(1, 0);
+    ptype T(v);
+    ptype ListT(0);
+    paccessor_decl * as[2]    = { mk_paccessor_decl(1, symbol("head"), T), 
+                                  mk_paccessor_decl(1, symbol("tail"), ListT) };
+    pconstructor_decl * cs[2] = { mk_pconstructor_decl(1, symbol("nil"), symbol("is-nil"), 0, 0),
+                                  mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) };
+    m_list = mk_pdatatype_decl(1, symbol("List"), 2, cs);
+    inc_ref(m_list);
+}
+
+pdecl_manager::pdecl_manager(ast_manager & m):
+    m_manager(m),
+    m_allocator(m.get_allocator()),
+    m_new_dt_eh(0) {
+    m_list = 0;
+    m_datatype_fid = m.get_family_id("datatype");
+}
+
+pdecl_manager::~pdecl_manager() {
+    dec_ref(m_list);
+    reset_sort_info();
+    SASSERT(m_sort2psort.empty());
+    SASSERT(m_table.empty());
+}
+
+psort * pdecl_manager::mk_psort_cnst(sort * s) {
+    psort * r = 0;
+    if (m_sort2psort.find(s, r))
+        return r;
+    r = new (a().allocate(sizeof(psort_sort))) psort_sort(m_id_gen.mk(), *this, s);
+    m_sort2psort.insert(s, r);
+    return r;
+}
+
+psort * pdecl_manager::register_psort(psort * n) {
+    psort * r = m_table.insert_if_not_there(n);
+    if (r != n) {
+        del_decl_core(n);
+        return r;
+    }
+    return n;
+}
+
+psort * pdecl_manager::mk_psort_var(unsigned num_params, unsigned vidx) {
+    psort_var * n = new (a().allocate(sizeof(psort_var))) psort_var(m_id_gen.mk(), num_params, vidx);
+    return register_psort(n);
+}
+
+paccessor_decl * pdecl_manager::mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p) {
+    return new (a().allocate(sizeof(paccessor_decl))) paccessor_decl(m_id_gen.mk(), num_params, *this, s, p);
+}
+ 
+pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params, 
+                                                        symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as) {
+    return new (a().allocate(sizeof(pconstructor_decl))) pconstructor_decl(m_id_gen.mk(), num_params, *this,
+                                                                           s, r, num, as);
+}
+
+pdatatype_decl * pdecl_manager::mk_pdatatype_decl(unsigned num_params, symbol const & s, unsigned num, pconstructor_decl * const * cs) {
+    return new (a().allocate(sizeof(pdatatype_decl))) pdatatype_decl(m_id_gen.mk(), num_params, *this,
+                                                                     s, num, cs);
+}
+
+pdatatypes_decl * pdecl_manager::mk_pdatatypes_decl(unsigned num_params, unsigned num, pdatatype_decl * const * dts) {
+    return new (a().allocate(sizeof(pdatatypes_decl))) pdatatypes_decl(m_id_gen.mk(), num_params, *this,
+                                                                       num, dts);
+}
+
+psort * pdecl_manager::mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args) {
+    psort * n = new (a().allocate(sizeof(psort_app))) psort_app(m_id_gen.mk(), num_params, *this, d, num_args, args);
+    return register_psort(n);
+}
+
+psort * pdecl_manager::mk_psort_app(psort_decl * d) {
+    SASSERT(d->get_num_params() == 0 || d->get_num_params() == PSORT_DECL_VAR_PARAMS);
+    sort * s = d->instantiate(*this, 0, static_cast<sort*const*>(0));
+    if (s == 0)
+        return 0;
+    return mk_psort_cnst(s);
+}
+
+psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def) {
+    return new (a().allocate(sizeof(psort_user_decl))) psort_user_decl(m_id_gen.mk(), num_params, *this, n, def);
+}
+
+psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) {
+    return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k);
+}
+
+sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args) {
+    // ignoring stack overflows... sorts are not deeply nested
+    return p->instantiate(*this, args);
+}
+
+void pdecl_manager::del_decl_core(pdecl * p) {
+    TRACE("pdecl_manager", 
+          tout << "del_decl_core:\n";
+          if (p->is_psort()) static_cast<psort*>(p)->display(tout); 
+          else static_cast<psort_decl*>(p)->display(tout);
+          tout << "\n";);
+    size_t sz = p->obj_size();
+    m_id_gen.recycle(p->get_id());
+    p->finalize(*this);
+    p->~pdecl();
+    m_allocator.deallocate(sz, p);
+}
+
+void pdecl_manager::del_decl(pdecl * p) {
+    if (p->is_psort()) {
+        psort * _p = static_cast<psort*>(p);
+        if (_p->is_sort_wrapper())
+            m_sort2psort.erase(static_cast<psort_sort*>(_p)->get_sort());
+        else
+            m_table.erase(_p);
+    }
+    del_decl_core(p); 
+}
+
+void pdecl_manager::del_decls() {
+    while (!m_to_delete.empty()) {
+        pdecl * p = m_to_delete.back();
+        m_to_delete.pop_back();
+        del_decl(p);
+    }
+}
+
+psort_inst_cache * pdecl_manager::mk_inst_cache(unsigned num_params) {
+    return new (a().allocate(sizeof(psort_inst_cache))) psort_inst_cache(num_params);
+}
+
+void pdecl_manager::del_inst_cache(psort_inst_cache * c) {
+    if (c) {
+        c->finalize(*this);
+        c->~psort_inst_cache();
+        a().deallocate(sizeof(psort_inst_cache), c);
+    }
+}
+
+datatype_decl_plugin * pdecl_manager::get_dt_plugin() const {
+    return static_cast<datatype_decl_plugin*>(m().get_plugin(m_datatype_fid));
+}
+
+void pdecl_manager::save_info(sort * s, psort_decl * d, unsigned num_args, sort * const * args) {
+    if (m_sort2info.contains(s))
+        return;
+    sort_info * info = new (a().allocate(sizeof(app_sort_info))) app_sort_info(*this, d, num_args, args);
+    m().inc_ref(s);
+    m_sort2info.insert(s, info);
+}
+
+void pdecl_manager::save_info(sort * s, psort_decl * d, unsigned num_indices, unsigned const * indices) {
+    if (m_sort2info.contains(s))
+        return;
+    sort_info * info = new (a().allocate(sizeof(indexed_sort_info))) indexed_sort_info(*this, d, num_indices, indices);
+    m().inc_ref(s);
+    m_sort2info.insert(s, info);
+}
+
+void pdecl_manager::reset_sort_info() {
+    obj_map<sort, sort_info *>::iterator it  = m_sort2info.begin();
+    obj_map<sort, sort_info *>::iterator end = m_sort2info.end();
+    for (; it != end; ++it) {
+        sort * s         = (*it).m_key;
+        sort_info * info = (*it).m_value;
+        m().dec_ref(s);
+        unsigned sz = info->obj_size();
+        info->finalize(*this);
+        info->~sort_info();
+        m_allocator.deallocate(sz, info);
+    }
+    m_sort2info.reset();
+}
+
+void pdecl_manager::display(std::ostream & out, sort * s) const {
+    sort_info * info = 0;
+    if (m_sort2info.find(s, info)) {
+        info->display(out, *this);
+        return;
+    }
+    out << s->get_name();
+}
+
+format * pdecl_manager::pp(sort * s) const {
+    sort_info * info = 0;
+    if (m_sort2info.find(s, info)) {
+        return info->pp(*this);
+    }
+    unsigned num_params = s->get_num_parameters();
+    if (s->get_family_id() != null_family_id && num_params > 0) {
+        // Small hack to display FP and BitVec sorts that were not explicitly referenced by the user.
+        unsigned i = 0;
+        for (i = 0; i < num_params; i++) {
+            if (!s->get_parameter(i).is_int())
+                break;
+        }
+        if (i == num_params) {
+            // all parameters are integer
+            ptr_buffer<format> b;
+            b.push_back(mk_string(m(), s->get_name().str().c_str()));
+            for (unsigned i = 0; i < num_params; i++)
+                b.push_back(mk_unsigned(m(), s->get_parameter(i).get_int()));
+            return mk_seq1(m(), b.begin(), b.end(), f2f(), "_");
+        }
+    }
+    return mk_string(m(), s->get_name().str().c_str());
+}

src/cmd_context/pdecl.h

@@ -0,0 +1,329 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdecl.h
+
+Abstract:
+
+    Parametric declarations for SMT-LIB 2.0 + inductive data-types.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-03-02.
+
+Revision History:
+
+--*/
+#ifndef _PDECL_H_
+#define _PDECL_H_
+
+#include"ast.h"
+#include"obj_hashtable.h" 
+#include"dictionary.h"
+#include"format.h"
+
+class pdecl_manager;
+
+class pdecl {
+protected:
+    friend class pdecl_manager;
+    unsigned m_id;
+    unsigned m_num_params;
+    unsigned m_ref_count;
+    void inc_ref() { m_ref_count++; }
+    void dec_ref() { SASSERT(m_ref_count > 0); --m_ref_count; }
+    virtual bool is_psort() const { return false; }
+    virtual size_t obj_size() const = 0;
+    pdecl(unsigned id, unsigned num_params):m_id(id), m_num_params(num_params), m_ref_count(0) {}
+    virtual void finalize(pdecl_manager & m) {}
+    virtual ~pdecl() {}
+public:
+    virtual bool check_num_params(pdecl * other) const { return m_num_params == other->m_num_params; }
+    unsigned get_num_params() const { return m_num_params; }
+    unsigned get_id() const { return m_id; }
+    unsigned get_ref_count() const { return m_ref_count; }
+    unsigned hash() const { return m_id; }
+    virtual void display(std::ostream & out) const {}
+};
+
+class psort_inst_cache;
+
+#if defined(__APPLE__) && defined(__MACH__)
+// CMW: for some unknown reason, llvm on OSX does not like the name `psort'
+#define psort Z3_psort
+#endif
+
+/**
+   \brief Parametric sorts.
+*/
+class psort : public pdecl {
+protected:
+    psort_inst_cache * m_inst_cache;
+    friend class pdecl_manager;
+    psort(unsigned id, unsigned num_params):pdecl(id, num_params), m_inst_cache(0) {}
+    virtual bool is_psort() const { return true; }
+    virtual void finalize(pdecl_manager & m);
+    virtual ~psort() {}
+    virtual void cache(pdecl_manager & m, sort * const * s, sort * r);
+    virtual sort * find(sort * const * s) const;
+public:
+    virtual bool is_sort_wrapper() const { return false; }
+    virtual sort * instantiate(pdecl_manager & m, sort * const * s) { return 0; }
+    // we use hash-consing for psorts.
+    virtual char const * hcons_kind() const = 0;
+    virtual unsigned hcons_hash() const = 0;
+    virtual bool hcons_eq(psort const * other) const = 0;
+};
+
+// for hash consing
+struct psort_hash_proc { unsigned operator()(psort * p) const { return p->hcons_hash(); } };
+struct psort_eq_proc { bool operator()(psort * p1, psort * p2) const { return p1->hcons_eq(p2); } };
+typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> psort_table;
+
+#define PSORT_DECL_VAR_PARAMS UINT_MAX
+
+class psort_decl : public pdecl {
+protected:
+    friend class pdecl_manager;
+    symbol                        m_name;
+    psort_inst_cache *            m_inst_cache;
+    void cache(pdecl_manager & m, sort * const * s, sort * r);
+    sort * find(sort * const * s);
+    psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
+    virtual void finalize(pdecl_manager & m);
+    virtual ~psort_decl() {}
+public:
+    virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) = 0;
+    virtual sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) { return 0; }
+    virtual sort * instantiate(pdecl_manager & m) { return instantiate(m, 0, static_cast<sort*const*>(0)); }
+    // return true if the declaration accepts a variable number of parameters.
+    // Only builtin declarations can have a variable number of parameters.
+    bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; }
+    symbol const & get_name() const { return m_name; }
+};
+
+class psort_user_decl : public psort_decl {
+protected:
+    friend class pdecl_manager;
+    psort * m_def;
+    psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p);
+    virtual size_t obj_size() const { return sizeof(psort_user_decl); }
+    virtual void finalize(pdecl_manager & m);
+    virtual ~psort_user_decl() {}
+public:
+    virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
+    virtual void display(std::ostream & out) const;
+};
+
+class psort_builtin_decl : public psort_decl {
+protected:
+    friend class pdecl_manager;
+    family_id m_fid;
+    decl_kind m_kind;
+    psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k);
+    virtual size_t obj_size() const { return sizeof(psort_builtin_decl); }
+    virtual ~psort_builtin_decl() {}
+public:
+    virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
+    virtual sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s);
+    virtual void display(std::ostream & out) const;
+};
+
+class datatype_decl_plugin;
+class datatype_decl;
+class constructor_decl;
+class accessor_decl;
+
+class pdatatypes_decl;
+class pdatatype_decl;
+class pconstructor_decl;
+class paccessor_decl;
+
+enum ptype_kind {
+    PTR_PSORT,       // psort
+    PTR_REC_REF,     // recursive reference
+    PTR_MISSING_REF  // a symbol, it is useful for building parsers.
+};
+
+class ptype {
+    ptype_kind m_kind;
+    union {
+        psort * m_sort;
+        int    m_idx;
+    };
+    symbol     m_missing_ref;
+public:
+    ptype():m_kind(PTR_PSORT), m_sort(0) {}
+    ptype(int idx):m_kind(PTR_REC_REF), m_idx(idx) {}
+    ptype(psort * s):m_kind(PTR_PSORT), m_sort(s) {}
+    ptype(symbol const & s):m_kind(PTR_MISSING_REF), m_missing_ref(s) {}
+    ptype_kind kind() const { return m_kind; }
+    psort * get_psort() const { SASSERT(kind() == PTR_PSORT); return m_sort; }
+    int get_idx() const { SASSERT(kind() == PTR_REC_REF); return m_idx; }
+    symbol const & get_missing_ref() const { SASSERT(kind() == PTR_MISSING_REF); return m_missing_ref; }
+    void display(std::ostream & out, pdatatype_decl const * const * dts) const;
+};
+
+class paccessor_decl : public pdecl {
+    friend class pdecl_manager;
+    friend class pconstructor_decl;
+    symbol   m_name;
+    ptype    m_type;
+    paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r);
+    virtual void finalize(pdecl_manager & m);
+    virtual size_t obj_size() const { return sizeof(paccessor_decl); }
+    bool has_missing_refs(symbol & missing) const;
+    bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
+    accessor_decl * instantiate_decl(pdecl_manager & m, sort * const * s);
+    symbol const & get_name() const { return m_name; }
+    ptype const & get_type() const { return m_type; }
+    virtual ~paccessor_decl() {}
+public:
+    void display(std::ostream & out, pdatatype_decl const * const * dts) const;
+};
+
+class pconstructor_decl : public pdecl {
+    friend class pdecl_manager;
+    friend class pdatatype_decl;
+    symbol                     m_name;
+    symbol                     m_recogniser_name;
+    ptr_vector<paccessor_decl> m_accessors;
+    pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+                      symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors);
+    virtual void finalize(pdecl_manager & m);
+    virtual size_t obj_size() const { return sizeof(pconstructor_decl); }
+    bool has_missing_refs(symbol & missing) const;
+    bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
+    symbol const & get_name() const { return m_name; }
+    symbol const & get_recognizer_name() const { return m_recogniser_name; }
+    constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s);
+    virtual ~pconstructor_decl() {}
+public:
+    void display(std::ostream & out, pdatatype_decl const * const * dts) const;
+};
+
+class pdatatype_decl : public psort_decl {
+    friend class pdecl_manager;
+    friend class pdatatypes_decl;
+    ptr_vector<pconstructor_decl> m_constructors;
+    pdatatypes_decl *             m_parent;
+    pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, 
+                   unsigned num_constructors, pconstructor_decl * const * constructors);
+    virtual void finalize(pdecl_manager & m);
+    virtual size_t obj_size() const { return sizeof(pdatatype_decl); }
+    bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
+    datatype_decl * instantiate_decl(pdecl_manager & m, sort * const * s);
+    virtual ~pdatatype_decl() {}
+public:
+    sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
+    virtual void display(std::ostream & out) const;
+    bool has_missing_refs(symbol & missing) const;
+};
+
+/**
+   \brief Represents a set of parametric mutually recursive inductive data-types.
+*/
+class pdatatypes_decl : public pdecl {
+    friend class pdecl_manager;
+    friend class pdatatype_decl;
+    ptr_vector<pdatatype_decl> m_datatypes;
+    pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, unsigned num_datatypes, pdatatype_decl * const * dts);
+    virtual void finalize(pdecl_manager & m);
+    virtual size_t obj_size() const { return sizeof(pdatatypes_decl); }
+    bool fix_missing_refs(symbol & missing);
+    bool instantiate(pdecl_manager & m, sort * const * s);
+    virtual ~pdatatypes_decl() {}
+public:
+    pdatatype_decl const * const * children() const { return m_datatypes.c_ptr(); }
+};
+
+class new_datatype_eh {
+public:
+    virtual ~new_datatype_eh() {}
+    virtual void operator()(sort * dt) = 0;
+};
+
+class pdecl_manager {
+    ast_manager &                m_manager;
+    small_object_allocator &     m_allocator;
+    id_gen                       m_id_gen;
+    obj_map<sort, psort *>       m_sort2psort;
+    psort_table                  m_table;
+    ptr_vector<pdecl>            m_to_delete;
+    pdatatype_decl *             m_list;
+    family_id                    m_datatype_fid;
+    new_datatype_eh *            m_new_dt_eh;
+
+    struct sort_info;
+    struct app_sort_info;
+    struct indexed_sort_info;
+
+    obj_map<sort, sort_info *>   m_sort2info; // for pretty printing sorts
+    
+    void init_list();
+    void del_decl_core(pdecl * p);
+    void del_decl(pdecl * p);
+    void del_decls();
+    psort * register_psort(psort * n);
+    void reset_sort_info();
+public:
+    pdecl_manager(ast_manager & m);
+    ~pdecl_manager();
+    ast_manager & m() const { return m_manager; }
+    small_object_allocator & a() const { return m_allocator; }
+    family_id get_datatype_fid() const { return m_datatype_fid; }
+    void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; }
+    psort * mk_psort_cnst(sort * s);
+    psort * mk_psort_var(unsigned num_params, unsigned vidx);
+    psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args);
+    psort * mk_psort_app(psort_decl * d);
+    psort_decl * mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def);
+    psort_decl * mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k);
+    paccessor_decl * mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p);
+    pconstructor_decl * mk_pconstructor_decl(unsigned num_params, symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as);
+    pdatatype_decl * mk_pdatatype_decl(unsigned num_params, symbol const & s, unsigned num, pconstructor_decl * const * cs);
+    pdatatypes_decl * mk_pdatatypes_decl(unsigned num_params, unsigned num, pdatatype_decl * const * dts);
+    pdatatype_decl * mk_plist_decl() { if (!m_list) init_list(); return m_list; }
+    bool fix_missing_refs(pdatatypes_decl * s, symbol & missing) { return s->fix_missing_refs(missing); }
+    sort * instantiate(psort * s, unsigned num, sort * const * args);
+
+    void lazy_dec_ref(pdecl * p) { p->dec_ref(); if (p->get_ref_count() == 0) m_to_delete.push_back(p); }
+    template<typename T>
+    void lazy_dec_ref(unsigned num, T * const * ps) { for (unsigned i = 0; i < num; i++) lazy_dec_ref(ps[i]); }
+    void inc_ref(pdecl * p) { if (p) { p->inc_ref(); } }
+    void dec_ref(pdecl * p) { if (p) { lazy_dec_ref(p); del_decls(); } }
+    template<typename T>
+    void inc_ref(unsigned num, T * const * ps) { for (unsigned i = 0; i < num; i++) inc_ref(ps[i]); }
+    template<typename T>
+    void dec_ref(unsigned num, T * const * ps) { lazy_dec_ref(num, ps); del_decls(); }
+    psort_inst_cache * mk_inst_cache(unsigned num_params);
+    void del_inst_cache(psort_inst_cache * c);
+    void notify_new_dt(sort * dt) { if (m_new_dt_eh) (*m_new_dt_eh)(dt); }
+    datatype_decl_plugin * get_dt_plugin() const;
+
+    void save_info(sort * s, psort_decl * d, unsigned num_args, sort * const * args);
+    void save_info(sort * s, psort_decl * d, unsigned num_indices, unsigned const * indices);
+    void display(std::ostream & out, sort * s) const;
+    format_ns::format * pp(sort * s) const;
+};
+
+
+typedef obj_ref<pdecl, pdecl_manager>             pdecl_ref;
+typedef obj_ref<psort, pdecl_manager>             psort_ref;
+typedef obj_ref<paccessor_decl, pdecl_manager>    paccessor_decl_ref;
+typedef obj_ref<pconstructor_decl, pdecl_manager> pconstructor_decl_ref;
+typedef obj_ref<pdatatype_decl, pdecl_manager>    pdatatype_decl_ref;
+typedef obj_ref<pdatatypes_decl, pdecl_manager>   pdatatypes_decl_ref;
+
+typedef ref_vector<pdecl, pdecl_manager>          pdecl_ref_vector;
+typedef ref_vector<psort_decl, pdecl_manager>     psort_decl_ref_vector;
+typedef ref_vector<psort, pdecl_manager>          psort_ref_vector;
+
+typedef ref_buffer<paccessor_decl, pdecl_manager>    paccessor_decl_ref_buffer;
+typedef ref_buffer<pconstructor_decl, pdecl_manager> pconstructor_decl_ref_buffer;
+typedef ref_buffer<pdatatype_decl, pdecl_manager>    pdatatype_decl_ref_buffer;
+typedef ref_buffer<pdatatypes_decl, pdecl_manager>   pdatatypes_decl_ref_buffer;
+
+#endif

src/cmd_context/progress_callback.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2008 Microsoft Corporation
+
+Module Name:
+
+    progress_callback.h
+
+Abstract:
+
+    Virtual callback for reporting progress.
+
+Author:
+
+    Michal Moskal (micmo) 2009-02-17.
+
+Revision History:
+
+--*/
+#ifndef _PROGRESS_CALLBACK_H_
+#define _PROGRESS_CALLBACK_H_
+
+class progress_callback {
+public:
+    virtual ~progress_callback() {}
+    
+    // Called approx. every m_progress_sampling_freq miliseconds
+    virtual void slow_progress_sample() { }
+    
+    // Called on every check for reqsource limit exceeded (mach more frequent).
+    virtual void fast_progress_sample() { }
+};
+
+#endif

src/cmd_context/simplify_cmd.cpp

@@ -0,0 +1,128 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    simplify_cmd.cpp
+
+Abstract:
+    SMT2 front-end 'simplify' command.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-20
+
+Notes:
+
+--*/
+#include"cmd_context.h"
+#include"th_rewriter.h"
+#include"shared_occs.h"
+#include"ast_smt_pp.h"
+#include"for_each_expr.h"
+#include"parametric_cmd.h"
+#include"scoped_timer.h"
+#include"scoped_ctrl_c.h"
+#include"cancel_eh.h"
+#include<iomanip>
+
+class simplify_cmd : public parametric_cmd {
+    expr *                   m_target;
+public:
+    simplify_cmd(char const * name = "simplify"):parametric_cmd(name) {}
+
+    virtual char const * get_usage() const { return "<term> (<keyword> <value>)*"; }
+
+    virtual char const * get_main_descr() const { 
+        return "simplify the given term using builtin theory simplification rules.";
+    }
+    
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
+        th_rewriter::get_param_descrs(p);
+        insert_timeout(p);
+        p.insert(":print", CPK_BOOL, "(default: true)  print the simplified term.");
+        p.insert(":print-proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one.");
+        p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics.");
+    }
+    
+    virtual ~simplify_cmd() {
+    }
+    
+    virtual void prepare(cmd_context & ctx) { 
+        parametric_cmd::prepare(ctx);
+        m_target   = 0; 
+    }
+
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+        if (m_target == 0) return CPK_EXPR;
+        return parametric_cmd::next_arg_kind(ctx);
+    }
+    
+    virtual void set_next_arg(cmd_context & ctx, expr * arg) {
+        m_target = arg;
+    }
+    
+    virtual void execute(cmd_context & ctx) {
+        if (m_target == 0)
+            throw cmd_exception("invalid simplify command, argument expected");
+        expr_ref r(ctx.m());
+        proof_ref pr(ctx.m());
+        if (m_params.get_bool(":som", false))
+            m_params.set_bool(":flat", true);
+        th_rewriter s(ctx.m(), m_params);
+        unsigned cache_sz;
+        unsigned num_steps = 0;
+        unsigned timeout   = m_params.get_uint(":timeout", UINT_MAX);
+        bool failed = false;
+        cancel_eh<th_rewriter> eh(s);
+        { 
+            scoped_ctrl_c ctrlc(eh);
+            scoped_timer timer(timeout, &eh);
+            cmd_context::scoped_watch sw(ctx);
+            try {
+                s(m_target, r, pr);
+            }
+            catch (z3_error & ex) {
+                throw ex;
+            }
+            catch (z3_exception & ex) {
+                ctx.regular_stream() << "(error \"simplifier failed: " << ex.msg() << "\")" << std::endl;
+                failed = true;
+                r = m_target;
+            }
+            cache_sz  = s.get_cache_size();
+            num_steps = s.get_num_steps();
+            s.cleanup();
+        }
+        if (m_params.get_bool(":print", true)) {
+            ctx.display(ctx.regular_stream(), r);
+            ctx.regular_stream() << std::endl; 
+        }
+        if (!failed && m_params.get_bool(":print-proofs", false)) {
+            ast_smt_pp pp(ctx.m());
+            pp.set_logic(ctx.get_logic().str().c_str());
+            pp.display_expr_smt2(ctx.regular_stream(), pr.get());
+            ctx.regular_stream() << std::endl;
+        }
+        if (m_params.get_bool(":print-statistics", false)) {
+            shared_occs s1(ctx.m());
+            if (!failed)
+                s1(r);
+            unsigned long long max_mem = memory::get_max_used_memory();
+            unsigned long long mem = memory::get_allocation_size();
+            ctx.regular_stream() << "(:time " << std::fixed << std::setprecision(2) << ctx.get_seconds() << " :num-steps " << num_steps
+                                 << " :memory " << std::fixed << std::setprecision(2) << static_cast<double>(mem)/static_cast<double>(1024*1024)
+                                 << " :max-memory " << std::fixed << std::setprecision(2) << static_cast<double>(max_mem)/static_cast<double>(1024*1024)
+                                 << " :cache-size: " << cache_sz
+                                 << " :num-nodes-before " << get_num_exprs(m_target);
+            if (!failed)
+                ctx.regular_stream() << " :num-shared " << s1.num_shared() << " :num-nodes " << get_num_exprs(r);
+            ctx.regular_stream() << ")" << std::endl;
+        }
+    }
+};
+
+
+void install_simplify_cmd(cmd_context & ctx, char const * cmd_name) {
+    ctx.insert(alloc(simplify_cmd, cmd_name));
+}

src/cmd_context/simplify_cmd.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    simplify_cmd.h
+
+Abstract:
+    SMT2 front-end 'simplify' command.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-20
+
+Notes:
+
+--*/
+#ifndef _SIMPLIFY_CMD_H_
+#define _SIMPLIFY_CMD_H_
+
+class cmd_context;
+
+void install_simplify_cmd(cmd_context & ctx, char const * cmd_name = "simplify");
+
+#endif

src/cmd_context/solver.cpp

@@ -0,0 +1,195 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver.h
+
+Abstract:
+
+    abstract solver interface
+
+Author:
+
+    Leonardo (leonardo) 2011-03-19
+
+Notes:
+
+--*/
+#include"solver.h"
+// #include"smt_solver.h"
+
+unsigned solver::get_num_assertions() const {
+    NOT_IMPLEMENTED_YET();
+    return 0;
+}
+
+expr * solver::get_assertion(unsigned idx) const {
+    NOT_IMPLEMENTED_YET();
+    return 0;
+}
+
+void solver::display(std::ostream & out) const {
+    out << "(solver)";
+}
+
+#if 0
+class default_solver : public solver {
+    front_end_params * m_params;
+    smt::solver *     m_context;
+public:
+    default_solver():m_params(0), m_context(0) {}
+
+    virtual ~default_solver() {
+        if (m_context != 0)
+            dealloc(m_context);
+    }
+
+    virtual void set_front_end_params(front_end_params & p) {
+        m_params = &p;
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        if (m_context == 0)
+            return;
+        m_context->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        if (m_context == 0) {
+            ast_manager m;
+            m.register_decl_plugins();
+            front_end_params p;
+            smt::solver s(m, p);
+            s.collect_param_descrs(r);
+        }
+        else {
+            m_context->collect_param_descrs(r);
+        }
+    }
+
+    virtual void init(ast_manager & m, symbol const & logic) {
+        SASSERT(m_params);
+        reset();
+        #pragma omp critical (solver)
+        {
+            m_context = alloc(smt::solver, m, *m_params);
+        }
+        if (logic != symbol::null)
+            m_context->set_logic(logic);
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        if (m_context == 0) {
+            return;
+        }
+        else {
+            m_context->collect_statistics(st);
+        }
+    }
+
+    virtual void reset() {
+        if (m_context != 0) {
+            #pragma omp critical (solver)
+            {
+                dealloc(m_context);
+                m_context = 0;
+            }
+        }
+    }
+
+    virtual void assert_expr(expr * t) {
+        SASSERT(m_context);
+        m_context->assert_expr(t);
+    }
+
+    virtual void push() {
+        SASSERT(m_context);
+        m_context->push();
+    }
+
+    virtual void pop(unsigned n) {
+        SASSERT(m_context);
+        m_context->pop(n);
+    }
+
+    virtual unsigned get_scope_level() const {
+        if (m_context)
+            return m_context->get_scope_level();
+        else
+            return 0;
+    }
+
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
+        SASSERT(m_context);
+        return m_context->check(num_assumptions, assumptions);
+    }
+
+    virtual void get_unsat_core(ptr_vector<expr> & r) {
+        SASSERT(m_context);
+        unsigned sz = m_context->get_unsat_core_size();
+        for (unsigned i = 0; i < sz; i++)
+            r.push_back(m_context->get_unsat_core_expr(i));
+    }
+
+    virtual void get_model(model_ref & m) {
+        SASSERT(m_context);
+        m_context->get_model(m);
+    }
+
+    virtual proof * get_proof() {
+        SASSERT(m_context);
+        return m_context->get_proof();
+    }
+
+    virtual std::string reason_unknown() const {
+        SASSERT(m_context);
+        return m_context->last_failure_as_string();
+    }
+
+    virtual void get_labels(svector<symbol> & r) {
+        SASSERT(m_context);
+        buffer<symbol> tmp;
+        m_context->get_relevant_labels(0, tmp);
+        r.append(tmp.size(), tmp.c_ptr());
+    }
+
+    virtual void set_cancel(bool f) {
+        #pragma omp critical (solver)
+        {
+            if (m_context) 
+                m_context->set_cancel(f);
+        }
+    }
+
+    virtual void set_progress_callback(progress_callback * callback) {
+        SASSERT(m_context);
+        m_context->set_progress_callback(callback);
+    }
+
+    virtual unsigned get_num_assertions() const {
+        if (m_context)
+            return m_context->size();
+        else
+            return 0;
+    }
+    
+    virtual expr * get_assertion(unsigned idx) const {
+        SASSERT(m_context);
+        SASSERT(idx < get_num_assertions());
+        return m_context->get_formulas()[idx];
+    }
+
+    virtual void display(std::ostream & out) const {
+        if (m_context)
+            m_context->display(out);
+        else
+            out << "(solver)";
+    }
+   
+};
+
+solver * mk_default_solver() {
+    return alloc(default_solver);
+}
+#endif

src/cmd_context/solver.h

@@ -0,0 +1,63 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver.h
+
+Abstract:
+
+    abstract solver interface
+
+Author:
+
+    Leonardo (leonardo) 2011-03-19
+
+Notes:
+
+--*/
+#ifndef _SOLVER_H_
+#define _SOLVER_H_
+
+#include"check_sat_result.h"
+#include"front_end_params.h"
+#include"progress_callback.h"
+#include"params.h"
+
+class solver : public check_sat_result {
+public:
+    virtual ~solver() {}
+    
+    // for backward compatibility
+    virtual void set_front_end_params(front_end_params & p) {} 
+
+    virtual void updt_params(params_ref const & p) {}
+    virtual void collect_param_descrs(param_descrs & r) {}
+
+    virtual void set_produce_proofs(bool f) {}
+    virtual void set_produce_models(bool f) {}
+    virtual void set_produce_unsat_cores(bool f) {}
+    
+    virtual void init(ast_manager & m, symbol const & logic) = 0;
+    virtual void reset() = 0;
+    virtual void assert_expr(expr * t) = 0;
+    virtual void push() = 0;
+    virtual void pop(unsigned n) = 0;
+    virtual unsigned get_scope_level() const = 0;
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
+
+    virtual void set_cancel(bool f) {}
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
+
+    virtual void set_progress_callback(progress_callback * callback) = 0;
+
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+
+    virtual void display(std::ostream & out) const;
+};
+
+solver * mk_default_solver();
+
+#endif

src/cmd_context/strategic_solver.cpp

@@ -0,0 +1,485 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    strategic_solver.h
+
+Abstract:
+
+    Strategies -> Solver
+
+Author:
+
+    Leonardo (leonardo) 2011-05-19
+
+Notes:
+
+--*/
+#include"strategic_solver.h"
+#include"cmd_context.h"
+#include"scoped_timer.h"
+#include"params2front_end_params.h"
+#include"ast_smt2_pp.h"
+
+// minimum verbosity level for portfolio verbose messages
+#define PS_VB_LVL 15
+
+strategic_solver::strategic_solver():
+    m_manager(0),
+    m_fparams(0),
+    m_force_tactic(false),
+    m_inc_mode(false),
+    m_check_sat_executed(false),
+    m_inc_solver(0),
+    m_inc_solver_timeout(UINT_MAX),
+    m_inc_unknown_behavior(IUB_USE_TACTIC_IF_QF),
+    m_default_fct(0),
+    m_curr_tactic(0),
+    m_proof(0),
+    m_callback(0) {
+    m_use_inc_solver_results = false;
+    DEBUG_CODE(m_num_scopes = 0;);
+    m_produce_proofs = false;
+    m_produce_models = false;
+    m_produce_unsat_cores = false;
+}
+
+strategic_solver::~strategic_solver() {
+    SASSERT(!m_curr_tactic);
+    dictionary<tactic_factory*>::iterator it  = m_logic2fct.begin();
+    dictionary<tactic_factory*>::iterator end = m_logic2fct.end();
+    for (; it != end; ++it) {
+        dealloc(it->m_value);
+    }
+    if (m_proof)
+        m().dec_ref(m_proof);
+}
+
+bool strategic_solver::has_quantifiers() const {
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        if (::has_quantifiers(get_assertion(i)))
+            return true;
+    }
+    return false;
+}
+
+/**
+   \brief Return true if a tactic should be used when the incremental solver returns unknown.
+*/
+bool strategic_solver::use_tactic_when_undef() const {
+    switch (m_inc_unknown_behavior) {
+    case IUB_RETURN_UNDEF: return false;
+    case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
+    case IUB_USE_TACTIC: return true;
+    default:
+        UNREACHABLE();
+        return false;
+    }
+}
+
+void strategic_solver::set_inc_solver(solver * s) {
+    SASSERT(m_inc_solver == 0);
+    SASSERT(m_num_scopes == 0);
+    m_inc_solver = s;
+    if (m_callback)
+        m_inc_solver->set_progress_callback(m_callback);
+}
+
+void strategic_solver::updt_params(params_ref const & p) {
+    if (m_inc_solver)
+        m_inc_solver->updt_params(p);
+    if (m_fparams)
+        params2front_end_params(p, *m_fparams);
+}
+
+
+void strategic_solver::collect_param_descrs(param_descrs & r) {
+    if (m_inc_solver)
+        m_inc_solver->collect_param_descrs(r);
+}
+
+/**
+   \brief Set a timeout for each check_sat query that is processed by the inc_solver.
+   timeout == UINT_MAX means infinite
+   After the timeout a strategy is used.
+*/
+void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
+    m_inc_solver_timeout = timeout;
+}
+
+/**
+   \brief Set the default tactic factory.
+   It is used if there is no tactic for a given logic.
+*/
+void strategic_solver::set_default_tactic(tactic_factory * fct) {
+    m_default_fct = fct;
+}
+
+/**
+   \brief Set a tactic factory for a given logic.
+*/
+void strategic_solver::set_tactic_for(symbol const & logic, tactic_factory * fct) {
+    tactic_factory * old_fct;
+    if (m_logic2fct.find(logic, old_fct)) {
+        dealloc(old_fct);
+    }
+    m_logic2fct.insert(logic, fct);
+}
+
+void strategic_solver::init(ast_manager & m, symbol const & logic) {
+    m_manager = &m;
+    m_logic   = logic;
+    if (m_inc_mode) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->init(m, logic);
+    }
+}
+
+// delayed inc solver initialization
+void strategic_solver::init_inc_solver() {
+    if (m_inc_mode) 
+        return; // solver was already initialized
+    if (!m_inc_solver)
+        return; // inc solver was not installed
+    m_inc_mode = true;
+    m_inc_solver->set_front_end_params(*m_fparams);
+    m_inc_solver->init(m(), m_logic);
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        m_inc_solver->assert_expr(get_assertion(i));
+    }
+}
+
+void strategic_solver::collect_statistics(statistics & st) const {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->collect_statistics(st);
+    }
+    else {
+        if (m_curr_tactic) 
+            m_curr_tactic->collect_statistics(st); // m_curr_tactic is still being executed.
+        else
+            st.copy(m_stats);
+    }
+}
+
+void strategic_solver::reset() {
+    m_logic    = symbol::null;
+    m_inc_mode = false;
+    m_check_sat_executed = false;
+    if (m_inc_solver)
+        m_inc_solver->reset();
+    SASSERT(!m_curr_tactic);
+    m_use_inc_solver_results = false;
+    reset_results();
+}
+
+void strategic_solver::reset_results() {
+    m_use_inc_solver_results = false;
+    m_model = 0;
+    if (m_proof) {
+        m().dec_ref(m_proof);
+        m_proof = 0;
+    }
+    m_reason_unknown.clear();
+    m_stats.reset();
+}
+
+void strategic_solver::assert_expr(expr * t) {
+    if (m_check_sat_executed && !m_inc_mode) {
+        // a check sat was already executed --> switch to incremental mode
+        init_inc_solver();
+        SASSERT(m_inc_solver == 0 || m_inc_mode);
+    }
+    if (m_inc_mode) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->assert_expr(t);
+    }
+}
+
+void strategic_solver::push() {
+    DEBUG_CODE(m_num_scopes++;);
+    init_inc_solver();
+    if (m_inc_solver)
+        m_inc_solver->push();
+}
+
+void strategic_solver::pop(unsigned n) {
+    DEBUG_CODE({
+            SASSERT(n <= m_num_scopes);
+            m_num_scopes -= n;
+        });
+    init_inc_solver();
+    if (m_inc_solver)
+        m_inc_solver->pop(n);
+}
+
+unsigned strategic_solver::get_scope_level() const {
+    if (m_inc_solver)
+        return m_inc_solver->get_scope_level();
+    else
+        return 0;
+}
+
+struct aux_timeout_eh : public event_handler {
+    solver *        m_solver;
+    volatile bool   m_canceled;
+    aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
+    virtual void operator()() {
+        m_solver->cancel();
+        m_canceled = true;
+    }
+};
+
+struct strategic_solver::mk_tactic {
+    strategic_solver *  m_solver;
+
+    mk_tactic(strategic_solver * s, tactic_factory * f):m_solver(s) {
+        ast_manager & m = s->m();
+        params_ref p;
+        front_end_params2params(*s->m_fparams, p);
+        tactic * tct = (*f)(m, p);
+        tct->set_front_end_params(*s->m_fparams);
+        tct->set_logic(s->m_logic);
+        if (s->m_callback)
+            tct->set_progress_callback(s->m_callback);
+        #pragma omp critical (strategic_solver) 
+        {
+            s->m_curr_tactic = tct;
+        }
+    }
+
+    ~mk_tactic() {
+        #pragma omp critical (strategic_solver)
+        {
+            m_solver->m_curr_tactic = 0;
+        }
+    }
+};
+
+tactic_factory * strategic_solver::get_tactic_factory() const {
+    tactic_factory * f = 0;
+    if (m_logic2fct.find(m_logic, f))
+        return f;
+    return m_default_fct.get();
+}
+
+lbool strategic_solver::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
+    if (!m_inc_solver) {
+        IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver was not installed, returning unknown...\n";);
+        m_use_inc_solver_results = false;
+        m_reason_unknown         = "incomplete";
+        return l_undef; 
+    }
+    init_inc_solver();
+    m_use_inc_solver_results = true;
+    return m_inc_solver->check_sat(num_assumptions, assumptions);
+}
+
+lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    reset_results();
+    m_check_sat_executed = true;
+    if (num_assumptions > 0 || // assumptions were provided
+        (!m_fparams->m_auto_config && !m_force_tactic) // auto config and force_tactic are turned off
+        ) {
+        // must use incremental solver
+        return check_sat_with_assumptions(num_assumptions, assumptions);
+    }
+
+    tactic_factory * factory = get_tactic_factory();
+    if (factory == 0)
+        init_inc_solver(); // try to switch to incremental solver
+    
+    if (m_inc_mode) {
+        SASSERT(m_inc_solver);
+        unsigned timeout = m_inc_solver_timeout;
+        if (factory == 0)
+            timeout = UINT_MAX; // there is no tactic available
+        if (timeout == UINT_MAX) {
+            IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (without a timeout).\n";);            
+            m_use_inc_solver_results = true;
+            lbool r = m_inc_solver->check_sat(0, 0);
+            if (r != l_undef || factory == 0 || !use_tactic_when_undef()) {
+                m_use_inc_solver_results = true;
+                return r;
+            }
+        }
+        else {
+            IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (with timeout).\n";);            
+            SASSERT(factory != 0);
+            aux_timeout_eh eh(m_inc_solver.get());
+            lbool r;
+            {
+                scoped_timer timer(m_inc_solver_timeout, &eh);
+                r = m_inc_solver->check_sat(0, 0);
+            }
+            if ((r != l_undef || !use_tactic_when_undef()) && !eh.m_canceled) {
+                m_use_inc_solver_results = true;
+                return r;
+            }
+        }
+        IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver failed, trying tactic.\n";);                        
+    }
+    
+    m_use_inc_solver_results = false;
+    
+    if (factory == 0) {
+        IF_VERBOSE(PS_VB_LVL, verbose_stream() << "there is no tactic available for the current logic.\n";);            
+        m_reason_unknown         = "incomplete";
+        return l_undef; 
+    }
+
+    goal_ref g = alloc(goal, m(), m_produce_proofs, m_produce_models, m_produce_unsat_cores);
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        g->assert_expr(get_assertion(i));
+    }
+    expr_dependency_ref core(m());
+    
+    mk_tactic tct_maker(this, factory);
+    SASSERT(m_curr_tactic);
+
+    proof_ref pr(m());
+    lbool r = ::check_sat(*(m_curr_tactic.get()), g, m_model, pr, core, m_reason_unknown);
+    m_curr_tactic->collect_statistics(m_stats);
+    if (pr) {
+        m_proof = pr; 
+        m().inc_ref(m_proof);
+    }
+    return r;
+}
+
+void strategic_solver::set_cancel(bool f) {
+    if (m_inc_solver)
+        m_inc_solver->set_cancel(f);
+    #pragma omp critical (strategic_solver)
+    {
+        if (m_curr_tactic)
+            m_curr_tactic->set_cancel(f);
+    }
+}
+
+void strategic_solver::get_unsat_core(ptr_vector<expr> & r) {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->get_unsat_core(r); 
+    }
+}
+
+void strategic_solver::get_model(model_ref & m) {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->get_model(m);
+    }
+    else {
+        m = m_model;
+    }
+}
+
+proof * strategic_solver::get_proof() {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        return m_inc_solver->get_proof();
+    }
+    else {
+        return m_proof;
+    }
+}
+
+std::string strategic_solver::reason_unknown() const {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        return m_inc_solver->reason_unknown();
+    }
+    return m_reason_unknown;
+}
+
+void strategic_solver::get_labels(svector<symbol> & r) {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->get_labels(r);
+    }
+}
+
+void strategic_solver::set_progress_callback(progress_callback * callback) { 
+    m_callback = callback; 
+    if (m_inc_solver)
+        m_inc_solver->set_progress_callback(callback);
+}
+
+void strategic_solver::display(std::ostream & out) const {
+    if (m_manager) {
+        unsigned num = get_num_assertions();
+        out << "(solver";
+        for (unsigned i = 0; i < num; i++) {
+            out << "\n  " << mk_ismt2_pp(get_assertion(i), m(), 2);
+        }
+        out << ")";
+    }
+    else {
+        out << "(solver)";
+    }
+}
+
+strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx):
+    m_ctx(ctx) {
+}
+
+unsigned strategic_solver_cmd::get_num_assertions() const {
+    return static_cast<unsigned>(m_ctx.end_assertions() - m_ctx.begin_assertions());
+}
+
+expr * strategic_solver_cmd::get_assertion(unsigned idx) const {
+    SASSERT(idx < get_num_assertions());
+    return m_ctx.begin_assertions()[idx];
+}
+
+strategic_solver_api::ctx::ctx(ast_manager & m):m_assertions(m) {
+}
+
+void strategic_solver_api::init(ast_manager & m, symbol const & logic) {
+    strategic_solver::init(m, logic);
+    m_ctx = alloc(ctx, m);
+}
+
+unsigned strategic_solver_api::get_num_assertions() const {
+    if (m_ctx == 0)
+        return 0;
+    return m_ctx->m_assertions.size();
+}
+
+expr * strategic_solver_api::get_assertion(unsigned idx) const {
+    SASSERT(m_ctx);
+    return m_ctx->m_assertions.get(idx);
+}
+
+void strategic_solver_api::assert_expr(expr * t) {
+    SASSERT(m_ctx);
+    strategic_solver::assert_expr(t);
+    m_ctx->m_assertions.push_back(t);
+}
+
+void strategic_solver_api::push() {
+    SASSERT(m_ctx);
+    strategic_solver::push();
+    m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
+}
+
+void strategic_solver_api::pop(unsigned n) {
+    SASSERT(m_ctx);
+    unsigned new_lvl = m_ctx->m_scopes.size() - n;
+    unsigned old_sz  = m_ctx->m_scopes[new_lvl];
+    m_ctx->m_assertions.shrink(old_sz);
+    m_ctx->m_scopes.shrink(new_lvl);
+    strategic_solver::pop(n);
+}
+
+void strategic_solver_api::reset() {
+    m_ctx = 0;
+    strategic_solver::reset();
+}
+
+
+

src/cmd_context/strategic_solver.h

@@ -0,0 +1,155 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    strategic_solver.h
+
+Abstract:
+
+    Strategies -> Solver
+
+Author:
+
+    Leonardo (leonardo) 2011-05-19
+
+Notes:
+
+--*/
+#ifndef _STRATEGIC_SOLVER_H_
+#define _STRATEGIC_SOLVER_H_
+
+#include"solver.h"
+#include"tactic.h"
+
+class progress_callback;
+struct front_end_params;
+
+class strategic_solver : public solver {
+public:
+    // Behavior when the incremental solver returns unknown.
+    enum inc_unknown_behavior {
+        IUB_RETURN_UNDEF,      // just return unknown
+        IUB_USE_TACTIC_IF_QF,  // invoke tactic if problem is quantifier free
+        IUB_USE_TACTIC         // invoke tactic
+    };
+
+private:
+    ast_manager *        m_manager;
+    front_end_params *   m_fparams;
+    symbol               m_logic;
+    bool                 m_force_tactic; // use tactics even when auto_config = false
+    bool                 m_inc_mode;
+    bool                 m_check_sat_executed;
+    scoped_ptr<solver>   m_inc_solver;
+    unsigned             m_inc_solver_timeout;
+    inc_unknown_behavior m_inc_unknown_behavior;
+    scoped_ptr<tactic_factory>  m_default_fct;
+    dictionary<tactic_factory*> m_logic2fct;
+
+    ref<tactic>          m_curr_tactic;
+    
+    bool                 m_use_inc_solver_results;
+    model_ref            m_model;
+    proof *              m_proof;
+    std::string          m_reason_unknown;
+    statistics           m_stats;
+
+#ifdef Z3DEBUG
+    unsigned             m_num_scopes;
+#endif
+
+    bool                 m_produce_proofs;
+    bool                 m_produce_models;
+    bool                 m_produce_unsat_cores;
+
+    progress_callback *  m_callback;
+
+    void reset_results();
+    void init_inc_solver();
+    tactic_factory * get_tactic_factory() const;
+    lbool check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions);
+
+    struct mk_tactic;
+
+    bool has_quantifiers() const;
+    bool use_tactic_when_undef() const;
+
+public:
+    strategic_solver();
+    ~strategic_solver();
+
+    ast_manager & m() const { SASSERT(m_manager); return *m_manager; }
+
+    void set_inc_solver(solver * s);
+    void set_inc_solver_timeout(unsigned timeout);
+    void set_default_tactic(tactic_factory * fct);
+    void set_tactic_for(symbol const & logic, tactic_factory * fct);
+    void set_inc_unknown_behavior(inc_unknown_behavior b) { m_inc_unknown_behavior = b; }
+    void force_tactic(bool f) { m_force_tactic = f; }
+
+    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; }
+
+    virtual void updt_params(params_ref const & p);
+    virtual void collect_param_descrs(param_descrs & r);
+
+    virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
+    virtual void set_produce_models(bool f) { m_produce_models = f; }
+    virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
+
+    virtual unsigned get_num_assertions() const = 0;
+    virtual expr * get_assertion(unsigned idx) const = 0;
+    
+    virtual void display(std::ostream & out) const;
+    
+    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void collect_statistics(statistics & st) const;
+    virtual void reset();
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual unsigned get_scope_level() const;
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r);
+    virtual void set_cancel(bool f);
+    virtual void set_progress_callback(progress_callback * callback);
+};
+
+// Specialization for the SMT 2.0 command language frontend
+class strategic_solver_cmd : public strategic_solver {
+    cmd_context &        m_ctx;
+public:
+    strategic_solver_cmd(cmd_context & ctx);
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+};
+
+// Specialization for Z3 API
+class strategic_solver_api : public strategic_solver {
+    struct ctx {
+        expr_ref_vector              m_assertions;
+        unsigned_vector              m_scopes;
+        ctx(ast_manager & m);
+    };
+    scoped_ptr<ctx>            m_ctx;
+public:
+    strategic_solver_api() {}
+
+    virtual void init(ast_manager & m, symbol const & logic);
+
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual void reset();
+
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+};
+
+
+
+#endif

src/cmd_context/tactic2solver.cpp

@@ -0,0 +1,249 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic2solver.cpp
+
+Abstract:
+
+    Wrapper for implementing the solver interface
+    using a tactic.
+
+    This is a light version of the strategic solver.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#include"tactic2solver.h"
+#include"params2front_end_params.h"
+#include"ast_smt2_pp.h"
+
+tactic2solver::ctx::ctx(ast_manager & m, symbol const & logic):
+    m_logic(logic),
+    m_assertions(m) {
+}
+
+tactic2solver::~tactic2solver() {
+}
+
+void tactic2solver::init(ast_manager & m, symbol const & logic) {
+    m_ctx = alloc(ctx, m, logic);
+}
+
+void tactic2solver::updt_params(params_ref const & p) {
+    m_params = p;
+}
+
+void tactic2solver::collect_param_descrs(param_descrs & r) {
+    if (m_ctx) {
+        if (!m_ctx->m_tactic) {
+            #pragma omp critical (tactic2solver)
+            {
+                m_ctx->m_tactic = get_tactic(m_ctx->m(), m_params);
+            }
+
+            if (m_ctx->m_tactic) {
+                m_ctx->m_tactic->collect_param_descrs(r);
+            }
+
+            #pragma omp critical (tactic2solver)
+            {
+                m_ctx->m_tactic = 0;
+            }
+        }
+        else {
+            m_ctx->m_tactic->collect_param_descrs(r);
+        }
+    }
+}
+
+void tactic2solver::reset() {
+    SASSERT(m_ctx);
+    m_ctx->m_assertions.reset();
+    m_ctx->m_scopes.reset();
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver::assert_expr(expr * t) {
+    SASSERT(m_ctx);
+    m_ctx->m_assertions.push_back(t);
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver::push() {
+    SASSERT(m_ctx);
+    m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver::pop(unsigned n) {
+    SASSERT(m_ctx);
+    unsigned new_lvl = m_ctx->m_scopes.size() - n;
+    unsigned old_sz  = m_ctx->m_scopes[new_lvl];
+    m_ctx->m_assertions.shrink(old_sz);
+    m_ctx->m_scopes.shrink(new_lvl);
+    m_ctx->m_result = 0;
+}
+
+unsigned tactic2solver::get_scope_level() const {
+    SASSERT(m_ctx);
+    return m_ctx->m_scopes.size();
+}
+
+lbool tactic2solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    SASSERT(m_ctx);
+    ast_manager & m = m_ctx->m();
+    params_ref p = m_params;
+    if (m_fparams)
+        front_end_params2params(*m_fparams, p);
+    #pragma omp critical (tactic2solver)
+    {
+        m_ctx->m_tactic = get_tactic(m, p);
+        if (m_ctx->m_tactic) {
+            m_ctx->m_result = alloc(simple_check_sat_result, m);
+        }
+    }
+    if (!m_ctx->m_tactic)
+        return l_undef;
+    tactic & t                       = *(m_ctx->m_tactic);
+    simple_check_sat_result & result = *(m_ctx->m_result);
+    if (m_fparams)
+        t.set_front_end_params(*m_fparams);
+    goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
+    t.set_logic(m_ctx->m_logic);
+    unsigned sz = m_ctx->m_assertions.size();
+    for (unsigned i = 0; i < sz; i++) {
+        g->assert_expr(m_ctx->m_assertions.get(i));
+    }
+    for (unsigned i = 0; i < num_assumptions; i++) {
+        g->assert_expr(assumptions[i], m.mk_asserted(assumptions[i]), m.mk_leaf(assumptions[i]));
+    }
+
+    model_ref           md;
+    proof_ref           pr(m);
+    expr_dependency_ref core(m);
+    std::string         reason_unknown = "unknown";
+    try {
+        switch (::check_sat(t, g, md, pr, core, reason_unknown)) {
+        case l_true: 
+            result.set_status(l_true);
+            break;
+        case l_false: 
+            result.set_status(l_false);
+            break;
+        default: 
+            result.set_status(l_undef);
+            if (reason_unknown != "")
+                result.m_unknown = reason_unknown;
+            break;
+        }
+    }
+    catch (z3_error & ex) {
+        throw ex;
+    }
+    catch (z3_exception & ex) {
+        TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
+        result.set_status(l_undef);
+        result.m_unknown = ex.msg();
+    }
+    t.collect_statistics(result.m_stats);
+    result.m_model = md;
+    result.m_proof = pr;
+    if (m_produce_unsat_cores) {
+        ptr_vector<expr> core_elems;
+        m.linearize(core, core_elems);
+        result.m_core.append(core_elems.size(), core_elems.c_ptr());
+    }
+    
+    #pragma omp critical (tactic2solver)
+    {
+        m_ctx->m_tactic = 0;
+    }
+    return result.status();
+}
+
+void tactic2solver::set_cancel(bool f) {
+    #pragma omp critical (tactic2solver)
+    {
+        if (m_ctx && m_ctx->m_tactic)
+            m_ctx->m_tactic->set_cancel(f);
+    }
+}
+
+void tactic2solver::collect_statistics(statistics & st) const {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->collect_statistics(st);
+}
+
+void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->get_unsat_core(r);
+}
+
+void tactic2solver::get_model(model_ref & m) {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->get_model(m);
+}
+
+proof * tactic2solver::get_proof() {
+    if (m_ctx->m_result.get())
+        return m_ctx->m_result->get_proof();
+    else
+        return 0;
+}
+
+std::string tactic2solver::reason_unknown() const {
+    if (m_ctx->m_result.get())
+        return m_ctx->m_result->reason_unknown();
+    else
+        return std::string("unknown");
+}
+
+unsigned tactic2solver::get_num_assertions() const {
+    if (m_ctx) 
+        return m_ctx->m_assertions.size();
+    else
+        return 0;
+}
+
+expr * tactic2solver::get_assertion(unsigned idx) const {
+    SASSERT(m_ctx);
+    return m_ctx->m_assertions.get(idx);
+}
+
+void tactic2solver::display(std::ostream & out) const {
+    if (m_ctx) {
+        ast_manager & m = m_ctx->m_assertions.m();
+        unsigned num = m_ctx->m_assertions.size();
+        out << "(solver";
+        for (unsigned i = 0; i < num; i++) {
+            out << "\n  " << mk_ismt2_pp(m_ctx->m_assertions.get(i), m, 2);
+        }
+        out << ")";
+    }
+    else {
+        out << "(solver)";
+    }
+}
+
+void tactic2solver_cmd::set_tactic(tactic_factory * f) {
+    m_tactic_factory = f;
+}
+
+tactic * tactic2solver_cmd::get_tactic(ast_manager & m, params_ref const & p) {
+    if (m_tactic_factory == 0)
+        return 0;
+    return (*m_tactic_factory)(m, p);
+}
+
+tactic * tactic2solver_api::get_tactic(ast_manager & m, params_ref const & p) {
+    m_tactic->cleanup();
+    m_tactic->updt_params(p);
+    return m_tactic.get();
+}
+

src/cmd_context/tactic2solver.h

@@ -0,0 +1,110 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic2solver.h
+
+Abstract:
+
+    Wrapper for implementing the external solver interface
+    using a tactic.
+
+    This is a light version of the strategic solver.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#ifndef _TACTIC2SOLVER_H_
+#define _TACTIC2SOLVER_H_
+
+#include"solver.h"
+#include"tactic.h"
+
+class tactic2solver : public solver {
+    struct ctx {
+        symbol                       m_logic;
+        expr_ref_vector              m_assertions;
+        unsigned_vector              m_scopes;
+        ref<simple_check_sat_result> m_result;
+        tactic_ref                   m_tactic;
+        ctx(ast_manager & m, symbol const & logic);
+        ast_manager & m() const { return m_assertions.m(); }
+    };
+    scoped_ptr<ctx>            m_ctx;
+    front_end_params *         m_fparams;
+    params_ref                 m_params;
+    bool                       m_produce_models;
+    bool                       m_produce_proofs;
+    bool                       m_produce_unsat_cores;
+public:
+    tactic2solver():m_ctx(0), m_fparams(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {}
+    virtual ~tactic2solver();
+
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p) = 0;
+    
+    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; } 
+
+    virtual void updt_params(params_ref const & p);
+    virtual void collect_param_descrs(param_descrs & r);
+
+    virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
+    virtual void set_produce_models(bool f) { m_produce_models = f; }
+    virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
+
+    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void reset();
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual unsigned get_scope_level() const;
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+
+    virtual void set_cancel(bool f);
+
+    virtual void collect_statistics(statistics & st) const;
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r) {}
+
+    virtual void set_progress_callback(progress_callback * callback) {}
+
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+
+    virtual void display(std::ostream & out) const;
+};
+
+/**
+   \brief Specialization for cmd_context
+*/
+class tactic2solver_cmd : public tactic2solver {
+    scoped_ptr<tactic_factory> m_tactic_factory;
+public:
+    virtual ~tactic2solver_cmd() {}
+    /**
+       \brief Set tactic that will be used to process the satisfiability queries.
+    */
+    void set_tactic(tactic_factory * f); 
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+/**
+   \brief Specialization for API
+*/
+class tactic2solver_api : public tactic2solver {
+    tactic_ref m_tactic;
+public:
+    tactic2solver_api(tactic * t):m_tactic(t) {}
+    virtual ~tactic2solver_api() {}
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+
+#endif

src/cmd_context/tactic_cmds.cpp

@@ -0,0 +1,814 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactic_cmds.cpp
+
+Abstract:
+    Support for tactics in SMT 2.0 frontend.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-20
+
+Notes:
+
+--*/
+#include<sstream>
+#include"tactic_cmds.h"
+#include"cmd_context.h"
+#include"cmd_util.h"
+#include"parametric_cmd.h"
+#include"scoped_timer.h"
+#include"scoped_ctrl_c.h"
+#include"cancel_eh.h"
+#include"model_smt2_pp.h"
+#include"params2front_end_params.h"
+#include"ast_smt2_pp.h"
+#include"tactic.h"
+#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);
+}
+
+tactic * tactic_cmd::mk(ast_manager & m) { 
+    return (*m_factory)(m, params_ref()); 
+}
+
+probe_info::probe_info(symbol const & n, char const * d, probe * p):
+    m_name(n),
+    m_descr(d),
+    m_probe(p) {
+}
+
+probe_info::~probe_info() {
+}
+
+class declare_tactic_cmd : public cmd {
+    symbol           m_name;
+    sexpr *          m_decl;
+public:
+    declare_tactic_cmd():
+        cmd("declare-tactic"),
+        m_decl(0) {
+    }
+
+    virtual char const * get_usage() const { return "<symbol> <tactic>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "declare a new tactic, use (help-tactic) for the tactic language syntax."; }
+    virtual unsigned get_arity() const { return 2; }
+    virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_decl = 0; }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
+        if (m_name == symbol::null) return CPK_SYMBOL;
+        return CPK_SEXPR;
+    }
+    virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_name = s; }
+    virtual void set_next_arg(cmd_context & ctx, sexpr * n) { m_decl = n; } 
+    virtual void execute(cmd_context & ctx) {
+        tactic_ref t = sexpr2tactic(ctx, m_decl); // make sure the tactic is well formed.
+        ctx.insert_user_tactic(m_name, m_decl);
+    }
+};
+
+ATOMIC_CMD(get_user_tactics_cmd, "get-user-tactics", "display tactics defined using the declare-tactic command.", {
+    ctx.regular_stream() << "(";
+    std::ostringstream buf;
+    cmd_context::user_tactic_iterator it  = ctx.begin_user_tactics();
+    cmd_context::user_tactic_iterator end = ctx.end_user_tactics();
+    for (bool first = true; it != end; ++it) {
+        if (first) first = false; else buf << "\n ";
+        buf << "(declare-tactic " << it->m_key << " ";
+        it->m_value->display(buf); 
+        buf << ")";
+    }
+    std::string r = buf.str();
+    ctx.regular_stream() << escaped(r.c_str());
+    ctx.regular_stream() << ")\n";
+});
+
+void help_tactic(cmd_context & ctx) {
+    std::ostringstream buf;
+    buf << "combinators:\n";
+    buf << "- (and-then <tactic>+) executes the given tactics sequencially.\n";
+    buf << "- (or-else <tactic>+) tries the given tactics in sequence until one of them succeeds.\n";
+    buf << "- (par-or <tactic>+) executes the given tactics in parallel until one of them succeeds.\n";
+    buf << "- (par-then <tactic1> <tactic2>) executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.\n";
+    buf << "- (try-for <tactic> <num>) excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds.\n";
+    buf << "- (if <probe> <tactic> <tactic>) if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second.\n";
+    buf << "- (when <probe> <tactic>) shorthand for (if <probe> <tactic> skip).\n";
+    buf << "- (fail-if <probe>) fail if <probe> evaluates to true.\n";
+    buf << "- (using-params <tactic> <attribute>*) executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params.\n";
+    buf << "builtin tactics:\n";
+    cmd_context::tactic_cmd_iterator it  = ctx.begin_tactic_cmds();
+    cmd_context::tactic_cmd_iterator end = ctx.end_tactic_cmds();
+    for (; it != end; ++it) {
+        tactic_cmd * cmd = *it;
+        buf << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
+        tactic_ref t = cmd->mk(ctx.m());
+        param_descrs descrs;
+        t->collect_param_descrs(descrs);
+        descrs.display(buf, 4);
+    }
+    buf << "builtin probes:\n";
+    cmd_context::probe_iterator it2  = ctx.begin_probes();
+    cmd_context::probe_iterator end2 = ctx.end_probes();
+    for (; it2 != end2; ++it2) {
+        probe_info * pinfo = *it2;
+        buf << "- " << pinfo->get_name() << " " << pinfo->get_descr() << "\n";
+    }
+    ctx.regular_stream() << "\"" << escaped(buf.str().c_str()) << "\"\n";
+}
+
+ATOMIC_CMD(help_tactic_cmd, "help-tactic", "display the tactic combinators and primitives.", help_tactic(ctx););
+
+class exec_given_tactic_cmd : public parametric_cmd {
+protected:
+    sexpr * m_tactic;
+public:
+    exec_given_tactic_cmd(char const * name):
+        parametric_cmd(name) {
+    }
+
+    virtual char const * get_usage() const { return "<tactic> (<keyword> <value>)*"; }
+    
+    virtual void prepare(cmd_context & ctx) { 
+        parametric_cmd::prepare(ctx);
+        m_tactic = 0;
+    }
+
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+        if (m_tactic == 0) return CPK_SEXPR;
+        return parametric_cmd::next_arg_kind(ctx);
+    }
+    
+    virtual void set_next_arg(cmd_context & ctx, sexpr * arg) {
+        m_tactic = arg;
+    }
+    
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
+        insert_timeout(p);
+        insert_max_memory(p);
+        p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics.");
+    }
+    
+    void display_statistics(cmd_context & ctx, tactic * t) {
+        statistics stats;
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        stats.update("time", ctx.get_seconds());
+        stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
+        stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
+        t->collect_statistics(stats);
+        stats.display_smt2(ctx.regular_stream());
+    }
+};
+
+typedef simple_check_sat_result check_sat_tactic_result;
+
+class check_sat_using_tactict_cmd : public exec_given_tactic_cmd {
+public:
+    check_sat_using_tactict_cmd():
+        exec_given_tactic_cmd("check-sat-using") {
+    }
+
+    virtual char const * get_main_descr() const { return "check if the current context is satisfiable using the given tactic, use (help-tactic) for the tactic language syntax."; }
+
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
+        exec_given_tactic_cmd::init_pdescrs(ctx, p);
+        p.insert(":print-unsat-core", CPK_BOOL, "(default: false) print unsatisfiable core.");
+        p.insert(":print-proof", CPK_BOOL, "(default: false) print proof.");
+        p.insert(":print-model", CPK_BOOL, "(default: false) print model.");
+    }
+    
+    virtual void execute(cmd_context & ctx) {
+        params_ref p = ps();
+        front_end_params2params(ctx.params(), p);
+        tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
+        tref->set_front_end_params(ctx.params());
+        tref->set_logic(ctx.get_logic());
+        ast_manager & m = ctx.m();
+        unsigned timeout   = p.get_uint(":timeout", UINT_MAX);
+        goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
+        assert_exprs_from(ctx, *g);
+        TRACE("check_sat_using", g->display(tout););
+        model_ref           md;
+        proof_ref           pr(m);
+        expr_dependency_ref core(m);
+        std::string reason_unknown;
+        ref<check_sat_tactic_result> result = alloc(check_sat_tactic_result, m);
+        ctx.set_check_sat_result(result.get());
+        {
+            tactic & t = *tref;
+            cancel_eh<tactic>  eh(t);
+            { 
+                scoped_ctrl_c ctrlc(eh);
+                scoped_timer timer(timeout, &eh);
+                cmd_context::scoped_watch sw(ctx);
+                lbool r = l_undef;
+                try {
+                    r = check_sat(t, g, md, pr, core, reason_unknown);
+                    ctx.display_sat_result(r);
+                    result->set_status(r);
+                    if (r == l_undef) {
+                        if (reason_unknown != "") {
+                            result->m_unknown = reason_unknown;
+                            // ctx.diagnostic_stream() << "\"" << escaped(reason_unknown.c_str(), true) << "\"" << std::endl; 
+                        }
+                        else {
+                            result->m_unknown = "unknown";
+                        }
+                    }
+                }
+                catch (z3_error & ex) {
+                    throw ex;
+                }
+                catch (z3_exception & ex) {
+                    result->set_status(l_undef);
+                    result->m_unknown = ex.msg();
+                    ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
+                }
+                ctx.validate_check_sat_result(r);
+            }
+            t.collect_statistics(result->m_stats);
+        }
+        
+        if (ctx.produce_unsat_cores()) {
+            ptr_vector<expr> core_elems;
+            m.linearize(core, core_elems);
+            result->m_core.append(core_elems.size(), core_elems.c_ptr());
+            if (p.get_bool(":print-unsat-core", false)) {
+                ctx.regular_stream() << "(unsat-core";
+                ptr_vector<expr>::const_iterator it  = core_elems.begin();
+                ptr_vector<expr>::const_iterator end = core_elems.end();
+                for (; it != end; ++it) {
+                    ctx.regular_stream() << " ";
+                    ctx.display(ctx.regular_stream(), *it);
+                }
+                ctx.regular_stream() << ")" << std::endl;
+            }
+        }
+        
+        if (ctx.produce_models() && md) {
+            result->m_model = md;
+            if (p.get_bool(":print-model", false)) {
+                ctx.regular_stream() << "(model " << std::endl;
+                model_smt2_pp(ctx.regular_stream(), ctx, *md, 2);
+                ctx.regular_stream() << ")" << std::endl;
+            }
+            if (result->status() == l_true)
+                ctx.validate_model();
+        }
+
+        if (ctx.produce_proofs() && pr) {
+            result->m_proof = pr;
+            if (p.get_bool(":print-proof", false)) {
+                ctx.regular_stream() << mk_ismt2_pp(pr, m) << "\n";
+            }
+        }
+
+        if (p.get_bool(":print-statistics", false))
+            display_statistics(ctx, tref.get());
+    }
+};
+
+class apply_tactic_cmd : public exec_given_tactic_cmd {
+public:
+    apply_tactic_cmd():
+        exec_given_tactic_cmd("apply") {
+    }
+
+    virtual char const * get_main_descr() const { return "apply the given tactic to the current context, and print the resultant set of goals."; }
+
+    virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
+        p.insert(":print", CPK_BOOL, "(default: true) print resultant goals.");
+#ifndef _EXTERNAL_RELEASE
+        p.insert(":print-proof", CPK_BOOL, "(default: false) print proof associated with each assertion.");
+#endif
+        p.insert(":print-model-converter", CPK_BOOL, "(default: false) print model converter.");
+        p.insert(":print-benchmark", CPK_BOOL, "(default: false) display resultant goals as a SMT2 benchmark.");
+#ifndef _EXTERNAL_RELEASE
+        p.insert(":print-dependencies", CPK_BOOL, "(default: false) print dependencies when displaying the resultant set of goals.");
+#endif
+        exec_given_tactic_cmd::init_pdescrs(ctx, p);
+    }
+    
+    virtual void execute(cmd_context & ctx) {
+        params_ref p = ps();
+        front_end_params2params(ctx.params(), p);
+        tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
+        {
+            tactic & t = *(tref.get());
+            ast_manager & m = ctx.m();
+            goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
+            assert_exprs_from(ctx, *g);
+            
+            unsigned timeout   = p.get_uint(":timeout", UINT_MAX); 
+            
+            goal_ref_buffer     result_goals;
+            model_converter_ref mc;
+            proof_converter_ref pc;
+            expr_dependency_ref core(m);
+
+            std::string reason_unknown;
+            bool failed = false;
+            cancel_eh<tactic>  eh(t);
+            { 
+                scoped_ctrl_c ctrlc(eh);
+                scoped_timer timer(timeout, &eh);
+                cmd_context::scoped_watch sw(ctx);
+                try {
+                    exec(t, g, result_goals, mc, pc, core);
+                }
+                catch (tactic_exception & ex) {
+                    ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
+                    failed = true;
+                }
+            }
+            
+            if (!failed && p.get_bool(":print", true)) {
+                bool print_dependencies = p.get_bool(":print-dependencies", false);
+                ctx.regular_stream() << "(goals\n";
+                unsigned sz = result_goals.size();
+                for (unsigned i = 0; i < sz; i++) {
+                    if (print_dependencies)
+                        result_goals[i]->display_with_dependencies(ctx);
+                    else
+                        result_goals[i]->display(ctx);
+                }
+                ctx.regular_stream() << ")\n";
+            }
+
+#ifndef _EXTERNAL_RELEASE
+            if (!failed && ctx.produce_proofs() && p.get_bool(":print-proof", false)) {
+                // TODO
+            }
+#endif
+
+            if (!failed && p.get_bool(":print-benchmark", false)) { 
+                unsigned num_goals = result_goals.size();
+                SASSERT(num_goals > 0);
+                if (num_goals == 1) {
+                    // easy case
+                    goal * fg = result_goals[0];
+                    unsigned sz = fg->size();
+                    ptr_buffer<expr> assertions;
+                    for (unsigned i = 0; i < sz; i++) {
+                        assertions.push_back(fg->form(i));
+                    }
+                    ctx.display_smt2_benchmark(ctx.regular_stream(), assertions.size(), assertions.c_ptr());
+                }
+                else {
+                    // create a big OR
+                    expr_ref_buffer or_args(m);
+                    ptr_vector<expr> formulas;
+                    for (unsigned i = 0; i < num_goals; i++) {
+                        formulas.reset();
+                        result_goals[i]->get_formulas(formulas);
+                        if (formulas.size() == 1)
+                            or_args.push_back(formulas[0]);
+                        else
+                            or_args.push_back(m.mk_and(formulas.size(), formulas.c_ptr()));
+                    }
+                    expr_ref assertion_ref(m);
+                    assertion_ref = m.mk_or(or_args.size(), or_args.c_ptr());
+                    expr * assertions[1] = { assertion_ref.get() };
+                    ctx.display_smt2_benchmark(ctx.regular_stream(), 1, assertions);
+                }
+            }
+            
+            if (!failed && mc && p.get_bool(":print-model-converter", false)) 
+                mc->display(ctx.regular_stream());
+            
+            if (p.get_bool(":print-statistics", false))
+                display_statistics(ctx, tref.get());
+        }
+    }
+};
+
+           
+void install_core_tactic_cmds(cmd_context & ctx) {
+    ctx.insert(alloc(declare_tactic_cmd));
+    ctx.insert(alloc(get_user_tactics_cmd));
+    ctx.insert(alloc(help_tactic_cmd));
+    ctx.insert(alloc(check_sat_using_tactict_cmd));
+    ctx.insert(alloc(apply_tactic_cmd));
+}
+
+static tactic * mk_and_then(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children < 2)
+        throw cmd_exception("invalid and-then combinator, at least one argument expected", n->get_line(), n->get_pos());
+    if (num_children == 2)
+        return sexpr2tactic(ctx, n->get_child(1));
+    tactic_ref_buffer args;
+    for (unsigned i = 1; i < num_children; i++)
+        args.push_back(sexpr2tactic(ctx, n->get_child(i)));
+    return and_then(args.size(), args.c_ptr());
+}
+
+static tactic * mk_or_else(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children < 2)
+        throw cmd_exception("invalid or-else combinator, at least one argument expected", n->get_line(), n->get_pos());
+    if (num_children == 2)
+        return sexpr2tactic(ctx, n->get_child(1));
+    tactic_ref_buffer args;
+    for (unsigned i = 1; i < num_children; i++)
+        args.push_back(sexpr2tactic(ctx, n->get_child(i)));
+    return or_else(args.size(), args.c_ptr());
+}
+
+static tactic * mk_par(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children < 2)
+        throw cmd_exception("invalid par-or combinator, at least one argument expected", n->get_line(), n->get_pos());
+    if (num_children == 2)
+        return sexpr2tactic(ctx, n->get_child(1));
+    tactic_ref_buffer args;
+    for (unsigned i = 1; i < num_children; i++)
+        args.push_back(sexpr2tactic(ctx, n->get_child(i)));
+    return par(args.size(), args.c_ptr());
+}
+
+static tactic * mk_par_then(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children < 2)
+        throw cmd_exception("invalid par-then combinator, at least one argument expected", n->get_line(), n->get_pos());
+    if (num_children == 2)
+        return sexpr2tactic(ctx, n->get_child(1));
+    tactic_ref_buffer args;
+    for (unsigned i = 1; i < num_children; i++)
+        args.push_back(sexpr2tactic(ctx, n->get_child(i)));
+    return par_and_then(args.size(), args.c_ptr());
+}
+
+static tactic * mk_try_for(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 3)
+        throw cmd_exception("invalid try-for combinator, two arguments expected", n->get_line(), n->get_pos());
+    if (!n->get_child(2)->is_numeral() || !n->get_child(2)->get_numeral().is_unsigned())
+        throw cmd_exception("invalid try-for combinator, second argument must be an unsigned integer", n->get_line(), n->get_pos());
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    unsigned timeout = n->get_child(2)->get_numeral().get_unsigned();
+    return try_for(t, timeout);
+}
+
+static tactic * mk_repeat(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 3 && num_children != 2)
+        throw cmd_exception("invalid repeat combinator, one or two arguments expected", n->get_line(), n->get_pos());
+    unsigned max = UINT_MAX;
+    if (num_children == 3) {
+        if (!n->get_child(2)->is_numeral() || !n->get_child(2)->get_numeral().is_unsigned())
+            throw cmd_exception("invalid repeat combinator, second argument must be an unsigned integer", n->get_line(), n->get_pos());
+        max = n->get_child(2)->get_numeral().get_unsigned();
+    }
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    return repeat(t, max);
+}
+
+static tactic * mk_using_params(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children < 2)
+        throw cmd_exception("invalid using-params combinator, at least one argument expected", n->get_line(), n->get_pos());
+    if (num_children == 2)
+        return sexpr2tactic(ctx, n->get_child(1));
+    tactic_ref t = sexpr2tactic(ctx, n->get_child(1));
+    param_descrs descrs;
+    t->collect_param_descrs(descrs);
+    params_ref p;
+    unsigned i = 2;
+    while (i < num_children) {
+        sexpr * c = n->get_child(i);
+        i++;
+        if (!c->is_keyword())
+            throw cmd_exception("invalid using-params combinator, keyword expected", c->get_line(), c->get_pos());
+        if (i == num_children)
+            throw cmd_exception("invalid using-params combinator, parameter value expected", c->get_line(), c->get_pos());
+        symbol param_name = c->get_symbol();
+        c = n->get_child(i);
+        i++;
+        switch (descrs.get_kind(param_name)) {
+        case CPK_INVALID:
+            throw cmd_exception("invalid using-params combinator, unknown parameter ", param_name, c->get_line(), c->get_pos());
+        case CPK_BOOL:
+            if (!c->is_symbol() || (c->get_symbol() != "true" && c->get_symbol() != "false"))
+                throw cmd_exception("invalid parameter value, true or false expected", c->get_line(), c->get_pos());
+            p.set_bool(param_name, c->get_symbol() == "true");
+            break;
+        case CPK_UINT:
+            if (!c->is_numeral() || !c->get_numeral().is_unsigned())
+                throw cmd_exception("invalid parameter value, unsigned integer expected", c->get_line(), c->get_pos());
+            p.set_uint(param_name, c->get_numeral().get_unsigned());
+            break;
+        case CPK_NUMERAL:
+            if (!c->is_numeral())
+                throw cmd_exception("invalid parameter value, numeral expected", c->get_line(), c->get_pos());
+            p.set_rat(param_name, c->get_numeral());
+            break;
+        case CPK_SYMBOL:
+            if (!c->is_symbol())
+                throw cmd_exception("invalid parameter value, symbol expected", c->get_line(), c->get_pos());
+            p.set_sym(param_name, c->get_symbol());
+            break;
+        case CPK_DOUBLE:
+            if (!c->is_numeral())
+                throw cmd_exception("invalid parameter value, numeral expected", c->get_line(), c->get_pos());
+            p.set_double(param_name, c->get_numeral().get_double());
+            break;
+        default:
+            throw cmd_exception("invalid using-params combinator, unsupported parameter kind");
+        }
+    }
+    return using_params(t.get(), p);
+}
+
+static tactic * mk_if(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 4)
+        throw cmd_exception("invalid if/conditional combinator, three arguments expected", n->get_line(), n->get_pos());
+    probe_ref   c = sexpr2probe(ctx, n->get_child(1));
+    tactic_ref  t = sexpr2tactic(ctx, n->get_child(2));
+    tactic_ref  e = sexpr2tactic(ctx, n->get_child(3));
+    return cond(c.get(), t.get(), e.get());
+}
+
+static tactic * mk_fail_if(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 2)
+        throw cmd_exception("invalid fail-if tactic, one argument expected", n->get_line(), n->get_pos());
+    probe_ref   c = sexpr2probe(ctx, n->get_child(1));
+    return fail_if(c.get());
+}
+
+static tactic * mk_when(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 3)
+        throw cmd_exception("invalid when combinator, two arguments expected", n->get_line(), n->get_pos());
+    probe_ref   c = sexpr2probe(ctx, n->get_child(1));
+    tactic_ref  t = sexpr2tactic(ctx, n->get_child(2));
+    return cond(c.get(), t.get(), mk_skip_tactic());
+}
+
+static tactic * mk_echo(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children < 2)
+        throw cmd_exception("invalid echo tactic, must have at least one argument", n->get_line(), n->get_pos());
+    tactic_ref res;
+    for (unsigned i = 1; i < num_children; i++) {
+        sexpr * curr = n->get_child(i);
+        bool last = (i == num_children - 1);
+        tactic * t;
+        if (curr->is_string()) 
+            t = mk_echo_tactic(ctx, curr->get_string().c_str(), last);
+        else
+            t = mk_probe_value_tactic(ctx, 0, sexpr2probe(ctx, curr), last);
+        tactic * new_res;
+        if (res.get() == 0)
+            new_res = t;
+        else
+            new_res = and_then(res.get(), t);
+        if (last)
+            return new_res;
+        res = new_res;
+    }
+    UNREACHABLE();
+    return 0;
+}
+
+static tactic * mk_fail_if_branching(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 3 && num_children != 2)
+        throw cmd_exception("invalid fail-if-branching combinator, one or two arguments expected", n->get_line(), n->get_pos());
+    unsigned threshold = 1;
+    if (num_children == 3) {
+        if (!n->get_child(2)->is_numeral() || !n->get_child(2)->get_numeral().is_unsigned())
+            throw cmd_exception("invalid fail-if-branching combinator, second argument must be an unsigned integer", n->get_line(), n->get_pos());
+        threshold = n->get_child(2)->get_numeral().get_unsigned();
+    }
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    return fail_if_branching(t, threshold);
+}
+
+static tactic * mk_if_no_proofs(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 2)
+        throw cmd_exception("invalid if-no-proofs combinator, one argument expected", n->get_line(), n->get_pos());
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    return if_no_proofs(t);
+}
+
+static tactic * mk_if_no_models(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 2)
+        throw cmd_exception("invalid if-no-models combinator, one argument expected", n->get_line(), n->get_pos());
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    return if_no_models(t);
+}
+
+static tactic * mk_if_no_unsat_cores(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 2)
+        throw cmd_exception("invalid if-no-unsat-cores combinator, one argument expected", n->get_line(), n->get_pos());
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    return if_no_unsat_cores(t);
+}
+
+static tactic * mk_skip_if_failed(cmd_context & ctx, sexpr * n) {
+    SASSERT(n->is_composite());
+    unsigned num_children = n->get_num_children();
+    if (num_children != 2)
+        throw cmd_exception("invalid skip-if-failed combinator, one argument expected", n->get_line(), n->get_pos());
+    tactic * t = sexpr2tactic(ctx, n->get_child(1));
+    return skip_if_failed(t);
+}
+
+tactic * sexpr2tactic(cmd_context & ctx, sexpr * n) {
+    if (n->is_symbol()) {
+        tactic_cmd * cmd = ctx.find_tactic_cmd(n->get_symbol());
+        if (cmd != 0)
+            return cmd->mk(ctx.m());
+        sexpr * decl = ctx.find_user_tactic(n->get_symbol());
+        if (decl != 0)
+            return sexpr2tactic(ctx, decl);
+        throw cmd_exception("invalid tactic, unknown tactic ", n->get_symbol(), n->get_line(), n->get_pos());
+    }
+    else if (n->is_composite()) {
+        unsigned num_children = n->get_num_children();
+        if (num_children == 0)
+            throw cmd_exception("invalid tactic, arguments expected", n->get_line(), n->get_pos());
+        sexpr * head = n->get_child(0);
+        if (!head->is_symbol())
+            throw cmd_exception("invalid tactic, symbol expected", n->get_line(), n->get_pos());
+        symbol const & cmd_name = head->get_symbol();
+        if (cmd_name == "and-then" || cmd_name == "then")
+            return mk_and_then(ctx, n);
+        else if (cmd_name == "or-else")
+            return mk_or_else(ctx, n);
+        else if (cmd_name == "par")
+            return mk_par(ctx, n);
+        else if (cmd_name == "par-or")
+            return mk_par(ctx, n);
+        else if (cmd_name == "par-then")
+            return mk_par_then(ctx, n);
+        else if (cmd_name == "try-for")
+            return mk_try_for(ctx, n);
+        else if (cmd_name == "repeat")
+            return mk_repeat(ctx, n);
+        else if (cmd_name == "if" || cmd_name == "ite" || cmd_name == "cond")
+            return mk_if(ctx, n);
+        else if (cmd_name == "fail-if")
+            return mk_fail_if(ctx, n);
+        else if (cmd_name == "fail-if-branching")
+            return mk_fail_if_branching(ctx, n);
+        else if (cmd_name == "when")
+            return mk_when(ctx, n);
+        else if (cmd_name == "!" || cmd_name == "using-params" || cmd_name == "with")
+            return mk_using_params(ctx, n);
+        else if (cmd_name == "echo")
+            return mk_echo(ctx, n);
+        else if (cmd_name == "if-no-proofs")
+            return mk_if_no_proofs(ctx, n);
+        else if (cmd_name == "if-no-models")
+            return mk_if_no_models(ctx, n);
+        else if (cmd_name == "if-no-unsat-cores")
+            return mk_if_no_unsat_cores(ctx, n);
+        else if (cmd_name == "skip-if-failed")
+            return mk_skip_if_failed(ctx, n);
+        else
+            throw cmd_exception("invalid tactic, unknown tactic combinator ", cmd_name, n->get_line(), n->get_pos());
+    }
+    else {
+        throw cmd_exception("invalid tactic, unexpected input", n->get_line(), n->get_pos());
+    }
+}
+
+static probe * mk_not_probe (cmd_context & ctx, sexpr * n) {                                                         
+    SASSERT(n->is_composite());                                                                               
+    unsigned num_children = n->get_num_children();                                                            
+    if (num_children != 2)                                                                                    
+        throw cmd_exception("invalid probe expression, one argument expected", n->get_line(), n->get_pos()); 
+    return mk_not(sexpr2probe(ctx, n->get_child(1)));
+}
+
+#define MK_BIN_PROBE(NAME)                                                                                      \
+static probe * NAME ## _probe (cmd_context & ctx, sexpr * n) {                                                  \
+    SASSERT(n->is_composite());                                                                                 \
+    unsigned num_children = n->get_num_children();                                                              \
+    if (num_children != 3)                                                                                      \
+        throw cmd_exception("invalid probe expression, two arguments expected", n->get_line(), n->get_pos());   \
+    ref<probe> p1 = sexpr2probe(ctx, n->get_child(1));                                                          \
+    ref<probe> p2 = sexpr2probe(ctx, n->get_child(2));                                                          \
+    return NAME(p1.get(), p2.get());                                                                            \
+}
+
+MK_BIN_PROBE(mk_eq);
+MK_BIN_PROBE(mk_le);
+MK_BIN_PROBE(mk_lt);
+MK_BIN_PROBE(mk_ge);
+MK_BIN_PROBE(mk_gt);
+MK_BIN_PROBE(mk_implies);
+MK_BIN_PROBE(mk_div);
+MK_BIN_PROBE(mk_sub);
+
+#define MK_NARY_PROBE(NAME)                                                                                     \
+static probe * NAME ## _probe(cmd_context & ctx, sexpr * n) {                                                   \
+    SASSERT(n->is_composite());                                                                                 \
+    unsigned num_children = n->get_num_children();                                                              \
+    if (num_children < 2)                                                                                       \
+        throw cmd_exception("invalid probe, at least one argument expected", n->get_line(), n->get_pos());      \
+    probe * r = sexpr2probe(ctx, n->get_child(1));                                                              \
+    if (num_children == 2)                                                                                      \
+        return r;                                                                                               \
+    ref<probe> prev = r;                                                                                        \
+    unsigned i = 1;                                                                                             \
+    while (true) {                                                                                              \
+        r = NAME(prev.get(), sexpr2probe(ctx, n->get_child(i)));                                                \
+        if (i == num_children - 1)                                                                              \
+            return r;                                                                                           \
+        i++;                                                                                                    \
+        prev = r;                                                                                               \
+    }                                                                                                           \
+}
+
+MK_NARY_PROBE(mk_and);
+MK_NARY_PROBE(mk_or);
+MK_NARY_PROBE(mk_add);
+MK_NARY_PROBE(mk_mul);
+
+probe * sexpr2probe(cmd_context & ctx, sexpr * n) {
+    if (n->is_symbol()) {
+        probe_info * pinfo = ctx.find_probe(n->get_symbol());
+        if (pinfo != 0)
+            return pinfo->get();
+        throw cmd_exception("invalid probe, unknown builtin probe ", n->get_symbol(), n->get_line(), n->get_pos());
+    }
+    else if (n->is_numeral()) {
+        rational const & v = n->get_numeral();
+        if (!v.is_int32())
+            throw cmd_exception("invalid probe, constant is too big to fit in a fixed size integer", n->get_line(), n->get_pos());
+        return mk_const_probe(static_cast<int>(v.get_int64()));
+    }
+    else if (n->is_composite()) {
+        unsigned num_children = n->get_num_children();
+        if (num_children == 0)
+            throw cmd_exception("invalid probe, arguments expected", n->get_line(), n->get_pos());
+        sexpr * head = n->get_child(0);
+        if (!head->is_symbol())
+            throw cmd_exception("invalid probe, symbol expected", n->get_line(), n->get_pos());
+        symbol const & p_name = head->get_symbol();
+        
+        if (p_name == "=")
+            return mk_eq_probe(ctx, n);
+        else if (p_name == "<=")
+            return mk_le_probe(ctx, n);
+        else if (p_name == ">=")
+            return mk_ge_probe(ctx, n);
+        else if (p_name == "<")
+            return mk_lt_probe(ctx, n);
+        else if (p_name == ">")
+            return mk_gt_probe(ctx, n);
+        else if (p_name == "and")
+            return mk_and_probe(ctx, n);
+        else if (p_name == "or")
+            return mk_or_probe(ctx, n);
+        else if (p_name == "=>" || p_name == "implies")
+            return mk_implies_probe(ctx, n);
+        else if (p_name == "not") 
+            return mk_not_probe(ctx, n);
+        else if (p_name == "*")
+            return mk_mul_probe(ctx, n);
+        else if (p_name == "+") 
+            return mk_add_probe(ctx, n);
+        else if (p_name == "-") 
+            return mk_sub_probe(ctx, n);
+        else if (p_name == "/")
+            return mk_div_probe(ctx, n);
+        else
+            throw cmd_exception("invalid probe, unknown probe expression ", p_name, n->get_line(), n->get_pos());
+    }
+    else {
+        throw cmd_exception("invalid probe, unexpected input", n->get_line(), n->get_pos());
+    }
+}
+

src/cmd_context/tactic_cmds.h

@@ -0,0 +1,67 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactic_cmds.h
+
+Abstract:
+    Support for tactics in SMT 2.0 frontend.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-20
+
+Notes:
+
+--*/
+#ifndef _TACTIC_CMDS_H_
+#define _TACTIC_CMDS_H_
+
+#include"ast.h"
+#include"cmd_context_types.h"
+#include"ref.h"
+
+class tactic;
+class probe;
+class tactic_factory;
+
+class tactic_cmd {
+    symbol           m_name;
+    char const *     m_descr;
+    tactic_factory * m_factory;
+public:
+    tactic_cmd(symbol const & n, char const * d, tactic_factory * f):
+        m_name(n), m_descr(d), m_factory(f) {
+        SASSERT(m_factory);
+    }
+
+    ~tactic_cmd();
+
+    symbol get_name() const { return m_name; }
+    
+    char const * get_descr() const { return m_descr; }
+    
+    tactic * mk(ast_manager & m);
+};
+
+void install_core_tactic_cmds(cmd_context & ctx);
+tactic * sexpr2tactic(cmd_context & ctx, sexpr * n);
+
+class probe_info {
+    symbol           m_name;
+    char const *     m_descr;
+    ref<probe>       m_probe;
+public:
+    probe_info(symbol const & n, char const * d, probe * p);
+    ~probe_info();
+
+    symbol get_name() const { return m_name; }
+    char const * get_descr() const { return m_descr; }
+    
+    probe * get() const { return m_probe.get(); }
+};
+
+probe * sexpr2probe(cmd_context & ctx, sexpr * n);
+
+#endif

src/cmd_context/tactic_manager.cpp

@@ -0,0 +1,62 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic_manager.cpp
+
+Abstract:
+
+    Collection of tactics & probes
+
+Author:
+
+    Leonardo (leonardo) 2012-03-06
+
+Notes:
+
+--*/
+#include"tactic_manager.h"
+
+tactic_manager::~tactic_manager() {
+    finalize_tactic_cmds();
+    finalize_probes();
+}
+
+void tactic_manager::insert(tactic_cmd * c) {
+    symbol const & s = c->get_name();
+    SASSERT(!m_name2tactic.contains(s));
+    m_name2tactic.insert(s, c);
+    m_tactics.push_back(c);
+}
+
+void tactic_manager::insert(probe_info * p) {
+    symbol const & s = p->get_name();
+    SASSERT(!m_name2probe.contains(s));
+    m_name2probe.insert(s, p);
+    m_probes.push_back(p);
+}
+
+tactic_cmd * tactic_manager::find_tactic_cmd(symbol const & s) const {
+    tactic_cmd * c = 0;
+    m_name2tactic.find(s, c);
+    return c;
+}
+
+probe_info * tactic_manager::find_probe(symbol const & s) const {
+    probe_info * p = 0;
+    m_name2probe.find(s, p);
+    return p;
+}
+
+void tactic_manager::finalize_tactic_cmds() {
+    std::for_each(m_tactics.begin(), m_tactics.end(), delete_proc<tactic_cmd>());
+    m_tactics.reset();
+    m_name2tactic.reset();
+}
+
+void tactic_manager::finalize_probes() {
+    std::for_each(m_probes.begin(), m_probes.end(), delete_proc<probe_info>());
+    m_probes.reset();
+    m_name2probe.reset();
+}

src/cmd_context/tactic_manager.h

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic_manager.h
+
+Abstract:
+    Collection of tactics & probes
+
+Author:
+
+    Leonardo (leonardo) 2012-03-06
+
+Notes:
+
+--*/
+#ifndef _TACTIC_MANAGER_H_
+#define _TACTIC_MANAGER_H_
+
+#include"tactic_cmds.h"
+#include"dictionary.h"
+
+class tactic_manager {
+protected:
+    dictionary<tactic_cmd*>  m_name2tactic;
+    dictionary<probe_info*>  m_name2probe;
+    ptr_vector<tactic_cmd>   m_tactics;
+    ptr_vector<probe_info>   m_probes;
+    void finalize_tactic_cmds();
+    void finalize_probes();
+public:
+    ~tactic_manager();
+
+    void insert(tactic_cmd * c);
+    void insert(probe_info * p);
+    tactic_cmd * find_tactic_cmd(symbol const & s) const; 
+    probe_info * find_probe(symbol const & s) const; 
+
+    unsigned num_tactics() const { return m_tactics.size(); }
+    unsigned num_probes() const { return m_probes.size(); }
+    tactic_cmd * get_tactic(unsigned i) const { return m_tactics[i]; }
+    probe_info * get_probe(unsigned i) const { return m_probes[i]; }
+    
+    typedef ptr_vector<tactic_cmd>::const_iterator tactic_cmd_iterator;
+    tactic_cmd_iterator begin_tactic_cmds() const { return m_tactics.begin(); }
+    tactic_cmd_iterator end_tactic_cmds() const { return m_tactics.end(); }
+
+    typedef ptr_vector<probe_info>::const_iterator probe_iterator;
+    probe_iterator begin_probes() const { return m_probes.begin(); }
+    probe_iterator end_probes() const { return m_probes.end(); }
+};
+
+#endif
+
+
+