Merge pull request #8943 from Z3Prover/copilot/update-simple-solver-incremental-mode

nielsen: use simple_solver incrementally with push/pop scopes in DFS

src/smt/seq/seq_nielsen.cpp

@@ -461,6 +461,7 @@ namespace seq {
     nielsen_node* nielsen_graph::mk_child(nielsen_node* parent) {
         nielsen_node* child = mk_node();
         child->clone_from(*parent);
+        child->m_parent_ic_count = parent->int_constraints().size();
         return child;
     }
 
@@ -1720,10 +1721,14 @@ namespace seq {
             return search_result::unsat;
         }
 
-        // integer feasibility check: collect side constraints along the path
+        // Assert any new int_constraints added during simplify_and_init for this
-        // and verify they are jointly satisfiable using the LP solver.
+        // node into the current solver scope. Constraints inherited from the parent
-        // Must run AFTER simplify_and_init (which may add int_constraints)
+        // (indices 0..m_parent_ic_count-1) are already present at the enclosing
-        // and BEFORE the SAT check (equation satisfied doesn't imply ints are feasible).
+        // scope level; only the newly-added tail needs to be asserted here.
+        assert_node_new_int_constraints(node);
+
+        // integer feasibility check: the solver now holds all path constraints
+        // incrementally; just query the solver directly
         if (!cur_path.empty() && !check_int_feasibility(node, cur_path)) {
             node->set_reason(backtrack_reason::arithmetic);
             ++m_stats.m_num_arith_infeasible;
@@ -1762,7 +1767,15 @@ namespace seq {
         bool any_unknown = false;
         for (nielsen_edge* e : node->outgoing()) {
             cur_path.push_back(e);
+            // Push a solver scope for this edge and assert its side integer
+            // constraints.  The child's own new int_constraints will be asserted
+            // inside the recursive call (above).  On return, pop the scope so
+            // that backtracking removes those assertions.
+            m_solver.push();
+            for (auto const& ic : e->side_int())
+                m_solver.assert_expr(int_constraint_to_expr(ic));
             search_result r = search_dfs(e->tgt(), depth + 1, cur_path);
+            m_solver.pop(1);
             if (r == search_result::sat)
                 return search_result::sat;
             cur_path.pop_back();
@@ -3325,41 +3338,22 @@ namespace seq {
         return expr_ref(m.mk_true(), m);
     }
 
-    void nielsen_graph::collect_path_int_constraints(nielsen_node* node,
+    void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) {
-                                                      svector<nielsen_edge*> const& cur_path,
+        // Assert only the int_constraints that are new to this node (beyond those
-                                                      vector<int_constraint>& out) {
+        // inherited from its parent via clone_from).  The parent's constraints are
-        // collect from root node
+        // already present in the enclosing solver scope; asserting them again would
-        if (m_root) {
+        // be redundant (though harmless).  This is called by search_dfs right after
-            for (auto const& ic : m_root->int_constraints())
+        // simplify_and_init, which is where new constraints are produced.
-                out.push_back(ic);
+        for (unsigned i = node->m_parent_ic_count; i < node->int_constraints().size(); ++i)
-        }
+            m_solver.assert_expr(int_constraint_to_expr(node->int_constraints()[i]));
-
-        // collect from edges along the path and their target nodes
-        for (nielsen_edge* e : cur_path) {
-            for (auto const& ic : e->side_int())
-                out.push_back(ic);
-            if (e->tgt()) {
-                for (auto const& ic : e->tgt()->int_constraints())
-                    out.push_back(ic);
-            }
-        }
     }
 
     bool nielsen_graph::check_int_feasibility(nielsen_node* node, svector<nielsen_edge*> const& cur_path) {
-        vector<int_constraint> constraints;
+        // In incremental mode the solver already holds all path constraints
-        collect_path_int_constraints(node, cur_path, constraints);
+        // (root length constraints at the base level, edge side_int and node
-
+        // int_constraints pushed/popped as the DFS descends and backtracks).
-        if (constraints.empty())
+        // A plain check() is therefore sufficient.
-            return true; // no integer constraints, trivially feasible
+        return m_solver.check() != l_false;
-
-
-        m_solver.push();
-        for (auto const& ic : constraints)
-            m_solver.assert_expr(int_constraint_to_expr(ic));
-
-        lbool result = m_solver.check();
-        m_solver.pop(1);
-        return result != l_false;
     }
 
     bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs,
@@ -3368,19 +3362,14 @@ namespace seq {
         ast_manager& m = m_sg.get_manager();
         arith_util arith(m);
 
-        vector<int_constraint> constraints;
+        // The solver already holds all path constraints incrementally.
-        collect_path_int_constraints(node, cur_path, constraints);
+        // Temporarily add NOT(lhs <= rhs), i.e. lhs >= rhs + 1.
-
+        // If that is unsat, then lhs <= rhs is entailed.
-        m_solver.push();
-        for (auto const& ic : constraints)
-            m_solver.assert_expr(int_constraint_to_expr(ic));
-
-        // Assert NOT(lhs <= rhs), i.e., lhs > rhs, i.e., lhs >= rhs + 1
-        // If this is unsat, then lhs <= rhs is entailed by the path constraints.
         expr_ref one(arith.mk_int(1), m);
         expr_ref rhs_plus_one(arith.mk_add(rhs, one), m);
-        m_solver.assert_expr(arith.mk_ge(lhs, rhs_plus_one));
 
+        m_solver.push();
+        m_solver.assert_expr(arith.mk_ge(lhs, rhs_plus_one));
         lbool result = m_solver.check();
         m_solver.pop(1);
         return result == l_false;

src/smt/seq/seq_nielsen.h

@@ -522,6 +522,12 @@ namespace seq {
         // evaluation index for run tracking
         unsigned                m_eval_idx = 0;
 
+        // number of int_constraints inherited from the parent node at clone time.
+        // int_constraints[0..m_parent_ic_count) are already asserted at the
+        // parent's solver scope; only [m_parent_ic_count..end) need to be
+        // asserted when this node's solver scope is entered.
+        unsigned                m_parent_ic_count = 0;
+
     public:
         nielsen_node(nielsen_graph* graph, unsigned id);
 
@@ -954,20 +960,24 @@ namespace seq {
         // Mirrors ZIPT's Constraint.Shared forwarding mechanism.
         void assert_root_constraints_to_solver();
 
-        // collect int_constraints along the path from root to the given node,
+        // Assert the int_constraints of `node` that are new relative to its
-        // including constraints from edges and nodes.
+        // parent (indices [m_parent_ic_count..end)) into the current solver scope.
-        void collect_path_int_constraints(nielsen_node* node,
+        // Called by search_dfs after simplify_and_init so that the newly derived
-                                          svector<nielsen_edge*> const& cur_path,
+        // bounds become visible to subsequent check() and check_lp_le() calls.
-                                          vector<int_constraint>& out);
+        void assert_node_new_int_constraints(nielsen_node* node);
 
         // check integer feasibility of the constraints along the current path.
-        // returns true if feasible, false if infeasible.
+        // returns true if feasible (including unknown), false only if l_false.
+        // Precondition: all path constraints have been incrementally asserted to
+        // m_solver by search_dfs via push/pop, so a plain check() suffices.
+        // l_undef (resource limit / timeout) is treated as feasible so that the
+        // search continues rather than reporting a false unsatisfiability.
         bool check_int_feasibility(nielsen_node* node, svector<nielsen_edge*> const& cur_path);
 
         // check whether lhs <= rhs is implied by the path constraints.
-        // mirrors ZIPT's NielsenNode.IsLe(): collects path constraints,
+        // mirrors ZIPT's NielsenNode.IsLe(): temporarily asserts NOT(lhs <= rhs)
-        // asserts their conjunction plus NOT(lhs <= rhs), and returns true
+        // and returns true iff the result is unsatisfiable (i.e., lhs <= rhs is
-        // iff the result is unsatisfiable (i.e., lhs <= rhs is entailed).
+        // entailed).  Path constraints are already in the solver incrementally.
         bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* node, svector<nielsen_edge*> const& cur_path);
 
         // create an integer constraint: lhs <kind> rhs