z3-src 500.0.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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    context_params.h

Abstract:

    Goodies for managing context parameters in the cmd_context and
    api_context

Author:

    Leonardo (leonardo) 2012-12-01

Notes:

--*/
#pragma once

#include "util/params.h"
#include "util/zstring.h"

class context_params {
    void set_bool(bool & opt, char const * param, char const * value);
    void set_uint(unsigned & opt, char const * param, char const * value);

    unsigned    m_rlimit { 0 };

public:
    unsigned         m_timeout { UINT_MAX } ;
    std::string      m_dot_proof_file;
    std::string      m_trace_file_name;
    bool             m_auto_config { true };
    bool             m_proof { false };
    bool             m_debug_ref_count { false };
    bool             m_trace { false };
    bool             m_well_sorted_check { false };
    bool             m_model { true };
    bool             m_model_validate { false };
    bool             m_dump_models { false };
    bool             m_unsat_core { false };
    bool             m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager.
    bool             m_statistics { false };
    std::string      m_encoding { "unicode" };

    unsigned rlimit() const { return m_rlimit; }
    context_params();
    void set(char const * param, char const * value);
    void set_rlimit(unsigned lim) { m_rlimit = lim; }
    void updt_params();
    void updt_params(params_ref const & p);
    static void collect_param_descrs(param_descrs & d);
    /*
      REG_PARAMS('context_params::collect_param_descrs')
    */

    /**
       \brief Goodies for extracting parameters for creating a solver object.
    */
    void get_solver_params(params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);

    static void collect_solver_param_descrs(param_descrs & d);

    /**
       \brief Include in p parameters derived from this context_params.
       These are parameters that are meaningful for tactics and solvers.
       Example: auto_config
    */
    params_ref merge_default_params(params_ref const & p);

    /**
       \brief Is this a parameter that can only be set for the shell.
    */
    bool is_shell_only_parameter(char const* p) const;


};