Home
last modified time | relevance | path

Searched refs:cross_nested (Results 1 – 14 of 14) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/math/lp/
H A Dhorner.cpp70 bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) { in lemmas_on_expr()
90 cross_nested cn( in lemmas_on_row()
H A Dhorner.h47 bool lemmas_on_expr(cross_nested&, nex_sum*);
H A Dnex.h131 friend class cross_nested; variable
181 friend class cross_nested; variable
276 friend class cross_nested; variable
H A Dcross_nested.h26 class cross_nested {
46 cross_nested(std::function<bool (const nex*)> call_on_result, in cross_nested() function
448 ~cross_nested() { in ~cross_nested()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/
H A Dhorner.cpp70 bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) { in lemmas_on_expr()
90 cross_nested cn( in lemmas_on_row()
H A Dhorner.h47 bool lemmas_on_expr(cross_nested&, nex_sum*);
H A Dnex.h132 friend class cross_nested;
182 friend class cross_nested;
277 friend class cross_nested;
H A Dcross_nested.h26 class cross_nested {
46 cross_nested(std::function<bool (const nex*)> call_on_result, in cross_nested() function
448 ~cross_nested() { in ~cross_nested()
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dtheory_arith_nl.h1401 expr_ref s = cross_nested(depth + 1, e, nullptr); in horner()
1427 expr_ref theory_arith<Ext>::cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var) { in cross_nested() function
1503 expr_ref h = cross_nested(depth + 1, rest, nullptr); in cross_nested()
1532 expr_ref cn = cross_nested(0, p, var); in is_cross_nested_consistent()
H A Dtheory_arith.h1016 expr_ref cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var);
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dtheory_arith_nl.h1401 expr_ref s = cross_nested(depth + 1, e, nullptr); in horner()
1427 expr_ref theory_arith<Ext>::cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var) { in cross_nested() function
1503 expr_ref h = cross_nested(depth + 1, rest, nullptr); in cross_nested()
1532 expr_ref cn = cross_nested(0, p, var); in is_cross_nested_consistent()
H A Dtheory_arith.h1016 expr_ref cross_nested(unsigned depth, buffer<coeff_expr> & p, expr * var);
/dports/math/z3/z3-z3-4.8.13/src/test/lp/
H A Dlp.cpp74 void test_cn_on_expr(nex_sum *t, cross_nested& cn) { in test_cn_on_expr()
126 cross_nested cn( in test_simplify()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/lp/
H A Dlp.cpp74 void test_cn_on_expr(nex_sum *t, cross_nested& cn) { in spki()
126 cross_nested cn( in spki()