Reorganizing the code

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

src/framework/README

@@ -0,0 +1 @@
+tactic and command context frameworks.

src/framework/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/framework/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/framework/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/framework/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/framework/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/framework/cmd_context.h

@@ -0,0 +1,406 @@
+/*++
+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"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:
+    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; }
+    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); 
+    std::ostream & regular_stream() { return *m_regular; }
+    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;
+    void pp(func_decl * f, format_ns::format_ref & r) const;
+    void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const;
+    void pp(expr * n, format_ns::format_ref & r) const;
+    void display(std::ostream & out, sort * s, unsigned indent = 0) const;
+    void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const;
+    void display(std::ostream & out, expr * n, unsigned indent = 0) const;
+    void display(std::ostream & out, func_decl * f, unsigned indent = 0) const;
+
+    // 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/framework/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/framework/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/framework/converter.h

@@ -0,0 +1,142 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    converter.h
+
+Abstract:
+
+    Abstract class and templates for proof and model converters.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-14
+
+Notes:
+
+--*/
+#ifndef _CONVERTER_H_
+#define _CONVERTER_H_
+
+#include"vector.h"
+#include"ref.h"
+#include"ast_translation.h"
+
+class converter {
+    unsigned m_ref_count;
+public:
+    converter():m_ref_count(0) {}
+    virtual ~converter() {}
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { 
+        --m_ref_count;
+        if (m_ref_count == 0)
+            dealloc(this);
+    }
+
+    virtual void cancel() {}
+    
+    // for debugging purposes
+    virtual void display(std::ostream & out) {}
+};
+
+template<typename T>
+class concat_converter : public T {
+protected:
+    ref<T> m_c1;
+    ref<T> m_c2;
+
+    template<typename T2>
+    T * translate_core(ast_translation & translator) {
+        T * t1 = m_c1->translate(translator);
+        T * t2 = m_c2->translate(translator);
+        return alloc(T2, t1, t2);
+    }
+
+public:
+    concat_converter(T * c1, T * c2):m_c1(c1), m_c2(c2) {}
+    
+    virtual ~concat_converter() {}
+
+    virtual void cancel() {
+        m_c2->cancel();
+        m_c1->cancel();
+    }
+
+    virtual char const * get_name() const = 0;
+    
+    virtual void display(std::ostream & out) {
+        out << "(" << get_name() << "\n";
+        m_c1->display(out);
+        m_c2->display(out);
+        out << ")\n";
+    }
+};
+
+template<typename T>
+class concat_star_converter : public T {
+protected:
+    ref<T>          m_c1;
+    ptr_vector<T>   m_c2s;
+    unsigned_vector m_szs;
+
+    template<typename T2>
+    T * translate_core(ast_translation & translator) {
+        T * t1 = m_c1 ? m_c1->translate(translator) : 0;
+        ptr_buffer<T> t2s;
+        unsigned num = m_c2s.size();
+        for (unsigned i = 0; i < num; i++)
+            t2s.push_back(m_c2s[i] ? m_c2s[i]->translate(translator) : 0);
+        return alloc(T2, t1, num, t2s.c_ptr(), m_szs.c_ptr());
+    }
+
+public:
+    concat_star_converter(T * c1, unsigned num, T * const * c2s, unsigned * szs):
+        m_c1(c1) {
+        for (unsigned i = 0; i < num; i++) {
+            T * c2 = c2s[i];
+            if (c2)
+                c2->inc_ref();
+            m_c2s.push_back(c2);
+            m_szs.push_back(szs[i]);
+        }
+    }
+
+    virtual ~concat_star_converter() {
+        unsigned sz = m_c2s.size();
+        for (unsigned i = 0; i < sz; i++) {
+            T * c2 = m_c2s[i];
+            if (c2)
+                c2->dec_ref();
+        }
+    }
+
+    virtual void cancel() {
+        if (m_c1)
+            m_c1->cancel();
+        unsigned num = m_c2s.size();
+        for (unsigned i = 0; i < num; i++) {
+            if (m_c2s[i])
+                m_c2s[i]->cancel();
+        }
+    }
+
+    virtual char const * get_name() const = 0;
+    
+    virtual void display(std::ostream & out) {
+        out << "(" << get_name() << "\n";
+        if (m_c1)
+            m_c1->display(out);
+        out << "(\n";
+        unsigned num = m_c2s.size();
+        for (unsigned i = 0; i < num; i++)
+            if (m_c2s[i])
+                m_c2s[i]->display(out);
+        out << "))\n";
+    }
+};
+
+#endif
+

src/framework/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/framework/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/framework/goal.cpp

@@ -0,0 +1,630 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal.cpp
+
+Abstract:
+
+    Proof / Model finding Goals
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-12
+
+Revision History:
+
+--*/
+#include"goal.h"
+#include"cmd_context.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+#include"for_each_expr.h"
+#include"well_sorted.h"
+
+std::ostream & operator<<(std::ostream & out, goal::precision p) {
+    switch (p) {
+    case goal::PRECISE: out << "precise"; break;
+    case goal::UNDER:   out << "under"; break;
+    case goal::OVER:    out << "over"; break;
+    case goal::UNDER_OVER: out << "under-over"; break;
+    }
+    return out;
+}
+
+void goal::copy_to(goal & target) const {
+    SASSERT(&m_manager == &(target.m_manager));
+    if (this == &target)
+        return;
+
+    m().copy(m_forms, target.m_forms);
+    m().copy(m_proofs, target.m_proofs);
+    m().copy(m_dependencies, target.m_dependencies);
+
+    target.m_depth                = std::max(m_depth, target.m_depth);
+    SASSERT(target.m_proofs_enabled == m_proofs_enabled);
+    SASSERT(target.m_core_enabled   == m_core_enabled);
+    target.m_inconsistent         = m_inconsistent;
+    target.m_precision            = mk_union(prec(), target.prec());
+}
+
+void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
+    if (m().is_true(f))
+        return;
+    if (m().is_false(f)) {
+        m().del(m_forms);
+        m().del(m_proofs);
+        m().del(m_dependencies);
+        m_inconsistent = true;
+    }
+    else {
+        SASSERT(!m_inconsistent);
+    }
+    m().push_back(m_forms, f);
+    if (proofs_enabled())
+        m().push_back(m_proofs, pr);
+    if (unsat_core_enabled())
+        m().push_back(m_dependencies, d);
+}
+
+void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
+    if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
+        if (!save_first) {
+            push_back(f, 0, d);
+        }
+        return; 
+    }
+    typedef std::pair<expr *, bool> expr_pol;
+    sbuffer<expr_pol, 64> todo;
+    todo.push_back(expr_pol(f, true));
+    while (!todo.empty()) {
+        if (m_inconsistent)
+            return;
+        expr_pol p  = todo.back();
+        expr * curr = p.first;
+        bool   pol  = p.second;
+        todo.pop_back();
+        if (pol && m().is_and(curr)) {
+            app * t = to_app(curr);
+            unsigned i = t->get_num_args();
+            while (i > 0) {
+                --i;
+                todo.push_back(expr_pol(t->get_arg(i), true));
+            }
+        }
+        else if (!pol && m().is_or(curr)) {
+            app * t = to_app(curr);
+            unsigned i = t->get_num_args();
+            while (i > 0) {
+                --i;
+                todo.push_back(expr_pol(t->get_arg(i), false));
+            }
+        }
+        else if (m().is_not(curr)) {
+            todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
+        }
+        else {
+            if (!pol) 
+                curr = m().mk_not(curr);
+            if (save_first) {
+                f  = curr;
+                save_first = false;
+            }
+            else {
+                push_back(curr, 0, d);
+            }
+        }
+    }
+}
+
+void goal::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    unsigned num = f->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        if (m_inconsistent)
+            return;
+        slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr);
+    }
+}
+
+void goal::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    unsigned num = f->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        if (m_inconsistent)
+            return;
+        expr * child = f->get_arg(i);
+        if (m().is_not(child)) {
+            expr * not_child = to_app(child)->get_arg(0);
+            slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
+        }
+        else {
+            expr_ref not_child(m());
+            not_child = m().mk_not(child);
+            slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
+        }
+    }
+}
+
+void goal::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    if (m().is_and(f)) 
+        process_and(save_first, to_app(f), pr, d, out_f, out_pr);
+    else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) 
+        process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr);
+    else if (save_first) {
+        out_f  = f;
+        out_pr = pr;
+    }
+    else {
+        push_back(f, pr, d);
+    }
+}
+
+void goal::slow_process(expr * f, proof * pr, expr_dependency * d) {
+    expr_ref out_f(m());
+    proof_ref out_pr(m());
+    slow_process(false, f, pr, d, out_f, out_pr);
+}
+
+void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    if (proofs_enabled())
+        slow_process(f, pr, d);
+    else
+        quick_process(false, f, d);
+}
+
+void goal::get_formulas(ptr_vector<expr> & result) {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        result.push_back(form(i));
+    }
+}
+
+void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    if (proofs_enabled()) {
+        expr_ref out_f(m());
+        proof_ref out_pr(m());
+        slow_process(true, f, pr, d, out_f, out_pr);
+        if (!m_inconsistent) {
+            if (m().is_false(out_f)) {
+                push_back(out_f, out_pr, d);
+            }
+            else {
+                m().set(m_forms, i, out_f);
+                m().set(m_proofs, i, out_pr);
+                if (unsat_core_enabled()) 
+                    m().set(m_dependencies, i, d);
+            }
+        }
+    }
+    else {
+        quick_process(true, f, d);
+        if (!m_inconsistent) {
+            if (m().is_false(f)) {
+                push_back(f, 0, d);
+            }
+            else {
+                m().set(m_forms, i, f);
+                if (unsat_core_enabled()) 
+                    m().set(m_dependencies, i, d);
+            }
+        }
+    }
+}
+
+void goal::reset_core() {
+    m().del(m_forms);
+    m().del(m_proofs);
+    m().del(m_dependencies);
+}
+
+void goal::reset_all() {
+    reset_core();
+    m_depth = 0;
+    m_inconsistent = false;
+    m_precision = PRECISE;
+}
+
+void goal::reset() { 
+    reset_core(); 
+    m_inconsistent = false; 
+}
+
+void goal::display(cmd_context & ctx, std::ostream & out) const {
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  ";
+        ctx.display(out, form(i), 2);
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
+void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) const {
+    ptr_vector<expr> deps;
+    obj_hashtable<expr> to_pp;
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  |-";
+        deps.reset();
+        m().linearize(dep(i), deps);
+        ptr_vector<expr>::iterator it  = deps.begin();
+        ptr_vector<expr>::iterator end = deps.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            if (is_uninterp_const(d)) {
+                out << " " << mk_ismt2_pp(d, m());
+            }
+            else {
+                out << " #" << d->get_id();
+                to_pp.insert(d);
+            }
+        }
+        out << "\n  ";
+        ctx.display(out, form(i), 2);
+    }
+    if (!to_pp.empty()) {
+        out << "\n  :dependencies-definitions (";
+        obj_hashtable<expr>::iterator it  = to_pp.begin();
+        obj_hashtable<expr>::iterator end = to_pp.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            out << "\n  (#" << d->get_id() << "\n  ";
+            ctx.display(out, d, 2);
+            out << ")";
+        }
+        out << ")";
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
+void goal::display_with_dependencies(std::ostream & out) const {
+    ptr_vector<expr> deps;
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  |-";
+        deps.reset();
+        m().linearize(dep(i), deps);
+        ptr_vector<expr>::iterator it  = deps.begin();
+        ptr_vector<expr>::iterator end = deps.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            if (is_uninterp_const(d)) {
+                out << " " << mk_ismt2_pp(d, m());
+            }
+            else {
+                out << " #" << d->get_id();
+            }
+        }
+        out << "\n  " << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
+void goal::display(cmd_context & ctx) const {
+    display(ctx, ctx.regular_stream());
+}
+
+void goal::display_with_dependencies(cmd_context & ctx) const {
+    display_with_dependencies(ctx, ctx.regular_stream());
+}
+
+void goal::display(std::ostream & out) const {
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  ";
+        out << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << ")" << std::endl;
+}
+
+void goal::display_as_and(std::ostream & out) const {
+    ptr_buffer<expr> args;
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++)
+        args.push_back(form(i));
+    expr_ref tmp(m());
+    tmp = m().mk_and(args.size(), args.c_ptr());
+    out << mk_ismt2_pp(tmp, m()) << "\n";
+}
+
+void goal::display_ll(std::ostream & out) const {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << mk_ll_pp(form(i), m()) << "\n";
+    }
+}
+
+/**
+   \brief Assumes that the formula is already in CNF.
+*/
+void goal::display_dimacs(std::ostream & out) const {
+    obj_map<expr, unsigned> expr2var;
+    unsigned num_vars = 0;
+    unsigned num_cls  = size();
+    for (unsigned i = 0; i < num_cls; i++) {
+        expr * f = form(i);
+        unsigned num_lits;
+        expr * const * lits;
+        if (m().is_or(f)) {
+            num_lits = to_app(f)->get_num_args();
+            lits     = to_app(f)->get_args();
+        }
+        else {
+            num_lits = 1;
+            lits     = &f;
+        }
+        for (unsigned j = 0; j < num_lits; j++) {
+            expr * l = lits[j];
+            if (m().is_not(l))
+                l = to_app(l)->get_arg(0);
+            if (expr2var.contains(l))
+                continue;
+            num_vars++;
+            expr2var.insert(l, num_vars);
+        }
+    }
+    out << "p cnf " << num_vars << " " << num_cls << "\n";
+    for (unsigned i = 0; i < num_cls; i++) {
+        expr * f = form(i);
+        unsigned num_lits;
+        expr * const * lits;
+        if (m().is_or(f)) {
+            num_lits = to_app(f)->get_num_args();
+            lits     = to_app(f)->get_args();
+        }
+        else {
+            num_lits = 1;
+            lits     = &f;
+        }
+        for (unsigned j = 0; j < num_lits; j++) {
+            expr * l = lits[j];
+            if (m().is_not(l)) {
+                out << "-";
+                l = to_app(l)->get_arg(0);
+            }
+            unsigned id = UINT_MAX;
+            expr2var.find(l, id);
+            SASSERT(id != UINT_MAX);
+            out << id << " ";
+        }
+        out << "0\n";
+    }
+}
+
+unsigned goal::num_exprs() const {
+    expr_fast_mark1 visited;
+    unsigned sz = size();
+    unsigned r  = 0;
+    for (unsigned i = 0; i < sz; i++) {
+        r += get_num_exprs(form(i), visited);
+    }
+    return r;
+}
+
+void goal::shrink(unsigned j) {
+    SASSERT(j <= size());
+    unsigned sz = size();
+    for (unsigned i = j; i < sz; i++)
+        m().pop_back(m_forms);
+    if (proofs_enabled()) {
+        for (unsigned i = j; i < sz; i++)
+            m().pop_back(m_proofs);
+    }
+    if (unsat_core_enabled()) {
+        for (unsigned i = j; i < sz; i++)
+            m().pop_back(m_dependencies);
+    }
+}
+
+/**
+   \brief Eliminate true formulas.
+*/
+void goal::elim_true() {
+    unsigned sz = size();
+    unsigned j = 0;
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f = form(i);
+        if (m().is_true(f))
+            continue;
+        if (i == j) {
+            j++;
+            continue;
+        }
+        m().set(m_forms, j, f);
+        if (proofs_enabled())
+            m().set(m_proofs, j, m().get(m_proofs, i));
+        if (unsat_core_enabled())
+            m().set(m_dependencies, j, m().get(m_dependencies, i));
+        j++;
+    }
+    shrink(j);
+}
+
+/**
+   \brief Return the position of formula f in the goal.
+   Return UINT_MAX if f is not in the goal
+*/
+unsigned goal::get_idx(expr * f) const {
+    unsigned sz = size();
+    for (unsigned j = 0; j < sz; j++) {
+        if (form(j) == f)
+            return j;
+    }
+    return UINT_MAX;
+}
+
+/**
+   \brief Return the position of formula (not f) in the goal.
+   Return UINT_MAX if (not f) is not in the goal
+*/
+unsigned goal::get_not_idx(expr * f) const {
+    expr * atom;
+    unsigned sz = size();
+    for (unsigned j = 0; j < sz; j++) {
+        if (m().is_not(form(j), atom) && atom == f)
+            return j;
+    }
+    return UINT_MAX;
+}
+
+void goal::elim_redundancies() {
+    if (inconsistent())
+        return;
+    expr_ref_fast_mark1 neg_lits(m());
+    expr_ref_fast_mark2 pos_lits(m());
+    unsigned sz = size();
+    unsigned j  = 0;
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f = form(i);
+        if (m().is_true(f))
+            continue;
+        if (m().is_not(f)) {
+            expr * atom = to_app(f)->get_arg(0);
+            if (neg_lits.is_marked(atom))
+                continue;
+            if (pos_lits.is_marked(atom)) {
+                proof * p = 0;
+                if (proofs_enabled()) {
+                    proof * prs[2] = { pr(get_idx(atom)), pr(i) };
+                    p = m().mk_unit_resolution(2, prs);
+                }
+                expr_dependency_ref d(m());
+                if (unsat_core_enabled())
+                    d = m().mk_join(dep(get_idx(atom)), dep(i));
+                push_back(m().mk_false(), p, d);                    
+                return;
+            }
+            neg_lits.mark(atom);
+        }
+        else {
+            if (pos_lits.is_marked(f))
+                continue;
+            if (neg_lits.is_marked(f)) {
+                proof * p = 0;
+                if (proofs_enabled()) {
+                    proof * prs[2] = { pr(get_not_idx(f)), pr(i) };
+                    p = m().mk_unit_resolution(2, prs);
+                }
+                expr_dependency_ref d(m());
+                if (unsat_core_enabled())
+                    d = m().mk_join(dep(get_not_idx(f)), dep(i));
+                push_back(m().mk_false(), p, d);
+                return;
+            }
+            pos_lits.mark(f);
+        }
+        if (i == j) {
+            j++;
+            continue;
+        }
+        m().set(m_forms, j, f);
+        if (proofs_enabled())
+            m().set(m_proofs, j, pr(i));
+        if (unsat_core_enabled())
+            m().set(m_dependencies, j, dep(i));
+        j++;
+    }
+    shrink(j);
+}
+
+bool goal::is_well_sorted() const {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * t = form(i);
+        if (!::is_well_sorted(m(), t))
+            return false;
+    }
+    return true;
+}
+
+/**
+   \brief Assert expressions from ctx into t.
+*/
+void assert_exprs_from(cmd_context const & ctx, goal & t) {
+    if (ctx.produce_proofs() && ctx.produce_unsat_cores()) 
+        throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores");
+    ast_manager & m = t.m();
+    bool proofs_enabled = t.proofs_enabled();
+    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+    for (; it != end; ++it) {
+        t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0);
+    }
+    if (ctx.produce_unsat_cores()) {
+        SASSERT(!ctx.produce_proofs());
+        it  = ctx.begin_assumptions();
+        end = ctx.end_assumptions();
+        for (; it != end; ++it) {
+            t.assert_expr(*it, 0, m.mk_leaf(*it));
+        }
+    }
+    else {
+        SASSERT(ctx.begin_assumptions() == ctx.end_assumptions());
+    }
+}
+
+/**
+   \brief Translate the assertion set to a new one that uses a different ast_manager.
+*/
+goal * goal::translate(ast_translation & translator) const {
+    expr_dependency_translation dep_translator(translator);
+
+    ast_manager & m_to = translator.to();
+    goal * res = alloc(goal, m_to, m_to.proofs_enabled() && proofs_enabled(), models_enabled(), unsat_core_enabled());
+    
+    unsigned sz = m().size(m_forms);
+    for (unsigned i = 0; i < sz; i++) {
+        res->m().push_back(res->m_forms, translator(m().get(m_forms, i)));        
+        if (res->proofs_enabled())
+            res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i)));
+        if (res->unsat_core_enabled())
+            res->m().push_back(res->m_dependencies, dep_translator(m().get(m_dependencies, i)));
+    }
+
+    res->m_inconsistent = m_inconsistent;
+    res->m_depth        = m_depth;
+    res->m_precision    = m_precision;
+
+    return res;
+}
+
+bool is_equal(goal const & s1, goal const & s2) {
+    if (s1.size() != s2.size())
+        return false;
+    unsigned num1 = 0; // num unique ASTs in s1
+    unsigned num2 = 0; // num unique ASTs in s2
+    expr_fast_mark1 visited1;
+    expr_fast_mark2 visited2;
+    unsigned sz = s1.size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f1 = s1.form(i);
+        if (visited1.is_marked(f1))
+            continue;
+        num1++;
+        visited1.mark(f1);
+    }
+    SASSERT(num1 <= sz);
+    SASSERT(0 <= num1);
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f2 = s2.form(i);
+        if (visited2.is_marked(f2))
+            continue;
+        num2++;
+        visited2.mark(f2);
+        if (!visited1.is_marked(f2))
+            return false;
+    }
+    SASSERT(num2 <= sz);
+    SASSERT(0 <= num2);
+    SASSERT(num1 >= num2);
+    return num1 == num2;
+}

src/framework/goal.h

@@ -0,0 +1,255 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal.h
+
+Abstract:
+
+    A goal is essentially a set of formulas. Tactics are used to build 
+    proof and model finding procedures for these sets.
+    
+    Remark: In a previous version of Z3, goals were called assertion_sets.
+    Here is a summary of the main changes:
+       - Goals track whether they are the result of applying over/under approximation steps.
+         This prevent users from creating unsound strategies (e.g., user uses nia2sat, but does not check the sat_preserving flag).
+       - Goals track dependencies (aka light proofs) for unsat core extraction, and building multi-tier solvers.
+         This kind of dependency tracking is more powerful than the one used in the current Z3, since
+         it does not prevent the use of preprocessing steps such as "Gaussian Elimination".
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-12
+
+Revision History:
+
+--*/
+#ifndef _GOAL_H_
+#define _GOAL_H_
+
+#include"ast.h"
+#include"ast_translation.h"
+#include"for_each_expr.h"
+#include"ref.h"
+#include"ref_vector.h"
+#include"ref_buffer.h"
+
+class cmd_context;
+
+class goal {
+public:
+    enum precision {
+        PRECISE,      
+        UNDER,   // goal is the product of an under-approximation 
+        OVER,    // goal is the product of an over-approximation
+        UNDER_OVER // goal is garbage: the produce of combined under and over approximation steps.
+    };
+
+    static precision mk_union(precision p1, precision p2) { 
+        if (p1 == PRECISE) return p2;
+        if (p2 == PRECISE) return p1;
+        if (p1 != p2) return UNDER_OVER;
+        return p1;
+    }
+    
+protected:
+    ast_manager &         m_manager;
+    unsigned              m_ref_count;
+    expr_array            m_forms;
+    expr_array            m_proofs;
+    expr_dependency_array m_dependencies;
+    // attributes
+    unsigned              m_depth:26;          // depth of the goal in the goal tree.
+    unsigned              m_models_enabled:1;  // model generation is enabled.
+    unsigned              m_proofs_enabled:1;  // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true
+    unsigned              m_core_enabled:1;    // unsat core extraction is enabled.
+    unsigned              m_inconsistent:1;    // true if the goal is known to be inconsistent. 
+    unsigned              m_precision:2;       // PRECISE, UNDER, OVER.
+
+    void push_back(expr * f, proof * pr, expr_dependency * d);
+    void quick_process(bool save_first, expr * & f, expr_dependency * d);
+    void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void slow_process(expr * f, proof * pr, expr_dependency * d);
+    unsigned get_idx(expr * f) const;
+    unsigned get_not_idx(expr * f) const;
+    void shrink(unsigned j);
+    void reset_core();
+    
+public:
+    goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false):
+        m_manager(m), 
+        m_ref_count(0),
+        m_depth(0), 
+        m_models_enabled(models_enabled),
+        m_proofs_enabled(m.proofs_enabled()), 
+        m_core_enabled(core_enabled), 
+        m_inconsistent(false), 
+        m_precision(PRECISE) {
+    }
+    
+    goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
+        m_manager(m), 
+        m_ref_count(0),
+        m_depth(0), 
+        m_models_enabled(models_enabled),
+        m_proofs_enabled(proofs_enabled), 
+        m_core_enabled(core_enabled), 
+        m_inconsistent(false), 
+        m_precision(PRECISE) {
+        SASSERT(!proofs_enabled || m.proofs_enabled());
+    }
+
+    goal(goal const & src):
+        m_manager(src.m()),
+        m_ref_count(0),
+        m_depth(0), 
+        m_models_enabled(src.models_enabled()),
+        m_proofs_enabled(src.proofs_enabled()), 
+        m_core_enabled(src.unsat_core_enabled()), 
+        m_inconsistent(false), 
+        m_precision(PRECISE) {
+        copy_from(src);
+    }
+
+    // Copy configuration: depth, models/proofs/cores flags, and precision from src.
+    // The assertions are not copied
+    goal(goal const & src, bool):
+        m_manager(src.m()),
+        m_ref_count(0),
+        m_depth(src.m_depth), 
+        m_models_enabled(src.models_enabled()),
+        m_proofs_enabled(src.proofs_enabled()), 
+        m_core_enabled(src.unsat_core_enabled()), 
+        m_inconsistent(false), 
+        m_precision(src.m_precision) {
+    }
+    
+    ~goal() { reset_core(); }
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
+
+    ast_manager & m() const { return m_manager; }
+
+    unsigned depth() const { return m_depth; }
+    bool models_enabled() const { return m_models_enabled; }
+    bool proofs_enabled() const { return m_proofs_enabled; }
+    bool unsat_core_enabled() const { return m_core_enabled; }
+    bool inconsistent() const { return m_inconsistent; }
+    precision prec() const { return static_cast<precision>(m_precision); }
+    
+    void set_depth(unsigned d) { m_depth = d; }
+    void inc_depth() { m_depth++; }
+    void set_prec(precision d) { m_precision = d; }
+    void updt_prec(precision d) { m_precision = mk_union(prec(), d); }
+
+    void reset_all(); // reset goal and precision and depth attributes.
+    void reset(); // reset goal but preserve precision and depth attributes.
+
+    void copy_to(goal & target) const;
+    void copy_from(goal const & src) { src.copy_to(*this); }
+    
+    void assert_expr(expr * f, proof * pr, expr_dependency * d);
+    void assert_expr(expr * f) {
+        assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
+    }
+    
+    unsigned size() const { return m().size(m_forms); }
+
+    unsigned num_exprs() const;
+  
+    expr * form(unsigned i) const { return m().get(m_forms, i); }
+    proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m().get(m_proofs, i)) : 0; }
+    expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : 0; }
+
+    void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
+
+    void get_formulas(ptr_vector<expr> & result);
+    
+    void elim_true();
+    void elim_redundancies();
+
+    void display(cmd_context & ctx, std::ostream & out) const;
+    void display(cmd_context & ctx) const;
+    void display(std::ostream & out) const;
+    void display_ll(std::ostream & out) const;
+    void display_as_and(std::ostream & out) const;
+    void display_dimacs(std::ostream & out) const;
+    void display_with_dependencies(cmd_context & ctx, std::ostream & out) const;
+    void display_with_dependencies(cmd_context & ctx) const;
+    void display_with_dependencies(std::ostream & out) const;
+
+    bool sat_preserved() const { 
+        return prec() == PRECISE || prec() == UNDER; 
+    }
+
+    bool unsat_preserved() const {
+        return prec() == PRECISE || prec() == OVER;
+    }
+
+    bool is_decided_sat() const { 
+        return size() == 0 && sat_preserved();
+    }
+
+    bool is_decided_unsat() const {
+        return inconsistent() && unsat_preserved();
+    }
+
+    bool is_decided() const { 
+        return is_decided_sat() || is_decided_unsat();
+    }
+
+    bool is_well_sorted() const;
+
+    goal * translate(ast_translation & translator) const;
+};
+
+std::ostream & operator<<(std::ostream & out, goal::precision p);
+
+typedef ref<goal> goal_ref;
+typedef sref_vector<goal> goal_ref_vector;
+typedef sref_buffer<goal> goal_ref_buffer;
+
+template<typename GoalCollection>
+inline bool is_decided(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided(); }
+template<typename GoalCollection>
+inline bool is_decided_sat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_sat(); }
+template<typename GoalCollection>
+inline bool is_decided_unsat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_unsat(); }
+
+void assert_exprs_from(cmd_context const & ctx, goal & t);
+
+template<typename ForEachProc>
+void for_each_expr_at(ForEachProc& proc, goal const & s) {
+    expr_mark visited;
+    for (unsigned i = 0; i < s.size(); ++i) {
+        for_each_expr(proc, visited, s.form(i));
+    }
+}
+
+bool is_equal(goal const & g1, goal const & g2);
+
+template<typename Predicate>
+bool test(goal const & g, Predicate & proc) {
+    expr_fast_mark1 visited;
+    try {
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++)
+            quick_for_each_expr(proc, visited, g.form(i));
+    }
+    catch (typename Predicate::found) {
+        return true;
+    }
+    return false;
+}
+
+template<typename Predicate>
+bool test(goal const & g) {
+    Predicate proc(g.m());
+    return test(g, proc);
+}
+
+#endif

src/framework/goal_util.cpp

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    goal_util.cpp
+
+Abstract:
+
+    goal goodies.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-01-03.
+
+Revision History:
+
+--*/
+#include"goal_util.h"
+#include"goal.h"
+
+struct has_term_ite_functor {
+    struct found {};
+    ast_manager & m;
+    has_term_ite_functor(ast_manager & _m):m(_m) {}
+    void operator()(var *) {}
+    void operator()(quantifier *) {}
+    void operator()(app * n) { if (m.is_term_ite(n)) throw found(); }
+};
+
+bool has_term_ite(goal const & g) {
+    return test<has_term_ite_functor>(g);
+}

src/framework/goal_util.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    goal_util.h
+
+Abstract:
+
+    goal goodies.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-01-03.
+
+Revision History:
+
+--*/
+#ifndef _GOAL_UTIL_H_
+#define _GOAL_UTIL_H_
+
+class goal;
+bool has_term_ite(goal const & g);
+
+#endif

src/framework/model_converter.cpp

@@ -0,0 +1,150 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_converter.h
+
+Abstract:
+
+    Abstract interface for converting models.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-21
+
+Notes:
+
+--*/
+#include"model_converter.h"
+#include"model_v2_pp.h"
+
+class concat_model_converter : public concat_converter<model_converter> {
+public:
+    concat_model_converter(model_converter * mc1, model_converter * mc2):concat_converter<model_converter>(mc1, mc2) {}
+
+    virtual void operator()(model_ref & m) {
+        this->m_c2->operator()(m);
+        this->m_c1->operator()(m);
+    }
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        this->m_c2->operator()(m, goal_idx);
+        this->m_c1->operator()(m, 0);
+    }
+
+    virtual char const * get_name() const { return "concat-model-converter"; }
+
+    virtual model_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_model_converter>(translator);
+    }
+};
+
+model_converter * concat(model_converter * mc1, model_converter * mc2) {
+    if (mc1 == 0)
+        return mc2;
+    if (mc2 == 0)
+        return mc1;
+    return alloc(concat_model_converter, mc1, mc2);
+}
+
+class concat_star_model_converter : public concat_star_converter<model_converter> {
+public:
+    concat_star_model_converter(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * szs):
+        concat_star_converter<model_converter>(mc1, num, mc2s, szs) {
+    }
+
+    virtual void operator()(model_ref & m) {
+        // TODO: delete method after conversion is complete
+        UNREACHABLE();
+    }
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        unsigned num = this->m_c2s.size();
+        for (unsigned i = 0; i < num; i++) {
+            if (goal_idx < this->m_szs[i]) {
+                // found the model converter that should be used
+                model_converter * c2 = this->m_c2s[i];
+                if (c2)
+                    c2->operator()(m, goal_idx);
+                if (m_c1)
+                    this->m_c1->operator()(m, i);
+                return;
+            }
+            // invalid goal
+            goal_idx -= this->m_szs[i];
+        }
+        UNREACHABLE();
+    }
+    
+    virtual char const * get_name() const { return "concat-star-model-converter"; }
+
+    virtual model_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_star_model_converter>(translator);
+    }
+};
+
+model_converter * concat(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * szs) {
+    SASSERT(num > 0);
+    if (num == 1)
+        return concat(mc1, mc2s[0]);
+    unsigned i;
+    for (i = 0; i < num; i++) {
+        if (mc2s[i] != 0)
+            break;
+    }
+    if (i == num) {
+        // all mc2s are 0
+        return mc1;
+    }
+    return alloc(concat_star_model_converter, mc1, num, mc2s, szs);
+}
+
+class model2mc : public model_converter {
+    model_ref m_model;
+public:
+    model2mc(model * m):m_model(m) {}
+    virtual ~model2mc() {}
+
+    virtual void operator()(model_ref & m) {
+        m = m_model;
+    }
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        m = m_model;
+    }
+
+    virtual void cancel() {
+    }
+    
+    virtual void display(std::ostream & out) {
+        out << "(model->model-converter-wrapper\n";
+        model_v2_pp(out, *m_model);
+        out << ")\n";
+    }    
+    
+    virtual model_converter * translate(ast_translation & translator) {
+        model * m = m_model->translate(translator);
+        return alloc(model2mc, m);
+    }
+};
+
+model_converter * model2model_converter(model * m) {
+    if (m == 0)
+        return 0;
+    return alloc(model2mc, m);
+}
+
+void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) {
+    if (mc) {
+        m = alloc(model, mng);
+        (*mc)(m, 0);
+    }
+}
+
+void apply(model_converter_ref & mc, model_ref & m, unsigned gidx) {
+    if (mc) {
+        (*mc)(m, gidx);
+    }
+}
+

src/framework/model_converter.h

@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_converter.h
+
+Abstract:
+
+    Abstract interface for converting models.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-21
+
+Notes:
+
+--*/
+#ifndef _MODEL_CONVERTER_H_
+#define _MODEL_CONVERTER_H_
+
+#include"model.h"
+#include"converter.h"
+#include"ref.h"
+
+class model_converter : public converter {
+public:
+    virtual void operator()(model_ref & m) {}  // TODO: delete
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        // TODO: make it virtual after the transition to goal/tactic/tactical is complete
+        SASSERT(goal_idx == 0);
+        operator()(m);
+    }
+    
+    virtual model_converter * translate(ast_translation & translator) = 0;
+};
+
+typedef ref<model_converter> model_converter_ref;
+
+model_converter * concat(model_converter * mc1, model_converter * mc2);
+
+/**
+   \brief \c mc1 is the model converter for a sequence of subgoals of size \c num.
+   Given an i in [0, num), mc2s[i] is the model converter for subgoal i,
+   and num_subgoals[i] is the number of subgoals of subgoals[i].
+*/
+model_converter * concat(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * num_subgoals);
+
+model_converter * model2model_converter(model * m);
+
+void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m);
+
+void apply(model_converter_ref & mc, model_ref & m, unsigned gidx);
+
+typedef sref_vector<model_converter> model_converter_ref_vector;
+typedef sref_buffer<model_converter> model_converter_ref_buffer;
+
+#endif

src/framework/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/framework/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/framework/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/framework/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/framework/probe.cpp

@@ -0,0 +1,449 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    probe.cpp
+
+Abstract:
+
+    Evaluates/Probes a goal.
+    
+    A probe is used to build tactics (aka strategies) that
+    makes decisions based on the structure of a goal.
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-13.
+
+Revision History:
+
+--*/
+#include"probe.h"
+#include"arith_decl_plugin.h"
+#include"bv_decl_plugin.h"
+#include"goal_util.h"
+
+class memory_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024));
+    }
+};
+
+probe * mk_memory_probe() {
+    return alloc(memory_probe);
+}
+
+class depth_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(g.depth());
+    }
+};
+
+class size_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(g.size());
+    }
+};
+
+class num_exprs_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(g.num_exprs());
+    }
+};
+
+probe * mk_depth_probe() {
+    return alloc(depth_probe);
+}
+
+probe * mk_size_probe() {
+    return alloc(size_probe);
+}
+
+probe * mk_num_exprs_probe() {
+    return alloc(num_exprs_probe);
+}
+
+class unary_probe : public probe {
+protected:
+    probe * m_p;
+public:
+    unary_probe(probe * p):
+        m_p(p) {
+        SASSERT(p); 
+        p->inc_ref(); 
+    }
+    
+    ~unary_probe() { 
+        m_p->dec_ref(); 
+    }
+
+};
+
+class bin_probe : public probe {
+protected:
+    probe * m_p1;
+    probe * m_p2;
+public:
+    bin_probe(probe * p1, probe * p2):
+        m_p1(p1), 
+        m_p2(p2) { 
+        SASSERT(p1); 
+        SASSERT(p2);
+        p1->inc_ref(); 
+        p2->inc_ref(); 
+    }
+    
+    ~bin_probe() { 
+        m_p1->dec_ref(); 
+        m_p2->dec_ref(); 
+    }
+};
+
+class not_probe : public unary_probe {
+public:
+    not_probe(probe * p):unary_probe(p) {}
+    virtual result operator()(goal const & g) {
+        return result(!m_p->operator()(g).is_true());
+    }    
+};
+
+class and_probe : public bin_probe {
+public:
+    and_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).is_true() && m_p2->operator()(g).is_true());
+    }
+};
+
+class or_probe : public bin_probe {
+public:
+    or_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).is_true() || m_p2->operator()(g).is_true());
+    }
+};
+
+class eq_probe : public bin_probe {
+public:
+    eq_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() == m_p2->operator()(g).get_value());
+    }
+};
+
+class le_probe : public bin_probe {
+public:
+    le_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() <= m_p2->operator()(g).get_value());
+    }
+};
+
+class add_probe : public bin_probe {
+public:
+    add_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() + m_p2->operator()(g).get_value());
+    }
+};
+
+class sub_probe : public bin_probe {
+public:
+    sub_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() - m_p2->operator()(g).get_value());
+    }
+};
+
+class mul_probe : public bin_probe {
+public:
+    mul_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() * m_p2->operator()(g).get_value());
+    }
+};
+
+class div_probe : public bin_probe {
+public:
+    div_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() / m_p2->operator()(g).get_value());
+    }
+};
+
+class const_probe : public probe {
+    double m_val;
+public:
+    const_probe(double v):m_val(v) {}
+    
+    virtual result operator()(goal const & g) {
+        return result(m_val); 
+    }
+};
+
+probe * mk_const_probe(double v) {
+    return alloc(const_probe, v);
+}
+
+probe * mk_not(probe * p) {
+    return alloc(not_probe, p);
+}
+
+probe * mk_and(probe * p1, probe * p2) {
+    return alloc(and_probe, p1, p2);
+}
+
+probe * mk_or(probe * p1, probe * p2) {
+    return alloc(or_probe, p1, p2);
+}
+
+probe * mk_implies(probe * p1, probe * p2) {
+    return mk_or(mk_not(p1), p2);
+}
+
+probe * mk_eq(probe * p1, probe * p2) {
+    return alloc(eq_probe, p1, p2);
+}
+
+probe * mk_neq(probe * p1, probe * p2) {
+    return mk_not(mk_eq(p1, p2));
+}
+
+probe * mk_le(probe * p1, probe * p2) {
+    return alloc(le_probe, p1, p2);
+}
+
+probe * mk_ge(probe * p1, probe * p2) {
+    return mk_le(p2, p1);
+}
+
+probe * mk_lt(probe * p1, probe * p2) {
+    return mk_not(mk_ge(p1, p2));
+}
+
+probe * mk_gt(probe * p1, probe * p2) {
+    return mk_lt(p2, p1);
+}
+
+probe * mk_add(probe * p1, probe * p2) {
+    return alloc(add_probe, p1, p2);
+}
+
+probe * mk_mul(probe * p1, probe * p2) {
+    return alloc(mul_probe, p1, p2);
+}
+
+probe * mk_sub(probe * p1, probe * p2) {
+    return alloc(sub_probe, p1, p2);
+}
+
+probe * mk_div(probe * p1, probe * p2) {
+    return alloc(div_probe, p1, p2);
+}
+
+struct is_non_propositional_predicate {
+    struct found {};
+    ast_manager & m;
+
+    is_non_propositional_predicate(ast_manager & _m):m(_m) {}
+    void operator()(var *) { throw found();  }
+    void operator()(quantifier *) { throw found(); }
+    void operator()(app * n) {
+        if (!m.is_bool(n))
+            throw found();
+        
+        family_id fid = n->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return; 
+        
+        if (is_uninterp_const(n))
+            return;
+
+        throw found();
+    }
+};
+
+struct is_non_qfbv_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       u;
+
+    is_non_qfbv_predicate(ast_manager & _m):m(_m), u(m) {}
+
+    void operator()(var *) { throw found();  }
+    
+    void operator()(quantifier *) { throw found(); }
+    
+    void operator()(app * n) {
+        if (!m.is_bool(n) && !u.is_bv(n))
+            throw found();
+        family_id fid = n->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return; 
+        if (fid == u.get_family_id())
+            return;
+        if (is_uninterp_const(n))
+            return;
+
+        throw found();
+    }
+};
+
+class is_propositional_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_propositional_predicate>(g);
+    }
+};
+
+class is_qfbv_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qfbv_predicate>(g);
+    }
+};
+
+probe * mk_is_propositional_probe() {
+    return alloc(is_propositional_probe);
+}
+
+probe * mk_is_qfbv_probe() {
+    return alloc(is_qfbv_probe); 
+}
+
+class num_consts_probe : public probe {
+    bool         m_bool;   // If true, track only boolean constants. Otherwise, track only non boolean constants.
+    char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family.
+    struct proc {
+        ast_manager & m;
+        bool          m_bool;
+        family_id     m_fid;
+        unsigned      m_counter;
+        proc(ast_manager & _m, bool b, char const * family):m(_m), m_bool(b), m_counter(0) {
+            if (family != 0)
+                m_fid = m.get_family_id(family);
+            else
+                m_fid = null_family_id;
+        }
+        void operator()(quantifier *) {}
+        void operator()(var *) {}
+        void operator()(app * n) { 
+            if (n->get_num_args() == 0 && !m.is_value(n)) {
+                if (m_bool) {
+                    if (m.is_bool(n))
+                        m_counter++;
+                }
+                else {
+                    if (m_fid == null_family_id) {
+                        if (!m.is_bool(n))
+                            m_counter++;
+                    }
+                    else {
+                        if (m.get_sort(n)->get_family_id() == m_fid)
+                            m_counter++;
+                    }
+                }
+            }
+        }
+    };
+
+public:
+    num_consts_probe(bool b, char const * f):
+        m_bool(b), m_family(f) {
+    }
+    virtual result operator()(goal const & g) {
+        proc p(g.m(), m_bool, m_family);
+        unsigned sz = g.size();
+        expr_fast_mark1 visited;
+        for (unsigned i = 0; i < sz; i++) {
+            for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));        
+        }
+        return result(p.m_counter);
+    }
+};
+
+probe * mk_num_consts_probe() {
+    return alloc(num_consts_probe, false, 0);
+}
+
+probe * mk_num_bool_consts_probe() {
+    return alloc(num_consts_probe, true, 0);
+}
+
+probe * mk_num_arith_consts_probe() {
+    return alloc(num_consts_probe, false, "arith");
+}
+
+probe * mk_num_bv_consts_probe() {
+    return alloc(num_consts_probe, false, "bv");
+}
+
+class produce_proofs_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return g.proofs_enabled();
+    }
+};
+
+class produce_models_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return g.models_enabled();
+    }
+};
+
+class produce_unsat_cores_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return g.unsat_core_enabled();
+    }
+};
+
+probe * mk_produce_proofs_probe() {
+    return alloc(produce_proofs_probe);
+}
+
+probe * mk_produce_models_probe() {
+    return alloc(produce_models_probe);
+}
+
+probe * mk_produce_unsat_cores_probe() {
+    return alloc(produce_unsat_cores_probe);
+}
+
+struct has_pattern_probe : public probe {
+    struct found {};
+
+    struct proc {
+        void operator()(var * n) {}
+        void operator()(app * n) {}
+        void operator()(quantifier * n) { 
+            if (n->get_num_patterns() > 0 || n->get_num_no_patterns() > 0)
+                throw found();
+        }
+    };
+public:
+    virtual result operator()(goal const & g) {
+        try {
+            expr_fast_mark1 visited;
+            proc p;
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; i++) {
+                quick_for_each_expr(p, visited, g.form(i));
+            }
+            return false;
+        }
+        catch (found) {
+            return true;
+        }
+    }
+};
+
+probe * mk_has_pattern_probe() {
+    return alloc(has_pattern_probe);
+}

src/framework/probe.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    probe.h
+
+Abstract:
+
+    Evaluates/Probes a goal.
+    
+    A probe is used to build tactics (aka strategies) that
+    makes decisions based on the structure of a goal.
+
+    The current implementation is very simple.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-13.
+
+Revision History:
+
+--*/
+#ifndef _PROBE_H_
+#define _PROBE_H_
+
+#include"goal.h"
+
+class probe {
+public:
+    class result {
+        double m_value;
+    public:
+        result(double v = 0.0):m_value(v) {}
+        result(unsigned v):m_value(static_cast<double>(v)) {}
+        result(int v):m_value(static_cast<double>(v)) {}
+        result(bool b):m_value(b ? 1.0 : 0.0) {}
+
+        bool is_true() const { return m_value != 0.0; }
+        double get_value() const { return m_value; }
+    };
+
+private:
+    unsigned m_ref_count;
+
+public:
+    probe():m_ref_count(0) {}
+    virtual ~probe() {}
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { SASSERT(m_ref_count > 0); --m_ref_count; if (m_ref_count == 0) dealloc(this); }
+    
+    virtual result operator()(goal const & g) = 0;
+};
+
+typedef ref<probe> probe_ref;
+
+probe * mk_memory_probe();
+probe * mk_depth_probe();
+probe * mk_size_probe();
+probe * mk_num_exprs_probe();
+probe * mk_const_probe(double val);
+probe * mk_num_consts_probe();
+probe * mk_num_bool_consts_probe();
+probe * mk_num_arith_consts_probe();
+probe * mk_num_bv_consts_probe();
+probe * mk_produce_proofs_probe();
+probe * mk_produce_models_probe();
+probe * mk_produce_unsat_cores_probe();
+probe * mk_has_pattern_probe();
+
+// Some basic combinators for probes
+probe * mk_not(probe * p1);
+probe * mk_and(probe * p1, probe * p2);
+probe * mk_or(probe * p1, probe * p2);
+probe * mk_implies(probe * p1, probe * p2);
+probe * mk_eq(probe * p1, probe * p2);
+probe * mk_neq(probe * p1, probe * p2);
+probe * mk_le(probe * p1, probe * p2);
+probe * mk_lt(probe * p1, probe * p2);
+probe * mk_ge(probe * p1, probe * p2);
+probe * mk_gt(probe * p1, probe * p2);
+probe * mk_add(probe * p1, probe * p2);
+probe * mk_sub(probe * p1, probe * p2);
+probe * mk_mul(probe * p1, probe * p2);
+probe * mk_div(probe * p1, probe * p2);
+
+probe * mk_is_propositional_probe();
+probe * mk_is_qfbv_probe();
+
+#endif

src/framework/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/framework/proof_converter.cpp

@@ -0,0 +1,162 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    proof_converter.cpp
+
+Abstract:
+
+    Abstract interface for converting proofs, and basic combinators
+
+Author:
+
+    Leonardo (leonardo) 2011-11-14
+
+Notes:
+
+--*/
+#include"proof_converter.h"
+#include"ast_smt2_pp.h"
+
+class concat_proof_converter : public concat_converter<proof_converter> {
+public:
+    concat_proof_converter(proof_converter * pc1, proof_converter * pc2):concat_converter<proof_converter>(pc1, pc2) {}
+
+    virtual char const * get_name() const { return "concat-proof-converter"; }
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        proof_ref tmp(m);
+        this->m_c2->operator()(m, num_source, source, tmp);
+        proof * new_source = tmp.get();
+        this->m_c1->operator()(m, 1, &new_source, result);
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_proof_converter>(translator);
+    }
+};
+
+proof_converter * concat(proof_converter * pc1, proof_converter * pc2) {
+    if (pc1 == 0)
+        return pc2;
+    if (pc2 == 0)
+        return pc1;
+    return alloc(concat_proof_converter, pc1, pc2);
+}
+
+class concat_star_proof_converter : public concat_star_converter<proof_converter> {
+public:
+    concat_star_proof_converter(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * szs):
+        concat_star_converter<proof_converter>(pc1, num, pc2s, szs) {
+    }
+
+    virtual char const * get_name() const { return "concat-star-proof-converter"; }
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        unsigned num = this->m_szs.size();
+#ifdef Z3DEBUG
+        unsigned sum = 0;
+        for (unsigned i = 0; i < num; i++) {
+            sum += this->m_szs[i];
+        }
+        SASSERT(sum == num_source);
+#endif
+        proof_ref_buffer tmp_prs(m);
+        for (unsigned i = 0; i < num; i++) {
+            unsigned sz = m_szs[i];
+            proof_converter * c2 = m_c2s[i];
+            proof_ref pr(m);
+            if (c2) {
+                (*c2)(m, sz, source, pr);
+            }
+            else {
+                SASSERT(sz == 1);
+                pr = *source;
+            }
+            source += sz;
+            tmp_prs.push_back(pr.get());
+        }
+        if (m_c1) {
+            (*m_c1)(m, tmp_prs.size(), tmp_prs.c_ptr(), result);
+        }
+        else {
+            SASSERT(tmp_prs.size() == 1);
+            result = tmp_prs[0];
+        }
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_star_proof_converter>(translator);
+    }
+};
+
+proof_converter * concat(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * szs) {
+    SASSERT(num > 0);
+    if (num == 1)
+        return concat(pc1, pc2s[0]);
+    unsigned i;
+    for (i = 0; i < num; i++) {
+        if (pc2s[i] != 0)
+            break;
+    }
+    if (i == num) {
+        // all pc2s are 0
+        return pc1;
+    }
+    return alloc(concat_star_proof_converter, pc1, num, pc2s, szs);
+}
+
+class proof2pc : public proof_converter {
+    proof_ref m_pr;
+public:
+    proof2pc(ast_manager & m, proof * pr):m_pr(pr, m) {}
+    virtual ~proof2pc() {}
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        SASSERT(num_source == 0);
+        result = m_pr;
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return alloc(proof2pc, translator.to(), translator(m_pr.get()));
+    }
+
+    virtual void display(std::ostream & out) {
+        out << "(proof->proof-converter-wrapper\n" << mk_ismt2_pp(m_pr.get(), m_pr.get_manager()) << ")\n";
+    }    
+};
+
+proof_converter * proof2proof_converter(ast_manager & m, proof * pr) {
+    if (pr == 0)
+        return 0;
+    return alloc(proof2pc, m, pr);
+}
+
+void apply(ast_manager & m, proof_converter * pc, proof_ref & pr) {
+    if (pc) {
+        proof * _pr = pr.get();
+        (*pc)(m, 1, &_pr, pr);
+    }
+}
+
+/**
+   Let pc2s be a buffer of proof converters that are wrappers for proofs.
+   That is, they are functors of the form: unit -> Proof
+   Then, this function applies pc1 to the proofs produced by pc2s's and store
+   the resultant proof in result.
+   
+   pc1 and pc2s must be different from 0.
+*/
+void apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s, proof_ref & result) {
+    SASSERT(pc1);
+    proof_ref_buffer prs(m);
+    unsigned sz = pc2s.size();
+    for (unsigned i = 0; i < sz; i++) {
+        proof_ref pr(m);
+        SASSERT(pc2s[i]); // proof production is enabled
+        pc2s[i]->operator()(m, 0, 0, pr);
+        prs.push_back(pr);
+    }
+    (*pc1)(m, sz, prs.c_ptr(), result);
+}

src/framework/proof_converter.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    proof_converter.h
+
+Abstract:
+
+    Abstract interface for converting proofs, and basic combinators.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-26
+
+Notes:
+
+--*/
+#ifndef _PROOF_CONVERTER_H_
+#define _PROOF_CONVERTER_H_
+
+#include"ast.h"
+#include"converter.h"
+#include"ref.h"
+
+class proof_converter : public converter {
+public:
+    virtual ~proof_converter() { }
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) = 0;
+    virtual proof_converter * translate(ast_translation & translator) = 0;
+};
+
+typedef ref<proof_converter> proof_converter_ref;
+
+proof_converter * concat(proof_converter * pc1, proof_converter * pc2);
+
+/**
+   \brief \c pc1 is the proof converter for a sequence of subgoals of size \c num.
+   Given an i in [0, num), pc2s[i] is the proof converter for subgoal i,
+   and num_subgoals[i] is the number of subgoals of subgoals[i].
+*/
+proof_converter * concat(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * num_subgoals);
+
+proof_converter * proof2proof_converter(ast_manager & m, proof * pr);
+
+typedef sref_vector<proof_converter> proof_converter_ref_vector;
+typedef sref_buffer<proof_converter> proof_converter_ref_buffer;
+
+void apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s, proof_ref & result);
+void apply(ast_manager & m, proof_converter * pc, proof_ref & pr);
+
+#endif

src/framework/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/framework/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/framework/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/framework/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/framework/tactic.cpp

@@ -0,0 +1,331 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactic.h
+
+Abstract:
+
+    Abstract tactic object.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-13
+
+Notes:
+
+--*/
+#include<iomanip>
+#include"tactic.h"
+#include"probe.h"
+#include"stopwatch.h"
+#include"model_v2_pp.h"
+#include"cmd_context.h"
+
+void tactic::cancel() {
+    #pragma omp critical (tactic_cancel)
+    {
+        set_cancel(true);
+    }
+}
+
+void tactic::reset_cancel() {
+    #pragma omp critical (tactic_cancel)
+    {
+        set_cancel(false);
+    }
+}
+
+struct tactic_report::imp {
+    char const *    m_id;
+    goal const &    m_goal;
+    stopwatch       m_watch;
+    double          m_start_memory;
+
+    imp(char const * id, goal const & g):
+        m_id(id),
+        m_goal(g),
+        m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
+        m_watch.start();
+    }
+        
+    ~imp() {
+        m_watch.stop();
+        double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
+        verbose_stream() << "(" << m_id
+                         << " :num-exprs " << m_goal.num_exprs()
+                         << " :num-asts " << m_goal.m().get_num_asts()
+                         << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
+                         << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
+                         << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
+                         << ")" << std::endl;
+    }
+};
+
+tactic_report::tactic_report(char const * id, goal const & g) {
+    if (get_verbosity_level() >= TACTIC_VERBOSITY_LVL)
+        m_imp = alloc(imp, id, g);
+    else
+        m_imp = 0;
+}
+
+tactic_report::~tactic_report() {
+    if (m_imp)
+        dealloc(m_imp);
+}
+
+void report_tactic_progress(char const * id, unsigned val) {
+    if (val > 0) {
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << id << " " << val << ")" << std::endl;);
+    }
+}
+
+
+class skip_tactic : public tactic {
+public:
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        result.reset();
+        result.push_back(in.get());
+        mc = 0;
+        pc = 0;
+        core = 0;
+    }
+
+    virtual void cleanup() {}
+
+    virtual tactic * translate(ast_manager & m) { return this; }
+};
+
+tactic * mk_skip_tactic() {
+    return alloc(skip_tactic);
+}
+
+class fail_tactic : public tactic {
+public:
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        throw tactic_exception("fail tactic");
+    }
+
+    virtual void cleanup() {}
+
+    virtual tactic * translate(ast_manager & m) { return this; }
+};
+
+tactic * mk_fail_tactic() {
+    return alloc(fail_tactic);
+}
+
+class report_verbose_tactic : public skip_tactic {
+    char const * m_msg;
+    unsigned     m_lvl;
+public:
+    report_verbose_tactic(char const * msg, unsigned lvl) : m_msg(msg), m_lvl(lvl) {}
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        IF_VERBOSE(m_lvl, verbose_stream() << m_msg << "\n";);
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) {
+    return alloc(report_verbose_tactic, msg, lvl);
+}
+
+class trace_tactic : public skip_tactic {
+    char const * m_tag;
+public:
+    trace_tactic(char const * tag):m_tag(tag) {}
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        TRACE(m_tag, in->display(tout););
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_trace_tactic(char const * tag) {
+    return alloc(trace_tactic, tag);
+}
+
+class echo_tactic : public skip_tactic {
+    cmd_context & m_ctx;
+    char const *  m_msg;
+    bool          m_newline;
+public:
+    echo_tactic(cmd_context & ctx, char const * msg, bool newline):m_ctx(ctx), m_msg(msg), m_newline(newline) {}
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        #pragma omp critical (echo_tactic)
+        {
+            m_ctx.diagnostic_stream() << m_msg;
+            if (m_newline)
+                m_ctx.diagnostic_stream() << std::endl;
+        }
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline) {
+    return alloc(echo_tactic, ctx, msg, newline);
+}
+
+class probe_value_tactic : public skip_tactic {
+    cmd_context & m_ctx;
+    char const *  m_msg;
+    probe *       m_p;
+    bool          m_newline;
+public:
+    probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline):m_ctx(ctx), m_msg(msg), m_p(p), m_newline(newline) {
+        SASSERT(m_p);
+        m_p->inc_ref(); 
+    }
+    
+    ~probe_value_tactic() {
+        m_p->dec_ref();
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        double val = (*m_p)(*(in.get())).get_value();
+        #pragma omp critical (probe_value_tactic)
+        {
+            if (m_msg)
+                m_ctx.diagnostic_stream() << m_msg << " ";
+            m_ctx.diagnostic_stream() << val;
+            if (m_newline)
+                m_ctx.diagnostic_stream() << std::endl;
+        }
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline) {
+    return alloc(probe_value_tactic, ctx, msg, p, newline);
+}
+
+class fail_if_undecided_tactic : public skip_tactic {
+public:
+    fail_if_undecided_tactic() {}
+
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        if (!in->is_decided()) 
+            throw tactic_exception("undecided");
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_fail_if_undecided_tactic() {
+    return alloc(fail_if_undecided_tactic);
+}
+
+void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) {
+    t.reset_statistics();
+    t.reset_cancel();
+    try {
+        t(in, result, mc, pc, core);
+        t.cleanup();
+    }
+    catch (tactic_exception & ex) {
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(tactic-exception \"" << escaped(ex.msg()) << "\")" << std::endl;);
+        t.cleanup();
+        throw ex;
+    }
+}
+
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
+    bool models_enabled = g->models_enabled();
+    bool proofs_enabled = g->proofs_enabled();
+    bool cores_enabled  = g->unsat_core_enabled();
+    md   = 0;
+    pr   = 0;
+    core = 0;
+    ast_manager & m = g->m();
+    goal_ref_buffer r;
+    model_converter_ref mc;
+    proof_converter_ref pc;
+    try {
+        exec(t, g, r, mc, pc, core);
+    }
+    catch (tactic_exception & ex) {
+        reason_unknown = ex.msg();
+        return l_undef;
+    }
+    TRACE("tactic_mc", mc->display(tout););
+    TRACE("tactic_check_sat",
+          tout << "r.size(): " << r.size() << "\n";
+          for (unsigned i = 0; i < r.size(); i++) r[0]->display(tout););
+
+    if (is_decided_sat(r)) {
+        if (models_enabled) {
+            model_converter2model(m, mc.get(), md);
+            if (!md) {
+                // create empty model.
+                md = alloc(model, m);
+            }
+        }
+        return l_true;
+    }
+    else if (is_decided_unsat(r)) {
+        goal * final = r[0];
+        SASSERT(m.is_false(final->form(0)));
+        if (proofs_enabled) pr   = final->pr(0);
+        if (cores_enabled)  core = final->dep(0);
+        return l_false;
+    }
+    else {
+        if (models_enabled) model_converter2model(m, mc.get(), md);
+        reason_unknown = "incomplete";
+        return l_undef;
+    }
+}
+
+void fail_if_proof_generation(char const * tactic_name, goal_ref const & in) {
+    if (in->proofs_enabled()) {
+        std::string msg = tactic_name;
+        msg += " does not support proof production";
+        throw tactic_exception(msg.c_str());
+    }
+}
+
+void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in) {
+    if (in->unsat_core_enabled()) {
+        std::string msg = tactic_name;
+        msg += " does not support unsat core production";
+        throw tactic_exception(msg.c_str());
+    }
+}
+
+void fail_if_model_generation(char const * tactic_name, goal_ref const & in) {
+    if (in->models_enabled()) {
+        std::string msg = tactic_name;
+        msg += " does not generate models";
+        throw tactic_exception(msg.c_str());
+    }
+}

src/framework/tactic.h

@@ -0,0 +1,155 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactic.h
+
+Abstract:
+
+    Abstract tactic object.
+    It used to be called assertion_set_strategy.
+    The main improvement is the support for multiple subgoals.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-13
+
+Notes:
+
+--*/
+#ifndef _TACTIC_H_
+#define _TACTIC_H_
+
+#include"goal.h"
+#include"params.h"
+#include"statistics.h"
+#include"model_converter.h"
+#include"proof_converter.h"
+#include"tactic_exception.h"
+#include"lbool.h"
+
+struct front_end_params;
+class progress_callback;
+
+typedef ptr_buffer<goal> goal_buffer;
+
+class tactic {
+    unsigned m_ref_count;
+public:
+    tactic():m_ref_count(0) {}
+    virtual ~tactic() {}
+
+    void inc_ref() { m_ref_count++; }
+    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+
+    virtual void updt_params(params_ref const & p) {}
+    virtual void collect_param_descrs(param_descrs & r) {}
+
+    void cancel();
+    void reset_cancel();
+    virtual void set_cancel(bool f) {}
+    
+    /**
+       \brief Apply tactic to goal \c in.
+       
+       The list of resultant subgoals is stored in \c result.
+       The content of \c in may be destroyed during the operation.
+       
+       The resultant model converter \c mc can be used to convert a model for one of the returned subgoals
+       into a model for \in. If mc == 0, then model construction is disabled or any model for a subgoal
+       of \c in is also a model for \c in.
+       If \c result is decided_sat (i.e., it contains a single empty subgoal), then
+       the model converter is just wrapping the model.
+
+       The resultant proof converter \c pc can be used to convert proofs for each subgoal in \c result
+       into a proof for \c in. If pc == 0, then one of the following conditions should hold:
+         1- proof construction is disabled, 
+         2- result contains a single subgoal, and any proof of unsatisfiability for this subgoal is a proof for \c in.
+         3- result is an decided_unsat (i.e., it contains a single unsat subgoal). The actual proof can be extracted from this goal.
+         
+       The output parameter \c core is used to accumulate the unsat core of closed subgoals.
+       It must be 0 if dependency tracking is disabled, or the result is decided unsat, or 
+       no tagged assertions were used to close any subgoal.
+       
+       Note that, this signature is not compatible with the one described in the paper:
+       "The Strategy Challenge in SMT Solving".
+       The approach in the paper is conceptually simpler, but (for historical reasons) it would
+       require a lot of re-engineering in the Z3 code. In Z3, we keep a proof/justification for every formula
+       in a goal.
+       
+       Therefore, in most cases, pc == 0 and core == 0 for non-branching tactics.
+    */
+    virtual void operator()(/* in */  goal_ref const & in, 
+                            /* out */ goal_ref_buffer & result, 
+                            /* out */ model_converter_ref & mc, 
+                            /* out */ proof_converter_ref & pc,
+                            /* out */ expr_dependency_ref & core) = 0;
+
+    virtual void collect_statistics(statistics & st) const {}
+    virtual void reset_statistics() {}
+    virtual void cleanup() = 0;
+    virtual void reset() { cleanup(); }
+
+    // for backward compatibility
+    virtual void set_front_end_params(front_end_params & p) {}
+    virtual void set_logic(symbol const & l) {}
+    virtual void set_progress_callback(progress_callback * callback) {}
+
+    // translate tactic to the given manager
+    virtual tactic * translate(ast_manager & m) = 0;
+};
+
+typedef ref<tactic>         tactic_ref;
+typedef sref_vector<tactic> tactic_ref_vector;
+typedef sref_buffer<tactic> tactic_ref_buffer;
+
+// minimum verbosity level for tactics
+#define TACTIC_VERBOSITY_LVL 10
+
+class tactic_report {
+    struct imp;
+    imp *  m_imp;
+public:
+    tactic_report(char const * id, goal const & g);
+    ~tactic_report();
+};
+
+void report_tactic_progress(char const * id, unsigned val);
+
+tactic * mk_skip_tactic();
+tactic * mk_fail_tactic();
+tactic * mk_fail_if_undecided_tactic();
+
+tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl);
+tactic * mk_trace_tactic(char const * tag);
+tactic * mk_echo_tactic(cmd_context & ctx, char const * msg, bool newline = true);
+// Display the value returned by p in the diagnostic_stream
+class probe;
+tactic * mk_probe_value_tactic(cmd_context & ctx, char const * msg, probe * p, bool newline = true);
+
+
+class tactic_factory {
+public:
+    virtual ~tactic_factory() {}
+    virtual tactic * operator()(ast_manager & m, params_ref const & p) = 0;
+};
+
+#define MK_TACTIC_FACTORY(NAME, CODE)                                           \
+class NAME : public tactic_factory {                                            \
+public:                                                                         \
+    virtual ~NAME() {}                                                          \
+    virtual tactic * operator()(ast_manager & m, params_ref const & p) { CODE } \
+};
+
+#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST)  MK_TACTIC_FACTORY(NAME, return ST;)
+
+void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
+
+// Throws an exception if goal \c in requires proof generation.
+void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);
+void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in);
+void fail_if_model_generation(char const * tactic_name, goal_ref const & in);
+
+#endif

src/framework/tactic_cmds.cpp

@@ -0,0 +1,812 @@
+/*++
+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"
+
+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/framework/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/framework/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/framework/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
+
+
+

src/framework/tactical.h

@@ -0,0 +1,83 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactical.h
+
+Abstract:
+
+    Basic combinators
+
+Author:
+
+    Leonardo (leonardo) 2011-10-13
+
+Notes:
+
+--*/
+#ifndef _TACTICAL_H_
+#define _TACTICAL_H_
+
+#include"tactic.h"
+#include"probe.h"
+
+tactic * and_then(unsigned num, tactic * const * ts);
+tactic * and_then(tactic * t1, tactic * t2);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10);
+
+tactic * or_else(unsigned num, tactic * const * ts);
+tactic * or_else(tactic * t1, tactic * t2);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10);
+
+tactic * repeat(tactic * t, unsigned max = UINT_MAX); 
+/**
+   \brief Fails if \c t produeces more than \c threshold subgoals.
+   Otherwise, it behabes like \c t.
+*/
+tactic * fail_if_branching(tactic * t, unsigned threshold = 1);
+
+tactic * par(unsigned num, tactic * const * ts);
+tactic * par(tactic * t1, tactic * t2);
+tactic * par(tactic * t1, tactic * t2, tactic * t3);
+tactic * par(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
+
+tactic * par_and_then(unsigned num, tactic * const * ts);
+tactic * par_and_then(tactic * t1, tactic * t2);
+
+tactic * try_for(tactic * t, unsigned msecs);
+tactic * clean(tactic * t);
+tactic * using_params(tactic * t, params_ref const & p);
+
+// Create a tactic that fails if the result returned by probe p is true.
+tactic * fail_if(probe * p);
+tactic * fail_if_not(probe * p);
+// Execute t1 if p returns true, and t2 otherwise
+tactic * cond(probe * p, tactic * t1, tactic * t2);
+// Alias for cond(p, t, mk_skip_tactic())
+tactic * when(probe * p, tactic * t);
+
+// alias for (or-else t skip)
+tactic * skip_if_failed(tactic * t);
+
+// Execute the given tactic only if proof production is not enabled.
+// If proof production is enabled it is a skip
+tactic * if_no_proofs(tactic * t);
+tactic * if_no_unsat_cores(tactic * t);
+tactic * if_no_models(tactic * t);
+
+#endif