add back dotnet after adding ;*.cs to path

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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:

scripts/mk_util.py

@@ -1666,7 +1666,7 @@ class DotNetDLLComponent(Component):
   </PropertyGroup>
 
   <ItemGroup>
-    <Compile Include="..\%s\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
+    <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
   </ItemGroup>
 
 </Project>""" % (version, key, self.to_src_dir)

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;
         

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; }

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<clause> & 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) {
+            if (m_check_lemmas) {
-                check_lemma(m_lazy_clause.size(), m_lazy_clause.c_ptr(), true, nullptr);
+                m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.c_ptr(), false, nullptr));
             }
 
             DEBUG_CODE({

src/tactic/fd_solver/bounded_int2bv_solver.cpp

@@ -44,6 +44,7 @@ class bounded_int2bv_solver : public solver_na2as {
     mutable obj_map<func_decl, rational>   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();
+        if (m_flushed) {
-        return m_solver->get_num_assertions();
+            flush_assertions();
+            return m_solver->get_num_assertions();
+        }
+        else {
+            return m_assertions.size();
+        }
     }
 
     expr * get_assertion(unsigned idx) const override {
-        flush_assertions();
+        if (m_flushed) {
-        return m_solver->get_assertion(idx);
+            flush_assertions();
+            return m_solver->get_assertion(idx);
+        }
+        else {
+            return m_assertions.get(idx);
+        }
     }
 
 };