Package org.sosy_lab.java_smt.example

Some basic examples for using Java-SMT.

Class Summary

Class	Description
AllSatExample	This example shows different ways to get all satisfiable models for a given set of constraints.
Binoxxo	This program parses a user-given Binoxxo and solves it with an SMT solver.
Binoxxo.BinoxxoSolver<S>
Binoxxo.BooleanBasedBinoxxoSolver	This solver encodes nore steps into boolean logic, which makes it about 10x faster than the Binoxxo.IntegerBasedBinoxxoSolver.
Binoxxo.IntegerBasedBinoxxoSolver
FormulaClassifier	This program parses user-given formulas and prints out the (minimal) matching theory for them.
HoudiniApp	This application executes the inductive-invariant synthesis algorithm called "Houdini" taken from the paper Flanagan and Leino: "Houdini, an Annotation Assistant for ESC/Java".
Interpolation	Examples for Craig/sequential/tree interpolation.
NQueens	This example program solves a NQueens problem of given size and prints a possible solution.
OptimizationFormulaWeights	Example for optimizing the weight of some constraints.
OptimizationIntReal	Example for optimizing 'x' with the constraint '0 <= x < 10'.
PrettyPrinter	This program parses user-given formulas and prints them in a pretty format.
SimpleUserPropagator	Example of a simple user propagator that prohibits variables/expressions to be set to true.
SolverOverviewTable	This program takes all installed solvers and checks them for version, theories and features and prints them to StdOut in a nice table.
SolverOverviewTable.RowBuilder	This class builds the table row-by-row.
SolverOverviewTable.SolverInfo	just a wrapper for some data.
Sudoku	This program parses user-given Sudoku and solves it with an SMT solver.
Sudoku.BooleanBasedSudokuSolver
Sudoku.EnumerationBasedSudokuSolver
Sudoku.IntegerBasedSudokuSolver
Sudoku.SudokuSolver<S>