modulating data-type solver

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

src/ast/datatype_decl_plugin.cpp

@@ -732,7 +732,8 @@ void datatype_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol
 datatype_util::datatype_util(ast_manager & m):
     m_manager(m),
     m_family_id(m.mk_family_id("datatype")),
-    m_asts(m) {
+    m_asts(m),
+    m_start(0) {
 }
 
 datatype_util::~datatype_util() {
@@ -807,11 +808,11 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     // If there is no such constructor, then we select one that 
     //   2) each type T_i is not recursive or contains a constructor that does not depend on T
     ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty);
-    ptr_vector<func_decl>::const_iterator it  = constructors->begin();
-    ptr_vector<func_decl>::const_iterator end = constructors->end();
     // step 1)
-    for (; it != end; ++it) {
+    unsigned sz = constructors->size();
-        func_decl * c = *it;
+    ++m_start;
+    for (unsigned j = 0; j < sz; ++j) {        
+        func_decl * c = (*constructors)[(j + m_start) % sz];
         unsigned num_args = c->get_arity();
         unsigned i = 0;
         for (; i < num_args; i++) {
@@ -823,9 +824,8 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
             return c;
     }
     // step 2)
-    it  = constructors->begin();
+    for (unsigned j = 0; j < sz; ++j) {        
-    for (; it != end; ++it) {
+        func_decl * c = (*constructors)[(j + m_start) % sz];
-        func_decl * c = *it;
         TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
         unsigned num_args = c->get_arity();
         unsigned i = 0;
@@ -964,6 +964,7 @@ void datatype_util::reset() {
     std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
     m_vectors.reset();
     m_asts.reset();
+    ++m_start;
 }
 
 /**

src/ast/datatype_decl_plugin.h

@@ -176,7 +176,8 @@ class datatype_util {
     obj_map<sort, bool>                         m_is_enum;
     ast_ref_vector                              m_asts;
     ptr_vector<ptr_vector<func_decl> >          m_vectors;
-    
+    unsigned                                    m_start;
+
     func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
     func_decl * get_constructor(sort * ty, unsigned c_id);
 

src/smt/smt_consequences.cpp

@@ -102,7 +102,7 @@ namespace smt {
         }
     }
 
-    void context::delete_unfixed(obj_map<expr, expr*>& var2val) {
+    void context::delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed) {
         ast_manager& m = m_manager;
         ptr_vector<expr> to_delete;
         obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
@@ -137,14 +137,16 @@ namespace smt {
                 to_delete.push_back(k);
             }
         }
-        IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << to_delete.size() << " num-values: " << var2val.size() << ")\n";);
         for (unsigned i = 0; i < to_delete.size(); ++i) {
             var2val.remove(to_delete[i]);
+            unfixed.push_back(to_delete[i]);
         }
     }
 
     lbool context::get_consequences(expr_ref_vector const& assumptions, 
-                                    expr_ref_vector const& vars, expr_ref_vector& conseq) {
+                                    expr_ref_vector const& vars, 
+                                    expr_ref_vector& conseq, 
+                                    expr_ref_vector& unfixed) {
 
         m_antecedents.reset();
         lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
@@ -168,6 +170,9 @@ namespace smt {
                 trail.push_back(val);
                 var2val.insert(vars[i], val);
             } 
+            else {
+                unfixed.push_back(vars[i]);
+            }
         }
         extract_fixed_consequences(0, var2val, _assumptions, conseq);
         unsigned num_units = assigned_literals().size();
@@ -179,7 +184,6 @@ namespace smt {
         unsigned num_iterations = 0;
         unsigned model_threshold = 2;
         while (!var2val.empty()) {
-            ++num_iterations;
             obj_map<expr,expr*>::iterator it = var2val.begin();
             expr* e = it->m_key;
             expr* val = it->m_value;
@@ -212,22 +216,29 @@ namespace smt {
             }
             if (get_assignment(lit) == l_true) {
                 var2val.erase(e);
+                unfixed.push_back(e);
             }
             else if (get_assign_level(lit) > get_search_level()) {
                 TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";);
                 pop_to_search_lvl();
+                IF_VERBOSE(1, verbose_stream() << "(get-consequences re-iterating)\n";);
                 continue;
             }
             else {
                 TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";);
             }
+            ++num_iterations;
 
             TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";);
-            if (model_threshold <= num_iterations) {
+            if (model_threshold <= num_iterations || num_iterations <= 2) {
-                delete_unfixed(var2val);
+                unsigned num_deleted = unfixed.size();
+                delete_unfixed(var2val, unfixed);
+                num_deleted = unfixed.size() - num_deleted;
                 // The next time we check the model is after 1.5 additional iterations.
                 model_threshold *= 3;
                 model_threshold /= 2;                
+                IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << num_deleted << " num-values: " << var2val.size() << " num-iterations: " << num_iterations << ")\n";);
+
             }
             // repeat until we either have a model with negated literal or 
             // the literal is implied at base.
@@ -242,8 +253,7 @@ namespace smt {
                 conseq.push_back(fml);
                 var2val.erase(e);
                 SASSERT(get_assignment(lit) == l_false);
-            }
+            }        
-        
         }
         end_search();
         return l_true;

src/smt/smt_context.cpp

@@ -3422,7 +3422,6 @@ namespace smt {
     }
 
     lbool context::bounded_search() {
-        SASSERT(!inconsistent());
         unsigned counter = 0;
         
         TRACE("bounded_search", tout << "starting bounded search...\n";);

src/smt/smt_context.h

@@ -1347,7 +1347,7 @@ namespace smt {
         u_map<uint_set> m_antecedents;
         void extract_fixed_consequences(unsigned idx, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
         
-        void delete_unfixed(obj_map<expr, expr*>& var2val);
+        void delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed);
 
         expr_ref antecedent2fml(uint_set const& ante);
 
@@ -1391,7 +1391,7 @@ namespace smt {
 
         lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);        
 
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq);
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
         
         lbool setup_and_check(bool reset_cancel = true);
         

src/smt/smt_kernel.cpp

@@ -99,8 +99,8 @@ namespace smt {
             return m_kernel.check(num_assumptions, assumptions);
         }
 
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
-            return m_kernel.get_consequences(assumptions, vars, conseq);
+            return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
         }
         
         void get_model(model_ref & m) const {
@@ -268,8 +268,8 @@ namespace smt {
         return r;
     }
 
-    lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+    lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
-        return m_imp->get_consequences(assumptions, vars, conseq);
+        return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
     }
 
     void kernel::get_model(model_ref & m) const {

src/smt/smt_kernel.h

@@ -129,7 +129,8 @@ namespace smt {
         /**
            \brief extract consequences among variables.
         */
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq);
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
+                               expr_ref_vector& conseq, expr_ref_vector& unfixed);
 
         /**
            \brief Return the model associated with the last check command.

src/smt/smt_solver.cpp

@@ -68,7 +68,8 @@ namespace smt {
         }
 
         virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
-            return m_context.get_consequences(assumptions, vars, conseq);
+            expr_ref_vector unfixed(m_context.m());
+            return m_context.get_consequences(assumptions, vars, conseq, unfixed);
         }
 
         virtual void assert_expr(expr * t) {

src/smt/theory_datatype.h

@@ -97,6 +97,7 @@ namespace smt {
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual final_check_status final_check_eh();
         virtual void reset_eh();
+        virtual void restart_eh() { m_util.reset(); }
         virtual bool is_shared(theory_var v) const;
     public:
         theory_datatype(ast_manager & m, theory_datatype_params & p);

src/solver/solver.cpp

@@ -69,6 +69,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
         tmp = vars[i];
         val = eval(tmp);
         if (!m.is_value(val)) {
+            // vars[i] is unfixed
             continue;
         }
         if (m.is_bool(tmp) && is_uninterp_const(tmp)) {
@@ -81,6 +82,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
                 lit = m.mk_not(tmp);
             }
             else {
+                // vars[i] is unfixed
                 continue;
             }
             scoped_assumption_push _scoped_push(asms1, nlit);
@@ -89,6 +91,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
             case l_undef: 
                 return is_sat;
             case l_true:
+                // vars[i] is unfixed
                 break;
             case l_false:
                 get_unsat_core(core);
@@ -114,6 +117,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
             case l_undef: 
                 return is_sat;
             case l_true:
+                // vars[i] is unfixed
                 break;
             case l_false:
                 get_unsat_core(core);