diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0fac30e35..84931b47e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3076,6 +3076,11 @@ def mk_vs_proj_property_groups(f, name, target_ext, type):
f.write(' Unicode\n')
f.write(' false\n')
f.write(' \n')
+ f.write(' \n')
+ f.write(' %s\n' % type)
+ f.write(' Unicode\n')
+ f.write(' false\n')
+ f.write(' \n')
f.write(' \n')
f.write(' \n')
f.write(' \n')
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 94ce453b4..8028feae6 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -840,7 +840,7 @@ namespace smt {
}
#endif
TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << "\n";);
- TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";);
+ TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";);
set_bool_var(id, v);
m_bdata.reserve(v+1);
m_activity.reserve(v+1);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index d53371c3c..73e427b0b 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1291,7 +1291,9 @@ namespace smt {
IF_VERBOSE(1, verbose_stream()
<< "(smt.pb compile sorting network bound: "
- << k << " literals: " << in.size() << ")\n";);
+ << k << " literals: " << in.size()
+ << " clauses: " << sortnw.m_stats.m_num_compiled_clauses
+ << " vars: " << sortnw.m_stats.m_num_compiled_vars << ")\n";);
// auxiliary clauses get removed when popping scopes.
// we have to recompile the circuit after back-tracking.
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index f8b2f5325..0b136dda7 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -14,7 +14,7 @@ Author:
Nikolaj Bjorner (nbjorner) 2016-10-23
Notes:
-
+
--*/
#include "bounded_int2bv_solver.h"
@@ -76,7 +76,7 @@ public:
virtual solver* translate(ast_manager& m, params_ref const& p) {
return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p));
}
-
+
virtual void assert_expr(expr * t) {
m_assertions.push_back(t);
}
@@ -89,7 +89,7 @@ public:
}
virtual void pop_core(unsigned n) {
- m_assertions.reset();
+ m_assertions.reset();
m_solver->pop(n);
if (n > 0) {
@@ -109,7 +109,7 @@ public:
while (n > 0) {
dealloc(m_bounds.back());
- m_bounds.pop_back();
+ m_bounds.pop_back();
--n;
}
}
@@ -120,25 +120,25 @@ public:
}
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
- virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
+ virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); }
- virtual void get_model(model_ref & mdl) {
+ virtual void get_model(model_ref & mdl) {
m_solver->get_model(mdl);
if (mdl) {
extend_model(mdl);
- filter_model(mdl);
+ filter_model(mdl);
}
- }
+ }
virtual proof * get_proof() { return m_solver->get_proof(); }
virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
virtual void get_labels(svector & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
- virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
- virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+ virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+ virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
flush_assertions();
expr_ref_vector bvars(m);
for (unsigned i = 0; i < vars.size(); ++i) {
@@ -201,7 +201,7 @@ private:
value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
}
TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";);
- ext.insert(it->m_key, value);
+ ext.insert(it->m_key, value);
}
ext(mdl, 0);
}
@@ -224,7 +224,7 @@ private:
if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
func_decl* fbv;
rational offset;
- if (!m_int2bv.find(f, fbv)) {
+ if (!m_int2bv.find(f, fbv)) {
rational n = hi - lo + rational::one();
unsigned num_bits = get_num_bits(n);
expr_ref b(m);
@@ -253,11 +253,11 @@ private:
sub.insert(e, t);
}
else {
- IF_VERBOSE(1,
+ IF_VERBOSE(1,
verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n";
if (bm.has_lower(e, lo, s1)) {
verbose_stream() << "lower: " << lo << " " << s1 << "\n";
- }
+ }
if (bm.has_upper(e, hi, s2)) {
verbose_stream() << "upper: " << hi << " " << s2 << "\n";
});
@@ -284,7 +284,7 @@ private:
bm(m_assertions[i].get());
}
expr_safe_replace sub(m);
- accumulate_sub(sub);
+ accumulate_sub(sub);
proof_ref proof(m);
expr_ref fml1(m), fml2(m);
if (sub.empty()) {
@@ -292,8 +292,12 @@ private:
}
else {
for (unsigned i = 0; i < m_assertions.size(); ++i) {
- sub(m_assertions[i].get(), fml1);
+ sub(m_assertions[i].get(), fml1);
m_rewriter(fml1, fml2, proof);
+ if (m.canceled()) {
+ m_rewriter.reset();
+ return;
+ }
m_solver->assert_expr(fml2);
TRACE("int2bv", tout << fml2 << "\n";);
}
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index b0f11cb91..e89f9d188 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -102,9 +102,20 @@ public:
datatype_util dt(m);
bv_util bv(m);
+ expr_ref_vector bvars(m), conseq(m), bounds(m);
+
+ // ensure that enumeration variables that
+ // don't occur in the constraints
+ // are also internalized.
+ for (unsigned i = 0; i < vars.size(); ++i) {
+ expr_ref tmp(m.mk_eq(vars[i], vars[i]), m);
+ proof_ref proof(m);
+ m_rewriter(tmp, tmp, proof);
+ }
+ m_rewriter.flush_side_constraints(bounds);
+ m_solver->assert_expr(bounds);
// translate enumeration constants to bit-vectors.
- expr_ref_vector bvars(m), conseq(m);
for (unsigned i = 0; i < vars.size(); ++i) {
func_decl* f;
if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {