Package edu.udel.cis.vsl.sarl.prove.cvc

Class Translation

java.lang.Object

edu.udel.cis.vsl.sarl.prove.cvc.Translation

public class Translation
extends Object

This class is used to deal with integer division or modulo during the CVC translation. Since CVC4 currently can not deal with integer division or modulo, integer division and modulo operations will be translated into an "exists" expression. Below is an example:

z = x%y will become exists t__0, t__1 : z = t__1 && (y*t__0 + t__1 = x) && (t__1 >= 0 && t__1 < y)

z = x/y will become exists t__0, t__1 : z = t__0 && (y*t__0 + t__1 = x) && (t__1 >= 0 && t__1 < y)

Note that SARL assumes that all operands in integer division and modulo operations are non-negative.

Constructor Summary

Constructors

Constructor	Description
Translation()
Translation(FastList<String> res)
Translation(FastList<String> res, Boolean isDivOrModulo, FastList<String> auxConstraints, List<FastList<String>> auxVars)

Method Summary

Modifier and Type	Method	Description
Translation	clone()
FastList<String>	getAuxConstraints()
List<FastList<String>>	getAuxVars()
Boolean	getIsDivOrModulo()
FastList<String>	getResult()
void	setAuxConstraints(FastList<String> auxConstraints)
void	setAuxVars(List<FastList<String>> auxVars)
void	setIsDivOrModulo(Boolean isDivOrModulo)
String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Details

Translation

public Translation()

Translation

public Translation(FastList<String> res)

Translation

public Translation(FastList<String> res,
 Boolean isDivOrModulo,
 FastList<String> auxConstraints,
 List<FastList<String>> auxVars)

Method Details

getResult

public FastList<String> getResult()

getIsDivOrModulo

public Boolean getIsDivOrModulo()

setIsDivOrModulo

public void setIsDivOrModulo(Boolean isDivOrModulo)

getAuxConstraints

public FastList<String> getAuxConstraints()

setAuxConstraints

public void setAuxConstraints(FastList<String> auxConstraints)

getAuxVars

public List<FastList<String>> getAuxVars()

setAuxVars

public void setAuxVars(List<FastList<String>> auxVars)

clone

public Translation clone()

toString

public String toString()

Overrides:

toString in class Object