NYI control paths

Author: NikolajBjorner

src/ackermannization/lackr_model_converter_lazy.cpp

@@ -44,6 +44,7 @@ class lackr_model_converter_lazy : public model_converter {
 
     model_converter * translate(ast_translation & translator) override {
         NOT_IMPLEMENTED_YET();
+        return nullptr;
     }
 
     void display(std::ostream & out) override {

src/muz/spacer/spacer_antiunify.cpp

@@ -203,6 +203,7 @@ class ncc_less_than_key
 bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m,
                                            expr_ref& result) {
     NOT_IMPLEMENTED_YET();
+    return false;
 #if 0
     arith_util util(m);
 

src/smt/asserted_formulas.cpp

@@ -138,7 +138,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
     //m_params.set_bool("expand_nested_stores", true);
     m_params.set_bool("bv_sort_ac", true);
     // seq theory solver keeps terms in normal form and has to interact with side-effect of rewriting
-    // m_params.set_bool("coalesce_chars", m_smt_params.m_string_solver != symbol("seq"));
+    m_params.set_bool("coalesce_chars", m_smt_params.m_string_solver != symbol("seq"));
     m_params.set_bool("som", true);
     m_rewriter.updt_params(m_params);
     flush_cache();

src/smt/smt_induction.cpp

@@ -217,11 +217,22 @@ void create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs)
  * lit & a.eqs() => alpha
  * lit & a.eqs() & is-c(t) => ~beta
  *
- * where alpha = a.term()
+ * where 
+ *       lit   = is a formula containing t
+ *       alpha = a.term(), a variant of lit 
+ *               with some occurrences of t replaced by sk
  *       beta  = alpha[sk/access_k(sk)]
  * for each constructor c, that is recursive 
  * and contains argument of datatype sort s
  *
+ * The main claim is that the lemmas are valid and that
+ * they approximate induction reasoning.
+ * 
+ * alpha approximates minimal instance of the datatype s where 
+ * the instance of s is true. In the limit one can
+ * set beta to all instantiations of smaller values than sk.
+ * 
+ * 
  * TBD: consider k-inductive lemmas.
  */
 void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, literal lit) {

src/smt/theory_seq.cpp

@@ -1050,9 +1050,6 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps)  {
     }
     m_new_solution = true;
     m_rep.update(l, r, deps);
-    expr_ref sl(l, m);
-    m_rewrite(sl);
-    m_rep.update(sl, r, deps);
     enode* n1 = ensure_enode(l);
     enode* n2 = ensure_enode(r);    
     TRACE("seq", tout << mk_bounded_pp(l, m, 2) << " ==> " << mk_bounded_pp(r, m, 2) << "\n"; display_deps(tout, deps);

src/solver/solver_na2as.h

@@ -49,7 +49,7 @@ class solver_na2as : public solver {
     lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
 protected:
     virtual lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) = 0;
-    virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) { NOT_IMPLEMENTED_YET(); }
+    virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) { NOT_IMPLEMENTED_YET(); return l_undef; }
     virtual void push_core() = 0;
     virtual void pop_core(unsigned n) = 0;
 };

src/tactic/sls/sls_tracker.h

@@ -638,8 +638,10 @@ class sls_tracker {
             return get_random_bv(s);
         else if (m_manager.is_bool(s))
             return m_mpz_manager.dup(get_random_bool());
-        else
+        else {
             NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
+            return get_random_bv(nullptr);
+        }
     }    
 
     void randomize(ptr_vector<expr> const & as) {
@@ -962,8 +964,10 @@ class sls_tracker {
             return score_bool(n);
         else if (m_bv_util.is_bv(n))
             return score_bv(n);
-        else
+        else {
             NOT_IMPLEMENTED_YET();
+            return 0;
+        }
     }    
 
     ptr_vector<func_decl> & get_constants(expr * e) {