GitHub - michalt/z3-utvpi: UTVPI theory solver for Z3

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 22 Commits
report		report
.gitignore		.gitignore
Makefile		Makefile
README		README
TODO		TODO
common.h		common.h
example.smt		example.smt
example_tightening.smt		example_tightening.smt
reason.h		reason.h
test.cc		test.cc
utvpi_graph-inl.h		utvpi_graph-inl.h
utvpi_graph.h		utvpi_graph.h
utvpi_graph_q-inl.h		utvpi_graph_q-inl.h
utvpi_graph_q.h		utvpi_graph_q.h
utvpi_graph_z-inl.h		utvpi_graph_z-inl.h
utvpi_graph_z.h		utvpi_graph_z.h
utvpi_theory.h		utvpi_theory.h

Repository files navigation

Simple UTVPI (Unit Two Variable Per Inequality) theory solver for Z3 along with
report surveying DL (Difference Logic) and UTVPI in SMT solvers. The theory
solver is mainly based on the paper "An Efficient Decision Procedure for UTVPI
Constraints" by Lahiri and Musuvathi.

The report and implementation has been done as the final project for the course
"Advanced Analysis Techniques" at the Technical University of Denmark:
http://www2.imm.dtu.dk/courses/02913/
http://research.microsoft.com/en-us/events/z3dtu/