使用未解释函数符号的可满足性模理论过程的系统和方法

摘要

使用未解释函数符号的SMT过程的系统和方法。一种方法包括接收配置模型。该方法包括计算配置模型的变体，其包含非线性函数。该方法包括识别变体的非线性函数中的输入/输出对。该方法包括针对每个输入/输出对在外部应用上执行过程，以生成对应于该输入/输出对的每个输入的输出值。该方法包括将对应于输入/输出对的每个输入的该输出值与对应于输入/输出对的每个输入的输出相比较。该方法包括，当对应于输入/输出对的每个输入的输出值等于对应于输入/输出对的每个输入的输出时，系统则存储该变体为正确的指示。