mk_fresh_uncnstr_var_for (reference) in projects: dports

Project(s)

Full Search
Definition
Symbol
File Path
History
Type

Searched refs:mk_fresh_uncnstr_var_for (Results 1 – 2 of 2) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/tactic/core/
H A D	elim_uncnstr_tactic.cpp	91 bool mk_fresh_uncnstr_var_for(app * t, app * & v) { in mk_fresh_uncnstr_var_for() function 115 return mk_fresh_uncnstr_var_for(m().mk_app(f, arg), v); in mk_fresh_uncnstr_var_for() 257 mk_fresh_uncnstr_var_for(f, arg1, arg2, u); in process_eq() 264 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, u)) in process_eq() 357 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, u)) in process_le_ge() 412 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_arith_mul() 425 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_arith_mul() 461 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_bv_mul() 476 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_bv_mul() 490 if (!mk_fresh_uncnstr_var_for(f, arg, r)) in process_extract() [all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/
H A D	elim_uncnstr_tactic.cpp	90 bool mk_fresh_uncnstr_var_for(app * t, app * & v) { in mk_fresh_uncnstr_var_for() function 114 return mk_fresh_uncnstr_var_for(m().mk_app(f, arg), v); in mk_fresh_uncnstr_var_for() 256 mk_fresh_uncnstr_var_for(f, arg1, arg2, u); in process_eq() 263 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, u)) in process_eq() 356 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, u)) in process_le_ge() 411 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_arith_mul() 424 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_arith_mul() 460 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_bv_mul() 475 if (!mk_fresh_uncnstr_var_for(f, num, args, r)) in process_bv_mul() 489 if (!mk_fresh_uncnstr_var_for(f, arg, r)) in process_extract() [all …]