beach coding projects

[NikolajBjorner]

In case you feel an irresistible urge to code on SMT/z3 when not busy with beach volleyball, the list below assembles a set of projects and project directions. Some with very narrow scope and possible easily measurable benefit, others as stepping-stones to longer term projects.

Well-defined narrower projects:

• Remove bit-blasting of bvudiv, bvsdiv, bvurem, bvsrem and instead assertion quotient-remainder equalities in the bit-vector solver. Quotient remainder axioms are (according to preliminary tests) much more efficient than the circuits built by the bit-blaster.

• Integrate Daan Leijen’s efficient representations for tagged integers into mpz

  • Requires reading Daan’s unpublished paper + code and modifying a very few files in z3 (mpz.h, mpz.cpp).
  • Can be evaluated on QF_LIA.

• Replace memory_manager functionality by mimalloc.

  • Bug SIGBUS due to unaligned access #6015 could be addressed within the existing memory allocator, but mimalloc may have required functionality for tracking allocation size (a main feature of memory_manager that uses pointer arithmetic to store allocation size).

• Build and release pipelines for native M1 and M(k+1)

  • the user base of M1 is growing. There is currently no fully native build for MacOS Arm64.
  • the hosted Mac build machines are x64 so far. They can cross-compile using the --arm64 flag, but not test.
  • Complete the release pipeline for MacOS Arm64 so Java bindings work
  • Add pypi release for MacOS Arm64 that works.
  • bugs Failed to install using command:pip3 install z3-solver  #6024 pip install z3-solver: bad path or elf header #5926 Release arm64 / universal binaries for macOS #5848

• Get to the bottom of the NLSAT bug

  • Requires quite some math background to understand
  • Also requires quite some code review.
  • with Andrew Helwer and Neil Penning?

• Model-preserving transformations on Horn Clauses

  • To fix github issues in the inline pre-preprocessor
  • Requires some theory development for proving correctness of model preservation

• Any-time MaxSAT optimization with "core rotation"

  • the module for core enumeration used in the core-based max sat solvers is added end of April 2022 to find improved upper bounds. It finds reasonable upper bounds faster which is useful where maxsat does not terminate within a given time bound, but it is currently significantly slower than the default setting that enumerates disjoint cores once without locally optimizing models.
  • the starting point for the project is to take opt_cores.cpp as a starting point and tune it to find better local optima and back off from useless work.

• Efficient and Generalized Equality Rewriting

  • The tactic solve_eqs_tactic is bloated and inefficient. It finds a few independent equalities to eliminate and then calls itself in a loop. The loop is cut off artificially because each iteration is a linear overhead over the entire formula. A more efficient approach is to create a topological sort over substitution candidates and extract one substitution from a topologically sorted set of equalities – once.
  • The plugin architecture for theory specific equalities also could use a round of cleaning.

• Space Efficient Bounded Model Checking for Horn Clauses

  • Replace the current bmc method for non-linear horn clauses by something that resembles how recursive functions are unfolded. This approach was now developed in a specific context outside of z3 at TUV.

• To Xor or xnor?

  • Add CryptoMiniSAT theory solver for xor constraints as a sattelite solver to sat/smt.
  • A use case: https://github.com/Anonychn/SMT_Toy_Example/blob/main/Toy_Example_SMT.ipynb

• Expose and play with E-graphs.

  • The API does not expose congruence relation after search. It could expose a congruence relation and let users query it.
  • The main use case would be exposing congruences at base level (or search level, under assumptions). These represent necessary equalities, but are not necessarily complete when there are non-convex constraints and theories.

Larger projects:

• A modernized Pseudo-Boolean theory solver

  • Integrate LP relaxation,
  • use cut-based conflict resolution instead of older engine (it is called resolve_conflict_rs, but off by default given perf overhead)
  • generate proof hints. The theory is developed in Stephan Gocht's thesis. The proof format used by z3 is syntactically different. The hint checker can be modeled after the arith_proof_checker module.
  • Improved in-processing with stronger cuts.

• DRUP(T) - Proof replay and checking modulo theories

  • Wider goal of proof replay tactic

• In-processing for quantifiers in the new core

  • Allow Davis-Putnam elimination of predicates that occur only in limited positive/negative pairs. Also, possible as pre-processing. It will address a bug reported on EPR inefficiency.

• Prepare for SMT3

  • z3 embeds lambdas in a first-order signature by piggybacking on the theory of arrays. Thus, arrays are synonymous with function spaces. The SMT3 definition treats function spaces as first class. Does it make sense to extend the array-based lambda support for SMT3? In some cases parts of SMT3 could be supported, such as polymorphic axioms (a feature available in alt-ergo for many years).
  • support polymorphic function declarations.
  • support polymorphic axioms
  • native higher-order reasoning (indexing, matching, zipper-position)

• Topics in Optimization

  • support incrementality
  • support refinement (in the model callback it is possible to add constraints) of constraints
  • user propagator integration
  • Enable cube and conquer / branch and bound.
  • Parallel MaxSAT

Open - ended or longer-term projects

• Enable incrementality in context of global transformations

  • Wider goal to revamp tactics to be incremental. It requires being able to track a COI and re-add assertions removed by pre-processing.

• Local search and SMT

  • Better alternative local search methods that can act in tandem with complete search techniques – specifically for LIA and beyond.

• Exploiting User Propagators

  • Clemens Eisenhofer is exploiting user propagators for Alive2.

• Native Theory solver for large width bit-vectors

  • Project with Jakob Rath