% optmize_tool

The model tool is represented by the package {\ttfamily it.polito.policyorchestration.impl.\linebreak optimization.solver} and it allows representing the model of distribution by a set of boolean variables and equations, moreover it provides an easy way to create boolean variables, equation, disequations and constraints.
In others words it is an API to use the SAT Solver Optimize.
The workflow of the Optimize tool is the following:

\begin{itemize}
	\item 
	creation of a set of boolean variable;
	\item
	creation of a set of equation, expressed as OR, AND and NOT operators;
	\item
	creation of a set of constrains as assertions;
	\item
	creation of a cost function and its value is minimized;
	\item
	computation of an optimized model and setting a value for each boolean variable.
\end{itemize}

\subsection{Tool architecture}

The tool architecture is made up of two classes, the first one is an handler for Z3 SAT Solver and the second one is a class that exposes useful functions to handles Z3 data types.\newline
The structure of the tool is the following:

\begin{itemize}
	\item 
	\code{class OptimizeTool}: this class is a wrapper for the solver and its purpose is to manage all the useful functions to create boolean variables, equation and cost functions. Moreover is in charge of minimize the cost function and create a model which set all the value to the boolean variables.
	\newline
	The instance variables are:
	
	\begin{itemize}
		\item 
		\code{private Context ctx}\newline
		it is the context in which all the boolean variables and the equations are stored;
		\item 
		\code{private Optimize opt}\newline
		it represents the Optimize Solver which stored the constrains and minimize the cost function;
		\item 
		\code{private Model model}
		it the model that contains all the setted boolean variables after the optimization;
		\item 
		\code{private Status status}\newline
		it is the status of the model, it could be \code{SATISFIABLE}, \code{UNKNOWN} or \code{UNSATISFIABLE};
		\item 
		\code{private HashMap<String, BoolExpr> equationMap}\newline
		\code{private HashMap<String, BoolExpr> boolVariablesMap}\newline
		\code{private HashMap<String, ArithExpr> realVariablesMap}\newline
		they are maps to associate a ``name'' to boolean variables and to equations, instead of using directly the Z3 Objects.
		In this way who is using the Optimize tool need to manage only \code{String} variables.
	\end{itemize}
	
	The following methods are the wrappers for the Z3 SAT solver functions:
	
	\begin{itemize}
		\item 
		\code{public OptimizeTool()}\newline
		it is the constructor of the class, it initialized all the instance variables;
		\item
		\code{public void createBooleanVariable(String bool)}\newline
		it allows to create a new boolean variable named \code{bool} in \code{Context ctx} that will be stored in \code{boolVariablesMap};
		\item
		\code{public void addConstraints(String... constraints)}\newline
		it allows to add an assertion to the \code{Optimize opt} variable;
		\item
		\code{public void or(String equation, String... args)}\newline
		\code{public void and(String equation, String... args)}\newline
		\code{public void not(String equation, String arg)}\newline
		they are wrappers for the operators of the Z3 Solver, each method check if there is an equation already store in \code{equationMap}, if there is one the method add the \code{args} to the previous equation, if the method could not found it, it will create a new one;
		\item
		\code{public void Eq(String equation, String left, String right)}\newline
		it creates an equation of the form \code{left} = \code{right};
		\item
		\code{public void Le(String equation, ArithExpr left, ArithExpr right)}\newline
		it creates an disequation of the form \code{left} $\mathcal{<}$ \code{right};
		\item
		\code{public void addReal(String realvariable, ArithExpr... args)}\newline
		it creates an arithmetic expression that represents a real variable. This method is used to create a cost function;
		\item
		\code{public void minimizeRealVariable(String variable)}\newline
		it is the method that forces the Solver to optimize the variable passed in input;
		\item
		\code{public void calculateModel()}\newline
		it checks the \code{Status} of the model and if it is \code{SATISFIABLE} it sets the \code{model};
		\item
		\code{public boolean getBooleanVariableResult(String booleanName)}\newline
		it retrieves the values of the boolean variable given in input its name.
	\end{itemize}
	
	\item
	\code{class OptimizeFunctionHandler}: this class is not instantiatable and it provides additional functions useful for the tool, so it has no instance variables.\newline
	It structures as follow:
	
	\begin{itemize}
		\item
		{\ttfamily public static ArithExpr countTrue(OptimizeTool opt, List<BoolExpr>\newline listBool)}\newline
		it create an arithmetic expression that represents the sum of the element in \code{listBool} list. Each \code{BoolExpr} has the value of \num{1} if it is \textit{true} or the value of \num{0} if it is \textit{false};
		\item
		\code{public static List<BoolExpr> getMatchingBooleanVariable(OptimizeTool opt, String... matchingSubstring)}\newline
		it returns all the boolean expressions with their names contains all the strings passed as parameters;
		\item
		\code{public static boolean getBooleanValue(OptimizeTool opt, BoolExpr bool)}\newline
		it returns the value of the boolean expression;
		\item
		\code{public static ArithExpr convertIntToArithExpr(OptimizeTool opt, int n)}\newline
		it returns the arithmetic expression of the value passed as parameter;
		\item
		{\ttfamily public static String getPbooleanName(String ruleName, String filterinPo\-intName)}\newline
		{\ttfamily public static String getSbooleanName(String ruleName, String filterinPo\-intName)}\newline
		they creates the name for the boolean variables used in the tool;
		\item
		\code{private static ArithExpr countOneIfIsTrue(Context ctx, BoolExpr bool)}\newline
		it return an arithmetic expression that represent if the \code{bool} value is \textit{true} it counts \num{1} or else it counts \num{0}.
	\end{itemize}
	
\end{itemize}

\subsection{Modify the tool}

Both of the classes could be extended, in the \code{class OptimizeTool} new wrapper methods could be added to represents new equation or disequation (e.g. $\mathcal{>}, \leq$ or $\neq$) that in this tool are not needed.
The \code{class OptimizeFunctionHandler} is a class that exposes functions to manage the arithmetic and the bool expression, so any additional useful function could be placed in this class.