Fix variable-name caches for CVC4
CVC4 does not seem to cache these objects itself, so someone already
added caches like for Princess. This commit completes what was still
missing.
@@ -54,6 +54,7 @@ import org.sosy_lab.java_smt.solvers.cvc4.CVC4Formula.CVC4RationalFormula;
public class CVC4FormulaCreator extends FormulaCreator<Expr, Type, CVC4Environment, Expr> {
protected final Map<String, Expr> variablesCache = new HashMap<>();
+ private final Map<String, Expr> functionsCache = new HashMap<>();
private final ExprManager exprManager;
protected CVC4FormulaCreator(CVC4Environment pEnvironment) {
@@ -66,7 +67,8 @@ public class CVC4FormulaCreator extends FormulaCreator<Expr, Type, CVC4Environme
}
- public Expr makeVariable(String name, Type type) {
+ @Override
+ public Expr makeVariable(Type type, String name) {
if (variablesCache.containsKey(name)) {
Expr oldExp = variablesCache.get(name);
assert type.equals(oldExp.getType());
@@ -97,13 +99,6 @@ public class CVC4FormulaCreator extends FormulaCreator<Expr, Type, CVC4Environme
return exprManager.mkArrayType(pIndexType, pElementType);
}
- @Override
- public Expr makeVariable(Type pType, String pVarName) {
- Expr var = exprManager.mkVar(pVarName, pType);
- variablesCache.put(pVarName, var);
- return var;
- }
-
@Override
public Expr extractInfo(Formula pT) {
return CVC4FormulaManager.getCVC4Expr(pT);
@@ -411,11 +406,17 @@ public class CVC4FormulaCreator extends FormulaCreator<Expr, Type, CVC4Environme
@Override
public Expr declareUFImpl(String pName, Type pReturnType, List<Type> pArgTypes) {
+ if (!functionsCache.containsKey(pName)) {
vectorType args = new vectorType();
for (Type t : pArgTypes) {
args.add(t);
}
Type requestedFunctionType = exprManager.mkFunctionType(args, pReturnType);
- return exprManager.mkVar(pName, requestedFunctionType);
+ Expr result = exprManager.mkVar(pName, requestedFunctionType);
+ functionsCache.put(pName, result);
+ return result;
+ } else {
+ return functionsCache.get(pName);
+ }
}
}
