Package de.uzl.its.swat.solver

Class LocalSolver

java.lang.Object

de.uzl.its.swat.solver.LocalSolver

public class LocalSolver
extends Object

This class can is used to directly communicate with the solver (currently Z3). The solver interface only tries to find a solution for each branch (with the corresponding path constraints) and log it. It cannot be used to perform iterative symbolic execution and is primarily intended for debugging and testing purposes.

Constructor Summary

Constructors

Constructor	Description
LocalSolver()

Method Summary

Modifier and Type	Method	Description
static void	solve()	Retrieves all recorded constraints and collects input bounds and path constraints for each constraint.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

LocalSolver

public LocalSolver()

Method Details

solve

public static void solve()

Retrieves all recorded constraints and collects input bounds and path constraints for each constraint. Then, it tries to find a solution for each constraint and logs it.