diff options
| -rw-r--r-- | src/api/java/CMakeLists.txt | 12 | ||||
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 78 |
2 files changed, 83 insertions, 7 deletions
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index ad4183f25..754e20bf8 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -14,15 +14,15 @@ ## # create directories -file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/io/github/cvc5/api") -set(JNI_DIR "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/jni") +file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api") +set(JNI_DIR "${CMAKE_CURRENT_BINARY_DIR}/jni") file(MAKE_DIRECTORY ${JNI_DIR}) # Generate Kind.java configure_file(genkinds.py.in genkinds.py) set(JAVA_KIND_FILE - "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/io/github/cvc5/api/Kind.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/Kind.java" ) add_custom_command( @@ -34,7 +34,7 @@ add_custom_command( "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/io/github/cvc5/api/Kind" + --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/Kind" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" @@ -76,15 +76,13 @@ set(JAVA_FILES # specify generated jni headers set(JNI_HEADERS - ${JNI_DIR}/cvc5_Solver.h + ${JNI_DIR}/io_github_cvc5_api_Solver.h ) # generate jni headers add_custom_command( OUTPUT ${JNI_HEADERS} - BYPRODUCTS - ${JNI_HEADERS} COMMAND # generate jni header files ${Java_JAVAC_EXECUTABLE} -h ${JNI_DIR} ${JAVA_FILES} -d ${JNI_DIR} diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 2eb3d8d1d..4013a226c 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1077,6 +1077,84 @@ bool AletheProofPostprocessCallback::update(Node res, { return addAletheStepFromOr(AletheRule::ITE_POS1, res, children, {}, *cdp); } + case PfRule::CNF_ITE_NEG1: + { + return addAletheStepFromOr(AletheRule::ITE_NEG2, res, children, {}, *cdp); + } + case PfRule::CNF_ITE_NEG2: + { + return addAletheStepFromOr(AletheRule::ITE_NEG1, res, children, {}, *cdp); + } + // ======== CNF ITE Pos version 3 + // + // ----- ITE_POS1 ----- ITE_POS2 + // VP1 VP2 + // ------------------------------- RESOLUTION + // VP3 + // ------------------------------- REORDER + // VP4 + // ------------------------------- DUPLICATED_LITERALS + // (cl (not (ite C F1 F2)) F1 F2) + // + // VP1: (cl (not (ite C F1 F2)) C F2) + // VP2: (cl (not (ite C F1 F2)) (not C) F1) + // VP3: (cl (not (ite C F1 F2)) F2 (not (ite C F1 F2)) F1) + // VP4: (cl (not (ite C F1 F2)) (not (ite C F1 F2)) F1 F2) + // + // * the corresponding proof node is (or (not (ite C F1 F2)) F1 F2) + case PfRule::CNF_ITE_POS3: + { + Node vp1 = nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0], res[2]}); + Node vp2 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0].notNode(), res[1]}); + Node vp3 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[2], res[0], res[1]}); + Node vp4 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[0], res[1], res[2]}); + + return addAletheStep(AletheRule::ITE_POS1, vp1, vp1, {}, {}, *cdp) + && addAletheStep(AletheRule::ITE_POS2, vp2, vp2, {}, {}, *cdp) + && addAletheStep( + AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) + && addAletheStep(AletheRule::REORDER, vp4, vp4, {vp3}, {}, *cdp) + && addAletheStepFromOr( + AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); + } + // ======== CNF ITE Neg version 3 + // + // ----- ITE_NEG1 ----- ITE_NEG2 + // VP1 VP2 + // ------------------------------- RESOLUTION + // VP3 + // ------------------------------- REORDER + // VP4 + // ------------------------------- DUPLICATED_LITERALS + // (cl (ite C F1 F2) C (not F2)) + // + // VP1: (cl (ite C F1 F2) C (not F2)) + // VP2: (cl (ite C F1 F2) (not C) (not F1)) + // VP3: (cl (ite C F1 F2) (not F2) (ite C F1 F2) (not F1)) + // VP4: (cl (ite C F1 F2) (ite C F1 F2) (not F1) (not F2)) + // + // * the corresponding proof node is (or (ite C F1 F2) C (not F2)) + case PfRule::CNF_ITE_NEG3: + { + Node vp1 = nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0], res[2]}); + Node vp2 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], args[0][0].notNode(), res[1]}); + Node vp3 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[2], res[0], res[1]}); + Node vp4 = + nm->mkNode(kind::SEXPR, {d_cl, res[0], res[0], res[1], res[2]}); + + return addAletheStep(AletheRule::ITE_NEG1, vp1, vp1, {}, {}, *cdp) + && addAletheStep(AletheRule::ITE_NEG2, vp2, vp2, {}, {}, *cdp) + && addAletheStep( + AletheRule::RESOLUTION, vp3, vp3, {vp1, vp2}, {}, *cdp) + && addAletheStep(AletheRule::REORDER, vp4, vp4, {vp3}, {}, *cdp) + && addAletheStepFromOr( + AletheRule::DUPLICATED_LITERALS, res, {vp4}, {}, *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |