When I was using the Z3 SMT solver to solve some challenging problems many years ago, I often found myself spend most of the time on programming all kinds of formulas. This significantly slow down my development. So I decide to build my own set of classes that can help me quickly construct the formulas I want and use them to interact with multiple SAT/SMT solvers. Now, I constantly use uran to solve all kinds of interesting problems for my own research. In short, uran is an engine that you could place in between solvers and your own specification language, and totally seperate your code for the language that you design from underlying solvers.
- Boolean Circuit Gate.
- Quantifiers.
- Arithmetic Formula.
- Bit Vector.
- Increment SMT Solving.
- Iterative SMT Solving.
- dimacs (SAT Solvers)
- SMT2 (SMT Solvers)
- Array.
- Compact Sized Formula Generation.
You can find detailed structure of uran here.
All source code is under MIT License which you can find here.
Hao Wu