z3-src 503.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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    spacer_mev_array.h

Abstract:

    Utilities to evaluate arrays in the model.

Author:
   based on model_evaluator in muz/pdr/pdr_util.h

Revision History:

--*/
#pragma once

#include"ast/ast.h"
#include"ast/rewriter/rewriter_types.h"
#include"util/params.h"
#include"ast/array_decl_plugin.h"

/**
 * based on model_evaluator in muz/pdr/pdr_util.h
 */
class model_evaluator_array_util {
    ast_manager&    m;
    array_util      m_array;

    void eval_exprs(model& mdl, expr_ref_vector& es);

    bool extract_array_func_interp(model& mdl, expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);

public:

    model_evaluator_array_util (ast_manager& m):
        m (m),
        m_array (m)
    {}

    /**
     * best effort evaluator of extensional array equality.
     */
    void eval_array_eq(model& mdl, app* e, expr* arg1, expr* arg2, expr_ref& res);

    void eval(model& mdl, expr* e, expr_ref& r, bool model_completion = true);
};