From 07d8971ef97bedc658a7fb2f85db86d10c2cfe87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Oct 2025 02:53:13 -0700 Subject: [PATCH] add sketch for incremental algorithm Signed-off-by: Nikolaj Bjorner --- src/smt/smt_arith_value.h | 2 ++ src/smt/theory_finite_set_size.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h index 33f91c2d2..083d3adc8 100644 --- a/src/smt/smt_arith_value.h +++ b/src/smt/smt_arith_value.h @@ -50,5 +50,7 @@ namespace smt { lbool check_lp_feasible(vector> &ineqs, literal_vector &lit_core, enode_pair_vector &eq_core); final_check_status final_check(unsigned ); + lbool check_lp_feasible(vector> &ineqs, literal_vector &lit_core, + enode_pair_vector &eq_core); }; }; diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp index a7a4363bc..2bae076d6 100644 --- a/src/smt/theory_finite_set_size.cpp +++ b/src/smt/theory_finite_set_size.cpp @@ -302,7 +302,7 @@ namespace smt { * Enumerate all satisfying assignments to m_solver for atoms based on |s| * Extract Core from enumeration * Assert Core => |s_i| = sum_ij n_ij for each |s_i| cardinality expression - * NB. Soundness of using Core has not been rigorously established. + * NB. Soundness of using Core has not been rigorously established. * 2. We can check with theory_lra if slack_sums constraints are linear * feasible. If they are we can possibly terminate by extracting a model * If they are infeasible, temporarily strengthen m_solver using the negation of unsat core