/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/ |
H A D | lp_api.h | 35 bool m_is_int; variable 45 m_is_int(is_int), in bound() 62 bool is_int() const { return m_is_int; } in is_int() 71 if (m_is_int) { in get_value()
|
/dports/math/z3/z3-z3-4.8.13/src/math/lp/ |
H A D | lp_api.h | 35 bool m_is_int; variable 45 m_is_int(is_int), in bound() 62 bool is_int() const { return m_is_int; } in is_int() 71 if (m_is_int) { in get_value()
|
/dports/math/z3/z3-z3-4.8.13/src/api/java/ |
H A D | Statistics.java | 56 return m_is_int; in isUInt() 91 private boolean m_is_int = false; field in Statistics.Entry 99 m_is_int = true; in Entry()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/java/ |
H A D | Statistics.java | 56 return m_is_int; in isUInt() 91 private boolean m_is_int = false; field in Statistics.Entry 99 m_is_int = true; in Entry()
|
/dports/math/tvmet/tvmet-1.7.2/doc/ |
H A D | Util.h | 147 : m_name(s), m_description(d), m_is_int(i){ } in m_name() 150 bool is_int() const { return m_is_int; } in is_int() 154 bool m_is_int; variable
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
H A D | fm_tactic.cpp | 381 char_vector m_is_int; member 832 m_is_int.reset(); in init() 857 return m_is_int[x] != 0; in is_int() 936 m_is_int.push_back(is_int); in mk_var() 943 SASSERT(m_var2expr.size() == m_is_int.size()); in mk_var() 944 SASSERT(m_lowers.size() == m_is_int.size()); in mk_var() 945 SASSERT(m_uppers.size() == m_is_int.size()); in mk_var() 947 SASSERT(m_var2pos.size() == m_is_int.size()); in mk_var() 1145 char_vector const m_is_int; member 1155 bool int1 = m_is_int[p1.first] != 0; in operator ()() [all …]
|
H A D | bound_propagator.h | 110 char_vector m_is_int; variable 188 bool is_int(var x) const { return m_is_int[x] != 0; } in is_int()
|
H A D | bound_propagator.cpp | 140 m_is_int.reserve(x+1, false); in mk_var() 150 m_is_int[x] = is_int; in mk_var() 736 m_is_int.finalize(); in reset()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
H A D | fm_tactic.cpp | 384 char_vector m_is_int; member 835 m_is_int.reset(); in init() 860 return m_is_int[x] != 0; in is_int() 939 m_is_int.push_back(is_int); in mk_var() 946 SASSERT(m_var2expr.size() == m_is_int.size()); in mk_var() 947 SASSERT(m_lowers.size() == m_is_int.size()); in mk_var() 948 SASSERT(m_uppers.size() == m_is_int.size()); in mk_var() 950 SASSERT(m_var2pos.size() == m_is_int.size()); in mk_var() 1148 char_vector const m_is_int; member 1158 bool int1 = m_is_int[p1.first] != 0; in operator ()() [all …]
|
H A D | bound_propagator.h | 110 char_vector m_is_int; variable 188 bool is_int(var x) const { return m_is_int[x] != 0; } in is_int()
|
H A D | bound_propagator.cpp | 140 m_is_int.reserve(x+1, false); in mk_var() 150 m_is_int[x] = is_int; in mk_var() 736 m_is_int.finalize(); in reset()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/ |
H A D | expr2polynomial.h | 102 bool_vector m_is_int; variable
|
H A D | expr2polynomial.cpp | 511 return m_is_int[x]; in is_int() 516 m_is_int.reserve(x+1, false); in mk_var() 517 m_is_int[x] = is_int; in mk_var()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
H A D | expr2polynomial.h | 102 bool_vector m_is_int; variable
|
H A D | expr2polynomial.cpp | 511 return m_is_int[x]; in is_int() 516 m_is_int.reserve(x+1, false); in mk_var() 517 m_is_int[x] = is_int; in mk_var()
|
/dports/math/z3/z3-z3-4.8.13/src/qe/ |
H A D | qe_lite.cpp | 999 char_vector m_is_int; member in qel::fm::fm 1457 m_is_int.reset(); in init() 1481 return m_is_int[x] != 0; in is_int() 1560 m_is_int.push_back(is_int); in mk_var() 1567 SASSERT(m_var2expr.size() == m_is_int.size()); in mk_var() 1568 SASSERT(m_lowers.size() == m_is_int.size()); in mk_var() 1569 SASSERT(m_uppers.size() == m_is_int.size()); in mk_var() 1570 SASSERT(m_forbidden.size() == m_is_int.size()); in mk_var() 1769 char_vector const m_is_int; member 1779 bool int1 = m_is_int[p1.first] != 0; in operator ()() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
H A D | qe_lite.cpp | 999 char_vector m_is_int; member in qel::fm::fm 1457 m_is_int.reset(); in init() 1481 return m_is_int[x] != 0; in is_int() 1560 m_is_int.push_back(is_int); in mk_var() 1567 SASSERT(m_var2expr.size() == m_is_int.size()); in mk_var() 1568 SASSERT(m_lowers.size() == m_is_int.size()); in mk_var() 1569 SASSERT(m_uppers.size() == m_is_int.size()); in mk_var() 1570 SASSERT(m_forbidden.size() == m_is_int.size()); in mk_var() 1769 char_vector const m_is_int; member 1779 bool int1 = m_is_int[p1.first] != 0; in operator ()() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | theory_dense_diff_logic.h | 126 bool_vector m_is_int; variable 175 bool is_int(theory_var v) const { return m_is_int[v]; } in is_int()
|
H A D | theory_dense_diff_logic_def.h | 55 m_is_int.push_back(is_int); in mk_var() 370 m_is_int.shrink(old_num_vars); in del_vars() 424 m_is_int .reset(); in reset_eh() 617 SASSERT(m_is_int.size() == m_matrix.size()); in check_vector_sizes()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | theory_dense_diff_logic.h | 126 bool_vector m_is_int; variable 175 bool is_int(theory_var v) const { return m_is_int[v]; } in is_int()
|
H A D | theory_dense_diff_logic_def.h | 55 m_is_int.push_back(is_int); in mk_var() 370 m_is_int.shrink(old_num_vars); in del_vars() 424 m_is_int .reset(); in reset_eh() 617 SASSERT(m_is_int.size() == m_matrix.size()); in check_vector_sizes()
|
/dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
H A D | nlsat_solver.cpp | 318 return m_is_int.size(); in num_vars() 322 return m_is_int[x]; in is_int() 487 m_is_int. push_back(is_int); in register_var() 496 SASSERT(m_is_int.size() == m_perm.size()); in register_var() 824 for (var x = 0; x < m_is_int.size(); ++x) { in check_lemma() 825 checker.register_var(x, m_is_int[x]); in check_lemma() 2413 is_int.swap(m_is_int); in reorder() 2891 if (mx >= m_is_int.size()) return false; in solve_var() 2893 if (m_is_int[x]) continue; in solve_var() 3446 unsigned sz = m_is_int.size(); in display_smt2_arith_decls() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
H A D | nlsat_solver.cpp | 318 return m_is_int.size(); in num_vars() 322 return m_is_int[x]; in is_int() 487 m_is_int. push_back(is_int); in register_var() 496 SASSERT(m_is_int.size() == m_perm.size()); in register_var() 824 for (var x = 0; x < m_is_int.size(); ++x) { in check_lemma() 825 checker.register_var(x, m_is_int[x]); in check_lemma() 2413 is_int.swap(m_is_int); in reorder() 2891 if (mx >= m_is_int.size()) return false; in solve_var() 2893 if (m_is_int[x]) continue; in solve_var() 3446 unsigned sz = m_is_int.size(); in display_smt2_arith_decls() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/math/subpaving/ |
H A D | subpaving_t.h | 478 bool_vector m_is_int; variable 771 unsigned num_vars() const { return m_is_int.size(); } in num_vars() 773 bool is_int(var x) const { SASSERT(x < num_vars()); return m_is_int[x]; } in is_int()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/subpaving/ |
H A D | subpaving_t.h | 478 bool_vector m_is_int; variable 771 unsigned num_vars() const { return m_is_int.size(); } in num_vars() 773 bool is_int(var x) const { SASSERT(x < num_vars()); return m_is_int[x]; } in is_int()
|