diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-03 13:44:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-03 13:44:37 -0500 |
commit | e223134343162e5c2d5e65c34ac74540d326b37d (patch) | |
tree | 65acbab5671dc90bec6790f6a70be76e16fe037a /src | |
parent | 9f95889dd0853a249c4e01f82174704cf2bc628c (diff) | |
parent | c56eaf4423fbf65663a4e03c8a60ed937c99de7d (diff) |
Merge branch 'master' into fixStrRegressfixStrRegress
Diffstat (limited to 'src')
-rw-r--r-- | src/base/output.cpp | 16 | ||||
-rw-r--r-- | src/options/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/options/base_options.toml | 23 | ||||
-rw-r--r-- | src/options/mkoptions.py | 49 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 8 | ||||
-rw-r--r-- | src/options/options_handler.h | 4 | ||||
-rw-r--r-- | src/options/outputc.cpp | 26 | ||||
-rw-r--r-- | src/options/outputc.h | 38 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 18 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_bitblast.cpp | 92 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_bitblast.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 |
13 files changed, 237 insertions, 94 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/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index a5d89e371..613ba47bf 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -27,6 +27,46 @@ namespace theory { namespace bv { /** + * Notifies the BV solver when assertions were reset. + * + * This class is notified after every user-context pop and maintains a flag + * that indicates whether assertions have been reset. If the user-context level + * reaches level 0 it means that the assertions were reset. + */ +class NotifyResetAssertions : public context::ContextNotifyObj +{ + public: + NotifyResetAssertions(context::Context* c) + : context::ContextNotifyObj(c, false), + d_context(c), + d_doneResetAssertions(false) + { + } + + bool doneResetAssertions() { return d_doneResetAssertions; } + + void reset() { d_doneResetAssertions = false; } + + protected: + void contextNotifyPop() override + { + // If the user-context level reaches 0 it means that reset-assertions was + // called. + if (d_context->getLevel() == 0) + { + d_doneResetAssertions = true; + } + } + + private: + /** The user-context. */ + context::Context* d_context; + + /** Flag to notify whether reset assertions was called. */ + bool d_doneResetAssertions; +}; + +/** * Bit-blasting registrar. * * The CnfStream calls preRegister() if it encounters a theory atom. @@ -85,30 +125,15 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, : nullptr), d_factLiteralCache(s->getSatContext()), d_literalFactCache(s->getSatContext()), - d_propagate(options::bitvectorPropagate()) + d_propagate(options::bitvectorPropagate()), + d_resetNotify(new NotifyResetAssertions(s->getUserContext())) { if (pnm != nullptr) { d_bvProofChecker.registerTo(pnm->getChecker()); } - switch (options::bvSatSolver()) - { - case options::SatSolverMode::CRYPTOMINISAT: - d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); - break; - default: - d_satSolver.reset(prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); - } - d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), - d_bbRegistrar.get(), - d_nullContext.get(), - nullptr, - smt::currentResourceManager(), - prop::FormulaLitPolicy::INTERNAL, - "theory::bv::BVSolverBitblast")); + initSatSolver(); } void BVSolverBitblast::postCheck(Theory::Effort level) @@ -122,6 +147,16 @@ void BVSolverBitblast::postCheck(Theory::Effort level) } } + // If we permanently added assertions to the SAT solver and the assertions + // were reset, we have to reset the SAT solver and the CNF stream. + if (options::bvAssertInput() && d_resetNotify->doneResetAssertions()) + { + d_satSolver.reset(nullptr); + d_cnfStream.reset(nullptr); + initSatSolver(); + d_resetNotify->reset(); + } + NodeManager* nm = NodeManager::currentNM(); /* Process input assertions bit-blast queue. */ @@ -316,6 +351,27 @@ EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b) return EQUALITY_FALSE_IN_MODEL; } +void BVSolverBitblast::initSatSolver() +{ + switch (options::bvSatSolver()) + { + case options::SatSolverMode::CRYPTOMINISAT: + d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); + break; + default: + d_satSolver.reset(prop::SatSolverFactory::createCadical( + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); + } + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_bbRegistrar.get(), + d_nullContext.get(), + nullptr, + smt::currentResourceManager(), + prop::FormulaLitPolicy::INTERNAL, + "theory::bv::BVSolverBitblast")); +} + Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize) { if (node.isConst()) diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index c5134c6fc..1fb721deb 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -33,6 +33,7 @@ namespace cvc5 { namespace theory { namespace bv { +class NotifyResetAssertions; class BBRegistrar; /** @@ -70,6 +71,9 @@ class BVSolverBitblast : public BVSolver const std::set<Node>& termSet) override; private: + /** Initialize SAT solver and CNF stream. */ + void initSatSolver(); + /** * Get value of `node` from SAT solver. * @@ -153,6 +157,9 @@ class BVSolverBitblast : public BVSolver /** Option to enable/disable bit-level propagation. */ bool d_propagate; + + /** Notifies when reset-assertion was called. */ + std::unique_ptr<NotifyResetAssertions> d_resetNotify; }; } // namespace bv 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( |