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

/*++
Copyright (c) 2024 Microsoft Corporation

Module Name:

    bv_sls_terms.h

Abstract:

    A Stochastic Local Search (SLS) engine

Author:

    Nikolaj Bjorner (nbjorner) 2024-02-07
    
--*/
#pragma once

#include "util/lbool.h"
#include "util/scoped_ptr_vector.h"
#include "util/uint_set.h"
#include "ast/ast.h"
#include "ast/bv_decl_plugin.h"
#include "ast/sls/sls_stats.h"
#include "ast/sls/sls_powers.h"
#include "ast/sls/sls_bv_valuation.h"
#include "ast/sls/sls_context.h"

namespace sls {

    class bv_terms {
        ast_manager&        m;
        bv_util             bv;
        expr_ref_vector     m_axioms;
        vector<ptr_vector<expr>> m_uninterp_occurs;

        expr_ref ensure_binary(expr* e);

        expr_ref mk_sdiv(expr* x, expr* y);
        expr_ref mk_smod(expr* x, expr* y);
        expr_ref mk_srem(expr* x, expr* y);

        void register_uninterp(expr* e);

    public:
        bv_terms(context& ctx);       

        void register_term(expr* e);

        bool is_bv_predicate(expr* e) const;

        expr_ref_vector& axioms() { return m_axioms; }

        ptr_vector<expr> const& uninterp_occurs(expr* e);
    };
}