z3-src 501.0.1

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

/**++
  Copyright (c) 2017 Arie Gurfinkel

  Legacy implementations of frames. To be removed.

  Notes: this file is included from the middle of spacer_context.h
*/
#pragma once

class legacy_frames
{
    pred_transformer &m_pt;

    /// level formulas
    vector<expr_ref_vector>      m_levels;
    /// map property to level where it occurs.
    obj_map<expr, unsigned>      m_prop2level;
    /// properties that are invariant.
    expr_ref_vector              m_invariants;

    void simplify_formulas (tactic& tac, expr_ref_vector& v);

public:
    legacy_frames (pred_transformer &pt) :
    m_pt(pt), m_invariants (m_pt.get_ast_manager ()) {}
    pred_transformer& pt () const {return m_pt;}
    bool add_lemma (expr * lemma, unsigned level);
    void get_frame_lemmas (unsigned level, expr_ref_vector &out)
    {
        if(is_infty_level(level)) { out.append(m_invariants); }
        else if(level < m_levels.size()) { out.append(m_levels [level]); }
    }

    void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out);
    void add_frame () {m_levels.push_back (expr_ref_vector (m_pt.get_ast_manager ()));}

    unsigned size () const {return m_levels.size ();}
    unsigned lemma_size () const {return m_prop2level.size ();}


    void propagate_to_infinity (unsigned level);
    bool propagate_to_next_level (unsigned level);

    void simplify_formulas ();

    void inherit_frames (legacy_frames& other);

};