summaryrefslogtreecommitdiff
path: root/cryptominisat5/cryptominisat-5.6.3/tests/cnf-files/lit.cfg
blob: edbfc606e02c1df5e28c0d3d25bc17a3e0c5e164 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
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')
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback