expose incremental cubing over API

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

scripts/mk_util.py

@@ -2735,6 +2735,7 @@ def get_header_files_for_components(component_src_dirs):
 def mk_install_tactic_cpp(cnames, path):
     component_src_dirs = []
     for cname in cnames:
+        print("Component %s" % cname)
         c = get_component(cname)
         component_src_dirs.append(c.src_dir)
     h_files_full_path = get_header_files_for_components(component_src_dirs)

src/api/python/z3/z3.py

@@ -6294,10 +6294,33 @@ class Solver(Z3PPObject):
             candidates = _cs
         return _to_expr_ref(Z3_solver_lookahead(self.ctx.ref(), self.solver, candidates), self.ctx)        
 
+    def cube(self):
+        """Get set of cubes"""
+        rounds = 0
+        while True:
+            r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver), self.ctx)
+            if (is_false(r)):
+                if (rounds == 0):
+                    yield r
+                return
+            if (is_true(r)):
+                yield r
+                return
+            rounds += 1
+            yield r
+
     def proof(self):
         """Return a proof for the last `check()`. Proof construction must be enabled."""
         return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
 
+    def from_file(self, filename):
+        """Parse assertions from a file"""
+        self.add([f for f in parse_smt2_file(filename)])
+
+    def from_string(self, s):
+        """Parse assertions from a string"""
+        self.add([f for f in parse_smt2_string(s)])
+        
     def assertions(self):
         """Return an AST vector containing all added constraints.
 

src/sat/sat_lookahead.cpp

@@ -657,7 +657,6 @@ namespace sat {
             }
             // case watched::EXTERNAL:
             }
-            // std::cout << "tsum: " << tsum << "\n";
         }
 #endif
         // std::cout << "sum: " << sum << " afactor " << afactor << " sqfactor " << sqfactor << " tsum " << tsum << "\n";
@@ -2221,7 +2220,7 @@ namespace sat {
         SASSERT(dl_no_overflow(base));
         unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1);            
         scoped_level _sl(*this, dl_truth);
-        IF_VERBOSE(2, verbose_stream() << "double: " << l << "\n";);
+        IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";);
         init_lookahead_reward();
         assign(l);
         propagate();
@@ -2353,63 +2352,24 @@ namespace sat {
     }
 
     lbool lookahead::cube() {
-#if 0
         literal_vector lits;
         while (true) {
             lbool result = cube(lits);
             if (lits.empty() || result != l_undef) {
                 return result;
             }
-            display_cube(std::cout, cube);
+            display_cube(std::cout, lits);
-        }
-#endif
-        lbool result = l_false;
-        init_search();
-        m_model.reset();
-        scoped_level _sl(*this, c_fixed_truth);
-        literal_vector cube;
-        svector<bool> is_decision;
-        m_search_mode = lookahead_mode::searching;
-        double freevars_threshold = 0;
-        while (true) {
-            TRACE("sat", display(tout););
-            inc_istamp();
-            checkpoint();
-            literal l = choose();
-            if (inconsistent()) {
-                TRACE("sat", tout << "inconsistent: " << cube << "\n";);
-                freevars_threshold = m_freevars.size();                
-                if (!backtrack(cube, is_decision)) return result;
-                continue;
-            }
-            if (l == null_literal) {
-                return l_true;
-            }
-            unsigned depth = cube.size();
-            if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
-                (m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) {
-                display_cube(std::cout, cube);
-                freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
-                result = l_undef;
-                set_conflict();
-                if (!backtrack(cube, is_decision)) return result;
-                continue;
-            }
-            TRACE("sat", tout << "choose: " << l << " cube: " << cube << "\n";);
-            ++m_stats.m_decisions;
-            push(l, c_fixed_truth);
-            cube.push_back(l);
-            is_decision.push_back(true);
-            SASSERT(inconsistent() || !is_unsat());
         }
+        return l_undef;
     }
 
     lbool lookahead::cube(literal_vector& lits) {
         lits.reset();
-        bool is_first = (m_cube_state.m_lit == null_literal);
+        bool is_first = m_cube_state.m_first;
         if (is_first) {
             init_search();
             m_model.reset();
+            m_cube_state.m_first = false;
         }        
         scoped_level _sl(*this, c_fixed_truth);
         m_search_mode = lookahead_mode::searching;
@@ -2421,39 +2381,43 @@ namespace sat {
 
         while (true) {
             TRACE("sat", display(tout););
-            inc_istamp();
             checkpoint();
-            m_cube_state.m_lit = choose();
+            inc_istamp();
             if (inconsistent()) {
-                TRACE("sat", tout << "inconsistent: " << cube << "\n";);
+                TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
                 m_cube_state.m_freevars_threshold = m_freevars.size();                
-                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return m_cube_state.m_result;
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
                 continue;
             }
-            if (m_cube_state.m_lit == null_literal) {
+        pick_up_work:
-                return l_true;
-            }
             depth = m_cube_state.m_cube.size();
             if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
                 (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
                 m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
-                m_cube_state.m_result = l_undef;
                 set_conflict();
-                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return m_cube_state.m_result;
                 lits.append(m_cube_state.m_cube);
+                backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
                 return l_undef;
             }
-        pick_up_work:
+            literal lit = choose();
-            TRACE("sat", tout << "choose: " << m_cube_state.m_lit << " cube: " << m_cube_state.m_cube << "\n";);
+            if (inconsistent()) {
+                TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
+                m_cube_state.m_freevars_threshold = m_freevars.size();                
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
+                continue;
+            }
+            if (lit == null_literal) {
+                return l_true;
+            }
+            TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);
             ++m_stats.m_decisions;
-            push(m_cube_state.m_lit, c_fixed_truth);
+            push(lit, c_fixed_truth);
-            m_cube_state.m_cube.push_back(m_cube_state.m_lit);
+            m_cube_state.m_cube.push_back(lit);
             m_cube_state.m_is_decision.push_back(true);
             SASSERT(inconsistent() || !is_unsat());
         }
-        lbool result = m_cube_state.m_result;
         m_cube_state.reset();
-        return result;
+        return l_undef;
     }
 
     void lookahead::init_model() {

src/sat/sat_lookahead.h

@@ -140,17 +140,15 @@ namespace sat {
 #endif
 
         struct cube_state {
+            bool           m_first;
             svector<bool>  m_is_decision;
             literal_vector m_cube;
-            literal        m_lit;
-            lbool          m_result;
             double         m_freevars_threshold;
             cube_state() { reset(); }
             void reset() { 
+                m_first = true;
                 m_is_decision.reset(); 
                 m_cube.reset(); 
-                m_lit = null_literal; 
-                m_result = l_false; 
                 m_freevars_threshold = 0; 
             }
         };

src/sat/sat_params.pyg

@@ -40,7 +40,7 @@ def_module_params('sat',
                           ('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
-                          ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, hs (Heule Schur), heuleu (Heule Unit), or unit'),
+                          ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), or unit'),
                           ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'),
                           ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -345,6 +345,14 @@ public:
         return result;
     }
     virtual expr_ref cube() {
+        if (!m_internalized) {
+            dep2asm_t dep2asm;
+            m_model = 0;
+            lbool r = internalize_formulas();
+            if (r != l_true) return expr_ref(m.mk_true(), m);
+            m_internalized = true;
+        }
+        convert_internalized();
         sat::literal_vector lits;
         lbool result = m_solver.cube(lits);
         if (result == l_false || lits.empty()) {

src/tactic/portfolio/CMakeLists.txt

@@ -18,4 +18,5 @@ z3_add_component(portfolio
     ufbv_tactic
   TACTIC_HEADERS
     default_tactic.h
+    fd_solver.h
 )

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -163,7 +163,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); }
-    virtual expr_ref cube() { return m_solver->cube(); }
+    virtual expr_ref cube() { flush_assertions(); return m_solver->cube(); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

src/tactic/portfolio/fd_solver.h

@@ -29,7 +29,7 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p);
 tactic * mk_fd_tactic(ast_manager & m, params_ref const & p);
 
 /*
-  ADD_TACTIC("qffd",  "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)")
+    ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)")
 */
 
 #endif

src/tactic/portfolio/pb2bv_solver.cpp

@@ -99,7 +99,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); }
-    virtual expr_ref cube() { return m_solver->cube(); }
+    virtual expr_ref cube() { flush_assertions(); return m_solver->cube(); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }    
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {