Retranslate declarations of UFs back to their original declratation for
CVC5 as it creates a new Term every time you get it from an existing
Term
@@ -425,7 +425,7 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
getDeclarationKind(f),
argsTypes,
getFormulaType(f),
- f.getChild(0)));
+ normalize(f.getChild(0))));
} else {
// TODO: check if the below is correct
return visitor.visitFunction(
@@ -445,6 +445,25 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
}
}
+ /**
+ * CVC5 returns new objects when querying operators for UFs. The new operator has to be translated
+ * back to a common one.
+ */
+ private Term normalize(Term operator) {
+ Term function = functionsCache.get(getName(operator));
+ if (function != null) {
+ checkState(
+ function.getId() == operator.getId(),
+ "operator '%s' with ID %s differs from existing function '%s' with ID '%s'.",
+ operator,
+ operator.getId(),
+ function,
+ function.getId());
+ return function;
+ }
+ return operator;
+ }
+
// see src/theory/*/kinds in CVC5 sources for description of the different CVC5 kinds ;)
private static final ImmutableMap<Kind, FunctionDeclarationKind> KIND_MAPPING =
ImmutableMap.<Kind, FunctionDeclarationKind>builder()
