diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index ecd269273..0a96fc48c 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -13,7 +13,7 @@ jobs:
strategy:
matrix:
MT:
- cmdLine: 'python scripts/mk_make.py -d --java'
+ cmdLine: 'python scripts/mk_make.py -d --java --dotnet'
ST:
cmdLine: './configure --single-threaded'
steps:
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index aaba85b9d..63b9e96a1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1666,7 +1666,7 @@ class DotNetDLLComponent(Component):
-
+
""" % (version, key, self.to_src_dir)
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 878b5ceaf..07115491b 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -47,6 +47,7 @@ namespace recfun {
class replace {
public:
+ virtual ~replace() {}
virtual void reset() = 0;
virtual void insert(expr* d, expr* r) = 0;
virtual expr_ref operator()(expr* e) = 0;
@@ -197,7 +198,7 @@ namespace recfun {
};
}
- // Varus utils for recursive functions
+ // Various utils for recursive functions
class util {
friend class decl::plugin;
diff --git a/src/ast/rewriter/recfun_replace.h b/src/ast/rewriter/recfun_replace.h
index 5a24e8513..c45cff17b 100644
--- a/src/ast/rewriter/recfun_replace.h
+++ b/src/ast/rewriter/recfun_replace.h
@@ -33,6 +33,7 @@ class recfun_replace : public recfun::replace {
expr_safe_replace m_replace;
public:
recfun_replace(ast_manager& m): m(m), m_replace(m) {}
+ ~recfun_replace() override {}
void reset() override { m_replace.reset(); }
void insert(expr* s, expr* t) override { m_replace.insert(s, t); }
expr_ref operator()(expr* e) override { expr_ref r(m); m_replace(e, r); return r; }
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 4cbc80411..de036a46b 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -104,6 +104,7 @@ namespace nlsat {
id_gen m_cid_gen;
clause_vector m_clauses; // set of clauses
clause_vector m_learned; // set of learned clauses
+ clause_vector m_valids;
unsigned m_num_bool_vars;
atom_vector m_atoms; // bool_var -> atom
@@ -716,11 +717,13 @@ namespace nlsat {
void del_clauses(ptr_vector & cs) {
for (clause* cp : cs)
del_clause(cp);
+ cs.reset();
}
void del_clauses() {
del_clauses(m_clauses);
del_clauses(m_learned);
+ del_clauses(m_valids);
}
// We use a simple heuristic to sort literals
@@ -843,8 +846,19 @@ namespace nlsat {
TRACE("nlsat", display(tout << "violdated clause: ", *c) << "\n";);
}
}
+ for (clause* c : m_valids) {
+ bool found = false;
+ for (literal lit: *c) {
+ literal tlit(tr[lit.var()], lit.sign());
+ found |= checker.value(tlit) == l_true;
+ }
+ if (!found) {
+ IF_VERBOSE(0, display(verbose_stream() << "violdated tautology clause: ", *c) << "\n");
+ TRACE("nlsat", display(tout << "violdated tautology clause: ", *c) << "\n";);
+ }
+ }
+ UNREACHABLE();
}
- VERIFY(r == l_false);
for (bool_var b : tr) {
checker.dec_ref(b);
}
@@ -858,7 +872,7 @@ namespace nlsat {
out << "(check-sat)\n(reset)\n";
}
- clause * mk_clause(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
+ clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
SASSERT(num_lits > 0);
unsigned cid = m_cid_gen.mk();
void * mem = m_allocator.allocate(clause::get_obj_size(num_lits));
@@ -866,6 +880,12 @@ namespace nlsat {
for (unsigned i = 0; i < num_lits; i++)
inc_ref(lits[i]);
inc_ref(a);
+ return cls;
+ }
+
+ clause * mk_clause(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
+ SASSERT(num_lits > 0);
+ clause * cls = mk_clause_core(num_lits, lits, learned, a);
++m_lemma_count;
TRACE("nlsat_sort", display(tout << "mk_clause:\n", *cls) << "\n";);
std::sort(cls->begin(), cls->end(), lit_lt(*this));
@@ -1599,11 +1619,13 @@ namespace nlsat {
}
collect(assumptions, m_clauses);
collect(assumptions, m_learned);
+ del_clauses(m_valids);
if (m_check_lemmas) {
for (clause* c : m_learned) {
- check_lemma(c->size(), c->c_ptr(), false, nullptr);
+ //check_lemma(c->size(), c->c_ptr(), false, nullptr);
}
}
+
#if 0
for (clause* c : m_learned) {
IF_VERBOSE(0, display(verbose_stream() << "KEEP: ", c->size(), c->c_ptr()) << "\n");
@@ -1756,8 +1778,8 @@ namespace nlsat {
tout << "new valid clause:\n";
display(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr()) << "\n";);
- if (false && m_check_lemmas) {
- check_lemma(m_lazy_clause.size(), m_lazy_clause.c_ptr(), true, nullptr);
+ if (m_check_lemmas) {
+ m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.c_ptr(), false, nullptr));
}
DEBUG_CODE({
diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
index 39d1f02b3..33a649194 100644
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@@ -44,6 +44,7 @@ class bounded_int2bv_solver : public solver_na2as {
mutable obj_map m_bv2offset;
mutable bv2int_rewriter_ctx m_rewriter_ctx;
mutable bv2int_rewriter_star m_rewriter;
+ mutable bool m_flushed;
public:
@@ -57,7 +58,8 @@ public:
m_bv_fns(m),
m_int_fns(m),
m_rewriter_ctx(m, p, p.get_uint("max_bv_size", UINT_MAX)),
- m_rewriter(m, m_rewriter_ctx)
+ m_rewriter(m, m_rewriter_ctx),
+ m_flushed(false)
{
solver::updt_params(p);
m_bounds.push_back(alloc(bound_manager, m));
@@ -309,6 +311,7 @@ private:
void flush_assertions() const {
if (m_assertions.empty()) return;
+ m_flushed = true;
bound_manager& bm = *m_bounds.back();
for (expr* a : m_assertions) {
bm(a);
@@ -338,13 +341,23 @@ private:
}
unsigned get_num_assertions() const override {
- flush_assertions();
- return m_solver->get_num_assertions();
+ if (m_flushed) {
+ flush_assertions();
+ return m_solver->get_num_assertions();
+ }
+ else {
+ return m_assertions.size();
+ }
}
expr * get_assertion(unsigned idx) const override {
- flush_assertions();
- return m_solver->get_assertion(idx);
+ if (m_flushed) {
+ flush_assertions();
+ return m_solver->get_assertion(idx);
+ }
+ else {
+ return m_assertions.get(idx);
+ }
}
};