z3-src 503.2.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
49
50
51
52
53
54
55
56
57
58

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    spacer_farkas_learner.h

Abstract:

    SMT2 interface for the datalog SPACER

Author:

    Krystof Hoder (t-khoder) 2011-11-1.

Revision History:

--*/

#pragma once

#include "ast/ast.h"

namespace spacer {

class farkas_learner {
    typedef obj_hashtable<expr> expr_set;

    bool m_split_literals;

    void combine_constraints(unsigned cnt, app * const * constrs, rational const * coeffs, expr_ref& res);

    bool is_farkas_lemma(ast_manager& m, expr* e);

    void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas);

    bool is_pure_expr(func_decl_set const& symbs, expr* e, ast_manager& m) const;

public:
    farkas_learner(): m_split_literals(false) {}

    /**
        Traverse a proof and retrieve lemmas using the vocabulary from bs.
    */
    void get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas);

    void collect_statistics(statistics& st) const {}
    void reset_statistics() {}


    /** \brief see smt::farkas_util::set_split_literals */
    void set_split_literals(bool v) {m_split_literals = v;}

};


}