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
|
/********************* */
/*! \file options_handlers.h
** \verbatim
** Original author: Morgan Deters <mdeters@cs.nyu.edu>
** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com>
** 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 [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
#include <string>
namespace CVC4 {
namespace theory {
namespace quantifiers {
static const std::string instWhenHelp = "\
Modes currently supported by the --inst-when option:\n\
\n\
full (default)\n\
+ Run instantiation round at full effort, before theory combination.\n\
\n\
full-last-call\n\
+ Alternate running instantiation rounds at full effort and last\n\
call. In other words, interleave instantiation and theory combination.\n\
\n\
last-call\n\
+ Run instantiation at last call effort, after theory combination.\n\
\n\
";
static const std::string literalMatchHelp = "\
Literal match modes currently supported by the --literal-match option:\n\
\n\
none (default)\n\
+ Do not use literal matching.\n\
\n\
predicate\n\
+ Consider the phase requirements of predicate literals when applying heuristic\n\
quantifier instantiation. For example, the trigger P( x ) in the quantified \n\
formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
\n\
";
static const std::string axiomInstModeHelp = "\
Axiom instantiation modes currently supported by the --axiom-inst option:\n\
\n\
default \n\
+ Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\
instantiating axioms.\n\
\n\
trust \n\
+ Treat axioms only using heuristic instantiation. Return unknown if in the case\n\
that no instantiations are produced.\n\
\n\
priority \n\
+ Treat axioms only using heuristic instantiation. Resort to using all methods\n\
in the case that no instantiations are produced.\n\
\n\
";
inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "pre-full") {
return INST_WHEN_PRE_FULL;
} else if(optarg == "full") {
return INST_WHEN_FULL;
} else if(optarg == "full-last-call") {
return INST_WHEN_FULL_LAST_CALL;
} else if(optarg == "last-call") {
return INST_WHEN_LAST_CALL;
} else if(optarg == "help") {
puts(instWhenHelp.c_str());
exit(1);
} else {
throw OptionException(std::string("unknown option for --inst-when: `") +
optarg + "'. Try --inst-when help.");
}
}
inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) {
if(mode == INST_WHEN_PRE_FULL) {
throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
}
}
inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "none") {
return LITERAL_MATCH_NONE;
} else if(optarg == "predicate") {
return LITERAL_MATCH_PREDICATE;
} else if(optarg == "equality") {
return LITERAL_MATCH_EQUALITY;
} else if(optarg == "help") {
puts(literalMatchHelp.c_str());
exit(1);
} else {
throw OptionException(std::string("unknown option for --literal-matching: `") +
optarg + "'. Try --literal-matching help.");
}
}
inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) {
if(mode == LITERAL_MATCH_EQUALITY) {
throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
}
}
inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "default") {
return AXIOM_INST_MODE_DEFAULT;
} else if(optarg == "trust") {
return AXIOM_INST_MODE_TRUST;
} else if(optarg == "priority") {
return AXIOM_INST_MODE_PRIORITY;
} else if(optarg == "help") {
puts(axiomInstModeHelp.c_str());
exit(1);
} else {
throw OptionException(std::string("unknown option for --axiom-inst: `") +
optarg + "'. Try --axiom-inst help.");
}
}
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */
|
