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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    nlsat_scoped_literal_vector.h

Abstract:

    Scoped vector for nlsat literals.
    Just to be "cancel" safe.

Author:

    Leonardo de Moura (leonardo) 2012-01-13.

Revision History:

--*/
#pragma once

#include "nlsat/nlsat_solver.h"

namespace nlsat {

    class scoped_literal_vector {
        solver &       m_solver;
        literal_vector m_lits;
    public:
        scoped_literal_vector(solver & s):m_solver(s) {}
        ~scoped_literal_vector() { reset(); }

        scoped_literal_vector(scoped_literal_vector && other) noexcept = default;

        scoped_literal_vector & operator=(scoped_literal_vector && other) noexcept {
            if (this != &other) {
                SASSERT(&m_solver == &other.m_solver);
                reset();  // dec_ref our current literals
                m_lits = std::move(other.m_lits);
            }
            return *this;
        }
        
        // Delete copy operations to prevent accidental copies
        scoped_literal_vector(scoped_literal_vector const &) = delete;
        scoped_literal_vector & operator=(scoped_literal_vector const &) = delete;
        
        unsigned size() const { return m_lits.size(); }
        bool empty() const { return m_lits.empty(); }
        literal operator[](unsigned i) const { return m_lits[i]; }
        void reset() {
            for (literal l : m_lits) {
                m_solver.dec_ref(l);
            }
            m_lits.reset();
        }
        void push_back(literal l) {
            m_solver.inc_ref(l);
            m_lits.push_back(l);
        }
        void set(unsigned i, literal l) {
            m_solver.inc_ref(l);
            m_solver.dec_ref(m_lits[i]);
            m_lits[i] = l;
        }
        literal const * data() const { return m_lits.data(); }
        literal const * begin() const { return m_lits.begin(); }
        literal const * end() const { return m_lits.end(); }
        void shrink(unsigned new_sz) {
            SASSERT(new_sz <= m_lits.size());
            unsigned sz = m_lits.size();
            if (new_sz == sz)
                return;
            for (unsigned i = new_sz; i < sz; ++i) {
                m_solver.dec_ref(m_lits[i]);
            }
            m_lits.shrink(new_sz);
        }
        void append(unsigned sz, literal const * ls) {
            for (unsigned i = 0; i < sz; ++i)
                push_back(ls[i]);
        }
        void append(scoped_literal_vector const& ls) {
            append(ls.size(), ls.data());
        }
        void swap(scoped_literal_vector& other) noexcept {
            SASSERT(&m_solver == &other.m_solver);
            m_lits.swap(other.m_lits);
        }
    };


    class scoped_literal {
        solver &  m_solver;
        literal   m_lit;
    public:
        scoped_literal(solver & s):m_solver(s), m_lit(null_literal) {}
        ~scoped_literal() { m_solver.dec_ref(m_lit); }
        scoped_literal & operator=(literal l) { 
            m_solver.inc_ref(l);
            m_solver.dec_ref(m_lit);
            m_lit = l;
            return *this;
        }
        scoped_literal & operator=(scoped_literal const & l) { return operator=(l.m_lit); }
        operator literal&() { return m_lit; }
        operator literal const &() const { return m_lit; }
        void neg() { m_lit.neg(); }
    };
};