/dports/math/z3/z3-z3-4.8.13/src/api/ |
H A D | api_numeral.cpp | 194 return mk_c(c)->mk_external_string(strm.str()); in Z3_get_numeral_binary_string() 213 return mk_c(c)->mk_external_string(r.to_string()); in Z3_get_numeral_string() 222 return mk_c(c)->mk_external_string("roundNearestTiesToEven"); in Z3_get_numeral_string() 228 return mk_c(c)->mk_external_string("roundTowardPositive"); in Z3_get_numeral_string() 231 return mk_c(c)->mk_external_string("roundTowardNegative"); in Z3_get_numeral_string() 235 return mk_c(c)->mk_external_string("roundTowardZero"); in Z3_get_numeral_string() 242 return mk_c(c)->mk_external_string(buffer.str()); in Z3_get_numeral_string() 293 return mk_c(c)->mk_external_string(buffer.str()); in Z3_get_numeral_decimal_string() 300 return mk_c(c)->mk_external_string(buffer.str()); in Z3_get_numeral_decimal_string() 307 return mk_c(c)->mk_external_string(buffer.str()); in Z3_get_numeral_decimal_string() [all …]
|
H A D | api_parsers.cpp | 170 RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); in Z3_eval_smtlib2_string() 176 RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); in Z3_eval_smtlib2_string() 178 RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); in Z3_eval_smtlib2_string() 179 Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str())); in Z3_eval_smtlib2_string()
|
H A D | api_params.cpp | 121 return mk_c(c)->mk_external_string(buffer.str()); in Z3_params_to_string() 196 return mk_c(c)->mk_external_string(result); in Z3_param_descrs_get_documentation() 213 return mk_c(c)->mk_external_string(buffer.str()); in Z3_param_descrs_to_string()
|
H A D | api_context.h | 181 char * mk_external_string(char const * str, unsigned n); 182 char * mk_external_string(char const * str); 183 char * mk_external_string(std::string && str);
|
H A D | api_goal.cpp | 193 return mk_c(c)->mk_external_string(std::move(result)); in Z3_goal_to_string() 211 return mk_c(c)->mk_external_string(std::move(result)); in Z3_goal_to_dimacs_string()
|
H A D | api_context.cpp | 157 char * context::mk_external_string(char const * str) { in mk_external_string() function in api::context 162 char * context::mk_external_string(char const * str, unsigned n) { in mk_external_string() function in api::context 168 char * context::mk_external_string(std::string && str) { in mk_external_string() function in api::context
|
H A D | api_opt.cpp | 205 return mk_c(c)->mk_external_string(to_optimize_ptr(o)->reason_unknown()); in Z3_optimize_get_reason_unknown() 306 return mk_c(c)->mk_external_string(to_optimize_ptr(o)->to_string()); in Z3_optimize_to_string() 318 return mk_c(c)->mk_external_string(buffer.str()); in Z3_optimize_get_help()
|
H A D | api_rcf.cpp | 278 return mk_c(c)->mk_external_string(buffer.str()); in Z3_rcf_num_to_string() 289 return mk_c(c)->mk_external_string(buffer.str()); in Z3_rcf_num_to_decimal_string()
|
H A D | api_stats.cpp | 36 return mk_c(c)->mk_external_string(std::move(result)); in Z3_stats_to_string()
|
H A D | api_ast.cpp | 355 return mk_c(c)->mk_external_string(buffer.str()); in Z3_get_symbol_string() 358 return mk_c(c)->mk_external_string(_s.bare_str()); in Z3_get_symbol_string() 611 return mk_c(c)->mk_external_string(p.get_rational().to_string()); in Z3_get_decl_rational_parameter() 793 return mk_c(c)->mk_external_string(buffer.str()); in Z3_simplify_get_help() 916 return mk_c(c)->mk_external_string(buffer.str()); in Z3_ast_to_string() 951 return mk_c(c)->mk_external_string(buffer.str()); in Z3_benchmark_to_smtlib_string()
|
H A D | api_ast_vector.cpp | 136 return mk_c(c)->mk_external_string(buffer.str()); in Z3_ast_vector_to_string()
|
H A D | api_ast_map.cpp | 166 return mk_c(c)->mk_external_string(buffer.str()); in Z3_ast_map_to_string()
|
H A D | api_solver.cpp | 343 return mk_c(c)->mk_external_string(buffer.str()); in Z3_solver_get_help() 688 return mk_c(c)->mk_external_string(to_solver_ref(s)->reason_unknown()); in Z3_solver_get_reason_unknown() 715 return mk_c(c)->mk_external_string(buffer.str()); in Z3_solver_to_string() 726 return mk_c(c)->mk_external_string(buffer.str()); in Z3_solver_to_dimacs_string()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
H A D | api_numeral.cpp | 194 return mk_c(c)->mk_external_string(strm.str()); 213 return mk_c(c)->mk_external_string(r.to_string()); 222 return mk_c(c)->mk_external_string("roundNearestTiesToEven"); 228 return mk_c(c)->mk_external_string("roundTowardPositive"); 231 return mk_c(c)->mk_external_string("roundTowardNegative"); 235 return mk_c(c)->mk_external_string("roundTowardZero"); 242 return mk_c(c)->mk_external_string(buffer.str()); 293 return mk_c(c)->mk_external_string(buffer.str()); 300 return mk_c(c)->mk_external_string(buffer.str()); 307 return mk_c(c)->mk_external_string(buffer.str()); [all …]
|
H A D | api_parsers.cpp | 161 RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); 167 RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); 169 RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); 170 Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
|
H A D | api_params.cpp | 120 return mk_c(c)->mk_external_string(buffer.str()); in Z3_params_to_string() 195 return mk_c(c)->mk_external_string(result); in Z3_param_descrs_get_documentation() 212 return mk_c(c)->mk_external_string(buffer.str()); in Z3_param_descrs_to_string()
|
H A D | api_context.h | 186 char * mk_external_string(char const * str, unsigned n); 187 char * mk_external_string(char const * str); 188 char * mk_external_string(std::string && str);
|
H A D | api_goal.cpp | 192 return mk_c(c)->mk_external_string(std::move(result)); in Z3_goal_to_string() 210 return mk_c(c)->mk_external_string(std::move(result)); in Z3_goal_to_dimacs_string()
|
H A D | api_context.cpp | 166 char * context::mk_external_string(char const * str) { in mk_external_string() function in api::context 171 char * context::mk_external_string(char const * str, unsigned n) { in mk_external_string() function in api::context 177 char * context::mk_external_string(std::string && str) { in mk_external_string() function in api::context
|
H A D | api_opt.cpp | 202 return mk_c(c)->mk_external_string(to_optimize_ptr(o)->reason_unknown()); 303 return mk_c(c)->mk_external_string(to_optimize_ptr(o)->to_string()); 315 return mk_c(c)->mk_external_string(buffer.str());
|
H A D | api_rcf.cpp | 278 return mk_c(c)->mk_external_string(buffer.str()); in Z3_rcf_num_to_string() 289 return mk_c(c)->mk_external_string(buffer.str()); in Z3_rcf_num_to_decimal_string()
|
H A D | api_stats.cpp | 37 return mk_c(c)->mk_external_string(std::move(result)); in Z3_stats_to_string()
|
H A D | api_ast.cpp | 350 return mk_c(c)->mk_external_string(buffer.str()); in Z3_get_symbol_string() 353 return mk_c(c)->mk_external_string(_s.bare_str()); in Z3_get_symbol_string() 606 return mk_c(c)->mk_external_string(p.get_rational().to_string()); in Z3_get_decl_rational_parameter() 785 return mk_c(c)->mk_external_string(buffer.str()); in Z3_simplify_get_help() 908 return mk_c(c)->mk_external_string(buffer.str()); in Z3_ast_to_string() 943 return mk_c(c)->mk_external_string(buffer.str()); in Z3_benchmark_to_smtlib_string()
|
H A D | api_ast_vector.cpp | 135 return mk_c(c)->mk_external_string(buffer.str());
|
H A D | api_ast_map.cpp | 165 return mk_c(c)->mk_external_string(buffer.str()); in Z3_ast_map_to_string()
|