diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-25 16:39:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-25 21:39:02 +0000 |
| commit | cb748679157eb658ce5d1173d8f26957daf8f3df (patch) | |
| tree | 024859338fd336e43bba8b1775db5c0a9caeeca3 /src/theory/quantifiers/expr_miner.cpp | |
| parent | 2aaa6ec1dfc3d7a41f120ef5361272b63363347b (diff) | |
Add new method for enumerating unsat queries with SyGuS (#7459)
This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).
The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.
It does some minor refactoring of ExprMinerManager to support the new module.
Diffstat (limited to 'src/theory/quantifiers/expr_miner.cpp')
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index fad95612f..b0dd61d33 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -62,10 +62,13 @@ void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker, const LogicInfo& logicInfo) { Assert (!query.isNull()); - if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) + if (options().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { - initializeSubsolver( - checker, opts, logicInfo, true, options::sygusExprMinerCheckTimeout()); + initializeSubsolver(checker, + opts, + logicInfo, + true, + options().quantifiers.sygusExprMinerCheckTimeout); } else { |