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
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

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    qe_lite.h

Abstract:

    Light weight partial quantifier-elimination procedures

Author:

    Nikolaj Bjorner (nbjorner) 2012-10-17

Revision History:


--*/

#pragma once

#include "ast/ast.h"
#include "util/uint_set.h"
#include "util/params.h"
#include "ast/simplifiers/dependent_expr_state.h"

class tactic;

class qe_lite {
    class impl;
    impl * m_impl;

public:
    /** 
        use_array_der controls whether equalities over array reads are simplified
     */
    qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true);

    ~qe_lite();

    /**
       \brief
       Apply light-weight quantifier elimination
       on constants provided as vector of variables.
       Return the updated formula and updated set of variables that were not eliminated.

    */
    void operator()(app_ref_vector& vars, expr_ref& fml);

    /**
       \brief
       Apply light-weight quantifier elimination to variables present/absent in the index set.
       If 'index_of_bound' is true, then the index_set is treated as the set of
       bound variables. if 'index_of_bound' is false, then index_set is treated as the
       set of variables that are not bound (variables that are not in the index set are bound).
     */
    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml);

    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs);
    /**
        \brief full rewriting based light-weight quantifier elimination round.
    */
    void operator()(expr_ref& fml, proof_ref& pr);

    void operator()(expr* fml, expr_ref& result, proof_ref& pr) { result = fml; (*this)(result, pr); }

    void operator()(expr_ref& fml) { proof_ref pr(fml.m()); (*this)(fml, pr); }
};

tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());

dependent_expr_simplifier* mk_qe_lite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st);

/*
  ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
  ADD_SIMPLIFIER("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_simplifier(m, p, s)")
*/