Package org.sosy_lab.java_smt.api
Class Model.ValueAssignment
- java.lang.Object
-
- org.sosy_lab.java_smt.api.Model.ValueAssignment
-
-
Constructor Summary
Constructors Constructor Description ValueAssignment(Formula keyFormula, Formula valueFormula, BooleanFormula formula, String name, Object value, List<?> argumentInterpretation)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description boolean
equals(Object o)
Object
getArgInterpretation(int i)
ImmutableList<Object>
getArgumentsInterpretation()
Interpretation assigned for function arguments.int
getArity()
BooleanFormula
getAssignmentAsFormula()
The formula AST representing the equality of key and value.Formula
getKey()
The formula AST which is assigned a given value.String
getName()
Variable name for variables, function name for UFs, and array name for arrays.Object
getValue()
Value: see theEvaluator.evaluate(org.sosy_lab.java_smt.api.Formula)
methods for the possible types.Formula
getValueAsFormula()
The formula AST which is assigned to a given key.int
hashCode()
boolean
isFunction()
String
toString()
-
-
-
Method Detail
-
getKey
public Formula getKey()
The formula AST which is assigned a given value.
-
getValueAsFormula
public Formula getValueAsFormula()
The formula AST which is assigned to a given key.
-
getAssignmentAsFormula
public BooleanFormula getAssignmentAsFormula()
The formula AST representing the equality of key and value.
-
getName
public String getName()
Variable name for variables, function name for UFs, and array name for arrays.
-
getValue
public Object getValue()
Value: see theEvaluator.evaluate(org.sosy_lab.java_smt.api.Formula)
methods for the possible types.We return only values that can be used in Java, i.e., boolean or numeral values (Rational/Double/BigInteger/Long/Integer).
-
getArgumentsInterpretation
public ImmutableList<Object> getArgumentsInterpretation()
Interpretation assigned for function arguments. Empty for variables.
-
isFunction
public boolean isFunction()
-
getArity
public int getArity()
-
getArgInterpretation
public Object getArgInterpretation(int i)
-
-