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)40inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast<Z3_tactic_ref *>(g); } of_tactic(Z3_tactic_ref * g)41inline Z3_tactic of_tactic(Z3_tactic_ref * g) { return reinterpret_cast<Z3_tactic>(g); } to_tactic_ref(Z3_tactic g)42inline tactic * to_tactic_ref(Z3_tactic g) { return g == nullptr ? nullptr : to_tactic(g)->m_tactic.get(); } 43 to_probe(Z3_probe g)44inline Z3_probe_ref * to_probe(Z3_probe g) { return reinterpret_cast<Z3_probe_ref *>(g); } of_probe(Z3_probe_ref * g)45inline Z3_probe of_probe(Z3_probe_ref * g) { return reinterpret_cast<Z3_probe>(g); } to_probe_ref(Z3_probe g)46inline 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)56inline 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)57inline Z3_apply_result of_apply_result(Z3_apply_result_ref * g) { return reinterpret_cast<Z3_apply_result>(g); } 58 59