diff options
Diffstat (limited to 'cryptominisat5/cryptominisat-5.6.3/tests/cnf-files')
14 files changed, 280 insertions, 0 deletions
diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/CMakeLists.txt b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/CMakeLists.txt new file mode 100644 index 000000000..1aa3048e5 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/CMakeLists.txt @@ -0,0 +1,47 @@ +# Copyright (c) 2017, Mate Soos +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in +# all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +# THE SOFTWARE. + +# Create llvm-lit configuration file +configure_file(lit.site.cfg.in lit.site.cfg.in2 @ONLY) + +if (MSVC) + file(GENERATE + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/$<CONFIG>/lit.site.cfg + INPUT ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg.in2) + + + # Make sure this test-suite runs when "test" is target + add_test(NAME CNF + COMMAND ${LIT_TOOL} ${LIT_ARGS} . + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/$<CONFIG>/" + ) +else() + file(GENERATE + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg + INPUT ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg.in2) + + + # Make sure this test-suite runs when "test" is target + add_test(NAME CNF + COMMAND ${LIT_TOOL} ${LIT_ARGS} . + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" + ) +endif() + diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-1.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-1.cnf new file mode 100644 index 000000000..0ea82049d --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-1.cnf @@ -0,0 +1,4 @@ +c RUN: %solver --onlyindep --indep 1 --presimp 1 --varelim 1 --verb=0 %s | %OutputCheck %s +1 2 3 0 +4 5 6 0 +c CHECK: ^v .*1 diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-2.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-2.cnf new file mode 100644 index 000000000..7606969db --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-2.cnf @@ -0,0 +1,6 @@ +c RUN: %solver --verb=0 %s | %OutputCheck %s +c ind 1 0 +1 2 3 0 +2 0 +c CHECK: Independent .*1 +c CHECK: ^s SATISFIABLE$ diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-3.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-3.cnf new file mode 100644 index 000000000..c403c2d6d --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-3.cnf @@ -0,0 +1,4 @@ +c RUN: %solver --onlyindep --indep 1 --presimp 1 --varelim 1 --verb=0 %s | %OutputCheck %s +1 2 3 0 +4 5 6 0 +c CHECK-NOT: ^v .*4 diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars.cnf new file mode 100644 index 000000000..d4e0609f6 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars.cnf @@ -0,0 +1,10 @@ +c RUN: %solver --maxsol 20 --verb=0 %s | %OutputCheck %s +c ind 1 0 +1 2 3 0 +-1 3 0 +-1 2 0 +2 3 0 +-2 -3 0 +c CHECK: ^s SATISFIABLE$ +c CHECK-NOT: ^s SATISFIABLE$ +c CHECK: UNSATISFIABLE diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars_2.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars_2.cnf new file mode 100644 index 000000000..715211ef3 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars_2.cnf @@ -0,0 +1,11 @@ +c RUN: %solver --maxsol 20 --verb=0 %s | %OutputCheck %s +c ind 1 2 3 0 +1 2 3 0 +-1 3 0 +-1 2 0 +2 3 0 +-2 -3 0 +c CHECK: ^s SATISFIABLE$ +c CHECK: ^s SATISFIABLE$ +c CHECK-NOT: ^s SATISFIABLE$ +c CHECK: UNSATISFIABLE diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.cfg b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.cfg new file mode 100644 index 000000000..edbfc606e --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.cfg @@ -0,0 +1,144 @@ +# -*- Python -*- + +# Configuration file for the 'lit' test runner. + +import os +import sys +import re +import platform + +import lit.util +import lit.formats + +# name: The name of this test suite. +config.name = 'cryptominisat cnf-files' + +# Choose between lit's internal shell pipeline runner and a real shell. If +# LIT_USE_INTERNAL_SHELL is in the environment, we use that as an override. +use_lit_shell = os.environ.get("LIT_USE_INTERNAL_SHELL") +if use_lit_shell: + # 0 is external, "" is default, and everything else is internal. + execute_external = (use_lit_shell == "0") +else: + # Otherwise we default to internal on Windows and external elsewhere, as + # bash on Windows is usually very slow. + execute_external = (not sys.platform in ['win32']) + +# testFormat: The test format to use to interpret tests. +config.test_format = lit.formats.ShTest(execute_external) + +# suffixes: A list of file extensions to treat as test files. This is overriden +# by individual lit.local.cfg files in the test subdirectories. +config.suffixes = ['.cnf'] + +# excludes: A list of directories to exclude from the testsuite. The 'Inputs' +# subdirectories contain auxiliary inputs for various tests in their parent +# directories. +config.excludes = [] + +# test_source_root: The root path where tests are located. +config.test_source_root = os.path.dirname(os.path.abspath(__file__)) + +# test_exec_root: The root path where tests should be run. +cryptominisat_obj_root = getattr(config, 'cryptominisat_obj_root', None) +if cryptominisat_obj_root is not None: + config.test_exec_root = os.path.join(cryptominisat_obj_root, 'tests', 'cnf-files') + +# Tweak the PATH to include the tools dir. +#if llvm_obj_root is not None: +# llvm_tools_dir = getattr(config, 'llvm_tools_dir', None) +# if not llvm_tools_dir: +# lit_config.fatal('No LLVM tools dir set!') +# path = os.path.pathsep.join((llvm_tools_dir, config.environment['PATH'])) +# config.environment['PATH'] = path + +# Propagate 'HOME' through the environment. +if 'HOME' in os.environ: + config.environment['HOME'] = os.environ['HOME'] + +# Propagate 'INCLUDE' through the environment. +if 'INCLUDE' in os.environ: + config.environment['INCLUDE'] = os.environ['INCLUDE'] + +# Propagate 'LIB' through the environment. +if 'LIB' in os.environ: + config.environment['LIB'] = os.environ['LIB'] + +# Propagate the temp directory. Windows requires this because it uses \Windows\ +# if none of these are present. +if 'TMP' in os.environ: + config.environment['TMP'] = os.environ['TMP'] +if 'TEMP' in os.environ: + config.environment['TEMP'] = os.environ['TEMP'] + +# Check Python executable +pythonExec = getattr(config, 'python_executable') +if sys.executable != os.path.realpath(pythonExec): + lit_config.warning('Python executable mis-match: {} != {}'.format(sys.executable, os.path.realpath(pythonExec))) + +# Propagate PYTHON_EXECUTABLE into the environment +config.environment['PYTHON_EXECUTABLE'] = pythonExec + +### + +import os + +# Check that the object root is known. +if config.test_exec_root is None: + lit_config.fatal('Could not determine execution root for tests!') + +### Add cryptominisat specific substitutions + +# Allow user to override the solver +solverExecutable = lit_config.params.get('solver', config.cryptominisat_executable) +if not lit.util.which(solverExecutable): + lit_config.fatal('Cannot find solver: {solver}\n'.format(solver=solverExecutable)) +else: + solverExecutable = lit.util.which( solverExecutable ) + +# Allow user to provide extra arguments to solver +solverParams = lit_config.params.get('solver_params','') +solverParams += ' --zero-exit-status ' + +if config.simple == "" : + if config.sqlite != "" : + solverParams += ' --sql 2' + elif config.mysql != "" : + #database may not be set up :( TODO: auto-setup database + solverParams += ' --sql 0' + +if len(solverParams) > 0: + solverExecutable = solverExecutable + ' ' + solverParams + +# Inform user what solver is being used +lit_config.note('Using solver: {solver}\n'.format(solver=solverExecutable)) + +config.substitutions.append( ('%solver', solverExecutable) ) + +# Find OutputCheck +OutputCheckTool = os.path.join( os.path.dirname( os.path.dirname( config.test_source_root ) ), + 'utils', + 'OutputCheck', + 'bin', + 'OutputCheck' + ) +if not os.path.exists(OutputCheckTool): + lit_config.fatal('Cannot find OutputCheck executable: {OutputCheck}'.format(OutputCheck=OutputCheckTool)) + +# Add OutputCheck bin directory to PATH (for not utility) +path = os.path.pathsep.join(( os.path.dirname(OutputCheckTool), config.environment['PATH'])) +config.environment['PATH'] = path + + +# Allow user to specify extra flags to OutputCheck (e.g. -l debug) +OutputCheckFlags = lit_config.params.get('outputcheck_params','') +OutputCheckFlags += " --comment='c'" +if len(OutputCheckFlags) > 0: + OutputCheckTool += ' ' + OutputCheckFlags +config.substitutions.append( ('%OutputCheck', pythonExec + ' ' +OutputCheckTool) ) + +### Features + +# Shell execution +if execute_external: + config.available_features.add('shell') diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.site.cfg.in b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.site.cfg.in new file mode 100644 index 000000000..f7ff8a6ae --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.site.cfg.in @@ -0,0 +1,14 @@ +import sys + +## Autogenerated by cryptominisat configuration. +# Do not edit! +config.cryptominisat_src_root = "@cryptominisat5_SOURCE_DIR@" +config.cryptominisat_obj_root = "@cryptominisat5_BINARY_DIR@" +config.python_executable = "@PYTHON_EXECUTABLE@" +config.cryptominisat_executable = "$<TARGET_FILE:cryptominisat5>" +config.sqlite = "@USING_SQLITE@" +config.mysql = "@USING_SQLITE@" +config.simple = "@SIMPLE@" + +# Let the main config do the real work. +lit_config.load_config(config, "@cryptominisat5_SOURCE_DIR@/tests/cnf-files/lit.cfg") diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/reconftest.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/reconftest.cnf new file mode 100644 index 000000000..bcd7507cb --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/reconftest.cnf @@ -0,0 +1,8 @@ +c RUN: %solver --reconfat 0 --reconf 15 %s | %OutputCheck %s +1 2 0 +-1 2 0 +3 4 0 +1 2 3 4 0 +1 2 3 -4 0 +4 -2 0 +c CHECK: reconfigured solver to config 15 diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest.cnf new file mode 100644 index 000000000..6932e7348 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest.cnf @@ -0,0 +1,5 @@ +c RUN: %solver %s | %OutputCheck %s +p cnf 1 1 +1 0 +c CHECK: ^s SATISFIABLE$ +c CHECK-NEXT: ^v 1 0$
\ No newline at end of file diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest2.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest2.cnf new file mode 100644 index 000000000..46a33c21a --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest2.cnf @@ -0,0 +1,4 @@ +c RUN: %solver %s | %OutputCheck %s +1 0 +c CHECK: ^s SATISFIABLE$ +c CHECK-NEXT: ^v 1 0$ diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/verbosity.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/verbosity.cnf new file mode 100644 index 000000000..9ee5dc9e9 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/verbosity.cnf @@ -0,0 +1,4 @@ +c RUN: %solver --verb=0 %s | %OutputCheck %s +p cnf 1 1 +1 0 +c CHECK-NOT: ^c.*$
\ No newline at end of file diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor.cnf new file mode 100644 index 000000000..cdd2f58fe --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor.cnf @@ -0,0 +1,5 @@ +c RUN: %solver %s | %OutputCheck %s +p cnf 1 1 +x1 0 +c CHECK: s SATISFIABLE +c CHECK: v 1 0
\ No newline at end of file diff --git a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor_longer.cnf b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor_longer.cnf new file mode 100644 index 000000000..47c4f5a0b --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor_longer.cnf @@ -0,0 +1,14 @@ +c RUN: %solver %s | %OutputCheck %s +p cnf 10 10 +x1 2 3 4 5 6 7 8 9 10 0 +x-1 0 +x-2 0 +x-3 0 +x-4 0 +x-5 0 +x-6 0 +x-7 0 +x-8 0 +x-9 0 +c CHECK: s SATISFIABLE +c CHECK: v -1 -2 -3 -4 -5 -6 -7 -8 -9 10 0$
\ No newline at end of file |