Popular：
Virtualization DNS security formal verification reachability analysis compiler errors macro conflict web extension development framework Bitmap Graphics API inconsistencies All Tags

Building a Rewrite Rule Database: An Ambitious Project

2025-02-22
Building a Rewrite Rule Database: An Ambitious Project

This post proposes the creation of a database of rewrite rules encompassing various domains, including integer properties, differentiation, set theory, bitvectors, functional programs, and more. The author lists numerous existing projects and libraries containing rewrite rules and discusses the feasibility and challenges of unifying these rules into a common format. While some rules can be directly proven by existing SMT solvers, the author argues that a well-defined rewrite rule database is crucial for precise rewriting and manipulations in specific application contexts and will be a valuable resource for future research.

Read more
(www.philipzucker.com)
Development rewrite rules

SAT Solver Etudes I: A Deep Dive into Boolean Satisfiability

2025-01-08
SAT Solver Etudes I: A Deep Dive into Boolean Satisfiability

This blog post explores the fascinating world of SAT solvers, tracing their evolution from simple brute-force approaches to sophisticated algorithms like Davis-Putnam and Conflict-Driven Clause Learning (CDCL). It compares different techniques, highlighting recent advancements such as congruence closure, clausal equivalence sweeping, and bounded variable addition that have dramatically improved performance. The author provides Python code examples illustrating brute-force, Davis-Putnam-based, and given-clause-loop solvers. The post also touches upon partial evaluation techniques and future research directions, making it a compelling read for anyone interested in the intricacies of Boolean satisfiability.

Read more
(www.philipzucker.com)
AI SAT solver

Symbolic Execution by Overloading __bool__

2024-12-24
Symbolic Execution by Overloading __bool__

This article presents a clever technique for symbolic execution of Python code by overloading the __bool__ function in the Z3 Python library. The author leverages Z3's capabilities to translate Python conditional statements into Z3 expressions, enabling path exploration and result analysis. This approach bypasses complex AST traversal and allows direct use within Python code, simplifying symbolic execution.

Read more
(www.philipzucker.com)
Development symbolic execution __bool__ overloading