diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3f0ac70f5..ff7bb6378 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1039,8 +1039,9 @@ void SynthConjecture::printSynthSolution(std::ostream& out) bool is_unique_term = true; - if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen() - || options::sygusSolFilterImplied())) + if (status != 0 + && (options::sygusRewSynth() || options::sygusQueryGen() + || options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE)) { Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; std::map<Node, ExpressionMinerManager>::iterator its = @@ -1057,9 +1058,16 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); } - if (options::sygusSolFilterImplied()) + if (options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE) { - d_exprm[prog].enableFilterImpliedSolutions(); + if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_STRONG) + { + d_exprm[prog].enableFilterStrongSolutions(); + } + else if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_WEAK) + { + d_exprm[prog].enableFilterWeakSolutions(); + } } its = d_exprm.find(prog); } |