diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 0c6e2fae4..a355f8c88 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -2794,9 +2794,9 @@ int main() {
Z3_open_log("z3.log");
#endif
display_version();
- simple_example();
- demorgan();
- find_model_example1();
+ //simple_example();
+ //demorgan();
+ //find_model_example1();
find_model_example2();
prove_example1();
prove_example2();
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 0c79f0393..bd7ce0b3c 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1838,7 +1838,7 @@ namespace pdr {
}
- void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info>& rs) const {
+ void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info>& rs) {
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
for (; it != end; ++it) {
pred_transformer* r = it->m_value;
@@ -1962,7 +1962,7 @@ namespace pdr {
return m_search.get_trace(*this);
}
- expr_ref context::mk_unsat_answer() const {
+ expr_ref context::mk_unsat_answer() {
expr_ref_vector refs(m);
vector<relation_info> rs;
get_level_property(m_inductive_lvl, refs, rs);
@@ -2364,7 +2364,7 @@ namespace pdr {
return result == l_false;
}
- void context::display_certificate(std::ostream& strm) const {
+ void context::display_certificate(std::ostream& strm) {
switch(m_last_result) {
case l_false: {
expr_ref_vector refs(m);
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 54bf5a691..c3567bdd8 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -349,10 +349,10 @@ namespace pdr {
lbool expand_state(model_node& n, expr_ref_vector& cube, bool& uses_level);
void create_children(model_node& n);
expr_ref mk_sat_answer() const;
- expr_ref mk_unsat_answer() const;
+ expr_ref mk_unsat_answer();
// Generate inductive property
- void get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info> & rs) const;
+ void get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info> & rs);
// Initialization
@@ -406,7 +406,7 @@ namespace pdr {
std::ostream& display(std::ostream& strm) const;
- void display_certificate(std::ostream& strm) const;
+ void display_certificate(std::ostream& strm);
lbool solve();
diff --git a/src/muz/pdr/pdr_manager.h b/src/muz/pdr/pdr_manager.h
index 9049e4ca9..580075b78 100644
--- a/src/muz/pdr/pdr_manager.h
+++ b/src/muz/pdr/pdr_manager.h
@@ -181,26 +181,26 @@ namespace pdr {
return m_mux.is_homogenous_formula(f, n_index());
}
- func_decl * o2n(func_decl * p, unsigned o_idx) const {
+ func_decl * o2n(func_decl * p, unsigned o_idx) {
return m_mux.conv(p, o_index(o_idx), n_index());
}
- func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) const {
+ func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) {
return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx));
}
- func_decl * n2o(func_decl * p, unsigned o_idx) const {
+ func_decl * n2o(func_decl * p, unsigned o_idx) {
return m_mux.conv(p, n_index(), o_index(o_idx));
}
- void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) const
+ void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true)
{ m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous); }
- void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) const
+ void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true)
{ m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous); }
- void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) const
+ void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result)
{ m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous); }
- void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous=true) const
+ void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous=true)
{ m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous); }
/**
@@ -237,7 +237,7 @@ namespace pdr {
Increase indexes of state symbols in formula by dist.
The 'N' index becomes 'O' index with number dist-1.
*/
- void formula_shift(expr * src, expr_ref & tgt, unsigned dist) const {
+ void formula_shift(expr * src, expr_ref & tgt, unsigned dist) {
SASSERT(n_index()==0);
SASSERT(o_index(0)==1);
m_mux.shift_formula(src, dist, tgt);
diff --git a/src/muz/pdr/pdr_sym_mux.cpp b/src/muz/pdr/pdr_sym_mux.cpp
index 08b590e16..be20c502d 100644
--- a/src/muz/pdr/pdr_sym_mux.cpp
+++ b/src/muz/pdr/pdr_sym_mux.cpp
@@ -28,7 +28,7 @@ Revision History:
using namespace pdr;
-sym_mux::sym_mux(ast_manager & m, const vector<std::string> & suffixes)
+sym_mux::sym_mux(ast_manager & m, vector<std::string> & suffixes)
: m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes)
{
unsigned suf_sz = m_suffixes.size();
@@ -38,7 +38,7 @@ sym_mux::sym_mux(ast_manager & m, const vector<std::string> & suffixes)
}
}
-std::string sym_mux::get_suffix(unsigned i) const {
+std::string sym_mux::get_suffix(unsigned i) {
while(m_suffixes.size() <= i) {
std::string new_suffix;
symbol new_syffix_sym;
@@ -88,7 +88,7 @@ void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * dom
m_ref_holder.push_back(prefix);
}
-void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const {
+void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) {
SASSERT(m_prim2all.contains(prim));
decl_vector& tuple = m_prim2all.find_core(prim)->get_data().m_value;
SASSERT(tuple[0]==prim);
@@ -98,10 +98,10 @@ void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const {
func_decl * prefix;
TRUSTME(m_prim2prefix.find(prim, prefix));
std::string prefix_name = prefix->get_name().bare_str();
- for(unsigned i=tuple.size(); i<sz; ++i) {
- std::string name = prefix_name+get_suffix(i);
+ for(unsigned i = tuple.size(); i < sz; ++i) {
+ std::string name = prefix_name + get_suffix(i);
func_decl * new_sym = m.mk_func_decl(symbol(name.c_str()), prefix->get_arity(),
- prefix->get_domain(), prefix->get_range());
+ prefix->get_domain(), prefix->get_range());
tuple.push_back(new_sym);
m_ref_holder.push_back(new_sym);
@@ -110,7 +110,7 @@ void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const {
}
}
-func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const
+func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx)
{
if(src_idx==tgt_idx) { return sym; }
func_decl * prim = (src_idx==0) ? sym : get_primary(sym);
@@ -347,12 +347,12 @@ struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg
{
private:
ast_manager & m;
- const sym_mux & m_parent;
+ sym_mux & m_parent;
unsigned m_from_idx;
unsigned m_to_idx;
bool m_homogenous;
public:
- conv_rewriter_cfg(const sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous)
+ conv_rewriter_cfg(sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous)
: m(parent.get_manager()),
m_parent(parent),
m_from_idx(from_idx),
@@ -374,7 +374,7 @@ public:
}
};
-void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous) const
+void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous)
{
if(src_idx==tgt_idx) {
res = f;
@@ -389,10 +389,10 @@ struct sym_mux::shifting_rewriter_cfg : public default_rewriter_cfg
{
private:
ast_manager & m;
- const sym_mux & m_parent;
+ sym_mux & m_parent;
int m_shift;
public:
- shifting_rewriter_cfg(const sym_mux & parent, int shift)
+ shifting_rewriter_cfg(sym_mux & parent, int shift)
: m(parent.get_manager()),
m_parent(parent),
m_shift(shift) {}
@@ -413,7 +413,7 @@ public:
}
};
-void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const
+void sym_mux::shift_formula(expr * f, int dist, expr_ref & res)
{
if(dist==0) {
res = f;
@@ -425,7 +425,7 @@ void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const
}
void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx,
- expr_ref_vector & res) const
+ expr_ref_vector & res)
{
res.reset();
expr * const * begin = vect.c_ptr();
@@ -441,11 +441,11 @@ void sym_mux::filter_idx(expr_ref_vector & vect, unsigned idx) const {
unsigned i = 0;
while (i < vect.size()) {
expr* e = vect[i].get();
- if(contains(e, idx) && is_homogenous_formula(e, idx)) {
+ if (contains(e, idx) && is_homogenous_formula(e, idx)) {
i++;
}
else {
- //we don't allow mixing states inside vector elements
+ // we don't allow mixing states inside vector elements
SASSERT(!contains(e, idx));
vect[i] = vect.back();
vect.pop_back();
@@ -476,23 +476,20 @@ class sym_mux::nonmodel_sym_checker {
bool m_found;
public:
nonmodel_sym_checker(const sym_mux & parent) :
- m_parent(parent), m_found(false)
- {
+ m_parent(parent), m_found(false) {
}
- void operator()(expr * e)
- {
+ void operator()(expr * e) {
if(m_found || !is_app(e)) { return; }
-
+
func_decl * sym = to_app(e)->get_decl();
-
+
if(m_parent.is_non_model_sym(sym)) {
m_found = true;
}
}
- bool found() const
- {
+ bool found() const {
return m_found;
}
};
@@ -504,14 +501,15 @@ bool sym_mux::has_nonmodel_symbol(expr * e) const {
}
void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const {
- unsigned i=0;
- while(i<vect.size()) {
- if(!has_nonmodel_symbol(vect[i].get())) {
+ unsigned i = 0;
+ while (i < vect.size()) {
+ if (!has_nonmodel_symbol(vect[i].get())) {
i++;
- continue;
}
- vect[i] = vect.back();
- vect.pop_back();
+ else {
+ vect[i] = vect.back();
+ vect.pop_back();
+ }
}
}
@@ -526,10 +524,10 @@ public:
bool operator()(func_decl * sym1, func_decl * sym2)
{
unsigned idx1, idx2;
- if(!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; }
- if(!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; }
+ if (!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; }
+ if (!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; }
- if(idx1!=idx2) { return idx1<idx2; }
+ if (idx1 != idx2) { return idx1<idx2; }
return lt(sym1->get_name(), sym2->get_name());
}
};
@@ -545,9 +543,9 @@ std::string sym_mux::pp_model(const model_core & mdl) const {
std::sort(consts.begin(), consts.end(), decl_idx_comparator(*this));
std::stringstream res;
-
+
decl_vector::iterator end = consts.end();
- for(decl_vector::iterator it = consts.begin(); it!=end; it++) {
+ for (decl_vector::iterator it = consts.begin(); it!=end; it++) {
func_decl * d = *it;
std::string name = d->get_name().str();
const char * arrow = " -> ";
@@ -555,11 +553,11 @@ std::string sym_mux::pp_model(const model_core & mdl) const {
unsigned indent = static_cast<unsigned>(name.length() + strlen(arrow));
res << mk_pp(mdl.get_const_interp(d), m, indent) << "\n";
- if(it+1!=end) {
+ if (it+1 != end) {
unsigned idx1, idx2;
- if(!try_get_index(*it, idx1)) { idx1 = UINT_MAX; }
- if(!try_get_index(*(it+1), idx2)) { idx2 = UINT_MAX; }
- if(idx1!=idx2) { res << "\n"; }
+ if (!try_get_index(*it, idx1)) { idx1 = UINT_MAX; }
+ if (!try_get_index(*(it+1), idx2)) { idx2 = UINT_MAX; }
+ if (idx1 != idx2) { res << "\n"; }
}
}
return res.str();
diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h
index 986d961c7..a07b712ca 100644
--- a/src/muz/pdr/pdr_sym_mux.h
+++ b/src/muz/pdr/pdr_sym_mux.h
@@ -46,7 +46,7 @@ private:
mutable unsigned m_next_sym_suffix_idx;
mutable symbols m_used_suffixes;
/** Here we have default suffixes for each of the variants */
- mutable vector<std::string> m_suffixes;
+ vector<std::string> m_suffixes;
/**
@@ -89,12 +89,12 @@ private:
class index_collector;
class variable_collector;
- std::string get_suffix(unsigned i) const;
- void ensure_tuple_size(func_decl * prim, unsigned sz) const;
+ std::string get_suffix(unsigned i);
+ void ensure_tuple_size(func_decl * prim, unsigned sz);
expr_ref isolate_o_idx(expr* e, unsigned idx) const;
public:
- sym_mux(ast_manager & m, const vector<std::string> & suffixes);
+ sym_mux(ast_manager & m, vector<std::string> & suffixes);
ast_manager & get_manager() const { return m; }
@@ -130,7 +130,7 @@ public:
/**
Return symbol created from prefix, or 0 if the prefix was never used.
*/
- func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) const {
+ func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) {
func_decl * prim = try_get_primary_by_prefix(prefix);
if(!prim) {
return 0;
@@ -199,22 +199,22 @@ public:
/**
Convert symbol sym which has to be of src_idx variant into variant tgt_idx.
*/
- func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const;
+ func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx);
/**
Convert src_idx symbols in formula f variant into tgt_idx.
If homogenous is true, formula cannot contain symbols of other variants.
*/
- void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous=true) const;
+ void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous=true);
void conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx,
- expr_ref_vector & res) const;
+ expr_ref_vector & res);
/**
Shifts the muxed symbols in f by dist. Dist can be negative, but it should never shift
symbol index to a negative value.
*/
- void shift_formula(expr * f, int dist, expr_ref & res) const;
+ void shift_formula(expr * f, int dist, expr_ref & res);
/**
Remove from vect literals (atoms or negations of atoms) of symbols
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index fe4822406..279d84375 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -36,6 +36,7 @@ namespace sat {
memcpy(m_lits, lits, sizeof(literal) * sz);
mark_strengthened();
SASSERT(check_approx());
+ SASSERT(sz > 1);
}
var_approx_set clause::approx(unsigned num, literal const * lits) {
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 3495ca1d3..422db07aa 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -32,8 +32,8 @@ protected:
void free_memory() {
if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {
- memory::deallocate(m_buffer);
- }
+ dealloc_svect(m_buffer);
+ }
}
void expand() {
@@ -66,57 +66,57 @@ public:
typedef const T * const_iterator;
buffer():
- m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
- m_pos(0),
- m_capacity(INITIAL_SIZE) {
+ m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+ m_pos(0),
+ m_capacity(INITIAL_SIZE) {
}
-
+
buffer(const buffer & source):
- m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
- m_pos(0),
- m_capacity(INITIAL_SIZE) {
+ m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+ m_pos(0),
+ m_capacity(INITIAL_SIZE) {
unsigned sz = source.size();
for(unsigned i = 0; i < sz; i++) {
push_back(source.m_buffer[i]);
}
}
-
+
buffer(unsigned sz, const T & elem):
- m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
- m_pos(0),
- m_capacity(INITIAL_SIZE) {
+ m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
+ m_pos(0),
+ m_capacity(INITIAL_SIZE) {
for (unsigned i = 0; i < sz; i++) {
push_back(elem);
}
SASSERT(size() == sz);
}
-
+
~buffer() {
destroy();
}
-
+
void reset() {
if (CallDestructors) {
destroy_elements();
}
m_pos = 0;
}
-
+
void finalize() {
destroy();
m_buffer = reinterpret_cast<T *>(m_initial_buffer);
m_pos = 0;
m_capacity = INITIAL_SIZE;
}
-
+
unsigned size() const {
return m_pos;
}
-
+
bool empty() const {
return m_pos == 0;
}
-
+
iterator begin() {
return m_buffer;
}
@@ -130,15 +130,15 @@ public:
if (CallDestructors) {
iterator e = end();
for (; it != e; ++it) {
- it->~T();
+ it->~T();
}
}
}
-
+
const_iterator begin() const {
return m_buffer;
}
-
+
const_iterator end() const {
return m_buffer + size();
}