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

/*++
  Copyright (c) 2017 Microsoft Corporation

  Module Name:

  <name>

  Abstract:

  <abstract>

  Author:

  Lev Nachmanson (levnach)

  Revision History:


  --*/
#include <memory>
#include "util/vector.h"
#include <set>
#include <utility>
#include "math/lp/static_matrix_def.h"
#include "math/lp/lp_core_solver_base.h"
#include "math/lp/lp_primal_core_solver.h"
#include "math/lp/lar_solver.h"
namespace lp {
    
    template std::set<std::pair<unsigned, unsigned>> static_matrix<mpq, mpq>::get_domain();
    template void static_matrix<mpq, mpq>::add_new_element(unsigned, unsigned, const mpq&);
    template mpq& static_matrix<mpq, mpq>::add_new_element(unsigned, unsigned);
    template void static_matrix<mpq, numeric_pair<mpq>>::add_new_element(unsigned, unsigned, const mpq&);
    template mpq& static_matrix<mpq, numeric_pair<mpq>>::add_new_element(unsigned, unsigned);
    template std::set<std::pair<unsigned, unsigned>> static_matrix<mpq, numeric_pair<mpq> >::get_domain();
    template void static_matrix<mpq, mpq>::add_column_to_vector(mpq const&, unsigned int, mpq*) const;
    template bool static_matrix<mpq, mpq>::is_correct() const;

    template mpq static_matrix<mpq, mpq>::get_balance() const;
    template mpq static_matrix<mpq, mpq>::get_elem(unsigned int, unsigned int) const;
    template mpq static_matrix<mpq, mpq>::get_max_abs_in_column(unsigned int) const;
    template mpq static_matrix<mpq, mpq>::get_max_abs_in_row(unsigned int) const;
    template mpq static_matrix<mpq, mpq>::get_min_abs_in_column(unsigned int) const;
    template mpq static_matrix<mpq, mpq>::get_min_abs_in_row(unsigned int) const;
    template void static_matrix<mpq, mpq>::init_row_columns(unsigned int, unsigned int);
    template void static_matrix<mpq, mpq>::clear();
    template static_matrix<mpq, mpq>::ref& static_matrix<mpq, mpq>::ref::operator=(mpq const&);
    template void static_matrix<mpq, mpq>::set(unsigned int, unsigned int, mpq const&);

    template static_matrix<mpq, mpq>::static_matrix(unsigned int, unsigned int);
#ifdef Z3DEBUG
    template bool static_matrix<mpq, numeric_pair<mpq> >::is_correct() const;
#endif
    template mpq static_matrix<mpq, numeric_pair<mpq> >::get_elem(unsigned int, unsigned int) const;
    template void static_matrix<mpq, numeric_pair<mpq> >::init_empty_matrix(unsigned int, unsigned int);
    template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);


    template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
    template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
    template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int);
    template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell<empty_struct>&, unsigned int, int);
    template void static_matrix<mpq, numeric_pair<mpq> >::add_rows(mpq const&, unsigned int, unsigned int);
    template void static_matrix<mpq,mpq>::add_rows(mpq const &,unsigned int,unsigned int);
    template void static_matrix<mpq, mpq>:: pivot_term_to_row_given_cell<lar_term>(lar_term const & term, column_cell&c, unsigned j, int j_sign);
    template void static_matrix<mpq, mpq>::add_term_to_row<lar_term>(const mpq& alpha, lar_term const & term, unsigned ii);
    template void static_matrix<mpq, numeric_pair<mpq> >::remove_element(std::vector<row_cell<mpq>, std_allocator<row_cell<mpq> > >&, row_cell<mpq>&);
}