z3-src 503.2.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
57
58
59
60
61
62
63
64

/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

    euf_invariant.cpp

Abstract:

    Check invariants for EUF solver.

Author:

    Nikolaj Bjorner (nbjorner) 2020-09-07

--*/

#include "sat/smt/euf_solver.h"

namespace euf {

    /**
       \brief Check if expressions attached to bool_variables and enodes have a consistent assignment.
       For all a, b.  root(a) == root(b) ==> get_assignment(a) == get_assignment(b)
    */

    void solver::check_eqc_bool_assignment() const {
        for (enode* n : m_egraph.nodes()) {
            VERIFY(!m.is_bool(n->get_expr()) || 
                   s().value(enode2literal(n)) == s().value(enode2literal(n->get_root())));
        }
    }

    void solver::check_missing_bool_enode_propagation() const {
        for (enode* n : m_egraph.nodes()) 
            if (m.is_bool(n->get_expr()) && l_undef == s().value(enode2literal(n))) {
                if (!n->is_root()) {
                    VERIFY(l_undef == s().value(enode2literal(n->get_root())));
                }
                else
                    for (enode* o : enode_class(n)) {
                        VERIFY(l_undef == s().value(enode2literal(o)));
                    }
            }
    }

    void solver::check_missing_eq_propagation() const {
        if (s().inconsistent())
            return;
        for (enode* n : m_egraph.nodes())
            if (m.is_false(n->get_root()->get_expr()) && 
                m.is_eq(n->get_expr()) &&
                !m.is_bool(n->get_app()->get_arg(0)) && 
                (n->get_arg(0)->get_root() == n->get_arg(1)->get_root())) {
                enable_trace("euf");
                TRACE(euf, display(tout << n->get_expr_id() << ": " << mk_pp(n->get_expr(), m) << "\n" 
                                     << "#" << n->get_arg(0)->get_expr_id() << " == #" << n->get_arg(1)->get_expr_id() << " r: " << n->get_arg(0)->get_root_id() << "\n");
                      );
                UNREACHABLE();
            }
    }


}