From c099abeb9c3a45019b18daac19c4b4cd43b4c6f0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 31 Jan 2020 13:42:36 -0600 Subject: [PATCH] Allow PBE symmetry breaking with sygus stream (#3686) --- src/options/quantifiers_options.toml | 1 - src/smt/smt_engine.cpp | 14 +++++++------- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 95ec636ca..908846bea 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1138,7 +1138,6 @@ header = "options/quantifiers_options.h" long = "sygus-unif-pi=MODE" type = "SygusUnifPiMode" default = "NONE" - read_only = true help = "mode for synthesis via piecewise-indepedent unification" help_mode = "Modes for piecewise-independent unification." [[option.mode.NONE]] diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d10678bf6..83d8fb612 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2003,8 +2003,9 @@ void SmtEngine::setDefaults() { } // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm // is one that is specialized for returning a single solution. Non-basic - // sygus algorithms currently include the PBE solver, static template - // inference for invariant synthesis, and single invocation techniques. + // sygus algorithms currently include the PBE solver, UNIF+PI, static + // template inference for invariant synthesis, and single invocation + // techniques. bool reqBasicSygus = false; if (options::produceAbducts()) { @@ -2035,11 +2036,10 @@ void SmtEngine::setDefaults() { if (!options::sygusUnifPbe.wasSetByUser()) { options::sygusUnifPbe.set(false); - // also disable PBE-specific symmetry breaking unless PBE was enabled - if (!options::sygusSymBreakPbe.wasSetByUser()) - { - options::sygusSymBreakPbe.set(false); - } + } + if (options::sygusUnifPi.wasSetByUser()) + { + options::sygusUnifPi.set(options::SygusUnifPiMode::NONE); } if (!options::sygusInvTemplMode.wasSetByUser()) { -- 2.30.2