Home
last modified time | relevance | path

Searched refs:m_is_int (Results 1 – 25 of 31) sorted by relevance

12

/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/
H A Dlp_api.h35 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 Dlp_api.h35 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 DStatistics.java56 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 DStatistics.java56 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 DUtil.h147 : 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 Dfm_tactic.cpp381 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 Dbound_propagator.h110 char_vector m_is_int; variable
188 bool is_int(var x) const { return m_is_int[x] != 0; } in is_int()
H A Dbound_propagator.cpp140 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 Dfm_tactic.cpp384 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 Dbound_propagator.h110 char_vector m_is_int; variable
188 bool is_int(var x) const { return m_is_int[x] != 0; } in is_int()
H A Dbound_propagator.cpp140 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 Dexpr2polynomial.h102 bool_vector m_is_int; variable
H A Dexpr2polynomial.cpp511 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 Dexpr2polynomial.h102 bool_vector m_is_int; variable
H A Dexpr2polynomial.cpp511 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 Dqe_lite.cpp999 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 Dqe_lite.cpp999 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 Dtheory_dense_diff_logic.h126 bool_vector m_is_int; variable
175 bool is_int(theory_var v) const { return m_is_int[v]; } in is_int()
H A Dtheory_dense_diff_logic_def.h55 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 Dtheory_dense_diff_logic.h126 bool_vector m_is_int; variable
175 bool is_int(theory_var v) const { return m_is_int[v]; } in is_int()
H A Dtheory_dense_diff_logic_def.h55 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 Dnlsat_solver.cpp318 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 Dnlsat_solver.cpp318 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 Dsubpaving_t.h478 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 Dsubpaving_t.h478 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()

12