diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-31 13:42:36 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-31 13:42:36 -0600 |
| commit | c099abeb9c3a45019b18daac19c4b4cd43b4c6f0 (patch) | |
| tree | 632cd932d8ab3f8ac0583d3192e41c94a91ad353 | |
| parent | d5dcc0731061484bb6f4db8d3c04abe41ac795d2 (diff) | |
Allow PBE symmetry breaking with sygus stream (#3686)
| -rw-r--r-- | src/options/quantifiers_options.toml | 1 | ||||
| -rw-r--r-- | 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()) { |