clean up

14 files changed, 0 insertions, 280 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
deleted file mode 100644
index 1aa3048e5..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/CMakeLists.txt
+++ /dev/null
@@ -1,47 +0,0 @@
-# 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
deleted file mode 100644
index 0ea82049d..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-1.cnf
+++ /dev/null
@@ -1,4 +0,0 @@
-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
deleted file mode 100644
index 7606969db..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-2.cnf
+++ /dev/null
@@ -1,6 +0,0 @@
-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
deleted file mode 100644
index c403c2d6d..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep-3.cnf
+++ /dev/null
@@ -1,4 +0,0 @@
-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
deleted file mode 100644
index d4e0609f6..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars.cnf
+++ /dev/null
@@ -1,10 +0,0 @@
-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
deleted file mode 100644
index 715211ef3..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/indep_vars_2.cnf
+++ /dev/null
@@ -1,11 +0,0 @@
-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
deleted file mode 100644
index edbfc606e..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.cfg
+++ /dev/null
@@ -1,144 +0,0 @@
-# -*- 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
deleted file mode 100644
index f7ff8a6ae..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.site.cfg.in
+++ /dev/null
@@ -1,14 +0,0 @@
-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
deleted file mode 100644
index bcd7507cb..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/reconftest.cnf
+++ /dev/null
@@ -1,8 +0,0 @@
-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
deleted file mode 100644
index 6932e7348..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest.cnf
+++ /dev/null
@@ -1,5 +0,0 @@
-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
deleted file mode 100644
index 46a33c21a..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/simptest2.cnf
+++ /dev/null
@@ -1,4 +0,0 @@
-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
deleted file mode 100644
index 9ee5dc9e9..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/verbosity.cnf
+++ /dev/null
@@ -1,4 +0,0 @@
-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
deleted file mode 100644
index cdd2f58fe..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor.cnf
+++ /dev/null
@@ -1,5 +0,0 @@
-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
deleted file mode 100644
index 47c4f5a0b..000000000
--- a/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/xor_longer.cnf
+++ /dev/null
@@ -1,14 +0,0 @@
-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