blob: 7cdd4aac562540ac9125d51355cf6b4014da8deb (
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
145
146
|
/********************* */
/*! \file options_handlers.h
** \verbatim
** Original author: Liana Hadarean
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Custom handlers and predicates for TheoryBV options
**
** Custom handlers and predicates for TheoryBV options.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__BV__OPTIONS_HANDLERS_H
#define __CVC4__THEORY__BV__OPTIONS_HANDLERS_H
#include "theory/bv/bitblast_mode.h"
#include "main/options.h"
namespace CVC4 {
namespace theory {
namespace bv {
inline void abcEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
#ifndef CVC4_USE_ABC
if(value) {
std::stringstream ss;
ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
throw OptionException(ss.str());
}
#endif /* CVC4_USE_ABC */
}
inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* smt) throw(OptionException) {
#ifndef CVC4_USE_ABC
if(!value.empty()) {
std::stringstream ss;
ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
throw OptionException(ss.str());
}
#endif /* CVC4_USE_ABC */
}
static const std::string bitblastingModeHelp = "\
Bit-blasting modes currently supported by the --bitblast option:\n\
\n\
lazy (default)\n\
+ Separate boolean structure and term reasoning betwen the core\n\
SAT solver and the bv SAT solver\n\
\n\
eager\n\
+ Bitblast eagerly to bv SAT solver\n\
";
inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "lazy") {
if (!options::bitvectorPropagate.wasSetByUser()) {
options::bitvectorPropagate.set(true);
}
if (!options::bitvectorEqualitySolver.wasSetByUser()) {
options::bitvectorEqualitySolver.set(true);
}
if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
if (options::incrementalSolving() ||
options::produceModels()) {
options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF);
} else {
options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO);
}
}
if (!options::bitvectorInequalitySolver.wasSetByUser()) {
options::bitvectorInequalitySolver.set(true);
}
if (!options::bitvectorAlgebraicSolver.wasSetByUser()) {
options::bitvectorAlgebraicSolver.set(true);
}
return BITBLAST_MODE_LAZY;
} else if(optarg == "eager") {
if (options::incrementalSolving() &&
options::incrementalSolving.wasSetByUser()) {
throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
Try --bitblast=lazy"));
}
if (!options::bitvectorToBool.wasSetByUser()) {
options::bitvectorToBool.set(true);
}
if (!options::bvAbstraction.wasSetByUser() &&
!options::skolemizeArguments.wasSetByUser()) {
options::bvAbstraction.set(true);
options::skolemizeArguments.set(true);
}
return BITBLAST_MODE_EAGER;
} else if(optarg == "help") {
puts(bitblastingModeHelp.c_str());
exit(1);
} else {
throw OptionException(std::string("unknown option for --bitblast: `") +
optarg + "'. Try --bitblast=help.");
}
}
static const std::string bvSlicerModeHelp = "\
Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\
\n\
auto (default)\n\
+ Turn slicer on if input has only equalities over core symbols\n\
\n\
on\n\
+ Turn slicer on\n\
\n\
off\n\
+ Turn slicer off\n\
";
inline BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "auto") {
return BITVECTOR_SLICER_AUTO;
} else if(optarg == "on") {
return BITVECTOR_SLICER_ON;
} else if(optarg == "off") {
return BITVECTOR_SLICER_OFF;
} else if(optarg == "help") {
puts(bitblastingModeHelp.c_str());
exit(1);
} else {
throw OptionException(std::string("unknown option for --bv-eq-slicer: `") +
optarg + "'. Try --bv-eq-slicer=help.");
}
}
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__BV__OPTIONS_HANDLERS_H */
|
