diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-06-02 14:11:05 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-02 12:11:05 +0000 |
commit | 6d359817283f196034d8e36d0b9c1f10fb16d644 (patch) | |
tree | cb7d17927671a3b059575a86b55676eec922cef8 /src/theory/quantifiers | |
parent | 61b2694ac72d41aeff9c67e3631278e5a3bea5cb (diff) |
Move public wrapper functions out of options class (#6600)
This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/solution_filter.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 2 |
4 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 582d67b31..6069745e0 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, Node query) { Assert (!query.isNull()); - if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout)) + if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser) { initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout()); } diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 5a4c2d142..ccc0763b7 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/solution_filter.h" #include <fstream> + +#include "options/base_options.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -90,7 +92,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) else { Options& opts = smt::currentSmtEngine()->getOptions(); - std::ostream* smtOut = opts.getOut(); + std::ostream* smtOut = opts.base.out; (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")" << std::endl; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e4ec40325..62c61fe1e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -444,7 +444,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (printDebug) { Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.getOut(); + std::ostream& out = *sopts.base.out; out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; } } @@ -529,7 +529,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (printDebug) { Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.getOut(); + std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++) @@ -995,7 +995,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, // we have generated a solution, print it // get the current output stream Options& sopts = smt::currentSmtEngine()->getOptions(); - printSynthSolutionInternal(*sopts.getOut()); + printSynthSolutionInternal(*sopts.base.out); excludeCurrentSolution(enums, values); } diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 36602d3ae..48dce7cf3 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -828,7 +828,7 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) } // we have detected unsoundness in the rewriter Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream* out = sopts.getOut(); + std::ostream* out = sopts.base.out; (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; // debugging information (*out) << "Terms are not equivalent for : " << std::endl; |