Improvements of the OCaml API implementation #3
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This patch avoids the use of physical equality wherever possible and improves some details of the OCaml implementation.
This patch simplifies the implementation of the OCaml bindings. For example, the applyX wrapper functions have become unnecessary in the new OCaml API. It also removes the internal ML2C structure that was used as an intermediate layer between the C and the OCaml layer.
|
This looks good to me except for one thing, which is that all the exception wrappers have been removed. Are those exceptions thrown somewhere else now? |
|
Ah, right, looks like the exception wrappers were pushed down into C some time ago, so they were indeed redundant now, thanks for cleaning this up! |
|
Exactly. I did not see any exception wrapping taking place in the OCaml code... |
wintersteiger
pushed a commit
that referenced
this pull request
Oct 4, 2023
* Make spacer_sem_matcher::reset() public * Add .clang-format for src/muz/spacer * Mark substitution::get_bindings() as const * Fix in spacer_antiunify * Various helper methods in spacer_util Minor functions to compute number of free variables, detect presence of certain sub-expressions, etc. The diff is ugly because of clang-format * Add spacer_cluster for clustering lemmas A cluster of lemmas is a set of lemmas that are all instances of the same pattern, where a pattern is a qff formula with free variables. Currently, the instances are required to be explicit, that is, they are all obtained by substituting concrete values (i.e., numbers) for free variables of the pattern. Lemmas are clustered in cluster_db in each predicate transformer. * Integrate spacer_cluster into spacer_context * Custom clang-format pragmas for spacer_context spacer_context.(cpp|h) are large and have inconsistent formatting. Disable clang-format for them until merge with main z3 branch and re-format. * Computation of convex closure and matrix kernel Various LA functions. The implementations are somewhat preliminary. Convex closure is simplemented via syntactic convex closure procedure. Kernel computation considers many common cases. spacer_arith_kernel_sage implements kernel computation by call external Sage binary. It is used only for debugging and experiments. There is no link dependence on Sage. If desired, it can be removed. * Add spacer_concretize * Utility methods for spacer conjecture rule * Add spacer_expand_bnd_generalizer Generalizes arithmetic inequality literals of the form x <= c, by changing constant c to other constants found in the problem. * Add spacer_global_generalizer Global generalizer checks every new lemma against a cluster of previously learned lemmas, and, if possible, conjectures a new pob, that, when blocked, generalizes multiple existing lemmas. * Remove fp.spacer.print_json option The option is used to dump state of spacer into json for debugging. It has been replaced by `fp.spacer.trace_file` that allows dumping an execution of spacer. The json file can be reconstructed from the trace file elsewhere. * Workaround for segfault in spacer_proof_utils Issue #3 in hgvk94/z3 Segfault in some proof reduction. Avoid by bailing out on reduction. * Revert bug for incomplete models * Use local fresh variables in spacer_global_generalizer * Cleanup of spacer_convex_closure * Allow arbitrary expressions to name cols in convex_closure * WIP: convex closure * WIP: convex closure * Fix bindings order in spacer_global_generalizer The matcher creates substitution using std_order, which is reverse of expected order (variable 0 is last). Adjust the code appropriately for that. * Increase verbosity level for smt_context stats * Dead code in qe_mbp * bug fixes in spacer_global_generalizer::subsumer * Partially remove dependence of size of m_alphas I want m_alphas to potentially be greater than currently used alpha variables. This is helpful for reusing them across multiple calls to convex closure * Subtle bug in kernel computation Coefficient was being passed by reference and, therefore, was being changed indirectly. In the process, updated the code to be more generic to avoid rational computation in the middle of matrix manipulation. * another test for sparse_matrix_ops::kernel * Implementation of matrix kernel using Fraction Free Elimination Ensures that the kernel is int for int matrices. All divisions are exact. * clang-format sparse_matrix_ops.h * another implementation of ffe kernel in sparse_matrix_ops * Re-do arith_kernel and convex_closure * update spacer_global_generalization for new subsumer * remove spacer.gg.use_sage parameter * cleanup of spacer_global_generalizer * Removed dependency on sage * fix in spacer_convex_closure * spacer_sem_matcher: consider an additional semantic matching disabled until it is shown useful * spacer_global_generalizer: improve do_conjecture - if conjecture does not apply to pob, use lemma instead - better normalization - improve debug prints * spacer_conjecture: formatting * spacer_cluster: improve debug prints * spacer_context: improve debug prints * spacer_context: re-queue may pobs enabled even if global re-queue is disabled * spacer_cluster print formatting * reset methods on pob * cleanup of print and local variable names * formatting * reset generalization data once it has been used * refactored extra pob creation during global guidance * fix bug copying sparse matrix into spacer matrix * bug fix in spacer_convex_closure * formatting change in spacer_context * spacer_cluster: get_min_lvl chose level based on pob as well as lemmas * spacer_context: add desired_level to pob desired_level indicates at which level pob should be proved. A pob will be pushed to desired_level if necessary * spacer_context: renamed subsume stats the name of success/failed was switched * spacer_convex_closure: fix prototype of is_congruent_mod() * spacer_convex_closure: hacks in infer_div_pred() * spacer_util: do not expand literals with mod By default, equality literal t=p is expanded into t<=p && t>=p Disable the expansion in case t contains 'mod' operator since such expansion is usually not helpful for divisibility * spacer_util: rename m_util into m_arith * spacer_util: cleanup normalize() * spacer_util: formatting * spacer_context: formatting cleanup on subsume and conjecture * spacer_context: fix handling may pobs when abs_weakness is enabled A pob might be undef, so weakness must be bumped up * spacer_arith_kernel: enhance debug print * spacer_global_generalizer: improve matching on conjecture * spacer_global_generalizer: set desired level on conjecture pob * spacer_global_generalizer: debug print * spacer_global_generalizer: set min level on new pobs the new level should not be higher than the pob that was generalized * spacer_global_generalizer: do no re-create closed pobs If a generalized pob exist and closed, do not re-create it. * spacer_context: normalize twice * spacer_context: forward propagate only same kind of pobs * sketch of inductive generalizer A better implementation of inductive generalizer that in addition to dropping literals also attempts to weaken them. Current implementation is a sketch to be extended based on examples/requirements. * fix ordering in spacer_cluster_util * fix resetting of substitution matcher in spacer_conjecture Old code would forget to reset the substitution provided to the sem_matcher. Thus, if the substitution was matched once (i.e., one literal of interest is found), no other literal would be matched. * add spacer_util is_normalized() method used for debugging only * simplify normalization of pob expressions pob expressions are normalized to increase syntactic matching. Some of the normalization rules seem out of place, so removing them for now. * fix in spacer_global_generalizer If conjecture fails, do not try other generalization strategies -- they will not apply. * fix in spacer_context do not check that may pob is blocked by existing lemmas. It is likely to be blocked. Our goal is to block it again and generalize to a new lemma. This can be further improved by moving directly to generalization when pob is blocked by existing lemmas... Co-authored-by: hgvk94 <[email protected]>
wintersteiger
pushed a commit
that referenced
this pull request
Oct 4, 2023
…junctions (Z3Prover#6779) After introducing the rewriter.sort_disjunctions option (Z3Prover#6774), I noticed a segfault in a Z3 run that was working fine for me before the PR. I traced the difference to a slight discrepancy between the first patch I submitted and the one we ended up merging: my first version would skip sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while the patch in master returns BR_FAILED instead. This patch fixes that problem, and it makes slightly more sense to me to return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false` or a repeat) might have been simplified away. However I don't fully understand this code. ... and I can't say I understand why the segfault happens. Perhaps that is a separate issue? This is the file to reproduce: https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6 Here's a stack trace of the failure, mk_nflat_or_core is not involved. ``` (gdb) where #0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const () #1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () #2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () #3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () #4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () #5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () #6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () #7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () #8 0x0000555555c9c1b7 in smt::context::decide() () #9 0x0000555555ca39fd in smt::context::bounded_search() () #10 0x0000555555ca30c2 in smt::context::search() () #11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () #12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () #13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () #14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () #15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () #16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () #17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () #18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () #19 0x0000555556084dc0 in smt2::parser::parse_cmd() () #20 0x00005555560861b6 in smt2::parser::operator()() () #21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () #22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () Z3Prover#23 0x00005555555ee6f6 in main () (gdb) ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This patch brings some simplifications to Z3's OCaml bindings. It does not modify the public API.
Changes include
=(<>) instead of physical equality==(!=) throughout z3.ml