Searched refs:mk_skolem_binding (Results 1 – 2 of 2) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/muz/bmc/ |
| H A D | dl_bmc_engine.cpp | 531 expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args); in get_proof()
603 …expr_ref_vector mk_skolem_binding(rule& r, ptr_vector<sort> const& vars, expr_ref_vector const& ar… in mk_skolem_binding() function in datalog::bmc::nonlinear
622 expr_ref_vector binding = mk_skolem_binding(r, vars, args); in skolemize_vars()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/bmc/ |
| H A D | dl_bmc_engine.cpp | 531 expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args);
603 …expr_ref_vector mk_skolem_binding(rule& r, ptr_vector<sort> const& vars, expr_ref_vector const& ar…
622 expr_ref_vector binding = mk_skolem_binding(r, vars, args);
|