mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge pull request #1473 from waywardmonkeys/vector-reserve
Reserve vector space when possible.
This commit is contained in:
commit
755a1b8c1f
|
@ -507,6 +507,7 @@ namespace Duality {
|
|||
{
|
||||
std::vector<Term> _IndParams;
|
||||
int nargs = t.num_args();
|
||||
_IndParams.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
_IndParams.push_back(t.arg(i));
|
||||
Node *n = new Node(t.decl(),
|
||||
|
|
|
@ -234,6 +234,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(LocalizeRec(e, memo, t.arg(i)));
|
||||
hash_map<func_decl, int>::iterator rit = e->relMap.find(f);
|
||||
|
@ -352,6 +353,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(SubstRec(memo, t.arg(i)));
|
||||
res = f(args.size(), VEC2PTR(args));
|
||||
|
@ -379,6 +381,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(SubstRec(memo, map, t.arg(i)));
|
||||
hash_map<func_decl, func_decl>::iterator it = map.find(f);
|
||||
|
@ -409,6 +412,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(ExtractStores(memo, t.arg(i), cnstrs, renaming));
|
||||
res = f(args.size(), VEC2PTR(args));
|
||||
|
@ -655,6 +659,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(RemoveRedundancyRec(memo, smemo, t.arg(i)));
|
||||
|
||||
|
@ -703,6 +708,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(IneqToEqRec(memo, t.arg(i)));
|
||||
|
||||
|
@ -749,6 +755,7 @@ namespace Duality {
|
|||
res = ctx.constant(name.c_str(), t.get_sort());
|
||||
return res;
|
||||
}
|
||||
args.reserve(nargs);
|
||||
for (int i = 0; i < nargs; i++)
|
||||
args.push_back(SubstRec(memo, t.arg(i)));
|
||||
res = f(args.size(), VEC2PTR(args));
|
||||
|
@ -3308,6 +3315,7 @@ namespace Duality {
|
|||
std::string name = t.decl().name().str() + "_" + string_of_int(n);
|
||||
std::vector<sort> sorts;
|
||||
int nargs = t.num_args();
|
||||
sorts.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
sorts.push_back(t.arg(i).get_sort());
|
||||
return ctx.function(name.c_str(), nargs, VEC2PTR(sorts), t.get_sort());
|
||||
|
@ -3319,8 +3327,9 @@ namespace Duality {
|
|||
name = name.substr(0,name.rfind('_')) + "_" + string_of_int(n);
|
||||
int arity = f.arity();
|
||||
std::vector<sort> domain;
|
||||
domain.reserve(arity);
|
||||
for(int i = 0; i < arity; i++)
|
||||
domain.push_back(f.domain(i));
|
||||
domain.push_back(f.domain(i));
|
||||
return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
|
||||
}
|
||||
|
||||
|
@ -3330,8 +3339,9 @@ namespace Duality {
|
|||
name = name + "_" + string_of_int(n);
|
||||
int arity = f.arity();
|
||||
std::vector<sort> domain;
|
||||
domain.reserve(arity);
|
||||
for(int i = 0; i < arity; i++)
|
||||
domain.push_back(f.domain(i));
|
||||
domain.push_back(f.domain(i));
|
||||
return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
|
||||
}
|
||||
|
||||
|
@ -3355,6 +3365,7 @@ namespace Duality {
|
|||
}
|
||||
int nargs = t.num_args();
|
||||
std::vector<Term> args;
|
||||
args.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args.push_back(ScanBody(memo,t.arg(i),pmap,parms,nodes));
|
||||
res = f(nargs, VEC2PTR(args));
|
||||
|
@ -3403,6 +3414,7 @@ namespace Duality {
|
|||
else {
|
||||
int nargs = t.num_args();
|
||||
std::vector<Term> args;
|
||||
args.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args.push_back(RemoveLabelsRec(memo,t.arg(i),lbls));
|
||||
res = f(nargs, VEC2PTR(args));
|
||||
|
@ -3432,6 +3444,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
if(nargs == 0 && f.get_decl_kind() == Uninterpreted)
|
||||
ls->declare_constant(f); // keep track of background constants
|
||||
for(int i = 0; i < nargs; i++)
|
||||
|
@ -3474,6 +3487,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args.push_back(DeleteBoundRec(memo, level, num, t.arg(i)));
|
||||
res = f(args.size(), VEC2PTR(args));
|
||||
|
@ -3870,6 +3884,7 @@ namespace Duality {
|
|||
void RPFP::AddParamsToNode(Node *node, const std::vector<expr> ¶ms){
|
||||
int arity = node->Annotation.IndParams.size();
|
||||
std::vector<sort> domain;
|
||||
domain.reserve(arity + params.size());
|
||||
for(int i = 0; i < arity; i++)
|
||||
domain.push_back(node->Annotation.IndParams[i].get_sort());
|
||||
for(unsigned i = 0; i < params.size(); i++)
|
||||
|
@ -3936,6 +3951,7 @@ namespace Duality {
|
|||
func_decl fd = SuffixFuncDecl(new_lit,j);
|
||||
int nargs = new_lit.num_args();
|
||||
std::vector<Term> args;
|
||||
args.reserve(nargs);
|
||||
for(int k = 0; k < nargs; k++)
|
||||
args.push_back(new_lit.arg(k));
|
||||
new_lit = fd(nargs, VEC2PTR(args));
|
||||
|
@ -4126,6 +4142,7 @@ namespace Duality {
|
|||
// int idx;
|
||||
std::vector<Term> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args.push_back(ToRuleRec(e, memo, t.arg(i),quants));
|
||||
hash_map<func_decl,int>::iterator rit = e->relMap.find(f);
|
||||
|
|
|
@ -3424,6 +3424,7 @@ namespace Duality {
|
|||
func_decl f = t.decl();
|
||||
std::vector<expr> args;
|
||||
int nargs = t.num_args();
|
||||
args.reserve(nargs);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
args.push_back(AddParamToRels(memo, rmap, p, t.arg(i)));
|
||||
hash_map<func_decl,func_decl>::iterator rit = rmap.find(f);
|
||||
|
|
|
@ -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++)
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -273,6 +273,7 @@ namespace Duality {
|
|||
if (!heads.contains(fd)) {
|
||||
int arity = f.arity();
|
||||
std::vector<expr> args;
|
||||
args.reserve(arity);
|
||||
for (int j = 0; j < arity; j++)
|
||||
args.push_back(_d->ctx.fresh_func_decl("X", f.domain(j))());
|
||||
expr c = implies(_d->ctx.bool_val(false), f(args));
|
||||
|
|
Loading…
Reference in a new issue