z3-src 503.3.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

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    theory_opt.h

Abstract:

    Interface utilities used by optimization providing 
    theory solvers.

Author:

    Nikolaj Bjorner (nbjorner) 2013-10-18

Notes:

--*/

#include "util/inf_rational.h"
#include "util/inf_eps_rational.h"
#include "ast/arith_decl_plugin.h"
#include <optional>

#pragma once

class generic_model_converter;
namespace smt {
    class theory_opt {
    public:
        typedef inf_eps_rational<inf_rational> inf_eps;
        virtual ~theory_opt() = default;
        virtual inf_eps value(theory_var) = 0;
        virtual inf_eps maximize(theory_var v, expr_ref& blocker) = 0;
        struct upper_bound {
            rational value;
            // Otherwise the certificate depends on the current Boolean branch.
            bool is_global;
        };
        virtual inf_eps maximize_with_bound(theory_var v, expr_ref& blocker, std::optional<upper_bound>& upper) {
            upper.reset();
            return maximize(v, blocker);
        }
        virtual theory_var add_objective(app* term) = 0;
        bool is_linear(ast_manager& m, expr* term);
        bool is_numeral(arith_util& a, expr* term);
    };
}