1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     api_tactic.h
7 
8 Abstract:
9     API for creating tactics and goals.
10 
11 Author:
12 
13     Leonardo de Moura (leonardo) 2012-03-06.
14 
15 Revision History:
16 
17 --*/
18 #pragma once
19 
20 #include "api/api_goal.h"
21 #include "tactic/tactical.h"
22 
23 namespace api {
24     class context;
25 }
26 
27 
28 struct Z3_tactic_ref : public api::object {
29     tactic_ref   m_tactic;
Z3_tactic_refZ3_tactic_ref30     Z3_tactic_ref(api::context& c): api::object(c) {}
~Z3_tactic_refZ3_tactic_ref31     ~Z3_tactic_ref() override {}
32 };
33 
34 struct Z3_probe_ref : public api::object {
35     probe_ref    m_probe;
Z3_probe_refZ3_probe_ref36     Z3_probe_ref(api::context& c):api::object(c) {}
~Z3_probe_refZ3_probe_ref37     ~Z3_probe_ref() override {}
38 };
39 
to_tactic(Z3_tactic g)40 inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast<Z3_tactic_ref *>(g); }
of_tactic(Z3_tactic_ref * g)41 inline Z3_tactic of_tactic(Z3_tactic_ref * g) { return reinterpret_cast<Z3_tactic>(g); }
to_tactic_ref(Z3_tactic g)42 inline tactic * to_tactic_ref(Z3_tactic g) { return g == nullptr ? nullptr : to_tactic(g)->m_tactic.get(); }
43 
to_probe(Z3_probe g)44 inline Z3_probe_ref * to_probe(Z3_probe g) { return reinterpret_cast<Z3_probe_ref *>(g); }
of_probe(Z3_probe_ref * g)45 inline Z3_probe of_probe(Z3_probe_ref * g) { return reinterpret_cast<Z3_probe>(g); }
to_probe_ref(Z3_probe g)46 inline probe * to_probe_ref(Z3_probe g) { return g == nullptr ? nullptr : to_probe(g)->m_probe.get(); }
47 
48 struct Z3_apply_result_ref : public api::object {
49     goal_ref_buffer      m_subgoals;
50     model_converter_ref  m_mc;
51     proof_converter_ref  m_pc;
52     Z3_apply_result_ref(api::context& c, ast_manager & m);
~Z3_apply_result_refZ3_apply_result_ref53     ~Z3_apply_result_ref() override {}
54 };
55 
to_apply_result(Z3_apply_result g)56 inline Z3_apply_result_ref * to_apply_result(Z3_apply_result g) { return reinterpret_cast<Z3_apply_result_ref *>(g); }
of_apply_result(Z3_apply_result_ref * g)57 inline Z3_apply_result of_apply_result(Z3_apply_result_ref * g) { return reinterpret_cast<Z3_apply_result>(g); }
58 
59