From aa40316268eaecfd7b68c0031324e348369c521e Mon Sep 17 00:00:00 2001 From: nikolajbjorner Date: Thu, 19 Feb 2015 19:09:12 -0800 Subject: [PATCH] rewrite terminology for policheck Signed-off-by: nikolajbjorner --- src/api/api_interp.cpp | 12 ++++++------ src/api/java/Solver.java | 10 +++++----- src/duality/duality_rpfp.cpp | 14 +++++++------- src/interp/iz3scopes.cpp | 2 +- src/sat/sat_clause.cpp | 2 ++ 5 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index dd689dcb0..38d726761 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -293,10 +293,10 @@ extern "C" { else { model_ref _m; m_solver.get()->get_model(_m); - Z3_model_ref *crap = alloc(Z3_model_ref); - crap->m_model = _m.get(); - mk_c(c)->save_object(crap); - *model = of_model(crap); + Z3_model_ref *tmp_val = alloc(Z3_model_ref); + tmp_val->m_model = _m.get(); + mk_c(c)->save_object(tmp_val); + *model = of_model(tmp_val); } *out_interp = of_ast_vector(v); @@ -490,8 +490,8 @@ extern "C" { try { std::string foo(filename); if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ - Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); - Z3_app app = Z3_to_app(ctx, ass); + Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); + Z3_app app = Z3_to_app(ctx, assrts); int nconjs = Z3_get_app_num_args(ctx, app); assertions.resize(nconjs); for (int k = 0; k < nconjs; k++) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 4b330ff86..db3f46bfd 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -176,9 +176,9 @@ public class Solver extends Z3Object **/ public int getNumAssertions() throws Z3Exception { - ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( + ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); - return ass.size(); + return assrts.size(); } /** @@ -188,12 +188,12 @@ public class Solver extends Z3Object **/ public BoolExpr[] getAssertions() throws Z3Exception { - ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( + ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); - int n = ass.size(); + int n = assrts.size(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject()); + res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject()); return res; } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index e2a5d05dc..eefb3b85f 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1131,10 +1131,10 @@ namespace Duality { } std::vector *cnsts[2] = { &child->getTerms(), &assumptions->getTerms() }; for (unsigned i = 0; i < assumps.size(); i++) { - expr &ass = assumps[i]; - expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass; + expr &as = assumps[i]; + expr alit = (as.is_app() && as.decl().get_decl_kind() == Implies) ? as.arg(0) : as; bool isA = map.find(alit) != map.end(); - cnsts[isA ? 0 : 1]->push_back(ass); + cnsts[isA ? 0 : 1]->push_back(as); } } else @@ -3221,12 +3221,12 @@ done: std::vector assumps, core, conjuncts; AssertEdgeCache(edge,assumps); for(unsigned i = 0; i < edge->Children.size(); i++){ - expr ass = GetAnnotation(edge->Children[i]); + expr as = GetAnnotation(edge->Children[i]); std::vector clauses; - if(!ass.is_true()){ - CollectConjuncts(ass.arg(1),clauses); + if(!as.is_true()){ + CollectConjuncts(as.arg(1),clauses); for(unsigned j = 0; j < clauses.size(); j++) - GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + GetAssumptionLits(as.arg(0) || clauses[j],assumps); } } expr fmla = GetAnnotation(node); diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp index 389a64b6c..9c08a0e31 100755 --- a/src/interp/iz3scopes.cpp +++ b/src/interp/iz3scopes.cpp @@ -165,7 +165,7 @@ scopes::range scopes::range_glb(const range &rng1, const range &rng2){ return bar.first->second; //std::pair::iterator,bool> bar = rt->unique.insert(foo); // const range_lo *baz = &*(bar.first); - // return (range_lo *)baz; // exit const hell + // return (range_lo *)baz; // coerce const } scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){ diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index b5f6521b8..facd2897d 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -19,6 +19,7 @@ Revision History: #include #include"sat_clause.h" #include"z3_exception.h" +#include"trace.h" namespace sat { @@ -173,6 +174,7 @@ namespace sat { } void clause_allocator::del_clause(clause * cls) { + TRACE("sat", tout << "delete: " << cls->id() << " " << cls << "\n";); m_id_gen.recycle(cls->id()); size_t size = clause::get_obj_size(cls->m_capacity); #ifdef _AMD64_