mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

have sat cleaner use a fixed-point

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-10 11:38:35 -08:00
parent 9c318ed304
commit efaab6d8fd
4 changed files with 94 additions and 80 deletions

31
src/api/python/z3/z3.py
View file

@ -482,6 +482,7 @@ def _to_ast_ref(a, ctx):
else:
return _to_expr_ref(a, ctx)
#########################################
#
# Sorts
@ -6664,17 +6665,11 @@ class Solver(Z3PPObject):
def from_file(self, filename):
"""Parse assertions from a file"""
try:
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
def from_string(self, s):
"""Parse assertions from a string"""
try:
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
def cube(self, vars = None):
"""Get set of cubes
@ -7063,17 +7058,11 @@ class Fixedpoint(Z3PPObject):
def parse_string(self, s):
"""Parse rules and queries from a string"""
try:
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
def parse_file(self, f):
"""Parse rules and queries from a file"""
try:
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
def get_rules(self):
"""retrieve rules that have been added to fixedpoint context"""
@ -7410,17 +7399,11 @@ class Optimize(Z3PPObject):
def from_file(self, filename):
"""Parse assertions and objectives from a file"""
try:
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
def from_string(self, s):
"""Parse assertions and objectives from a string"""
try:
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
def assertions(self):
"""Return an AST vector containing all added constraints."""

74
src/ast/datatype_decl_plugin.cpp
View file

@ -143,7 +143,77 @@ namespace datatype {
}
return r;
}
size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); }
size* size::mk_power(size* a1, size* a2) {
return alloc(power, a1, a2);
}
sort_size plus::eval(obj_map<sort, sort_size> const& S) {
rational r(0);
ptr_vector<size> todo;
todo.push_back(m_arg1);
todo.push_back(m_arg2);
while (!todo.empty()) {
size* s = todo.back();
todo.pop_back();
plus* p = dynamic_cast<plus*>(s);
if (p) {
todo.push_back(p->m_arg1);
todo.push_back(p->m_arg2);
}
else {
sort_size sz = s->eval(S);
if (sz.is_infinite()) return sz;
if (sz.is_very_big()) return sz;
r += rational(sz.size(), rational::ui64());
}
}
return sort_size(r);
}
size* plus::subst(obj_map<sort,size*>& S) {
return mk_plus(m_arg1->subst(S), m_arg2->subst(S));
}
sort_size times::eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
return sort_size(r);
}
size* times::subst(obj_map<sort,size*>& S) {
return mk_times(m_arg1->subst(S), m_arg2->subst(S));
}
sort_size power::eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
if (s1.size() == 1) return s1;
if (s2.size() == 1) return s1;
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
return sort_size(r);
}
size* power::subst(obj_map<sort,size*>& S) {
return mk_power(m_arg1->subst(S), m_arg2->subst(S));
}
size* sparam::subst(obj_map<sort, size*>& S) {
return S[m_param];
}
}
namespace decl {
@ -667,7 +737,7 @@ namespace datatype {
continue;
}
ptr_vector<param_size::size> s_add;
ptr_vector<param_size::size> s_add;
for (constructor const* c : d) {
ptr_vector<param_size::size> s_mul;
for (accessor const* a : *c) {

57
src/ast/datatype_decl_plugin.h
View file

@ -132,71 +132,28 @@ namespace datatype {
size* m_arg1, *m_arg2;
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
rational r(0);
ptr_vector<size> todo;
todo.push_back(m_arg1);
todo.push_back(m_arg2);
while (!todo.empty()) {
size* s = todo.back();
todo.pop_back();
plus* p = dynamic_cast<plus*>(s);
if (p) {
todo.push_back(p->m_arg1);
todo.push_back(p->m_arg2);
}
else {
sort_size sz = s->eval(S);
if (sz.is_infinite()) return sz;
if (sz.is_very_big()) return sz;
r += rational(sz.size(), rational::ui64());
}
}
return sort_size(r);
}
size* subst(obj_map<sort,size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override;
};
struct times : public size {
size* m_arg1, *m_arg2;
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
~times() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
return sort_size(r);
}
size* subst(obj_map<sort,size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override;
};
struct power : public size {
size* m_arg1, *m_arg2;
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
~power() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
if (s1.size() == 1) return s1;
if (s2.size() == 1) return s1;
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
return sort_size(r);
}
size* subst(obj_map<sort,size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override;
};
struct sparam : public size {
sort_ref m_param;
sparam(sort_ref& p): m_param(p) {}
~sparam() override {}
size* subst(obj_map<sort,size*>& S) override { return S[m_param]; }
size* subst(obj_map<sort, size*>& S) override;
sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
};
};

12
src/sat/sat_cleaner.cpp
View file

@ -192,10 +192,14 @@ namespace sat {
report rpt(*this);
m_last_num_units = trail_sz;
m_cleanup_counter = 0;
cleanup_watches();
cleanup_clauses(s.m_clauses);
cleanup_clauses(s.m_learned);
s.propagate(false);
do {
trail_sz = s.m_trail.size();
cleanup_watches();
cleanup_clauses(s.m_clauses);
cleanup_clauses(s.m_learned);
s.propagate(false);
}
while (trail_sz < s.m_trail.size());
CASSERT("cleaner_bug", s.check_invariant());
return true;
}