z3/src/tactic/tactic.h

/*++
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:

--*/
#pragma once

#include "util/params.h"
#include "util/lbool.h"
#include "util/statistics.h"
#include "tactic/user_propagator_base.h"
#include "tactic/goal.h"
#include "tactic/tactic_exception.h"

class progress_callback;

typedef ptr_buffer<goal> goal_buffer;

class tactic : public user_propagator::core {
    unsigned m_ref_count = 0;
public:
    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) {}
    
    /**
       \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 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()(goal_ref const & in, goal_ref_buffer& result) = 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_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;

    static void checkpoint(ast_manager& m);

    void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
        throw default_exception("tactic does not support clause logging");
    }

    void user_propagate_init(
        void* ctx,
        user_propagator::push_eh_t& push_eh,
        user_propagator::pop_eh_t& pop_eh,
        user_propagator::fresh_eh_t& fresh_eh) override {
        throw default_exception("tactic does not support user propagation");
    }

    void user_propagate_register_expr(expr* e) override { }
    virtual char const* name() const = 0;

protected:
    friend class nary_tactical;
    friend class binary_tactical;
    friend class unary_tactical;

};

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);

class statistics_report {
    tactic* m_tactic = nullptr;
    std::function<void(statistics& st)> m_collector;
public:
    statistics_report(tactic& t):m_tactic(&t) {}
    statistics_report(std::function<void(statistics&)>&& coll): m_collector(std::move(coll)) {}
    ~statistics_report();
};

class skip_tactic : public tactic {
public:
    void operator()(goal_ref const & in, goal_ref_buffer& result) override;
    void cleanup() override {}
    tactic * translate(ast_manager & m) override { return this; } 
    char const* name() const override { return "skip"; }
    void collect_statistics(statistics& st) const override {}
    void user_propagate_initialize_value(expr* var, expr* value) override { }
};

tactic * mk_skip_tactic();
tactic * mk_fail_tactic();
tactic * mk_fail_if_undecided_tactic();
tactic*  mk_lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic*(ast_manager& m, params_ref const& p)>);

/*
  ADD_TACTIC("skip", "do nothing tactic.", "mk_skip_tactic()")
  ADD_TACTIC("fail", "always fail tactic.", "mk_fail_tactic()")
  ADD_TACTIC("fail-if-undecided", "fail if goal is undecided.", "mk_fail_if_undecided_tactic()")
*/

tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl);
tactic * mk_trace_tactic(char const * tag);

void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result);
lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, 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);
void fail_if_has_quantifiers(char const* tactic_name, goal_ref const& in);