diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-21 19:04:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-22 00:04:21 +0000 |
commit | 738f38bf6b5f2cf6a5812c056ae6f771bffb42e6 (patch) | |
tree | 144fc194b24ac8cb2a1b0133dbaf7cd3573281bf /src/theory/quantifiers | |
parent | 877768903c3b17b88cd27a85995c94d2ada24660 (diff) |
Make expression mining use configurable options and logic (#7426)
Required for doing options-specific internal fuzzing using SyGuS.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/expr_miner.h | 7 |
2 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index d648a7a29..fad95612f 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -53,17 +53,23 @@ Node ExprMiner::convertToSkolem(Node n) void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker, Node query) { + initializeChecker(checker, query, options(), logicInfo()); +} + +void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker, + Node query, + const Options& opts, + const LogicInfo& logicInfo) +{ Assert (!query.isNull()); if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { - initializeSubsolver(checker, - d_env, - true, - options::sygusExprMinerCheckTimeout()); + initializeSubsolver( + checker, opts, logicInfo, true, options::sygusExprMinerCheckTimeout()); } else { - initializeSubsolver(checker, d_env); + initializeSubsolver(checker, opts, logicInfo); } // also set the options checker->setOption("sygus-rr-synth-input", "false"); diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 3933b9635..702dbf5aa 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -85,7 +85,12 @@ class ExprMiner : protected EnvObj * of the argument "query", which is a formula whose free variables (of * kind BOUND_VARIABLE) are a subset of d_vars. */ - void initializeChecker(std::unique_ptr<SolverEngine>& smte, Node query); + void initializeChecker(std::unique_ptr<SolverEngine>& checker, Node query); + /** Also with configurable options and logic */ + void initializeChecker(std::unique_ptr<SolverEngine>& checker, + Node query, + const Options& opts, + const LogicInfo& logicInfo); /** * Run the satisfiability check on query and return the result * (sat/unsat/unknown). |