mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add tptp5 example to cmake, adding output SZS directives for Geoff

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-15 12:09:23 -07:00
parent 6f971a3a86
commit f3d657ebd1
2 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
contrib/cmake/examples/CMakeLists.txt
View file

@ -1,2 +1,3 @@
add_subdirectory(c) add_subdirectory(c)
add_subdirectory(c++) add_subdirectory(c++)
add_subdirectory(tptp)

4
examples/tptp/tptp5.cpp
View file

@ -2408,7 +2408,9 @@ static void prove_tptp() {
} }
if (g_generate_proof) { if (g_generate_proof) {
try { try {
std::cout << "SZS output start Proof\n";
display_proof(ctx, fmls, solver); display_proof(ctx, fmls, solver);
std::cout << "SZS output end Proof\n";
} }
catch (failure_ex& ex) { catch (failure_ex& ex) {
std::cerr << "Proof display could not be completed: " << ex.msg << "\n"; std::cerr << "Proof display could not be completed: " << ex.msg << "\n";
@ -2434,7 +2436,9 @@ static void prove_tptp() {
std::cout << "SZS status Satisfiable\n"; std::cout << "SZS status Satisfiable\n";
} }
if (g_generate_model) { if (g_generate_model) {
std::cout << "SZS output start Model\n";
display_model(ctx, solver.get_model()); display_model(ctx, solver.get_model());
std::cout << "SZS output end Model\n";
} }
break; break;
case z3::unknown: case z3::unknown: