1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 api_datalog.h
7
8 Abstract:
9 Datalog API
10 old external_relation_context_impl
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2012-02-29.
15
16 Revision History:
17
18 --*/
19 #pragma once
20
21 #include "api/z3.h"
22 #include "ast/ast.h"
23 #include "smt/params/smt_params.h"
24 #include "smt/smt_kernel.h"
25 #include "api/api_util.h"
26
27 typedef void (*reduce_app_callback_fptr)(void*, func_decl*, unsigned, expr*const*, expr**);
28 typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*const*, unsigned, expr*const*);
29
30 namespace api {
31 class fixedpoint_context;
32 class context;
33 };
34
35
36 struct Z3_fixedpoint_ref : public api::object {
37 api::fixedpoint_context * m_datalog;
38 params_ref m_params;
Z3_fixedpoint_refZ3_fixedpoint_ref39 Z3_fixedpoint_ref(api::context& c): api::object(c), m_datalog(nullptr) {}
~Z3_fixedpoint_refZ3_fixedpoint_ref40 ~Z3_fixedpoint_ref() override { dealloc(m_datalog); }
41 };
42
to_fixedpoint(Z3_fixedpoint s)43 inline Z3_fixedpoint_ref * to_fixedpoint(Z3_fixedpoint s) { return reinterpret_cast<Z3_fixedpoint_ref *>(s); }
of_datalog(Z3_fixedpoint_ref * s)44 inline Z3_fixedpoint of_datalog(Z3_fixedpoint_ref * s) { return reinterpret_cast<Z3_fixedpoint>(s); }
to_fixedpoint_ref(Z3_fixedpoint s)45 inline api::fixedpoint_context * to_fixedpoint_ref(Z3_fixedpoint s) { return to_fixedpoint(s)->m_datalog; }
46
47
48