3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

Investigating std::vector and #5178

This commit is contained in:
Nikolaj Bjorner 2021-04-24 14:50:59 -07:00
parent 385109d484
commit c03fac8390
4 changed files with 19 additions and 8 deletions

View file

@ -34,7 +34,7 @@ public:
void flush() {
SASSERT(b.size() == A.size());
unsigned sz = A.size();
auto sz = A.size();
for (unsigned i = 0; i < sz; i++) {
svector<numeral> & as = A[i];
m.del(b[i]);

View file

@ -133,7 +133,7 @@ namespace polynomial {
/**
\brief Number of distinct factors (not counting multiplicities).
*/
unsigned distinct_factors() const { return m_factors.size(); }
size_t distinct_factors() const { return m_factors.size(); }
/**
\brief Number of distinct factors (counting multiplicities).

View file

@ -39,8 +39,9 @@ namespace opt {
class model_based_opt {
public:
struct var {
unsigned m_id;
unsigned m_id { 0 };
rational m_coeff;
var() {}
var(unsigned id, rational const& c): m_id(id), m_coeff(c) {}
struct compare {
bool operator()(var x, var y) {

View file

@ -53,6 +53,15 @@ Revision History:
// };
//
// Note:
// polynomial.h contains declaration
// typedef svector<numeral> numeral_vector;
// it is crucial that it uses svector and not vector. The destructors on elements of the numeral vector are handled outside.
// Numeral gets instantiated by mpz and mpz does not support copy constructors.
// porting svector to vector is therefore blocked on the semantics of svector being
// copy-constructor free.
//
#include <vector>
template<typename T, bool CallDestructors=true, typename SZ = unsigned>
@ -63,13 +72,14 @@ public:
vector() {}
vector(SZ s) {
// resize(s, T());
// TODO resize(s, T());
}
vector(SZ s, T const& e) {
// resize(s, e);
// TODO resize(s, e);
}
vector(SZ s, T const* e) {
// TODO
}
void reset() { clear(); }
@ -100,11 +110,11 @@ public:
}
void erase(iterator pos) {
// TODO
}
void erase(T const& e) {
// TODO
}
void fill(T const & elem) {
for (auto& e : *this)
@ -133,7 +143,7 @@ public:
}
void append(unsigned n, T const* elems) {
// TODO
}
bool contains(T const & elem) const {