summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/output.cpp16
-rw-r--r--src/options/CMakeLists.txt2
-rw-r--r--src/options/base_options.toml23
-rw-r--r--src/options/mkoptions.py49
-rw-r--r--src/options/options_handler.cpp8
-rw-r--r--src/options/options_handler.h4
-rw-r--r--src/options/outputc.cpp26
-rw-r--r--src/options/outputc.h38
-rw-r--r--src/options/quantifiers_options.toml18
-rw-r--r--src/theory/quantifiers/instantiate.cpp37
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp11
-rw-r--r--test/regress/regress0/sygus/print-debug.sy2
-rw-r--r--test/regress/regress1/quantifiers/qid-debug-inst.smt22
13 files changed, 158 insertions, 78 deletions
diff --git a/src/base/output.cpp b/src/base/output.cpp
index a4003efd0..4ef76a772 100644
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -17,27 +17,25 @@
#include <iostream>
-using namespace std;
-
namespace cvc5 {
/* Definitions of the declared globals from output.h... */
null_streambuf null_sb;
-ostream null_os(&null_sb);
+std::ostream null_os(&null_sb);
NullC nullStream;
const std::string Cvc5ostream::s_tab = " ";
-const int Cvc5ostream::s_indentIosIndex = ios_base::xalloc();
+const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc();
-DebugC DebugChannel(&cout);
-WarningC WarningChannel(&cerr);
-MessageC MessageChannel(&cout);
+DebugC DebugChannel(&std::cout);
+WarningC WarningChannel(&std::cerr);
+MessageC MessageChannel(&std::cout);
NoticeC NoticeChannel(&null_os);
ChatC ChatChannel(&null_os);
-TraceC TraceChannel(&cout);
-std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer
+TraceC TraceChannel(&std::cout);
+std::ostream DumpOutC::dump_cout(std::cout.rdbuf()); // copy cout stream buffer
DumpOutC DumpOutChannel(&DumpOutC::dump_cout);
} // namespace cvc5
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index cc7b621a8..926693185 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -31,6 +31,8 @@ libcvc5_add_sources(
options_listener.h
options_public.cpp
options_public.h
+ outputc.cpp
+ outputc.h
printer_modes.cpp
printer_modes.h
set_language.cpp
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 64d373509..315a38f10 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -203,3 +203,26 @@ public = true
name = "resourceWeightHolder"
category = "undocumented"
type = "std::vector<std::string>"
+
+[[option]]
+ name = "outputTag"
+ short = "o"
+ long = "output=TAG"
+ type = "OutputTag"
+ handler = "enableOutputTag"
+ category = "regular"
+ help = "Enable output tag."
+ help_mode = "Output tags."
+[[option.mode.INST]]
+ name = "inst"
+ help = "print instantiations during solving"
+[[option.mode.SYGUS]]
+ name = "sygus"
+ help = "print enumerated terms and candidates generated by the sygus solver"
+
+# Stores then enabled output tags.
+[[option]]
+ name = "outputTagHolder"
+ category = "undocumented"
+ includes = ["<bitset>"]
+ type = "std::bitset<OutputTag__numValues>"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index e2fbd4cf1..45b1db4d6 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -129,7 +129,10 @@ TPL_DECL_MODE_ENUM = \
enum class {type}
{{
{values}
-}};"""
+}};
+
+static constexpr size_t {type}__numValues = {nvalues};
+"""
TPL_DECL_MODE_FUNC = \
"""
@@ -506,7 +509,10 @@ def help_mode_format(option):
wrapper = textwrap.TextWrapper(width=78, break_on_hyphens=False)
text = ['{}'.format(x) for x in wrapper.wrap(option.help_mode)]
- text.append('Available modes for --{} are:'.format(option.long.split('=')[0]))
+
+ optname, optvalue = option.long.split('=')
+ text.append('Available {}s for --{} are:'.format(
+ optvalue.lower(), optname))
for value, attrib in option.mode.items():
assert len(attrib) == 1
@@ -600,7 +606,8 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
mode_decl.append(
TPL_DECL_MODE_ENUM.format(
type=option.type,
- values=',\n '.join(values)))
+ values=',\n '.join(values),
+ nvalues=len(values)))
mode_decl.append(TPL_DECL_MODE_FUNC.format(type=option.type))
cases = [TPL_IMPL_MODE_CASE.format(
type=option.type, enum=x) for x in values]
@@ -730,6 +737,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
sorted(module.options, key=lambda x: x.long if x.long else x.name):
assert option.type != 'void' or option.name is None
assert option.name or option.short or option.long
+ mode_handler = option.handler and option.mode
argument_req = option.type not in ['bool', 'void']
docgen_option(option, help_common, help_others)
@@ -773,7 +781,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
name=option.name,
option='option',
value='true'))
- elif option.type != 'void' and option.name:
+ elif option.type != 'void' and option.name and not mode_handler:
cases.append(
TPL_CALL_ASSIGN.format(
module=module.id,
@@ -809,7 +817,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
name=option.name,
option='key',
value='optionarg == "true"'))
- elif argument_req and option.name:
+ elif argument_req and option.name and not mode_handler:
setoption_handlers.append(
TPL_CALL_ASSIGN.format(
module=module.id,
@@ -896,20 +904,21 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
# Define handler assign/assignBool
- if option.type == 'bool':
- custom_handlers.append(TPL_ASSIGN_BOOL.format(
- module=module.id,
- name=option.name,
- handler=handler,
- predicates='\n'.join(predicates)
- ))
- elif option.short or option.long:
- custom_handlers.append(TPL_ASSIGN.format(
- module=module.id,
- name=option.name,
- handler=handler,
- predicates='\n'.join(predicates)
- ))
+ if not mode_handler:
+ if option.type == 'bool':
+ custom_handlers.append(TPL_ASSIGN_BOOL.format(
+ module=module.id,
+ name=option.name,
+ handler=handler,
+ predicates='\n'.join(predicates)
+ ))
+ elif option.short or option.long:
+ custom_handlers.append(TPL_ASSIGN.format(
+ module=module.id,
+ name=option.name,
+ handler=handler,
+ predicates='\n'.join(predicates)
+ ))
# Default option values
default = option.default if option.default else ''
@@ -1026,8 +1035,6 @@ def parse_module(filename, module):
option = Option(attribs)
if option.mode and not option.help_mode:
perr(filename, 'defines modes but no help_mode', option)
- if option.mode and option.handler:
- perr(filename, 'defines modes and a handler', option)
if option.mode and option.default and \
option.default not in option.mode.keys():
perr(filename,
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 07138dce3..6958dcb12 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -512,6 +512,14 @@ void OptionsHandler::enableDebugTag(const std::string& option,
Trace.on(optarg);
}
+void OptionsHandler::enableOutputTag(const std::string& option,
+ const std::string& flag,
+ const std::string& optarg)
+{
+ d_options->base.outputTagHolder.set(
+ static_cast<size_t>(stringToOutputTag(optarg)));
+}
+
OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option,
const std::string& flag,
const std::string& optarg)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 3b3f80e6c..bf07729ae 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -156,6 +156,10 @@ public:
const std::string& flag,
const std::string& optarg);
+ void enableOutputTag(const std::string& option,
+ const std::string& flag,
+ const std::string& optarg);
+
private:
/** Pointer to the containing Options object.*/
diff --git a/src/options/outputc.cpp b/src/options/outputc.cpp
new file mode 100644
index 000000000..e14519123
--- /dev/null
+++ b/src/options/outputc.cpp
@@ -0,0 +1,26 @@
+#include "options/outputc.h"
+
+#include <iostream>
+
+namespace cvc5 {
+
+OutputC OutputChannel(&std::cout);
+
+Cvc5ostream OutputC::operator()(const options::OutputTag tag) const
+{
+ if (options::outputTagHolder()[static_cast<size_t>(tag)])
+ {
+ return Cvc5ostream(d_os);
+ }
+ else
+ {
+ return Cvc5ostream();
+ }
+}
+
+bool OutputC::isOn(const options::OutputTag tag) const
+{
+ return options::outputTagHolder()[static_cast<size_t>(tag)];
+}
+
+} // namespace cvc5
diff --git a/src/options/outputc.h b/src/options/outputc.h
new file mode 100644
index 000000000..647b891db
--- /dev/null
+++ b/src/options/outputc.h
@@ -0,0 +1,38 @@
+#include "cvc5_private_library.h"
+
+#ifndef CVC5__OPTIONS__OUTPUTC_H
+#define CVC5__OPTIONS__OUTPUTC_H
+
+#include <iostream>
+
+#include "cvc5_export.h"
+#include "base/output.h"
+#include "options/base_options.h"
+
+namespace cvc5 {
+
+class OutputC
+{
+ public:
+ explicit OutputC(std::ostream* os) : d_os(os) {}
+
+ Cvc5ostream operator()(const options::OutputTag tag) const;
+
+ bool isOn(const options::OutputTag tag) const;
+
+ private:
+ std::ostream* d_os;
+
+}; /* class OutputC */
+
+extern OutputC OutputChannel CVC5_EXPORT;
+
+#ifdef CVC5_MUZZLE
+#define Output ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::OutputChannel
+#else /* CVC5_MUZZLE */
+#define Output ::cvc5::OutputChannel
+#endif /* CVC5_MUZZLE */
+
+}
+
+#endif /* CVC5__OPTIONS__OUTPUTC_H */
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index cfb678991..4eb351199 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1538,14 +1538,6 @@ name = "Quantifiers"
default = "false"
help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
-[[option]]
- name = "debugSygus"
- category = "regular"
- long = "debug-sygus"
- type = "bool"
- default = "false"
- help = "print enumerated terms and candidates generated by the sygus solver (for debugging)"
-
# CEGQI applied to general quantified formulas
[[option]]
@@ -1834,16 +1826,6 @@ name = "Quantifiers"
default = "true"
help = "use store axiom during ho-elim"
-### Output options
-
-[[option]]
- name = "debugInst"
- category = "regular"
- long = "debug-inst"
- type = "bool"
- default = "false"
- help = "print instantiations during solving (for debugging)"
-
### SyGuS instantiation options
[[option]]
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 157f0f64b..17fd089d6 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -17,6 +17,7 @@
#include "expr/node_algorithm.h"
#include "options/base_options.h"
+#include "options/outputc.h"
#include "options/printer_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
@@ -676,33 +677,27 @@ bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
void Instantiate::notifyEndRound()
{
- bool debugInstTrace = Trace.isOn("inst-per-quant-round");
- if (options::debugInst() || debugInstTrace)
+ // debug information
+ if (Trace.isOn("inst-per-quant-round"))
{
- Options& sopts = smt::currentSmtEngine()->getOptions();
- std::ostream& out = *sopts.base.out;
- // debug information
- if (debugInstTrace)
+ for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
{
- for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
- {
- Trace("inst-per-quant-round")
- << " * " << i.second << " for " << i.first << std::endl;
- }
+ Trace("inst-per-quant-round")
+ << " * " << i.second << " for " << i.first << std::endl;
}
- if (options::debugInst())
+ }
+ if (Output.isOn(options::OutputTag::INST))
+ {
+ bool req = !options::printInstFull();
+ for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
{
- bool req = !options::printInstFull();
- for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
+ Node name;
+ if (!d_qreg.getNameForQuant(i.first, name, req))
{
- Node name;
- if (!d_qreg.getNameForQuant(i.first, name, req))
- {
- continue;
- }
- out << "(num-instantiations " << name << " " << i.second << ")"
- << std::endl;
+ continue;
}
+ Output(options::OutputTag::INST) << "(num-instantiations " << name << " "
+ << i.second << ")" << std::endl;
}
}
}
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 4e8d7d46d..b2b69687c 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -20,6 +20,7 @@
#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
+#include "options/outputc.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "smt/logic_exception.h"
@@ -384,7 +385,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
}
}
- bool printDebug = options::debugSygus();
+ bool printDebug = Output.isOn(options::OutputTag::SYGUS);
if (!constructed_cand)
{
// get the model value of the relevant terms from the master module
@@ -454,12 +455,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
}
}
Trace("sygus-engine") << std::endl;
- if (printDebug)
- {
- Options& sopts = smt::currentSmtEngine()->getOptions();
- std::ostream& out = *sopts.base.out;
- out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
- }
+ Output(options::OutputTag::SYGUS)
+ << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
}
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy
index aba9c715f..08b2f7c50 100644
--- a/test/regress/regress0/sygus/print-debug.sy
+++ b/test/regress/regress0/sygus/print-debug.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --debug-sygus
+; COMMAND-LINE: -o sygus
; EXPECT: (sygus-enum 0)
; EXPECT: (sygus-candidate (f 0))
; EXPECT: (sygus-enum 1)
diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
index b43c9697a..7b943f479 100644
--- a/test/regress/regress1/quantifiers/qid-debug-inst.smt2
+++ b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --debug-inst --no-check-unsat-cores
+; COMMAND-LINE: -o inst --no-check-unsat-cores
; EXPECT: (num-instantiations myQuant1 1)
; EXPECT: (num-instantiations myQuant2 1)
; EXPECT: unsat
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback