z3-src 415.4.3

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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    seq_offset_eq.h

Abstract:

    Container for maintaining equalities between lengths of sequences.

Author:

    Thai Minh Trinh 2017
    Nikolaj Bjorner (nbjorner) 2020-4-16

--*/
#pragma once

#include "util/obj_pair_hashtable.h"
#include "ast/seq_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "smt/smt_theory.h"
#include <optional>

namespace smt {

    class seq_offset_eq {
        theory&        th;
        ast_manager&   m;
        seq_util       seq;
        arith_util     a;
        obj_hashtable<enode>             m_has_offset_equality;
        obj_pair_map<enode, enode, int>  m_offset_equalities;
        int                              m_propagation_level;

        bool match_x_minus_y(expr* e, expr*& x, expr*& y) const;
        void len_offset(expr* e, int val);
        void prop_arith_to_len_offset();

    public:

        seq_offset_eq(theory& th, ast_manager& m);
        bool empty() const { return m_offset_equalities.empty(); }
        /**
           \brief determine if r1 = r2 + offset
           \return optional containing the offset if found, nullopt otherwise
         */
        std::optional<int> find(enode* r1, enode* r2) const;
        bool contains(enode* r1, enode* r2) const { return find(r1, r2).has_value(); }
        bool contains(enode* r);
        bool propagate();
        void pop_scope_eh(unsigned num_scopes);
    };

};