mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Reserve vector space when possible.

Browse source 
This fixes all current instances of the
`performance-inefficient-vector-operation`
warning in clang-tidy.
This commit is contained in:
Bruce Mitchener 2018-02-06 11:21:17 +07:00
parent b2bd4dd3b4
commit 54b3cd0071
6 changed files with 25 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/interp/iz3interp.cpp
View file

@ -97,6 +97,7 @@ struct frame_reducer : public iz3mgr {
// if multiple children of a tree node are used, we can't delete it
std::vector<int> used_children;
used_children.reserve(frames);
for(int i = 0; i < frames; i++)
used_children.push_back(0);
for(int i = 0; i < frames; i++)

2
src/interp/iz3translate.cpp
View file

@ -1146,6 +1146,7 @@ public:
my_cons.push_back(mk_not(farkas_con));
my_coeffs.push_back(make_int("1"));
std::vector<Iproof::node> my_hyps;
my_hyps.reserve(nargs);
for(int i = 0; i < nargs; i++)
my_hyps.push_back(iproof->make_hypothesis(my_cons[i]));
ast res = iproof->make_farkas(mk_false(),my_hyps,my_cons,my_coeffs);
@ -1203,6 +1204,7 @@ public:
int nargs = num_prems(proof);
if(nargs != (int)(my_coeffs.size()))
throw "bad gomory-cut theory lemma";
my_prem_cons.reserve(nargs);
for(int i = 0; i < nargs; i++)
my_prem_cons.push_back(conc(prem(proof,i)));
ast my_con = normalize_inequality(sum_inequalities(my_coeffs,my_prem_cons));