diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-29 11:11:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-29 16:11:05 +0000 |
| commit | b685ed411b6814f0810ce8f61d07aa49bd75ea3b (patch) | |
| tree | 75029fdd0b7b8d82f6296047c10818cb745c9cdb /src/smt/set_defaults.cpp | |
| parent | f2672e53fae29abe40fc69b004d1df5be0ce1e8b (diff) | |
Integrate central equality engine approach into theory engine, add option and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e12d3eb1d..c7a2c8916 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -970,6 +970,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set up of central equality engine + if (opts.theory.eeMode == options::EqEngineMode::CENTRAL) + { + if (!opts.arith.arithEqSolverWasSetByUser) + { + // use the arithmetic equality solver by default + opts.arith.arithEqSolver = true; + } + } if (opts.arith.arithEqSolver) { if (!opts.arith.arithCongManWasSetByUser) |