Searched refs:PGM_DISABLED (Results 1 – 12 of 12) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | scoped_proof.h | 44 scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} in scoped_no_proof()
|
| H A D | ast.h | 1412 PGM_DISABLED, enumerator
1507 …ast_manager(proof_gen_mode = PGM_DISABLED, char const * trace_file = nullptr, bool is_format_manag…
2200 bool proofs_enabled() const { return m_proof_mode != PGM_DISABLED; } in proofs_enabled()
2201 bool proofs_disabled() const { return m_proof_mode == PGM_DISABLED; } in proofs_disabled()
|
| H A D | ast.cpp | 1316 m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true); in ast_manager()
1333 m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true); in ast_manager()
1344 m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode), in ast_manager()
1349 m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true); in ast_manager()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | scoped_proof.h | 44 scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} in scoped_no_proof()
|
| H A D | ast.h | 1462 PGM_DISABLED, enumerator
1563 …ast_manager(proof_gen_mode = PGM_DISABLED, char const * trace_file = nullptr, bool is_format_manag…
2260 bool proofs_enabled() const { return m_proof_mode != PGM_DISABLED; } in proofs_enabled()
2261 bool proofs_disabled() const { return m_proof_mode == PGM_DISABLED; } in proofs_disabled()
|
| H A D | ast.cpp | 1394 m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true); in ast_manager()
1411 m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true); in ast_manager()
1422 m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode), in ast_manager()
1427 m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true); in ast_manager()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/params/ |
| H A D | context_params.cpp | 196 m_proof ? PGM_ENABLED : PGM_DISABLED, in mk_ast_manager()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_rule.cpp | 145 scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); in ScopedUpdatesClearer()
347 scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); in ScopedUpdatesClearer()
|
| H A D | dl_context.cpp | 468 scoped_proof_mode _scp(m, generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); in flush_add_rules()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_rule.cpp | 145 scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); in mk_rule()
347 scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); in mk_query()
|
| H A D | dl_context.cpp | 469 scoped_proof_mode _scp(m, generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); in flush_add_rules()
|
| /dports/math/z3/z3-z3-4.8.13/src/cmd_context/ |
| H A D | cmd_context.cpp | 317 m_proof ? PGM_ENABLED : PGM_DISABLED, in mk_ast_manager()
|