mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 15:25:46 +00:00
Code Activity
z3/src/cmd_context
History
Leonardo de Moura 557cda70b0 Set :global-decls to false 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-20 08:45:31 -08:00
..
extra_cmds had to nuke mip_tactic, it was based on the smt_solver_exp (experimental), that depends on assertion_sets. This change will affect Z3's performance on QF_LIA and QF_LRA benchmarks. The new mcsat should fix that. 2012-10-24 13:58:24 -07:00
basic_cmds.cpp cleanning solver initialization, and fixing named assertion support 2012-11-02 16:35:08 -07:00
basic_cmds.h checkpoint 2012-10-21 18:32:35 -07:00
check_logic.cpp checkpoint 2012-10-21 18:32:35 -07:00
check_logic.h checkpoint 2012-10-21 18:32:35 -07:00
cmd_context.cpp Set :global-decls to false 2012-11-20 08:45:31 -08:00
cmd_context.h add option to validate result of PDR. Add PDR tactic. Add fixedpoint parsing 2012-11-17 20:47:49 +01:00
cmd_context_to_goal.cpp added support for named assertions 2012-11-02 14:00:43 -07:00
cmd_context_to_goal.h checkpoint 2012-10-21 18:32:35 -07:00
cmd_util.cpp checkpoint 2012-10-21 18:32:35 -07:00
cmd_util.h checkpoint 2012-10-21 18:32:35 -07:00
echo_tactic.cpp checkpoint 2012-10-21 18:32:35 -07:00
echo_tactic.h checkpoint 2012-10-21 18:32:35 -07:00
eval_cmd.cpp checkpoint 2012-10-21 18:32:35 -07:00
eval_cmd.h checkpoint 2012-10-21 18:32:35 -07:00
parametric_cmd.cpp checkpoint 2012-10-21 18:32:35 -07:00
parametric_cmd.h checkpoint 2012-10-21 18:32:35 -07:00
pdecl.cpp fixed bugs found in regression tests 2012-11-07 07:36:40 -08:00
pdecl.h fixed some warnings reported by clang++ 2012-11-02 17:28:27 -07:00
README checkpoint 2012-10-21 18:32:35 -07:00
simplify_cmd.cpp checkpoint 2012-10-21 18:32:35 -07:00
simplify_cmd.h checkpoint 2012-10-21 18:32:35 -07:00
tactic_cmds.cpp auto generate install_tactics procedure 2012-10-25 14:46:17 -07:00
tactic_cmds.h checkpoint 2012-10-21 18:32:35 -07:00
tactic_manager.cpp checkpoint 2012-10-21 18:32:35 -07:00
tactic_manager.h checkpoint 2012-10-21 18:32:35 -07:00

README 

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.