port some misc improvements from the new memory branch
MODIFY
.travis.yml
.travis.yml
@@ -45,7 +45,7 @@ script:
matrix:
include:
- - env: CMAKE_CXX_COMPILER=g++-10 CMAKE_BUILD_TYPE=Debug
+ - env: CMAKE_CXX_COMPILER=g++-10 CMAKE_BUILD_TYPE=Debug CMAKE_CXX_FLAGS=-fsanitize=address,undefined
os: linux
dist: focal
addons: &gcc10
@@ -59,23 +59,6 @@ matrix:
dist: focal
addons: *gcc10
- - env: CMAKE_CXX_COMPILER=clang++-10 CMAKE_BUILD_TYPE=Debug CMAKE_CXX_FLAGS=-fsanitize=address,undefined
- os: linux
- dist: focal
- addons: &clang10
- apt:
- sources:
- - sourceline: "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-10 main"
- key_url: "https://apt.llvm.org/llvm-snapshot.gpg.key"
- packages:
- - *default_packages
- - clang-10
-
- - env: CMAKE_CXX_COMPILER=clang++-10 CMAKE_BUILD_TYPE=Release
- os: linux
- dist: focal
- addons: *clang10
-
- env: CMAKE_CXX_COMPILER=clang++-11 CMAKE_BUILD_TYPE=Debug CMAKE_CXX_FLAGS=-fsanitize=address,undefined
os: linux
dist: focal
@@ -87,6 +70,7 @@ matrix:
packages:
- *default_packages
- clang-11
+ - g++-10
- env: CMAKE_CXX_COMPILER=clang++-11 CMAKE_BUILD_TYPE=Release
os: linux
@@ -102,7 +86,6 @@ matrix:
- ninja
- re2c
- z3
- update: true
- env: CMAKE_BUILD_TYPE=Release
os: osx

MODIFY
ir/instr.h
ir/instr.h
@@ -323,8 +323,6 @@ public:
const BasicBlock& operator*() const;
target_iterator& operator++(void) { ++idx; return *this; }
bool operator==(const target_iterator &rhs) const { return idx == rhs.idx; }
- // FIXME: remove when we drop g++9 support
- bool operator!=(const target_iterator &rhs) const { return idx != rhs.idx; }
};
class it_helper {

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -33,7 +33,7 @@ static unsigned next_local_bid;
static unsigned next_global_bid;
static unsigned next_ptr_input;
-static bool observes_addresses() {
+static bool observesAddresses() {
return IR::has_ptr2int || IR::has_int2ptr;
}
@@ -535,7 +535,7 @@ expr Pointer::getValue(const char *name, const FunctionExpr &local_fn,
}
expr Pointer::getAddress(bool simplify) const {
- assert(observes_addresses());
+ assert(observesAddresses());
auto bid = getShortBid();
auto zero = expr::mkUInt(0, bits_size_t - 1);
@@ -672,7 +672,7 @@ expr Pointer::isAligned(unsigned align) {
expr blk_align = isBlockAligned(align);
- if (!observes_addresses() || (blk_align.isConst() && offset.isConst())) {
+ if (!observesAddresses() || (blk_align.isConst() && offset.isConst())) {
// This is stricter than checking getAddress(), but as addresses are not
// observed, program shouldn't be able to distinguish this from checking
// getAddress()
@@ -906,15 +906,11 @@ expr Pointer::isNull() const {
}
expr Pointer::isNonZero() const {
- if (observes_addresses())
+ if (observesAddresses())
return getAddress() != 0;
return !isNull();
}
-bool Pointer::operator<(const Pointer &rhs) const {
- return p < rhs.p;
-}
-
ostream& operator<<(ostream &os, const Pointer &p) {
if (p.isNull().isTrue())
return os << "null";
@@ -1054,10 +1050,6 @@ void Memory::AliasSet::printStats(ostream &os) {
<< (alias_buckets_hits.back() / total) << "%\n";
}
-bool Memory::AliasSet::operator<(const AliasSet &rhs) const {
- return tie(local, non_local) < tie(rhs.local, rhs.non_local);
-}
-
void Memory::AliasSet::print(ostream &os) const {
auto print = [&](const char *str, const auto &v) {
os << str;
@@ -1079,23 +1071,23 @@ void Memory::AliasSet::print(ostream &os) const {
}
-static set<Pointer> all_leaf_ptrs(Memory &m, const expr &ptr) {
+static set<Pointer> all_leaf_ptrs(const Memory &m, const expr &ptr) {
set<Pointer> ptrs;
- for (auto &ptr_val : allExprLeafs(ptr)) {
+ for (auto &ptr_val : ptr.leafs()) {
Pointer p(m, ptr_val);
auto offset = p.getOffset();
- for (auto &bid : allExprLeafs(p.getBid())) {
+ for (auto &bid : p.getBid().leafs()) {
ptrs.emplace(m, bid, offset);
}
}
return ptrs;
}
-static vector<expr> extract_possible_local_bids(Memory &m, const expr &eptr) {
- vector<expr> ret;
+static set<expr> extract_possible_local_bids(Memory &m, const expr &eptr) {
+ set<expr> ret;
for (auto &ptr : all_leaf_ptrs(m, eptr)) {
if (!ptr.isLocal().isFalse())
- ret.emplace_back(ptr.getShortBid());
+ ret.emplace(ptr.getShortBid());
}
return ret;
}
@@ -1132,7 +1124,7 @@ bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
if (auto algn = (local ? local_blk_align : non_local_blk_align).lookup(bid)) {
uint64_t blk_align;
ENSURE(algn->isUInt(blk_align));
- if (align > (1ull << blk_align) && (!observes_addresses() || const_offset))
+ if (align > (1ull << blk_align) && (!observesAddresses() || const_offset))
return false;
}
@@ -1511,7 +1503,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
state->addAxiom(p_align.ule(q_align));
}
- if (!observes_addresses())
+ if (!observesAddresses())
return;
if (has_null_block)
@@ -1612,8 +1604,7 @@ expr Memory::PtrInput::operator==(const PtrInput &rhs) const {
return val == rhs.val;
}
-pair<expr,expr>
-Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
+expr Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
bool has_local = escaped_local_blks.numMayAlias(true);
unsigned bits_bid = has_local ? bits_for_bid : bits_shortbid();
@@ -1651,7 +1642,7 @@ Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
ptr_alias.emplace(p.getBid(), move(alias));
state->addAxiom(expr::mkIf(p.isLocal(), expr::mk_or(local), nonlocal));
- return { p.release(), move(var) };
+ return p.release();
}
Memory::CallState Memory::CallState::mkIf(const expr &cond,
@@ -1682,13 +1673,9 @@ expr Memory::CallState::operator==(const CallState &rhs) const {
return ret;
}
-bool Memory::CallState::operator<(const CallState &rhs) const {
- return tie(non_local_block_val, non_local_block_liveness) <
- tie(rhs.non_local_block_val, rhs.non_local_block_liveness);
-}
-
Memory::CallState
-Memory::mkCallState(const vector<PtrInput> *ptr_inputs, bool nofree) const {
+Memory::mkCallState(const string &fnname, const vector<PtrInput> *ptr_inputs,
+ bool nofree) {
CallState st;
st.empty = false;
@@ -1818,7 +1805,7 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
auto align_bits = ilog2(align);
if (is_local) {
- if (observes_addresses()) {
+ if (observesAddresses()) {
// MSB of local block area's address is 1.
auto addr_var
= expr::mkFreshVar("local_addr",
@@ -1846,7 +1833,7 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
state->addAxiom(p.getAllocType() == alloc_ty);
}
- if (align_bits && observes_addresses())
+ if (align_bits && observesAddresses())
state->addAxiom(p.getAddress().extract(align_bits - 1, 0) == 0);
bool cond = (has_null_block && bid == 0) ||
@@ -1879,7 +1866,7 @@ void Memory::startLifetime(const expr &ptr_local) {
Pointer p(*this, ptr_local);
state->addUB(p.isLocal());
- if (observes_addresses())
+ if (observesAddresses())
state->addPre(disjoint_local_blocks(*this, p.getAddress(), p.blockSize(),
local_blk_addr));
@@ -2381,51 +2368,6 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
return ret;
}
-bool Memory::operator<(const Memory &rhs) const {
- // FIXME: remove this once we move to C++20
- assert(state == rhs.state);
- return
- tie(non_local_block_val, local_block_val,
- non_local_block_liveness, local_block_liveness, local_blk_addr,
- local_blk_size, local_blk_align, local_blk_kind,
- non_local_blk_size, non_local_blk_align,
- non_local_blk_kind, byval_blks, escaped_local_blks,
- ptr_alias, next_nonlocal_bid) <
- tie(rhs.non_local_block_val, rhs.local_block_val,
- rhs.non_local_block_liveness, rhs.local_block_liveness,
- rhs.local_blk_addr, rhs.local_blk_size, rhs.local_blk_align,
- rhs.local_blk_kind,
- rhs.non_local_blk_size, rhs.non_local_blk_align,
- rhs.non_local_blk_kind, rhs.byval_blks, rhs.escaped_local_blks,
- rhs.ptr_alias, rhs.next_nonlocal_bid);
-}
-
-bool Memory::cmpFnCallInput(const Memory &rhs) const {
- assert(state == rhs.state && state->isSource());
- // first compare non-local memory only
- auto nla = tie(non_local_block_val, non_local_block_liveness,
- non_local_blk_size, non_local_blk_align, non_local_blk_kind,
- byval_blks, escaped_local_blks);
- auto nlb = tie(rhs.non_local_block_val, rhs.non_local_block_liveness,
- rhs.non_local_blk_size, rhs.non_local_blk_align,
- rhs.non_local_blk_kind, rhs.byval_blks,
- rhs.escaped_local_blks);
- if (nla < nlb)
- return true;
- if (nla > nlb)
- return false;
-
- // if nothing local escaped, then memories are equivalent for the callee
- if (escaped_local_blks.numMayAlias(true) == 0)
- return false;
-
- return
- tie(local_block_val, local_block_liveness, local_blk_addr, local_blk_size,
- local_blk_align, local_blk_kind) <
- tie(rhs.local_block_val, rhs.local_block_liveness, rhs.local_blk_addr,
- rhs.local_blk_size, rhs.local_blk_align, rhs.local_blk_kind);
-}
-
#define P(name, expr) do { \
auto v = m.eval(expr, false); \
uint64_t n; \
@@ -2448,7 +2390,7 @@ void Memory::print(ostream &os, const Model &m) const {
P("size", p.blockSize());
P("align", expr::mkInt(1, 64) << p.blockAlignment().zextOrTrunc(64));
P("alloc type", p.getAllocType());
- if (observes_addresses())
+ if (observesAddresses())
P("address", p.getAddress());
os << '\n';
}
@@ -2498,17 +2440,20 @@ ostream& operator<<(ostream &os, const Memory &m) {
P("BLOCK SIZE:", local_blk_size, non_local_blk_size);
P("BLOCK ALIGN:", local_blk_align, non_local_blk_align);
P("BLOCK KIND:", local_blk_kind, non_local_blk_kind);
- if (m.numLocals() > 0) {
- os << "ESCAPED LOCAL BLOCKS: ";
- m.escaped_local_blks.print(os);
+ if (m.escaped_local_blks.numMayAlias(true) > 0) {
+ m.escaped_local_blks.print(os << "ESCAPED LOCAL BLOCKS: ");
+ }
+ if (!m.local_blk_addr.empty()) {
os << "\nLOCAL BLOCK ADDR: " << m.local_blk_addr << '\n';
}
+ if (!m.ptr_alias.empty()) {
os << "\nALIAS SETS:\n";
for (auto &[bid, alias] : m.ptr_alias) {
os << bid << ": ";
alias.print(os);
os << '\n';
}
+ }
return os;
}

MODIFY
ir/memory.h
ir/memory.h
@@ -193,8 +193,7 @@ public:
smt::expr isNull() const;
smt::expr isNonZero() const;
- // for container use only
- bool operator<(const Pointer &rhs) const;
+ auto operator<=>(const Pointer &rhs) const { return p <=> rhs.p; }
friend std::ostream& operator<<(std::ostream &os, const Pointer &p);
};
@@ -224,8 +223,7 @@ class Memory {
void computeAccessStats() const;
static void printStats(std::ostream &os);
- // for container use only
- bool operator<(const AliasSet &rhs) const;
+ auto operator<=>(const AliasSet &rhs) const = default;
void print(std::ostream &os) const;
};
@@ -243,9 +241,9 @@ class Memory {
MemBlock(smt::expr &&val, DataType type)
: val(std::move(val)), type(type) {}
- bool operator<(const MemBlock &other) const {
- return std::tie(val, undef, type) <
- std::tie(other.val, other.undef, other.type);
+ auto operator<=>(const MemBlock &rhs) const {
+ return std::tie(val, undef, type) <=>
+ std::tie(rhs.val, rhs.undef, rhs.type);
}
};
@@ -324,8 +322,7 @@ public:
static CallState mkIf(const smt::expr &cond, const CallState &then,
const CallState &els);
smt::expr operator==(const CallState &rhs) const;
- // for container use only
- bool operator<(const CallState &rhs) const;
+ auto operator<=>(const CallState &rhs) const = default;
friend class Memory;
};
@@ -348,16 +345,12 @@ public:
PtrInput(StateValue &&v, bool byval, bool nocapture) :
val(std::move(v)), byval(byval), nocapture(nocapture) {}
smt::expr operator==(const PtrInput &rhs) const;
- bool operator<(const PtrInput &rhs) const {
- return std::tie(val, byval, nocapture) <
- std::tie(rhs.val, rhs.byval, rhs.nocapture);
- }
+ auto operator<=>(const PtrInput &rhs) const = default;
};
- std::pair<smt::expr, smt::expr>
- mkFnRet(const char *name, const std::vector<PtrInput> &ptr_inputs);
- CallState mkCallState(const std::vector<PtrInput> *ptr_inputs, bool nofree)
- const;
+ smt::expr mkFnRet(const char *name, const std::vector<PtrInput> &ptr_inputs);
+ CallState mkCallState(const std::string &fnname,
+ const std::vector<PtrInput> *ptr_inputs, bool nofree);
void setState(const CallState &st);
// Allocates a new memory block and returns (pointer expr, allocated).
@@ -413,9 +406,7 @@ public:
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);
- // for container use only
- bool operator<(const Memory &rhs) const;
- bool cmpFnCallInput(const Memory &rhs) const;
+ auto operator<=>(const Memory &rhs) const = default;
static void printAliasStats(std::ostream &os) {
AliasSet::printStats(os);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -629,10 +629,7 @@ void State::addNoReturn() {
expr State::FnCallInput::operator==(const FnCallInput &rhs) const {
if (readsmem != rhs.readsmem ||
argmemonly != rhs.argmemonly ||
- (readsmem && (
- fncall_ranges != rhs.fncall_ranges ||
- m < rhs.m || rhs.m < m
- )))
+ (readsmem && (fncall_ranges != rhs.fncall_ranges || is_neq(m <=> rhs.m))))
return false;
AndExpr eq;
@@ -698,22 +695,6 @@ expr State::FnCallInput::refinedBy(
return refines();
}
-bool State::FnCallInput::operator<(const FnCallInput &rhs) const {
- return tie(args_nonptr, args_ptr, fncall_ranges, m, readsmem, argmemonly) <
- tie(rhs.args_nonptr, rhs.args_ptr, rhs.fncall_ranges, rhs.m,
- rhs.readsmem, rhs.argmemonly);
-#if 0
- auto a = tie(args_nonptr, args_ptr, fncall_ranges, readsmem, argmemonly);
- auto b = tie(rhs.args_nonptr, rhs.args_ptr, rhs.fncall_ranges, rhs.readsmem,
- rhs.argmemonly);
- if (a < b)
- return true;
- if (a > b)
- return false;
- return m.cmpFnCallInput(rhs.m);
-#endif
-}
-
State::FnCallOutput State::FnCallOutput::mkIf(const expr &cond,
const FnCallOutput &a,
const FnCallOutput &b) {
@@ -737,10 +718,6 @@ expr State::FnCallOutput::operator==(const FnCallOutput &rhs) const {
return ret;
}
-bool State::FnCallOutput::operator<(const FnCallOutput &rhs) const {
- return tie(retvals, ub, callstate) < tie(rhs.retvals, rhs.ub, rhs.callstate);
-}
-
vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<Memory::PtrInput> &&ptr_inputs,
@@ -762,10 +739,12 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return vector<StateValue>(out_types.size());
}
+ if (writes_memory) {
for (auto &v : ptr_inputs) {
if (!v.byval && !v.nocapture && !v.val.non_poison.isFalse())
memory.escapeLocalPtr(v.val.value);
}
+ }
vector<StateValue> retval;
@@ -785,8 +764,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
if (inserted) {
auto mk_val = [&](const Type &t, const string &name) {
return t.isPtrType()
- // TODO: remove 2nd ret val of mkFnRet
- ? memory.mkFnRet(name.c_str(), I->first.args_ptr).first
+ ? memory.mkFnRet(name.c_str(), I->first.args_ptr)
: expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
};
@@ -803,7 +781,8 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
I->second
= { move(values), expr::mkFreshVar(ub_name.c_str(), false),
writes_memory
- ? memory.mkCallState(argmemonly ? &I->first.args_ptr : nullptr,
+ ? memory.mkCallState(name,
+ argmemonly ? &I->first.args_ptr : nullptr,
attrs.has(FnAttrs::NoFree))
: Memory::CallState() };
@@ -811,7 +790,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
for (auto II = calls_fn.begin(), E = calls_fn.end(); II != E; ++II) {
if (II == I)
continue;
- fn_call_pre &= (I->first == II->first).implies(I->second == II->second);
+ auto in_eq = I->first == II->first;
+ if (!in_eq.isFalse())
+ fn_call_pre &= in_eq.implies(I->second == II->second);
}
}

MODIFY
ir/state.h
ir/state.h
@@ -147,7 +147,7 @@ private:
const ValueAnalysis::FnCallRanges &fncall_ranges,
const Memory &m, bool readsmem, bool argmemonly) const;
- bool operator<(const FnCallInput &rhs) const;
+ auto operator<=>(const FnCallInput &rhs) const = default;
};
struct FnCallOutput {
@@ -158,7 +158,7 @@ private:
static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then,
const FnCallOutput &els);
smt::expr operator==(const FnCallOutput &rhs) const;
- bool operator<(const FnCallOutput &rhs) const;
+ auto operator<=>(const FnCallOutput &rhs) const = default;
};
std::map<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;
smt::expr fn_call_pre = true;

MODIFY
ir/state_value.cpp
ir/state_value.cpp
@@ -77,10 +77,6 @@ StateValue StateValue::subst(const vector<pair<expr, expr>> &repls) const {
return { then.eq(v1) ? move(els) : move(then), move(np) };
}
-bool StateValue::operator<(const StateValue &rhs) const {
- return tie(value, non_poison) < tie(rhs.value, rhs.non_poison);
-}
-
ostream& operator<<(ostream &os, const StateValue &val) {
return os << val.value << " / " << val.non_poison;
}

MODIFY
ir/state_value.h
ir/state_value.h
@@ -36,8 +36,7 @@ struct StateValue {
StateValue
subst(const std::vector<std::pair<smt::expr, smt::expr>> &repls) const;
- // for container use only
- bool operator<(const StateValue &rhs) const;
+ auto operator<=>(const StateValue &rhs) const = default;
friend std::ostream& operator<<(std::ostream &os, const StateValue &val);
};

MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -18,7 +18,7 @@ static void z3_error_handler(Z3_context ctx, Z3_error_code err) {
return;
cerr << "Severe Z3 error: " << str << " [code=" << err << "]\n";
- exit(-1);
+ _Exit(-1);
}
namespace smt {

MODIFY
smt/expr.cpp
smt/expr.cpp
#include "util/compiler.h"
#include <algorithm>
#include <cassert>
+#include <climits>
#include <limits>
#include <memory>
#include <string>
@@ -587,6 +588,9 @@ expr expr::operator-(const expr &rhs) const {
}
expr expr::operator*(const expr &rhs) const {
+ uint64_t n, power;
+ if (rhs.isUInt(n) && is_power2(n, &power))
+ return *this << expr::mkUInt(power, rhs.sort());
return binopc(Z3_mk_bvmul, operator*, Z3_OP_BMUL, isOne, isZero);
}
@@ -1485,6 +1489,8 @@ expr expr::extract(unsigned high, unsigned low) const {
return a.extract(high - b_bw, low - b_bw);
if (low == 0)
return a.extract(high - b_bw, 0).concat(b);
+ if (a.isConst())
+ return a.extract(high - b_bw, 0).concat(b.extract(b_bw-1, low));
}
}
{
@@ -1813,6 +1819,35 @@ set<expr> expr::vars(const vector<const expr*> &exprs) {
return result;
}
+set<expr> expr::leafs(unsigned max) const {
+ C();
+ vector<expr> worklist = { *this };
+ unordered_set<Z3_ast> seen;
+ set<expr> ret;
+ do {
+ auto val = move(worklist.back());
+ worklist.pop_back();
+ if (!seen.emplace(val()).second)
+ continue;
+
+ expr cond, then, els;
+ if (val.isIf(cond, then, els)) {
+ worklist.emplace_back(move(then));
+ worklist.emplace_back(move(els));
+ } else {
+ ret.emplace(move(val));
+ }
+
+ if (ret.size() + worklist.size() >= max) {
+ for (auto &v : worklist)
+ ret.emplace(move(v));
+ break;
+ }
+ } while (!worklist.empty());
+
+ return ret;
+}
+
void expr::printUnsigned(ostream &os) const {
os << numeral_string();
}
@@ -1846,14 +1881,9 @@ ostream& operator<<(ostream &os, const expr &e) {
return os << (e.isValid() ? Z3_ast_to_string(ctx(), e()) : "(null)");
}
-bool expr::operator<(const expr &rhs) const {
- if (!isValid()) {
- return rhs.isValid();
- }
- if (!rhs.isValid())
- return false;
- assert((id() == rhs.id()) == eq(rhs));
- return id() < rhs.id();
+strong_ordering expr::operator<=>(const expr &rhs) const {
+ return
+ (isValid() ? id() : UINT_MAX) <=> (rhs.isValid() ? rhs.id() : UINT_MAX);
}
unsigned expr::id() const {
@@ -1864,29 +1894,4 @@ unsigned expr::hash() const {
return Z3_get_ast_hash(ctx(), ast());
}
-
-ExprLeafIterator::ExprLeafIterator(const expr &init)
- : worklist({init}), end(false) {
- ++*this;
-}
-
-void ExprLeafIterator::operator++(void) {
- assert(!end);
- while (!worklist.empty()) {
- val = move(worklist.back());
- worklist.pop_back();
- if (!val.isValid() || !seen.insert(val()).second)
- continue;
-
- expr cond, then, els;
- if (val.isIf(cond, then, els)) {
- worklist.emplace_back(move(then));
- worklist.emplace_back(move(els));
- } else {
- return;
- }
- }
- end = true;
-}
-
}

MODIFY
smt/expr.h
smt/expr.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include <compare>
#include <cstdint>
#include <ostream>
#include <set>
@@ -333,6 +334,8 @@ public:
std::set<expr> vars() const;
static std::set<expr> vars(const std::vector<const expr*> &exprs);
+ std::set<expr> leafs(unsigned max = 64) const;
+
void printUnsigned(std::ostream &os) const;
void printSigned(std::ostream &os) const;
void printHexadecimal(std::ostream &os) const;
@@ -341,7 +344,7 @@ public:
friend std::ostream &operator<<(std::ostream &os, const expr &e);
// for container use only
- bool operator<(const expr &rhs) const;
+ std::strong_ordering operator<=>(const expr &rhs) const;
unsigned id() const;
unsigned hash() const;
@@ -359,34 +362,6 @@ public:
};
-class ExprLeafIterator {
- std::vector<expr> worklist;
- std::unordered_set<Z3_ast> seen;
- expr val;
- bool end;
- ExprLeafIterator() : end(true) {}
- ExprLeafIterator(const expr &init);
-public:
- const expr& operator*() const { return val; }
- void operator++(void);
- bool operator!=(ExprLeafIterator &rhs) const { return end != rhs.end; }
- friend class ExprLeafIteratorHelper;
-};
-
-class ExprLeafIteratorHelper {
- const expr &init;
-public:
- ExprLeafIteratorHelper(const expr &init ) : init(init) {}
- ExprLeafIterator begin() const { return { init }; }
- ExprLeafIterator end() const { return {}; }
-};
-
-// returns set of all possible leaf expressions (best-effort simplification)
-static inline ExprLeafIteratorHelper allExprLeafs(const expr &e) {
- return { e };
-}
-
-
#define mkIf_fold(c, a, b) \
mkIf_fold_fn(c, [&]() { return a; }, [&]() { return b; })

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -187,8 +187,17 @@ FunctionExpr FunctionExpr::simplify() const {
return newfn;
}
-bool FunctionExpr::operator<(const FunctionExpr &rhs) const {
- return tie(fn, default_val) < tie(rhs.fn, rhs.default_val);
+weak_ordering FunctionExpr::operator<=>(const FunctionExpr &rhs) const {
+ if (auto cmp = fn <=> rhs.fn;
+ is_neq(cmp))
+ return cmp;
+
+ // libstdc++'s optional::operator<=> is buggy
+ // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=98842
+ if (default_val && rhs.default_val)
+ return *default_val <=> *rhs.default_val;
+
+ return (bool)default_val <=> (bool)rhs.default_val;
}
ostream& operator<<(ostream &os, const FunctionExpr &f) {

MODIFY
smt/exprs.h
smt/exprs.h
#include "smt/expr.h"
#include "util/compiler.h"
#include <cassert>
+#include <compare>
#include <map>
#include <ostream>
#include <set>
@@ -178,9 +179,9 @@ public:
auto begin() const { return fn.begin(); }
auto end() const { return fn.end(); }
+ bool empty() const { return fn.empty() && !default_val; }
- // for container use only
- bool operator<(const FunctionExpr &rhs) const;
+ std::weak_ordering operator<=>(const FunctionExpr &rhs) const;
friend std::ostream& operator<<(std::ostream &os, const FunctionExpr &e);
};

port some misc improvements from the new memory branch