z3-src 501.0.1

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


/*++
Copyright (c) 2018 Microsoft Corporation

Module Name:

    smt_arith_value.h

Abstract:

    Utility to extract arithmetic values from context.

Author:

    Nikolaj Bjorner (nbjorner) 2018-12-08.

Revision History:

--*/
#pragma once

#include "ast/arith_decl_plugin.h"
#include "smt/smt_context.h"
#include "smt/theory_lra.h"
#include "smt/theory_arith.h"
#include "smt/theory_bv.h"

namespace smt {
    class arith_value {
        context* m_ctx;        
        ast_manager& m;
        arith_util a;
        bv_util    b;
        theory_mi_arith* m_tha;
        theory_i_arith*  m_thi;
        theory_lra*      m_thr;
        theory_bv*       m_thb;
    public:
        arith_value(ast_manager& m);
        void init(context* ctx);
        bool get_lo_equiv(expr* e, rational& lo, bool& strict);
        bool get_up_equiv(expr* e, rational& up, bool& strict);
        bool get_value_equiv(expr* e, rational& value) const;
        bool get_lo(expr* e, rational& lo, bool& strict) const;
        bool get_up(expr* e, rational& up, bool& strict) const;
        bool get_value(expr* e, rational& value) const;
        expr_ref get_lo(expr* e) const;
        expr_ref get_up(expr* e) const;
        expr_ref get_fixed(expr* e) const;
        final_check_status final_check(unsigned );
        lbool check_lp_feasible(vector<std::pair<bool, expr_ref>> &ineqs, literal_vector &lit_core,
                                enode_pair_vector &eq_core);
    };
}