include:
- name: production
- config: production --all-bindings --lfsc --editline --poly --symfpu
+ config: production --all-bindings --editline --poly --symfpu
cache-key: production
python-bindings: true
check-examples: true
run_regression_args: --no-check-unsat-cores --no-check-proofs
- name: production-dbg
- config: production --assertions --tracing --unit-testing --symfpu --lfsc --editline
+ config: production --assertions --tracing --unit-testing --symfpu --editline
cache-key: dbg
os: ubuntu-latest
exclude_regress: 3-4
make -j2
ctest -j2 --output-on-failure
working-directory: examples
-
if(CRYPTOMINISAT_DIR)
list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}")
endif()
-if(DRAT2ER_DIR)
- list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}")
-endif()
if(GLPK_DIR)
list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
endif()
if(KISSAT_DIR)
list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}")
endif()
-if(LFSC_DIR)
- list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
-endif()
if(POLY_DIR)
list(APPEND CMAKE_PREFIX_PATH "${POLY_DIR}")
endif()
cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
cvc4_option(ENABLE_DUMPING "Enable dumping")
cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output")
-cvc4_option(ENABLE_PROOFS "Enable proof support")
cvc4_option(ENABLE_STATISTICS "Enable statistics")
cvc4_option(ENABLE_TRACING "Enable tracing")
cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
cvc4_option(USE_EDITLINE "Use Editline for better interactive support")
# >> 2-valued: ON OFF
# > for options where we don't need to detect if set by user (default: OFF)
-option(USE_DRAT2ER "Include drat2er for making eager BV proofs")
-option(USE_LFSC "Use LFSC proof checker")
option(USE_POLY "Use LibPoly for polynomial arithmetic")
option(USE_SYMFPU "Use SymFPU for floating point support")
option(USE_PYTHON2 "Force Python 2 (deprecated)")
set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory")
set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory")
set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
-set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory")
set(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
set(GMP_DIR "" CACHE STRING "Set GMP install directory")
set(KISSAT_DIR "" CACHE STRING "Set Kissat install directory")
-set(LFSC_DIR "" CACHE STRING "Set LFSC install directory")
set(POLY_DIR "" CACHE STRING "Set LibPoly install directory")
set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory")
add_check_c_cxx_flag("-pg")
endif()
-if(ENABLE_PROOFS)
- add_definitions(-DCVC4_PROOF)
-endif()
-
if(ENABLE_TRACING)
add_definitions(-DCVC4_TRACING)
endif()
add_definitions(-DCVC4_USE_CRYPTOMINISAT)
endif()
-if(USE_DRAT2ER)
- find_package(Drat2Er REQUIRED)
- add_definitions(-DCVC4_USE_DRAT2ER)
-endif()
-
if(USE_GLPK)
set(GPL_LIBS "${GPL_LIBS} glpk")
find_package(GLPK REQUIRED)
add_definitions(-DCVC4_USE_KISSAT)
endif()
-if(USE_LFSC)
- find_package(LFSC REQUIRED)
- add_definitions(-DCVC4_USE_LFSC)
-endif()
-
if(USE_POLY)
find_package(Poly REQUIRED)
add_definitions(-DCVC4_USE_POLY)
#-----------------------------------------------------------------------------#
# Add subdirectories
-# signatures needs to come before src since it adds source files to libcvc4.
-if(ENABLE_PROOFS)
- add_subdirectory(proofs/signatures)
-endif()
-
add_subdirectory(doc)
add_subdirectory(src)
add_subdirectory(test)
# libraries from deps/install/lib, we need to be cautious. Changing these
# shared libraries from deps/install/lib most probably breaks the binary.
# We only allow such an installation for custom installation prefixes
-# (in the assumption that only reasonably experienced users use this and
+# (in the assumption that only reasonably experienced users use this and
# also that custom installation prefixes are not used for longer periods of
# time anyway). Also, we print a big warning with further instructions.
if(NOT ENABLE_STATIC_BINARY)
print_config("ABC :" USE_ABC)
print_config("CaDiCaL :" USE_CADICAL)
print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
-print_config("drat2er :" USE_DRAT2ER)
print_config("GLPK :" USE_GLPK)
print_config("Kissat :" USE_KISSAT)
-print_config("LFSC :" USE_LFSC)
print_config("LibPoly :" USE_POLY)
message("")
print_config("Build libcvc4 only :" BUILD_LIB_ONLY)
if(CRYPTOMINISAT_DIR)
message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
endif()
-if(DRAT2ER_DIR)
- message("DRAT2ER dir : ${DRAT2ER_DIR}")
-endif()
if(GLPK_DIR)
message("GLPK dir : ${GLPK_DIR}")
endif()
if(KISSAT_DIR)
message("KISSAT dir : ${KISSAT_DIR}")
endif()
-if(LFSC_DIR)
- message("LFSC dir : ${LFSC_DIR}")
-endif()
if(POLY_DIR)
message("LibPoly dir : ${POLY_DIR}")
endif()
ABC (https://bitbucket.org/alanmi/abc)
CaDiCaL (https://github.com/arminbiere/cadical)
CryptoMiniSat (https://github.com/msoos/cryptominisat)
- LFSC checker (https://github.com/CVC4/LFSC)
LibPoly (https://github.com/SRI-CSL/libpoly)
libedit (https://thrysoee.dk/editline)
version of GLPK, the GNU Linear Programming Kit, available here:
https://github.com/timothy-king/glpk-cut-log
-
## Build dependencies
-The following tools and libraries are required to build and run CVC4.
+The following tools and libraries are required to build and run CVC4.
Versions given are minimum versions; more recent versions should be
compatible.
is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
of bit-vector operations.
It is required for supporting the theory of floating-point numbers and
-can be installed using the `contrib/get-symfpu` script.
+can be installed using the `contrib/get-symfpu` script.
Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
### CaDiCaL (Optional SAT solver)
[CaDiCaL](https://github.com/arminbiere/cadical)
is a SAT solver that can be used for solving non-incremental bit-vector
problems with eager bit-blasting. This dependency may improve performance.
-It can be installed using the `contrib/get-cadical script`.
+It can be installed using the `contrib/get-cadical script`.
Configure CVC4 with `configure.sh --cadical` to build with this dependency.
### CryptoMiniSat (Optional SAT solver)
[CryptoMinisat](https://github.com/msoos/cryptominisat)
is a SAT solver that can be used for solving bit-vector problems with eager
bit-blasting. This dependency may improve performance.
-It can be installed using the `contrib/get-cryptominisat` script.
+It can be installed using the `contrib/get-cryptominisat` script.
Configure CVC4 with `configure.sh --cryptominisat` to build with this
dependency.
[Kissat](https://github.com/arminbiere/kissat)
is a SAT solver that can be used for solving bit-vector problems with eager
bit-blasting. This dependency may improve performance.
-It can be installed using the `contrib/get-kissat` script.
+It can be installed using the `contrib/get-kissat` script.
Configure CVC4 with `configure.sh --kissat` to build with this
dependency.
-### LFSC (The LFSC Proof Checker)
-
-[LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally
-with --check-proofs. It can be installed using the `contrib/get-lfsc` script.
-Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
-
### LibPoly (Optional polynomial library)
[LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning.
[CLN](http://www.ginac.de/CLN)
is an alternative multiprecision arithmetic package that may offer better
-performance and memory footprint than GMP.
+performance and memory footprint than GMP.
Configure CVC4 with `configure.sh --cln` to build with this dependency.
Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
Note that the only installation option is manual installation via this script.
-CVC4 is no longer compatible with the main GLPK library.
+CVC4 is no longer compatible with the main GLPK library.
Configure CVC4 with `configure.sh --glpk` to build with this dependency.
Note that GLPK and glpk-cut-log are covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
bit-vector solver. When enabled, the bit-blasted formula is encoded into
and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
-ABC can be installed using the `contrib/get-abc` script.
+ABC can be installed using the `contrib/get-abc` script.
Configure CVC4 with `configure.sh --abc` to build with this dependency.
### Editline library (Improved Interactive Experience)
### Google Test Unit Testing Framework (Unit Tests)
[Google Test](https://github.com/google/googletest) is required to optionally
-run CVC4's unit tests (included with the distribution).
+run CVC4's unit tests (included with the distribution).
See [Testing CVC4](#Testing-CVC4) below for more details.
## Language bindings
All system test binaries are built into `<build_dir>/bin/test/system`.
We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
-as test target name.
+as test target name.
make ouroborous # build test/api/ouroborous.cpp
ctest -R ouroborous # run all tests that match '*ouroborous*'
All unit test binaries are built into `<build_dir>/bin/test/unit`.
We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
-`test/unit/<subdir>`) as test target name.
+`test/unit/<subdir>`) as test target name.
make map_util_black # build test/unit/base/map_util_black.cpp
ctest -R map_util_black # run all tests that match '*map_util_black*'
### Testing Regression Tests
We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
-in level `N` in `test/regress/regressN/<subdir>`) as test target name.
+in level `N` in `test/regress/regressN/<subdir>`) as test target name.
ctest -L regress # run all regression tests
ctest -L regress0 # run all regression tests in level 0
All custom test targets build and run a preconfigured set of tests.
-- `make check [-jN] [ARGS=-jN]`
+- `make check [-jN] [ARGS=-jN]`
The default build-and-test target for CVC4, builds and runs all examples,
all system and unit tests, and regression tests from levels 0 to 2.
-- `make systemtests [-jN] [ARGS=-jN]`
+- `make systemtests [-jN] [ARGS=-jN]`
Build and run all system tests.
-- `make units [-jN] [ARGS=-jN]`
+- `make units [-jN] [ARGS=-jN]`
Build and run all unit tests.
-- `make regress [-jN] [ARGS=-jN]`
+- `make regress [-jN] [ARGS=-jN]`
Build and run regression tests from levels 0 to 2.
-- `make runexamples [-jN] [ARGS=-jN]`
+- `make runexamples [-jN] [ARGS=-jN]`
Build and run all examples.
-- `make coverage [-jN] [ARGS=-jN]`
+- `make coverage [-jN] [ARGS=-jN]`
Build and run all tests (system and unit tests, regression tests level 0-4)
with gcov to determine code coverage.
--static build static libraries and binaries [default=no]
--static-binary statically link against system libraries
(must be disabled for static macOS builds) [default=yes]
- --proofs support for proof generation
--debug-symbols include debug symbols
--valgrind Valgrind instrumentation
--debug-context-mm use the debug context memory manager
--abc use the ABC AIG library
--cadical use the CaDiCaL SAT solver
--cryptominisat use the CryptoMiniSat SAT solver
- --drat2er use drat2er (required for eager BV proofs)
--kissat use the Kissat SAT solver
- --lfsc use the LFSC proof checker
--poly use the LibPoly library
--symfpu use SymFPU for floating point solver
--editline support the editline library
--antlr-dir=PATH path to ANTLR C headers and libraries
--cadical-dir=PATH path to top level of CaDiCaL source tree
--cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
- --drat2er-dir=PATH path to the top level of the drat2er installation
--glpk-dir=PATH path to top level of GLPK installation
--gmp-dir=PATH path to top level of GMP installation
--kissat-dir=PATH path to top level of Kissat source tree
- --lfsc-dir=PATH path to top level of LFSC source tree
--poly-dir=PATH path to top level of LibPoly source tree
--symfpu-dir=PATH path to top level of SymFPU source tree
cryptominisat=default
debug_context_mm=default
debug_symbols=default
-drat2er=default
dumping=default
glpk=default
gpl=default
kissat=default
-lfsc=default
poly=default
muzzle=default
ninja=default
profiling=default
-proofs=default
python2=default
python_bindings=default
java_bindings=default
antlr_dir=default
cadical_dir=default
cryptominisat_dir=default
-drat2er_dir=default
glpk_dir=default
gmp_dir=default
kissat_dir=default
-lfsc_dir=default
poly_dir=default
symfpu_dir=default
--debug-context-mm) debug_context_mm=ON;;
--no-debug-context-mm) debug_context_mm=OFF;;
- --drat2er) drat2er=ON;;
- --no-drat2er) drat2er=OFF;;
-
--dumping) dumping=ON;;
--no-dumping) dumping=OFF;;
--glpk) glpk=ON;;
--no-glpk) glpk=OFF;;
- --lfsc) lfsc=ON;;
- --no-lfsc) lfsc=OFF;;
-
--poly) poly=ON;;
--no-poly) poly=OFF;;
--muzzle) muzzle=ON;;
--no-muzzle) muzzle=OFF;;
- --proofs) proofs=ON;;
- --no-proofs) proofs=OFF;;
-
--static) shared=OFF; static_binary=ON;;
--no-static) shared=ON;;
--cryptominisat-dir) die "missing argument to $1 (try -h)" ;;
--cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;;
- --drat2er-dir) die "missing argument to $1 (try -h)" ;;
- --drat2er-dir=*) drat2er_dir=${1##*=} ;;
-
--glpk-dir) die "missing argument to $1 (try -h)" ;;
--glpk-dir=*) glpk_dir=${1##*=} ;;
--kissat-dir) die "missing argument to $1 (try -h)" ;;
--kissat-dir=*) kissat_dir=${1##*=} ;;
- --lfsc-dir) die "missing argument to $1 (try -h)" ;;
- --lfsc-dir=*) lfsc_dir=${1##*=} ;;
-
--poly-dir) die "missing argument to $1 (try -h)" ;;
--poly-dir=*) poly_dir=${1##*=} ;;
[ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
[ $muzzle != default ] \
&& cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $proofs != default ] \
- && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
[ $shared != default ] \
&& cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
[ $static_binary != default ] \
&& cmake_opts="$cmake_opts -DUSE_CLN=$cln"
[ $cryptominisat != default ] \
&& cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
-[ $drat2er != default ] \
- && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er"
[ $glpk != default ] \
&& cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
[ $kissat != default ] \
&& cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
-[ $lfsc != default ] \
- && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc"
[ $poly != default ] \
&& cmake_opts="$cmake_opts -DUSE_POLY=$poly"
[ $symfpu != default ] \
&& cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir"
[ "$cryptominisat_dir" != default ] \
&& cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
-[ "$drat2er_dir" != default ] \
- && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
[ "$glpk_dir" != default ] \
&& cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
[ "$gmp_dir" != default ] \
&& cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir"
[ "$kissat_dir" != default ] \
&& cmake_opts="$cmake_opts -DKISSAT=$kissat_dir"
-[ "$lfsc_dir" != default ] \
- && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
[ "$poly_dir" != default ] \
&& cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir"
[ "$symfpu_dir" != default ] \
target_link_libraries(cvc4 ${Kissat_LIBRARIES})
target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR})
endif()
-if(USE_DRAT2ER)
- target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
-endif()
if(USE_GLPK)
target_link_libraries(cvc4 ${GLPK_LIBRARIES})
target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
endif()
-if(USE_LFSC)
- target_link_libraries(cvc4 ${LFSC_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
-endif()
if(USE_POLY)
target_link_libraries(cvc4 ${POLY_LIBRARIES})
target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
return IS_ASSERTIONS_BUILD;
}
-bool Configuration::isProofBuild() {
- return IS_PROOFS_BUILD;
-}
-
bool Configuration::isCoverageBuild() {
return IS_COVERAGE_BUILD;
}
<< "See licenses/antlr3-LICENSE for copyright and licensing information."
<< "\n\n";
- if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc()
- || Configuration::isBuiltWithCadical()
+ if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
|| Configuration::isBuiltWithCryptominisat()
|| Configuration::isBuiltWithKissat()
|| Configuration::isBuiltWithSymFPU()
<< " See http://bitbucket.org/alanmi/abc for copyright and\n"
<< " licensing information.\n\n";
}
- if (Configuration::isBuiltWithLfsc()) {
- ss << " LFSC Proof Checker\n"
- << " See http://github.com/CVC4/LFSC for copyright and\n"
- << " licensing information.\n\n";
- }
if (Configuration::isBuiltWithCadical())
{
ss << " CaDiCaL - Simplified Satisfiability Solver\n"
bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
-bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; }
-
bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
-bool Configuration::isBuiltWithLfsc() {
- return IS_LFSC_BUILD;
-}
-
bool Configuration::isBuiltWithPoly()
{
return IS_POLY_BUILD;
static bool isAssertionBuild();
- static bool isProofBuild();
-
static bool isCoverageBuild();
static bool isProfilingBuild();
static bool isBuiltWithKissat();
- static bool isBuiltWithDrat2Er();
-
static bool isBuiltWithEditline();
- static bool isBuiltWithLfsc();
-
static bool isBuiltWithPoly();
static bool isBuiltWithSymFPU();
# define IS_ASSERTIONS_BUILD false
#endif /* CVC4_ASSERTIONS */
-#ifdef CVC4_PROOF
-# define IS_PROOFS_BUILD true
-#else /* CVC4_PROOF */
-# define IS_PROOFS_BUILD false
-#endif /* CVC4_PROOF */
-
#ifdef CVC4_COVERAGE
# define IS_COVERAGE_BUILD true
#else /* CVC4_COVERAGE */
# define IS_CRYPTOMINISAT_BUILD false
#endif /* CVC4_USE_CRYPTOMINISAT */
-#if CVC4_USE_DRAT2ER
-# define IS_DRAT2ER_BUILD true
-#else /* CVC4_USE_DRAT2ER */
-# define IS_DRAT2ER_BUILD false
-#endif /* CVC4_USE_DRAT2ER */
-
#if CVC4_USE_KISSAT
#define IS_KISSAT_BUILD true
#else /* CVC4_USE_KISSAT */
#define IS_KISSAT_BUILD false
#endif /* CVC4_USE_KISSAT */
-#if CVC4_USE_LFSC
-#define IS_LFSC_BUILD true
-#else /* CVC4_USE_LFSC */
-#define IS_LFSC_BUILD false
-#endif /* CVC4_USE_LFSC */
-
#if CVC4_USE_POLY
#define IS_POLY_BUILD true
#else /* CVC4_USE_POLY */
options::interactiveMode.set(value);
}
-void OptionsHandler::proofEnabledBuild(std::string option, bool value)
-{
-#ifdef CVC4_PROOF
- if (value && options::bitblastMode() == options::BitblastMode::EAGER
- && options::bvSatSolver() != options::SatSolverMode::MINISAT
- && options::bvSatSolver() != options::SatSolverMode::CRYPTOMINISAT)
- {
- throw OptionException(
- "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
- }
-#else
- if(value) {
- std::stringstream ss;
- ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
- throw OptionException(ss.str());
- }
-#endif /* CVC4_PROOF */
-}
-
-void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
-#ifndef CVC4_USE_LFSC
- if (value) {
- std::stringstream ss;
- ss << "option `" << option << "' requires a build of CVC4 with integrated "
- "LFSC; this binary was not built with LFSC";
- throw OptionException(ss.str());
- }
-#endif /* CVC4_USE_LFSC */
-}
-
void OptionsHandler::statsEnabledBuild(std::string option, bool value)
{
#ifndef CVC4_STATISTICS_ON
} else {
print_config_cond("scm", false);
}
-
+
std::cout << std::endl;
std::stringstream ss;
<< Configuration::getVersionMinor() << "."
<< Configuration::getVersionRelease();
print_config("library", ss.str());
-
+
std::cout << std::endl;
print_config_cond("debug code", Configuration::isDebugBuild());
print_config_cond("dumping", Configuration::isDumpingBuild());
print_config_cond("muzzled", Configuration::isMuzzledBuild());
print_config_cond("assertions", Configuration::isAssertionBuild());
- print_config_cond("proof", Configuration::isProofBuild());
print_config_cond("coverage", Configuration::isCoverageBuild());
print_config_cond("profiling", Configuration::isProfilingBuild());
print_config_cond("asan", Configuration::isAsanBuild());
print_config_cond("ubsan", Configuration::isUbsanBuild());
print_config_cond("tsan", Configuration::isTsanBuild());
print_config_cond("competition", Configuration::isCompetitionBuild());
-
+
std::cout << std::endl;
-
+
print_config_cond("abc", Configuration::isBuiltWithAbc());
print_config_cond("cln", Configuration::isBuiltWithCln());
print_config_cond("glpk", Configuration::isBuiltWithGlpk());
print_config_cond("cadical", Configuration::isBuiltWithCadical());
print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
- print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
print_config_cond("gmp", Configuration::isBuiltWithGmp());
print_config_cond("kissat", Configuration::isBuiltWithKissat());
- print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
print_config_cond("poly", Configuration::isBuiltWithPoly());
print_config_cond("editline", Configuration::isBuiltWithEditline());
print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
-
+
exit(0);
}
* initialization.
*/
void setProduceAssertions(std::string option, bool value);
- void proofEnabledBuild(std::string option, bool value);
- void LFSCEnabledBuild(std::string option, bool value);
void statsEnabledBuild(std::string option, bool value);
category = "regular"
long = "produce-unsat-cores"
type = "bool"
- predicates = ["proofEnabledBuild"]
help = "turn on unsat core generation"
[[option]]
long = "produce-unsat-assumptions"
type = "bool"
default = "false"
- predicates = ["proofEnabledBuild"]
read_only = true
help = "turn on unsat assumptions generation"
// d_proofManager must be created before Options has been finished
// being parsed from the input file. Because of this, we cannot trust
// that options::unsatCores() is set correctly yet.
-#ifdef CVC4_PROOF
d_proofManager.reset(new ProofManager(getUserContext()));
-#endif
d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
}
// Note: the proof manager must be destroyed before the theory engine.
// Because the destruction of the proofs depends on contexts owned be the
// theory solvers.
-#ifdef CVC4_PROOF
d_proofManager.reset(nullptr);
-#endif
d_pfManager.reset(nullptr);
d_ucManager.reset(nullptr);
UnsatCore SmtEngine::getUnsatCoreInternal()
{
-#if IS_PROOFS_BUILD
if (!options::unsatCores())
{
throw ModalException(
std::vector<Node> core;
d_ucManager->getUnsatCore(pfn, *d_asserts, core);
return UnsatCore(core);
-#else /* IS_PROOFS_BUILD */
- throw ModalException(
- "This build of CVC4 doesn't have proof support (required for unsat "
- "cores).");
-#endif /* IS_PROOFS_BUILD */
}
void SmtEngine::checkUnsatCore() {
{
getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
}
-#if IS_PROOFS_BUILD
if (!options::produceProofs())
{
throw ModalException("Cannot get a proof when proof option is off.");
std::ostringstream ss;
d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
return ss.str();
-#else /* IS_PROOFS_BUILD */
- throw ModalException("This build of CVC4 doesn't have proof support.");
-#endif /* IS_PROOFS_BUILD */
}
void SmtEngine::printInstantiations( std::ostream& out ) {
bool smtEngineInScope() { return s_smtEngine_current != NULL; }
ProofManager* currentProofManager() {
-#if IS_PROOFS_BUILD
Assert(s_smtEngine_current != NULL);
return s_smtEngine_current->getProofManager();
-#else /* IS_PROOFS_BUILD */
- InternalError()
- << "proofs/unsat cores are not on, but ProofManager requested";
- return NULL;
-#endif /* IS_PROOFS_BUILD */
}
ResourceManager* currentResourceManager()
add_subdirectory(java)
endif()
endif()
-
-if(LFSC_BINARY)
- add_subdirectory(signatures)
-endif()
-; REQUIRES: proof
; COMMAND-LINE: --produce-unsat-cores
; EXPECT: sat
(set-logic QF_AX)
; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
; REQUIRES: cryptominisat
-; REQUIRES: drat2er
; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
; EXPECT: unsat
(set-logic QF_UFBV)
-; REQUIRES: proof
; EXPECT: sat
(set-logic QF_UFBV)
(set-option :produce-unsat-cores true)
-; REQUIRES: proof
; EXPECT: sat
(set-logic ABV)
(set-option :check-unsat-cores true)
-; REQUIRES: proof
; EXPECT: sat
(set-logic QF_UFBV)
(set-option :check-unsat-cores true)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
-(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110)))
+(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110)))
(assert (or v0 v8))
(check-sat)
; REQUIRES: cryptominisat
-; REQUIRES: drat2er
; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
; EXPECT: unsat
(set-option :incremental false)
-; REQUIRES: proof
; COMMAND-LINE: --dump-unsat-cores-full
; EXPECT: unsat
; EXPECT: (
-; REQUIRES: proof
; COMMAND-LINE: --produce-unsat-cores --incremental
; EXPECT: sat
-; REQUIRES: proof
; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
; EXPECT: unsat
; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)))
-; REQUIRES: proof
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
-; REQUIRES: proof
; COMMAND-LINE: --produce-abducts
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
-; REQUIRES: proof
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
-; REQUIRES: proof
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
-; REQUIRES: proof
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
-; REQUIRES: proof
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
## directory for licensing information.
##
"""
-Usage:
-
- run_regression.py [--enable-proof] [--with-lfsc] [--dump]
- [--use-skip-return-code] [wrapper] cvc4-binary
- [benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p]
-
Runs benchmark and checks for correct exit status and output.
"""
cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary)
- # Disable proof and unsat core checks if CVC4 was not compiled with proofs.
- if 'proof' not in cvc4_features:
- check_unsat_cores = False
- check_proofs = False
-
basic_command_line_args = []
benchmark_basename = os.path.basename(benchmark_path)
target_link_libraries(${name} main-test)
target_link_libraries(${name} GTest::GTest)
target_link_libraries(${name} GTest::Main)
- if(USE_LFSC)
- # We don't link against LFSC, because CVC4 is already linked against it.
- target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
- endif()
if(USE_POLY)
# We don't link against libpoly, because CVC4 is already linked against it.
target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
{
-#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "false");
d_solver.checkSatAssuming(d_solver.mkFalse());
ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
-#endif
}
TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
{
-#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "true");
d_solver.setOption("produce-unsat-assumptions", "false");
d_solver.checkSatAssuming(d_solver.mkFalse());
ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
-#endif
}
TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
{
-#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "true");
d_solver.setOption("produce-unsat-assumptions", "true");
d_solver.checkSatAssuming(d_solver.mkFalse());
ASSERT_NO_THROW(d_solver.getUnsatAssumptions());
d_solver.checkSatAssuming(d_solver.mkTrue());
ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
-#endif
}
TEST_F(TestApiBlackSolver, getUnsatCore1)
{
-#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "false");
d_solver.assertFormula(d_solver.mkFalse());
d_solver.checkSat();
ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
-#endif
}
TEST_F(TestApiBlackSolver, getUnsatCore2)
{
-#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "false");
d_solver.setOption("produce-unsat-cores", "false");
d_solver.assertFormula(d_solver.mkFalse());
d_solver.checkSat();
ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
-#endif
}
TEST_F(TestApiBlackSolver, getUnsatCore3)
{
-#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "true");
d_solver.setOption("produce-unsat-cores", "true");
{
d_solver.assertFormula(t);
}
- Result res = d_solver.checkSat();
+ CVC4::api::Result res = d_solver.checkSat();
ASSERT_TRUE(res.isUnsat());
-#endif
}
TEST_F(TestApiBlackSolver, getValue1)
projects / cvc5.git / commitdiff