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

/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

    q_eval.h

Abstract:

    Evaluation of clauses

Author:

    Nikolaj Bjorner (nbjorner) 2021-01-24

--*/
#pragma once

#include "ast/has_free_vars.h"
#include "sat/smt/q_clause.h"

namespace euf {
    class solver;
}

namespace q {

    class eval {
        euf::solver&       ctx;
        ast_manager&       m;
        expr_fast_mark1    m_mark;
        euf::enode_vector  m_eval;
        euf::enode_vector  m_indirect_nodes;
        bool               m_freeze_swap = false;
        euf::enode_pair    m_diseq_undef;
        contains_vars      m_contains_vars;

        struct scoped_mark_reset;

        // compare s, t modulo binding
        lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
        lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
        
    public:
        eval(euf::solver& ctx);

        lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence);
        lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence);
        euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence);

        euf::enode_vector const& get_watch() { return m_indirect_nodes; }
    };
}