mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity
z3/src/cmd_context
History
Nikolaj Bjorner 7c743b3d16 add direct FromFile method to solvers so that model transformations are loaded along with assertions. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-02 09:25:18 -05:00
..
extra_cmds add feature to display benchmark in format seen by SAT solver 2017-09-21 18:32:46 -05:00
basic_cmds.cpp add parameter to specify the file into which dot proofs are to be printed 2017-10-24 10:16:56 +02:00
basic_cmds.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
check_logic.cpp add QF_DT 2017-09-17 01:39:39 +02:00
check_logic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
CMakeLists.txt [CMake] Fix dependencies for generating gparams_register_modules.cpp. 2017-06-21 23:56:46 +01:00
cmd_context.cpp added facility to persist model transformations 2017-11-02 00:05:52 -05:00
cmd_context.h add direct FromFile method to solvers so that model transformations are loaded along with assertions. 2017-11-02 09:25:18 -05:00
cmd_context_to_goal.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
cmd_context_to_goal.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
cmd_util.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
cmd_util.h Fix spelling errors 2016-07-09 11:46:43 +02:00
context_params.cpp add parameter to specify the file into which dot proofs are to be printed 2017-10-24 10:16:56 +02:00
context_params.h add parameter to specify the file into which dot proofs are to be printed 2017-10-24 10:16:56 +02:00
echo_tactic.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
echo_tactic.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
eval_cmd.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
eval_cmd.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
interpolant_cmds.cpp streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223 2017-10-23 21:16:46 -07:00
interpolant_cmds.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
parametric_cmd.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
parametric_cmd.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
pdecl.cpp remove V2 reference 2017-09-10 15:32:53 +03:00
pdecl.h remove V2 reference 2017-09-10 15:32:53 +03:00
README remove hassel table from unstable: does not compile under other plantforms 2013-05-31 17:48:19 -07:00
simplify_cmd.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
simplify_cmd.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
tactic_cmds.cpp model-add/del 2017-11-01 22:32:22 -05:00
tactic_cmds.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
tactic_manager.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
tactic_manager.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -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.