diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/template_infer.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/template_infer.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index ab9d5f845..043e8f5ed 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -36,7 +36,7 @@ void SygusTemplateInfer::initialize(Node q) // We are processing without single invocation techniques, now check if // we should fix an invariant template (post-condition strengthening or // pre-condition weakening). - options::SygusInvTemplMode tmode = options::sygusInvTemplMode(); + options::SygusInvTemplMode tmode = options().quantifiers.sygusInvTemplMode; if (tmode != options::SygusInvTemplMode::NONE) { // currently only works for single predicate synthesis @@ -44,7 +44,7 @@ void SygusTemplateInfer::initialize(Node q) { tmode = options::SygusInvTemplMode::NONE; } - else if (!options::sygusInvTemplWhenSyntax()) + else if (!options().quantifiers.sygusInvTemplWhenSyntax) { // only use invariant templates if no syntactic restrictions if (CegGrammarConstructor::hasSyntaxRestrictions(q)) @@ -106,7 +106,7 @@ void SygusTemplateInfer::initialize(Node q) // construct template Node templ; - if (options::sygusInvAutoUnfold()) + if (options().quantifiers.sygusInvAutoUnfold) { if (d_ti.isComplete()) { |