z3-src 503.2.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    dl_register_engine.cpp

Abstract:

    Class for creating Datalog engines.

Author:

    Nikolaj Bjorner (nbjorner) 2013-08-28

Revision History:

--*/
#include "muz/fp/dl_register_engine.h"
#include "muz/bmc/dl_bmc_engine.h"
#include "muz/clp/clp_context.h"
#include "muz/tab/tab_context.h"
#include "muz/rel/rel_context.h"
#include "muz/ddnf/ddnf.h"
#include "muz/spacer/spacer_dl_interface.h"

namespace datalog {
    register_engine::register_engine(): m_ctx(nullptr) {}
    
    engine_base* register_engine::mk_engine(DL_ENGINE engine_type) {
        switch(engine_type) {
        case SPACER_ENGINE:
            return alloc(spacer::dl_interface, *m_ctx);
        case DATALOG_ENGINE:
            return alloc(rel_context, *m_ctx);
        case BMC_ENGINE:
        case QBMC_ENGINE:
            return alloc(bmc, *m_ctx);
        case TAB_ENGINE:
            return alloc(tab, *m_ctx);
        case CLP_ENGINE:
            return alloc(clp, *m_ctx);
        case DDNF_ENGINE:
            return alloc(ddnf, *m_ctx);
        case LAST_ENGINE:
            UNREACHABLE();
            return nullptr;
        }
        UNREACHABLE();
        return nullptr;
    }

}