fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419

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

src/cmd_context/cmd_context.cpp

@@ -44,6 +44,7 @@ Notes:
 #include"model_v2_pp.h"
 #include"model_params.hpp"
 #include"th_rewriter.h"
+#include"tactic_exception.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -1463,7 +1464,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             throw ex;
         }
         catch (z3_exception & ex) {
-            throw cmd_exception(ex.msg());
+            m_solver->set_reason_unknown(ex.msg());
+            r = l_undef;
         }
         m_solver->set_status(r);
     }

src/opt/opt_context.cpp

@@ -132,7 +132,8 @@ namespace opt {
         m_objective_refs(m),
         m_enable_sat(false),
         m_is_clausal(false),
-        m_pp_neat(false)
+        m_pp_neat(false),
+        m_unknown("unknown")
     {
         params_ref p;
         p.set_bool("model", true);
@@ -487,7 +488,7 @@ namespace opt {
         if (m_solver.get()) {
             return m_solver->reason_unknown();
         }
-        return std::string("unknown"); 
+        return m_unknown;
     }
 
     void context::display_bounds(std::ostream& out, bounds_t const& b) const {

src/opt/opt_context.h

@@ -163,6 +163,7 @@ namespace opt {
         symbol                       m_maxsat_engine;
         symbol                       m_logic;
         svector<symbol>              m_labels;
+        std::string                  m_unknown;
     public:
         context(ast_manager& m);
         virtual ~context();
@@ -184,6 +185,7 @@ namespace opt {
         virtual void get_labels(svector<symbol> & r);
         virtual void get_unsat_core(ptr_vector<expr> & r) {}
         virtual std::string reason_unknown() const;
+        virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }
 
         virtual void display_assignment(std::ostream& out);
         virtual bool is_pareto() { return m_pareto.get() != 0; }

src/opt/opt_solver.cpp

@@ -290,6 +290,10 @@ namespace opt {
     std::string opt_solver::reason_unknown() const {
         return m_context.last_failure_as_string();
     }
+
+    void opt_solver::set_reason_unknown(char const* msg) {
+        m_context.set_reason_unknown(msg);
+    }
     
     void opt_solver::get_labels(svector<symbol> & r) {
         r.reset();

src/opt/opt_solver.h

@@ -99,6 +99,7 @@ namespace opt {
         virtual void get_model(model_ref & _m);        
         virtual proof * get_proof();
         virtual std::string reason_unknown() const;
+        virtual void set_reason_unknown(char const* msg);
         virtual void get_labels(svector<symbol> & r);
         virtual void set_progress_callback(progress_callback * callback);
         virtual unsigned get_num_assertions() const;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -60,6 +60,8 @@ class inc_sat_solver : public solver {
     model_converter_ref m_mc2;   
     expr_dependency_ref m_dep_core;
     svector<double>     m_weights;
+    std::string         m_unknown;
+
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
@@ -73,7 +75,8 @@ public:
         m_map(m),
         m_bb_rewriter(m, p),
         m_num_scopes(0), 
-        m_dep_core(m) {
+        m_dep_core(m),
+        m_unknown("no reason given") {
         m_params.set_bool("elim_vars", false);
         m_solver.updt_params(m_params);
         params_ref simp2_p = p;
@@ -243,8 +246,12 @@ public:
         UNREACHABLE();
         return 0;
     }
+    
     virtual std::string reason_unknown() const {
-        return "no reason given";
+        return m_unknown;
+    }
+    virtual void set_reason_unknown(char const* msg) {
+        m_unknown = msg;
     }
     virtual void get_labels(svector<symbol> & r) {
     }

src/smt/smt_context.cpp

@@ -72,6 +72,7 @@ namespace smt {
         m_not_l(null_literal),
         m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
         m_unsat_proof(m),
+        m_unknown("unknown"),
         m_unsat_core(m),
 #ifdef Z3DEBUG
         m_trail_enabled(true),
@@ -4110,8 +4111,7 @@ namespace smt {
               m_fingerprints.display(tout); 
               );
         failure fl = get_last_search_failure();
-        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
-            // don't generate model.
+        if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS) {
             return;
         }
 
@@ -4126,7 +4126,6 @@ namespace smt {
             if (m_fparams.m_model_compact)
                 m_proto_model->compress();
             TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
-            //SASSERT(validate_model());
         }
     }
 

src/smt/smt_context.h

@@ -71,6 +71,7 @@ namespace smt {
 
         std::ostream& display_last_failure(std::ostream& out) const;
         std::string last_failure_as_string() const;
+        void set_reason_unknown(char const* msg) { m_unknown = msg; }
         void set_progress_callback(progress_callback *callback);
 
 
@@ -197,6 +198,7 @@ namespace smt {
         // -----------------------------------
         proto_model_ref            m_proto_model;
         model_ref                  m_model;
+        std::string                m_unknown;
         void                       mk_proto_model(lbool r);
         struct scoped_mk_model;
 

src/smt/smt_context_pp.cpp

@@ -62,7 +62,7 @@ namespace smt {
     std::string context::last_failure_as_string() const {
         std::string r;
         switch(m_last_search_failure) {
-        case OK: r = "ok"; break;
+        case OK: r = m_unknown; break;
         case TIMEOUT: r = "timeout"; break;
         case MEMOUT: r = "memout"; break;
         case CANCELED: r = "canceled"; break;
@@ -79,7 +79,7 @@ namespace smt {
             break;
         }
         case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
-        case UNKNOWN: r = "incomplete"; break;
+        case UNKNOWN: r = m_unknown; break;
         }
         return r;
     }

src/smt/smt_kernel.cpp

@@ -123,6 +123,10 @@ namespace smt {
             return m_kernel.last_failure_as_string();
         }
 
+        void set_reason_unknown(char const* msg) {
+            m_kernel.set_reason_unknown(msg);
+        }
+
         void get_assignments(expr_ref_vector & result) {
             m_kernel.get_assignments(result);
         }
@@ -284,6 +288,10 @@ namespace smt {
         return m_imp->last_failure_as_string();
     }
 
+    void kernel::set_reason_unknown(char const* msg) {
+        m_imp->set_reason_unknown(msg);
+    }
+
     void kernel::get_assignments(expr_ref_vector & result) {
         m_imp->get_assignments(result);
     }

src/smt/smt_kernel.h

@@ -155,6 +155,12 @@ namespace smt {
         */
         std::string last_failure_as_string() const;
 
+
+        /**
+           \brief Set the reason for unknown.
+        */
+        void set_reason_unknown(char const* msg);
+
         /**
            \brief Return the set of formulas assigned by the kernel.
         */

src/smt/smt_solver.cpp

@@ -95,6 +95,10 @@ namespace smt {
             return m_context.last_failure_as_string();
         }
 
+        virtual void set_reason_unknown(char const* msg) {
+            m_context.set_reason_unknown(msg);
+        }
+
         virtual void get_labels(svector<symbol> & r) {
             buffer<symbol> tmp;
             m_context.get_relevant_labels(0, tmp);

src/smt/theory_seq.cpp

@@ -221,6 +221,11 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>propagate_automata\n";);
         return FC_CONTINUE;
     }
+    if (!check_extensionality()) {
+        ++m_stats.m_extensionality;
+        TRACE("seq", tout << ">>extensionality\n";);
+        return FC_CONTINUE;
+    }
     if (is_solved()) {
         TRACE("seq", tout << ">>is_solved\n";);
         return FC_DONE;
@@ -541,6 +546,45 @@ void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
     }
 }
 
+/*
+   \brief Check extensionality (for sequences).
+ */
+bool theory_seq::check_extensionality() {
+    context& ctx = get_context();
+    unsigned sz = get_num_vars();
+    unsigned_vector seqs;
+    bool added_assumption = false;
+    for (unsigned v = 0; v < sz; ++v) {
+        enode* n = get_enode(v);
+        expr* o1 = n->get_owner();
+        if (n != n->get_root()) {
+            continue;
+        }
+        if (!seqs.empty() && ctx.is_relevant(n) && m_util.is_seq(o1) && ctx.is_shared(n)) {
+            dependency* dep = 0;
+            expr_ref e1 = canonize(o1, dep);
+            for (unsigned i = 0; i < seqs.size(); ++i) {
+                enode* n2 = get_enode(seqs[i]);
+                expr* o2 = n2->get_owner();
+                if (m_exclude.contains(o1, o2)) {
+                    continue;
+                }
+                expr_ref e2 = canonize(n2->get_owner(), dep);
+                m_lhs.reset(); m_rhs.reset();
+                bool change = false;
+                if (!m_seq_rewrite.reduce_eq(o1, o2, m_lhs, m_rhs, change)) {
+                    m_exclude.update(o1, o2);
+                    continue;
+                }
+                TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
+                ctx.assume_eq(n, n2);                
+                return false;
+            }
+        }
+        seqs.push_back(v);
+    }
+    return true;
+}
 
 /*
    - Eqs = 0
@@ -1248,6 +1292,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq solve !=", m_stats.m_solve_nqs);
     st.update("seq solve =", m_stats.m_solve_eqs);
     st.update("seq add axiom", m_stats.m_add_axiom);
+    st.update("seq extensionality", m_stats.m_extensionality);
 }
 
 void theory_seq::init_model(expr_ref_vector const& es) {
@@ -1917,18 +1962,18 @@ void theory_seq::add_extract_axiom(expr* e) {
     expr_ref ls(m_util.str.mk_length(s), m);
     expr_ref lx(m_util.str.mk_length(x), m);
     expr_ref le(m_util.str.mk_length(e), m);
-    expr_ref ls_minus_i(mk_sub(ls, i), m);
+    expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
     expr_ref xe = mk_concat(x, e);
     expr_ref zero(m_autil.mk_int(0), m);
 
     literal i_ge_0  = mk_literal(m_autil.mk_ge(i, zero));
     literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
-    literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, ls), zero));
+    literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
     literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
 
     add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
     add_axiom(~i_ge_0, i_ge_ls, mk_eq(lx, i, false));
-    add_axiom(~i_ge_0, i_ge_ls, ~l_ge_ls, mk_eq(le, ls_minus_i, false));
+    add_axiom(~i_ge_0, i_ge_ls, ~li_ge_ls, mk_eq(le, l, false));
     add_axiom(~i_ge_0, i_ge_ls, l_ge_zero, mk_eq(le, zero, false));
 }
 

src/smt/theory_seq.h

@@ -239,6 +239,7 @@ namespace smt {
             unsigned m_solve_nqs;
             unsigned m_solve_eqs;
             unsigned m_add_axiom;
+            unsigned m_extensionality;
         };
         ast_manager&               m;
         dependency_manager         m_dm;
@@ -312,6 +313,7 @@ namespace smt {
         bool check_length_coherence(expr* e);
         bool propagate_length_coherence(expr* e);  
 
+        bool check_extensionality();
         bool solve_eqs(unsigned start);
         bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);

src/solver/check_sat_result.h

@@ -51,6 +51,7 @@ public:
     virtual void get_model(model_ref & m) = 0;
     virtual proof * get_proof() = 0;
     virtual std::string reason_unknown() const = 0;
+    virtual void set_reason_unknown(char const* msg) = 0;
     virtual void get_labels(svector<symbol> & r) = 0;
     virtual ast_manager& get_manager() = 0;
 };
@@ -75,6 +76,7 @@ struct simple_check_sat_result : public check_sat_result {
     virtual proof * get_proof();
     virtual std::string reason_unknown() const;
     virtual void get_labels(svector<symbol> & r);
+    virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }
 };
 
 #endif

src/solver/combined_solver.cpp

@@ -297,6 +297,11 @@ public:
             return m_solver2->reason_unknown();
     }
 
+    virtual void set_reason_unknown(char const* msg) {
+        m_solver1->set_reason_unknown(msg);
+        m_solver2->set_reason_unknown(msg);
+    }
+
     virtual void get_labels(svector<symbol> & r) {
         if (m_use_solver1_results)
             return m_solver1->get_labels(r);

src/solver/tactic2solver.cpp

@@ -65,6 +65,7 @@ public:
     virtual void get_model(model_ref & m);
     virtual proof * get_proof();
     virtual std::string reason_unknown() const;
+    virtual void set_reason_unknown(char const* msg);
     virtual void get_labels(svector<symbol> & r) {}
 
     virtual void set_progress_callback(progress_callback * callback) {}
@@ -225,6 +226,12 @@ std::string tactic2solver::reason_unknown() const {
         return std::string("unknown");
 }
 
+void tactic2solver::set_reason_unknown(char const* msg) {
+    if (m_result.get()) {
+        m_result->set_reason_unknown(msg);
+    }
+}
+
 unsigned tactic2solver::get_num_assertions() const {
     return m_assertions.size();
 }