mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +00:00
Code Activity

rewrite terminology for policheck

Browse source 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
This commit is contained in:
nikolajbjorner 2015-02-19 19:09:12 -08:00
parent 7735a40752
commit aa40316268
5 changed files with 21 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_interp.cpp
View file

@ -293,10 +293,10 @@ extern "C" {
else { else {
model_ref _m; model_ref _m;
m_solver.get()->get_model(_m); m_solver.get()->get_model(_m);
Z3_model_ref *crap = alloc(Z3_model_ref); Z3_model_ref *tmp_val = alloc(Z3_model_ref);
crap->m_model = _m.get(); tmp_val->m_model = _m.get();
mk_c(c)->save_object(crap); mk_c(c)->save_object(tmp_val);
*model = of_model(crap); *model = of_model(tmp_val);
} }
*out_interp = of_ast_vector(v); *out_interp = of_ast_vector(v);
@ -490,8 +490,8 @@ extern "C" {
try { try {
std::string foo(filename); std::string foo(filename);
if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ 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_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
Z3_app app = Z3_to_app(ctx, ass); Z3_app app = Z3_to_app(ctx, assrts);
int nconjs = Z3_get_app_num_args(ctx, app); int nconjs = Z3_get_app_num_args(ctx, app);
assertions.resize(nconjs); assertions.resize(nconjs);
for (int k = 0; k < nconjs; k++) for (int k = 0; k < nconjs; k++)

10
src/api/java/Solver.java
View file

@ -176,9 +176,9 @@ public class Solver extends Z3Object
**/ **/
public int getNumAssertions() throws Z3Exception public int getNumAssertions() throws Z3Exception
{ {
ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
getContext().nCtx(), getNativeObject())); getContext().nCtx(), getNativeObject()));
return ass.size(); return assrts.size();
} }
/** /**
@ -188,12 +188,12 @@ public class Solver extends Z3Object
**/ **/
public BoolExpr[] getAssertions() throws Z3Exception public BoolExpr[] getAssertions() throws Z3Exception
{ {
ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
getContext().nCtx(), getNativeObject())); getContext().nCtx(), getNativeObject()));
int n = ass.size(); int n = assrts.size();
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++) 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; return res;
} }

14
src/duality/duality_rpfp.cpp
View file

@ -1131,10 +1131,10 @@ namespace Duality {
} }
std::vector<expr> *cnsts[2] = { &child->getTerms(), &assumptions->getTerms() }; std::vector<expr> *cnsts[2] = { &child->getTerms(), &assumptions->getTerms() };
for (unsigned i = 0; i < assumps.size(); i++) { for (unsigned i = 0; i < assumps.size(); i++) {
expr &ass = assumps[i]; expr &as = assumps[i];
expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass; expr alit = (as.is_app() && as.decl().get_decl_kind() == Implies) ? as.arg(0) : as;
bool isA = map.find(alit) != map.end(); bool isA = map.find(alit) != map.end();
cnsts[isA ? 0 : 1]->push_back(ass); cnsts[isA ? 0 : 1]->push_back(as);
} }
} }
else else
@ -3221,12 +3221,12 @@ done:
std::vector<expr> assumps, core, conjuncts; std::vector<expr> assumps, core, conjuncts;
AssertEdgeCache(edge,assumps); AssertEdgeCache(edge,assumps);
for(unsigned i = 0; i < edge->Children.size(); i++){ for(unsigned i = 0; i < edge->Children.size(); i++){
expr ass = GetAnnotation(edge->Children[i]); expr as = GetAnnotation(edge->Children[i]);
std::vector<expr> clauses; std::vector<expr> clauses;
if(!ass.is_true()){ if(!as.is_true()){
CollectConjuncts(ass.arg(1),clauses); CollectConjuncts(as.arg(1),clauses);
for(unsigned j = 0; j < clauses.size(); j++) 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); expr fmla = GetAnnotation(node);

2
src/interp/iz3scopes.cpp
View file

@ -165,7 +165,7 @@ scopes::range scopes::range_glb(const range &rng1, const range &rng2){
return bar.first->second; return bar.first->second;
//std::pair<hash_set<scopes::range_lo>::iterator,bool> bar = rt->unique.insert(foo); //std::pair<hash_set<scopes::range_lo>::iterator,bool> bar = rt->unique.insert(foo);
// const range_lo *baz = &*(bar.first); // 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){ scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){

2
src/sat/sat_clause.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include<memory.h> #include<memory.h>
#include"sat_clause.h" #include"sat_clause.h"
#include"z3_exception.h" #include"z3_exception.h"
#include"trace.h"
namespace sat { namespace sat {
@ -173,6 +174,7 @@ namespace sat {
} }
void clause_allocator::del_clause(clause * cls) { void clause_allocator::del_clause(clause * cls) {
TRACE("sat", tout << "delete: " << cls->id() << " " << cls << "\n";);
m_id_gen.recycle(cls->id()); m_id_gen.recycle(cls->id());
size_t size = clause::get_obj_size(cls->m_capacity); size_t size = clause::get_obj_size(cls->m_capacity);
#ifdef _AMD64_ #ifdef _AMD64_