mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
|
|
||
|---|---|---|
| .. | ||
| extra_cmds | ||
| basic_cmds.cpp | ||
| basic_cmds.h | ||
| check_logic.cpp | ||
| check_logic.h | ||
| check_sat_result.h | ||
| cmd_context.cpp | ||
| cmd_context.h | ||
| cmd_context_to_goal.cpp | ||
| cmd_context_to_goal.h | ||
| cmd_util.cpp | ||
| cmd_util.h | ||
| echo_tactic.cpp | ||
| echo_tactic.h | ||
| eval_cmd.cpp | ||
| eval_cmd.h | ||
| parametric_cmd.cpp | ||
| parametric_cmd.h | ||
| pdecl.cpp | ||
| pdecl.h | ||
| progress_callback.h | ||
| README | ||
| simplify_cmd.cpp | ||
| simplify_cmd.h | ||
| solver.cpp | ||
| solver.h | ||
| strategic_solver.cpp | ||
| strategic_solver.h | ||
| tactic2solver.cpp | ||
| tactic2solver.h | ||
| tactic_cmds.cpp | ||
| tactic_cmds.h | ||
| tactic_manager.cpp | ||
| tactic_manager.h | ||
Command context provides the infrastructure for executing commands in front-ends such as SMT-LIB 2.0. It is also provides the solver abstraction to plugin solvers in this kind of front-end.