cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #11994 from ethereum/smt-solver-choice-tweaks

Browse Source 
`SMTSolverChoice` tweaks: fix `&` modifying the object and add more `const`/`noexcept`
This commit is contained in:
Kamil Śliwak 2021-09-22 17:55:33 +02:00 committed by GitHub
commit 72fc34494a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
libsmtutil/SolverInterface.h
View File

@ -42,11 +42,11 @@ struct SMTSolverChoice
bool smtlib2 = false; bool smtlib2 = false;
bool z3 = false; bool z3 = false;
static constexpr SMTSolverChoice All() { return {true, true, true}; } static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; }
static constexpr SMTSolverChoice CVC4() { return {true, false, false}; } static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; }
static constexpr SMTSolverChoice SMTLIB2() { return {false, true, false}; } static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, true, false}; }
static constexpr SMTSolverChoice Z3() { return {false, false, true}; } static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; }
static constexpr SMTSolverChoice None() { return {false, false, false}; } static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; }
static std::optional<SMTSolverChoice> fromString(std::string const& _solvers) static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
{ {
@ -65,7 +65,7 @@ struct SMTSolverChoice
return solvers; return solvers;
} }
SMTSolverChoice& operator&(SMTSolverChoice const& _other) SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
{ {
cvc4 &= _other.cvc4; cvc4 &= _other.cvc4;
smtlib2 &= _other.smtlib2; smtlib2 &= _other.smtlib2;
@ -73,9 +73,10 @@ struct SMTSolverChoice
return *this; return *this;
} }
SMTSolverChoice& operator&=(SMTSolverChoice const& _other) SMTSolverChoice operator&(SMTSolverChoice _other) const noexcept
{ {
return *this & _other; _other &= *this;
return _other;
} }
bool operator!=(SMTSolverChoice const& _other) const noexcept { return !(*this == _other); } bool operator!=(SMTSolverChoice const& _other) const noexcept { return !(*this == _other); }
@ -101,9 +102,9 @@ struct SMTSolverChoice
return true; return true;
} }
bool none() { return !some(); } bool none() const noexcept { return !some(); }
bool some() { return cvc4 || smtlib2 || z3; } bool some() const noexcept { return cvc4 || smtlib2 || z3; }
bool all() { return cvc4 && smtlib2 && z3; } bool all() const noexcept { return cvc4 && smtlib2 && z3; }
}; };
enum class CheckResult enum class CheckResult