From 66b38eac9f2c5ca8edfb2908da7203b1c599e990 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Oct 2019 20:07:55 -0700 Subject: [PATCH] add back dotnet after adding ;*.cs to path Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 2 +- scripts/mk_util.py | 2 +- src/ast/recfun_decl_plugin.h | 3 +- src/ast/rewriter/recfun_replace.h | 1 + src/nlsat/nlsat_solver.cpp | 32 ++++++++++++++++--- .../fd_solver/bounded_int2bv_solver.cpp | 23 ++++++++++--- 6 files changed, 50 insertions(+), 13 deletions(-) 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); + } } };