| /dports/math/z3/z3-z3-4.8.13/src/muz/rel/ |
| H A D | dl_table_relation.h | 111 void add_table_fact(const table_fact & f);
|
| H A D | rel_context.cpp | 565 rel.add_table_fact(fact); in add_fact()
|
| H A D | dl_table_relation.cpp | 431 void table_relation::add_table_fact(const table_fact & f) { in add_table_fact() function in datalog::table_relation
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/rel/ |
| H A D | dl_table_relation.h | 111 void add_table_fact(const table_fact & f);
|
| H A D | dl_table_relation.cpp | 431 void table_relation::add_table_fact(const table_fact & f) { in add_table_fact() function in datalog::table_relation
|
| H A D | rel_context.cpp | 565 rel.add_table_fact(fact);
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_context.h | 450 void add_table_fact(func_decl * pred, const table_fact & fact);
451 void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]);
|
| H A D | dl_context.cpp | 648 void context::add_table_fact(func_decl * pred, const table_fact & fact) { in add_table_fact() function in datalog::context
662 void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) { in add_table_fact() function in datalog::context
672 add_table_fact(pred, fact); in add_table_fact()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_context.h | 450 void add_table_fact(func_decl * pred, const table_fact & fact);
451 void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]);
|
| H A D | dl_context.cpp | 647 void context::add_table_fact(func_decl * pred, const table_fact & fact) { in add_table_fact() function in datalog::context
661 void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) { in add_table_fact() function in datalog::context
671 add_table_fact(pred, fact); in add_table_fact()
|
| /dports/math/z3/z3-z3-4.8.13/src/api/ |
| H A D | api_datalog.cpp | 110 void add_table_fact(func_decl* r, unsigned num_args, unsigned args[]) { in add_table_fact() function in api::fixedpoint_context
111 m_context.add_table_fact(r, num_args, args); in add_table_fact()
274 to_fixedpoint_ref(d)->add_table_fact(to_func_decl(r), num_args, args); in Z3_fixedpoint_add_fact()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
| H A D | api_datalog.cpp | 110 void add_table_fact(func_decl* r, unsigned num_args, unsigned args[]) { in add_table_fact() function in api::fixedpoint_context
111 m_context.add_table_fact(r, num_args, args); in add_table_fact()
273 to_fixedpoint_ref(d)->add_table_fact(to_func_decl(r), num_args, args); in Z3_fixedpoint_add_fact()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/fp/ |
| H A D | datalog_parser.cpp | 1408 m_context.add_table_fact(pred, fact); in parse_rel_file()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/fp/ |
| H A D | datalog_parser.cpp | 1408 m_context.add_table_fact(pred, fact); in parse_rel_file()
|