mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Merge pull request #349 from NikolajBjorner/master

Browse source 
add macro for converting std::vectors to pointers (leaking abstraction)
This commit is contained in:
Nikolaj Bjorner 2015-12-01 18:36:16 -08:00
parent 2916f14b40 485ac9c39d
commit 216c1b2989
5 changed files with 50 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
src/duality/duality_rpfp.cpp
View file

@ -206,12 +206,12 @@ namespace Duality {
0, 0,
0, 0,
num_pats, num_pats,
&pats[0], VEC2PTR(pats),
num_no_pats, num_no_pats,
&no_pats[0], VEC2PTR(no_pats),
bound, bound,
&sorts[0], VEC2PTR(sorts),
&names[0], VEC2PTR(names),
new_body); new_body);
return expr(ctx,foo); return expr(ctx,foo);
#endif #endif
@ -244,7 +244,7 @@ namespace Duality {
res = HideVariable(t, e->number); res = HideVariable(t, e->number);
} }
else { else {
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
} }
} }
} }
@ -354,7 +354,7 @@ namespace Duality {
int nargs = t.num_args(); int nargs = t.num_args();
for (int i = 0; i < nargs; i++) for (int i = 0; i < nargs; i++)
args.push_back(SubstRec(memo, t.arg(i))); args.push_back(SubstRec(memo, t.arg(i)));
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
} }
else if (t.is_quantifier()) { else if (t.is_quantifier()) {
std::vector<expr> pats; std::vector<expr> pats;
@ -384,7 +384,7 @@ namespace Duality {
hash_map<func_decl, func_decl>::iterator it = map.find(f); hash_map<func_decl, func_decl>::iterator it = map.find(f);
if (it != map.end()) if (it != map.end())
f = it->second; f = it->second;
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
} }
else if (t.is_quantifier()) { else if (t.is_quantifier()) {
std::vector<expr> pats; std::vector<expr> pats;
@ -411,7 +411,7 @@ namespace Duality {
int nargs = t.num_args(); int nargs = t.num_args();
for (int i = 0; i < nargs; i++) for (int i = 0; i < nargs; i++)
args.push_back(ExtractStores(memo, t.arg(i), cnstrs, renaming)); args.push_back(ExtractStores(memo, t.arg(i), cnstrs, renaming));
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
if (f.get_decl_kind() == Store) { if (f.get_decl_kind() == Store) {
func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort()); func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort());
expr y = fresh(); expr y = fresh();
@ -720,7 +720,7 @@ namespace Duality {
} }
} }
} }
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
} }
else if (t.is_quantifier()) { else if (t.is_quantifier()) {
Term body = IneqToEqRec(memo, t.body()); Term body = IneqToEqRec(memo, t.body());
@ -751,7 +751,7 @@ namespace Duality {
} }
for (int i = 0; i < nargs; i++) for (int i = 0; i < nargs; i++)
args.push_back(SubstRec(memo, t.arg(i))); args.push_back(SubstRec(memo, t.arg(i)));
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
} }
else if (t.is_quantifier()) else if (t.is_quantifier())
res = CloneQuantifier(t, SubstRec(memo, t.body())); res = CloneQuantifier(t, SubstRec(memo, t.body()));
@ -1064,7 +1064,7 @@ namespace Duality {
if (core_size && core) { if (core_size && core) {
std::vector<expr> full_core(alit_stack.size()), core1(n); std::vector<expr> full_core(alit_stack.size()), core1(n);
std::copy(assumptions, assumptions + n, core1.begin()); std::copy(assumptions, assumptions + n, core1.begin());
res = slvr().check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); res = slvr().check(alit_stack.size(), VEC2PTR(alit_stack), core_size, VEC2PTR(full_core));
full_core.resize(*core_size); full_core.resize(*core_size);
if (res == unsat) { if (res == unsat) {
FilterCore(core1, full_core); FilterCore(core1, full_core);
@ -1073,7 +1073,7 @@ namespace Duality {
} }
} }
else else
res = slvr().check(alit_stack.size(), &alit_stack[0]); res = slvr().check(alit_stack.size(), VEC2PTR(alit_stack));
alit_stack.resize(oldsiz); alit_stack.resize(oldsiz);
return res; return res;
} }
@ -1241,7 +1241,7 @@ namespace Duality {
check_result RPFP_caching::CheckCore(const std::vector<Term> &assumps, std::vector<Term> &core){ check_result RPFP_caching::CheckCore(const std::vector<Term> &assumps, std::vector<Term> &core){
core.resize(assumps.size()); core.resize(assumps.size());
unsigned core_size; unsigned core_size;
check_result res = slvr().check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]); check_result res = slvr().check(assumps.size(),(expr *)VEC2PTR(assumps),&core_size, VEC2PTR(core));
if(res == unsat) if(res == unsat)
core.resize(core_size); core.resize(core_size);
else else
@ -1451,13 +1451,13 @@ namespace Duality {
if (underapprox_core) { if (underapprox_core) {
std::vector<expr> unsat_core(us.size()); std::vector<expr> unsat_core(us.size());
unsigned core_size = 0; unsigned core_size = 0;
res = slvr_check(us.size(), &us[0], &core_size, &unsat_core[0]); res = slvr_check(us.size(), VEC2PTR(us), &core_size, VEC2PTR(unsat_core));
underapprox_core->resize(core_size); underapprox_core->resize(core_size);
for (unsigned i = 0; i < core_size; i++) for (unsigned i = 0; i < core_size; i++)
(*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]); (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]);
} }
else { else {
res = slvr_check(us.size(), &us[0]); res = slvr_check(us.size(), VEC2PTR(us));
bool dump = false; bool dump = false;
if (dump) { if (dump) {
std::vector<expr> cnsts; std::vector<expr> cnsts;
@ -1477,7 +1477,7 @@ namespace Duality {
check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){ check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){
// check_result temp1 = slvr_check(); // no idea why I need to do this // check_result temp1 = slvr_check(); // no idea why I need to do this
ClearProofCore(); ClearProofCore();
check_result res = slvr_check(assumps.size(),&assumps[0]); check_result res = slvr_check(assumps.size(), VEC2PTR(assumps));
model mod = slvr().get_model(); model mod = slvr().get_model();
if(!mod.null()) if(!mod.null())
dualModel = mod;; dualModel = mod;;
@ -1939,7 +1939,7 @@ namespace Duality {
else { else {
for (int i = 0; i < nargs; i++) for (int i = 0; i < nargs; i++)
args.push_back(ResolveIte(memo, t.arg(i), lits, done, dont_cares)); args.push_back(ResolveIte(memo, t.arg(i), lits, done, dont_cares));
res = f(args.size(), &args[0]); res = f(args.size(), VEC2PTR(args));
} }
} }
else res = t; else res = t;
@ -1975,7 +1975,7 @@ namespace Duality {
else { else {
for (int i = 0; i < nargs; i++) for (int i = 0; i < nargs; i++)
args.push_back(ElimIteRec(memo, t.arg(i), cnsts)); args.push_back(ElimIteRec(memo, t.arg(i), cnsts));
res = t.decl()(args.size(), &args[0]); res = t.decl()(args.size(), VEC2PTR(args));
} }
} }
else if (t.is_quantifier()) else if (t.is_quantifier())
@ -2762,14 +2762,14 @@ namespace Duality {
} }
// verify // verify
check_result res = s.check(lits.size(),&lits[0]); check_result res = s.check(lits.size(), VEC2PTR(lits));
if(res != unsat){ if(res != unsat){
// add the axioms in the off chance they are useful // add the axioms in the off chance they are useful
const std::vector<expr> &theory = ls->get_axioms(); const std::vector<expr> &theory = ls->get_axioms();
for(unsigned i = 0; i < theory.size(); i++) for(unsigned i = 0; i < theory.size(); i++)
s.add(theory[i]); s.add(theory[i]);
for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something! for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
if(s.check(lits.size(),&lits[0]) == unsat) if(s.check(lits.size(), VEC2PTR(lits)) == unsat)
goto is_unsat; goto is_unsat;
throw "should be unsat"; throw "should be unsat";
} }
@ -2777,7 +2777,7 @@ namespace Duality {
for(unsigned i = 0; i < conjuncts.size(); ){ for(unsigned i = 0; i < conjuncts.size(); ){
std::swap(conjuncts[i],conjuncts.back()); std::swap(conjuncts[i],conjuncts.back());
std::swap(lits[i],lits.back()); std::swap(lits[i],lits.back());
check_result res = s.check(lits.size()-1,&lits[0]); check_result res = s.check(lits.size()-1, VEC2PTR(lits));
if(res != unsat){ if(res != unsat){
std::swap(conjuncts[i],conjuncts.back()); std::swap(conjuncts[i],conjuncts.back());
std::swap(lits[i],lits.back()); std::swap(lits[i],lits.back());
@ -2801,7 +2801,7 @@ namespace Duality {
lits.push_back(!b); lits.push_back(!b);
expr bv = dualModel.eval(b); expr bv = dualModel.eval(b);
if(eq(bv,ctx.bool_val(true))){ if(eq(bv,ctx.bool_val(true))){
check_result res = slvr_check(lits.size(),&lits[0]); check_result res = slvr_check(lits.size(), VEC2PTR(lits));
if(res == unsat) if(res == unsat)
lits.pop_back(); lits.pop_back();
else else
@ -2823,10 +2823,10 @@ namespace Duality {
RedVars(negnodes[i], b, v); RedVars(negnodes[i], b, v);
lits.push_back(!b); lits.push_back(!b);
} }
check_result res = slvr_check(lits.size(),&lits[0]); check_result res = slvr_check(lits.size(), VEC2PTR(lits));
if(res == unsat && posnodes.size()){ if(res == unsat && posnodes.size()){
lits.resize(posnodes.size()); lits.resize(posnodes.size());
res = slvr_check(lits.size(),&lits[0]); res = slvr_check(lits.size(), VEC2PTR(lits));
} }
dualModel = slvr().get_model(); dualModel = slvr().get_model();
#if 0 #if 0
@ -3379,7 +3379,7 @@ namespace Duality {
int nargs = t.num_args(); int nargs = t.num_args();
for(int i = 0; i < nargs; i++) for(int i = 0; i < nargs; i++)
sorts.push_back(t.arg(i).get_sort()); sorts.push_back(t.arg(i).get_sort());
return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort()); return ctx.function(name.c_str(), nargs, VEC2PTR(sorts), t.get_sort());
} }
Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n) Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n)
@ -3390,7 +3390,7 @@ namespace Duality {
std::vector<sort> domain; std::vector<sort> domain;
for(int i = 0; i < arity; i++) 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, &domain[0], f.range()); return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
} }
Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n) Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n)
@ -3401,7 +3401,7 @@ namespace Duality {
std::vector<sort> domain; std::vector<sort> domain;
for(int i = 0; i < arity; i++) 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, &domain[0], f.range()); return ctx.function(name.c_str(), arity, VEC2PTR(domain), f.range());
} }
// Scan the clause body for occurrences of the predicate unknowns // Scan the clause body for occurrences of the predicate unknowns
@ -3426,7 +3426,7 @@ namespace Duality {
std::vector<Term> args; std::vector<Term> args;
for(int i = 0; i < nargs; i++) for(int i = 0; i < nargs; i++)
args.push_back(ScanBody(memo,t.arg(i),pmap,parms,nodes)); args.push_back(ScanBody(memo,t.arg(i),pmap,parms,nodes));
res = f(nargs,&args[0]); res = f(nargs, VEC2PTR(args));
} }
else if (t.is_quantifier()) else if (t.is_quantifier())
res = CloneQuantifier(t,ScanBody(memo,t.body(),pmap,parms,nodes)); res = CloneQuantifier(t,ScanBody(memo,t.body(),pmap,parms,nodes));
@ -3474,7 +3474,7 @@ namespace Duality {
std::vector<Term> args; std::vector<Term> args;
for(int i = 0; i < nargs; i++) for(int i = 0; i < nargs; i++)
args.push_back(RemoveLabelsRec(memo,t.arg(i),lbls)); args.push_back(RemoveLabelsRec(memo,t.arg(i),lbls));
res = f(nargs,&args[0]); res = f(nargs, VEC2PTR(args));
} }
} }
else if (t.is_quantifier()) else if (t.is_quantifier())
@ -3505,7 +3505,7 @@ namespace Duality {
ls->declare_constant(f); // keep track of background constants ls->declare_constant(f); // keep track of background constants
for(int i = 0; i < nargs; i++) for(int i = 0; i < nargs; i++)
args.push_back(SubstBoundRec(memo, subst, level, t.arg(i))); args.push_back(SubstBoundRec(memo, subst, level, t.arg(i)));
res = f(args.size(),&args[0]); res = f(args.size(), VEC2PTR(args));
} }
else if (t.is_quantifier()){ else if (t.is_quantifier()){
int bound = t.get_quantifier_num_bound(); int bound = t.get_quantifier_num_bound();
@ -3545,7 +3545,7 @@ namespace Duality {
int nargs = t.num_args(); int nargs = t.num_args();
for(int i = 0; i < nargs; i++) for(int i = 0; i < nargs; i++)
args.push_back(DeleteBoundRec(memo, level, num, t.arg(i))); args.push_back(DeleteBoundRec(memo, level, num, t.arg(i)));
res = f(args.size(),&args[0]); res = f(args.size(), VEC2PTR(args));
} }
else if (t.is_quantifier()){ else if (t.is_quantifier()){
int bound = t.get_quantifier_num_bound(); int bound = t.get_quantifier_num_bound();
@ -3729,7 +3729,7 @@ namespace Duality {
Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
} }
#endif #endif
Node *node = CreateNode(R(Indparams.size(),&Indparams[0])); Node *node = CreateNode(R(Indparams.size(),VEC2PTR(Indparams)));
//nodes.push_back(node); //nodes.push_back(node);
pmap[R] = node; pmap[R] = node;
if (is_query) if (is_query)
@ -4007,7 +4007,7 @@ namespace Duality {
std::vector<Term> args; std::vector<Term> args;
for(int k = 0; k < nargs; k++) for(int k = 0; k < nargs; k++)
args.push_back(new_lit.arg(k)); args.push_back(new_lit.arg(k));
new_lit = fd(nargs,&args[0]); new_lit = fd(nargs, VEC2PTR(args));
in_edge->F.RelParams[j] = fd; in_edge->F.RelParams[j] = fd;
hash_map<ast,expr> map; hash_map<ast,expr> map;
map[lit] = new_lit; map[lit] = new_lit;
@ -4201,10 +4201,10 @@ namespace Duality {
if(rit != e->relMap.end()){ if(rit != e->relMap.end()){
Node* child = e->Children[rit->second]; Node* child = e->Children[rit->second];
FuncDecl op = child->Name; FuncDecl op = child->Name;
res = op(args.size(),&args[0]); res = op(args.size(), VEC2PTR(args));
} }
else { else {
res = f(args.size(),&args[0]); res = f(args.size(), VEC2PTR(args));
if(nargs == 0 && t.decl().get_decl_kind() == Uninterpreted) if(nargs == 0 && t.decl().get_decl_kind() == Uninterpreted)
quants.push_back(t); quants.push_back(t);
} }

2
src/duality/duality_solver.cpp
View file

@ -3457,7 +3457,7 @@ namespace Duality {
arg_sorts.push_back(params[j].get_sort()); arg_sorts.push_back(params[j].get_sort());
arg_sorts.push_back(ctx.int_sort()); arg_sorts.push_back(ctx.int_sort());
std::string new_name = std::string("@db@") + node->Name.name().str(); std::string new_name = std::string("@db@") + node->Name.name().str();
func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), &arg_sorts[0],ctx.bool_sort()); func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), VEC2PTR(arg_sorts),ctx.bool_sort());
std::vector<expr> args = params; std::vector<expr> args = params;
args.push_back(dvar); args.push_back(dvar);
expr pat = f(args); expr pat = f(args);

21
src/duality/duality_wrapper.cpp
View file

@ -120,7 +120,7 @@ namespace Duality {
a.resize(args.size()); a.resize(args.size());
for(unsigned i = 0; i < args.size(); i++) for(unsigned i = 0; i < args.size(); i++)
a[i] = to_expr(args[i].raw()); a[i] = to_expr(args[i].raw());
return make(op,args.size(), args.size() ? &a[0] : 0); return make(op,args.size(), args.size() ? VEC2PTR(a) : 0);
} }
expr context::make(decl_kind op){ expr context::make(decl_kind op){
@ -165,11 +165,11 @@ namespace Duality {
bound_asts.push_back(a); bound_asts.push_back(a);
} }
expr_ref abs_body(m()); expr_ref abs_body(m());
expr_abstract(m(), 0, num_bound, &bound_asts[0], to_expr(body.raw()), abs_body); expr_abstract(m(), 0, num_bound, VEC2PTR(bound_asts), to_expr(body.raw()), abs_body);
expr_ref result(m()); expr_ref result(m());
result = m().mk_quantifier( result = m().mk_quantifier(
op == Forall, op == Forall,
names.size(), &types[0], &names[0], abs_body.get(), names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(),
0, 0,
::symbol(), ::symbol(),
::symbol(), ::symbol(),
@ -195,7 +195,7 @@ namespace Duality {
expr_ref result(m()); expr_ref result(m());
result = m().mk_quantifier( result = m().mk_quantifier(
op == Forall, op == Forall,
names.size(), &types[0], &names[0], to_expr(body.raw()), names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()),
0, 0,
::symbol(), ::symbol(),
::symbol(), ::symbol(),
@ -305,7 +305,7 @@ namespace Duality {
std::vector< ::expr *> _args(n); std::vector< ::expr *> _args(n);
for(unsigned i = 0; i < n; i++) for(unsigned i = 0; i < n; i++)
_args[i] = to_expr(args[i].raw()); _args[i] = to_expr(args[i].raw());
return ctx().cook(m().mk_app(to_func_decl(raw()),n,&_args[0])); return ctx().cook(m().mk_app(to_func_decl(raw()),n,VEC2PTR(_args)));
} }
int solver::get_num_decisions(){ int solver::get_num_decisions(){
@ -377,7 +377,7 @@ namespace Duality {
std::vector< ::expr *> _patterns(num_patterns); std::vector< ::expr *> _patterns(num_patterns);
for(unsigned i = 0; i < num_patterns; i++) for(unsigned i = 0; i < num_patterns; i++)
_patterns[i] = to_expr(patterns[i].raw()); _patterns[i] = to_expr(patterns[i].raw());
return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw()))); return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, VEC2PTR(_patterns), to_expr(b.raw())));
} }
expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){ expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
@ -414,7 +414,7 @@ namespace Duality {
_domain[i] = to_sort(domain[i].raw()); _domain[i] = to_sort(domain[i].raw());
::func_decl* d = m().mk_fresh_func_decl(prefix, ::func_decl* d = m().mk_fresh_func_decl(prefix,
_domain.size(), _domain.size(),
&_domain[0], VEC2PTR(_domain),
to_sort(range.raw())); to_sort(range.raw()));
return func_decl(*this,d); return func_decl(*this,d);
} }
@ -453,16 +453,15 @@ namespace Duality {
lb = Z3_interpolate( lb = Z3_interpolate(
ctx(), ctx(),
_assumptions.size(), _assumptions.size(),
&_assumptions[0], VEC2PTR(_assumptions),
0, 0,
0, 0,
&_interpolants[0], VEC2PTR(_interpolants),
&_model, &_model,
&_labels, &_labels,
incremental, incremental,
_theory.size(), _theory.size(),
&_theory[0] VEC2PTR(_theory));
);
if(lb == Z3_L_FALSE){ if(lb == Z3_L_FALSE){
interpolants.resize(_interpolants.size()); interpolants.resize(_interpolants.size());

6
src/duality/duality_wrapper.h
View file

@ -891,7 +891,7 @@ namespace Duality {
_assumptions[i] = to_expr(assumptions[i]); _assumptions[i] = to_expr(assumptions[i]);
} }
the_model = 0; the_model = 0;
lbool r = m_solver->check_sat(n,&_assumptions[0]); lbool r = m_solver->check_sat(n, VEC2PTR(_assumptions));
if(core_size && core){ if(core_size && core){
ptr_vector< ::expr> _core; ptr_vector< ::expr> _core;
@ -1182,7 +1182,7 @@ namespace Duality {
std::vector< ::sort *> sv(arity); std::vector< ::sort *> sv(arity);
for(unsigned i = 0; i < arity; i++) for(unsigned i = 0; i < arity; i++)
sv[i] = domain[i]; sv[i] = domain[i];
::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range); ::func_decl* d = m().mk_func_decl(name,arity, VEC2PTR(sv),range);
return func_decl(*this,d); return func_decl(*this,d);
} }
@ -1227,7 +1227,7 @@ namespace Duality {
inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); } inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
inline expr func_decl::operator()(const std::vector<expr> &args) const { inline expr func_decl::operator()(const std::vector<expr> &args) const {
return operator()(args.size(),&args[0]); return operator()(args.size(), VEC2PTR(args));
} }
inline expr func_decl::operator()() const { inline expr func_decl::operator()() const {
return operator()(0,0); return operator()(0,0);

1
src/util/util.h
View file

@ -59,6 +59,7 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8);
#define SPRINTF sprintf #define SPRINTF sprintf
#endif #endif
#define VEC2PTR(_x_) ((_x_).size() ? &(_x_)[0] : 0)
#ifdef _WINDOWS #ifdef _WINDOWS
// Disable thread local declspec as it seems to not work downlevel. // Disable thread local declspec as it seems to not work downlevel.