Systems and methods for SMT processes using uninterpreted function symbols

1. A method performed by a data processing system, comprising:

receiving a configuration model;

computing a variant for the configuration model that includes a non-linear function;

identifying input/output pairs in the non-linear function of the variant;

executing a process on an external application for each input/output pair to produce an output value corresponding to each input of the input/output pairs;

comparing the output value corresponding to each input of the input/output pairs with the output corresponding to each input of the input/output pairs; and

when the output value corresponding to each input of the input/output pairs is equal to the output corresponding to each input of the input/output pairs, then storing an indication that the variant is correct.

2. The method of claim 1 , further comprising, when the output value corresponding to each input of the input/output pairs is not equal to the output corresponding to each input of the input/output pairs, then adding one or more constraints to the configuration model.

3. The method of claim 2 , further comprising storing an updated configuration model including the added constraints.

4. The method of claim 1 , wherein identifying input/output pairs in the non-linear function of the variant is performed by a satisfiability modulo theories solver.

5. The method of claim 1 , wherein the non-linear function is represented in a satisfiability modulo theories(SMT) solver as an uninterpreted function symbol.

6. The method of claim 1 , further comprising adding additional constraints to the configuration model to limit a search space of an SMT computation.

7. A data processing system having at least a processor and an accessible memory, the data processing system configured to:

receive a configuration model;

compute a variant for the configuration model that includes a non-linear function;

identify input/output pairs in the non-linear function of the variant;

execute a process on an external application for each input/output pair to produce an output value corresponding to each input of the input/output pairs;

compare the output value corresponding to each input of the input/output pairs with the output corresponding to each input of the input/output pairs; and

when the output value corresponding to each input of the input/output pairs is equal to the output corresponding to each input of the input/output pairs, store an indication that the variant is correct.

8. The data processing system of claim 7 , wherein the data processing system is further configured to, when the output value corresponding to each input of the input/output pairs is not equal to the output corresponding to each input of the input/output pairs, add one or more constraints to the configuration model.

9. The data processing system of claim 8 , wherein the data processing system is further configured to store an updated configuration model including the added constraints.

10. The data processing system of claim 7 , wherein identifying input/output pairs in the non-linear function of the variant is performed by a satisfiability modulo theories (SMT) solver.

11. The data processing system of claim 7 , wherein the non-linear function is represented in a satisfiability modulo theories solver as an uninterpreted function symbol.

12. The data processing system of claim 7 , wherein the data processing system is further configured to add additional constraints to the configuration model to limit a search space of a satisfiability modulo theories (SMT) computation.

13. A non-transitory machine-readable medium encoded with executable instructions that, when executed, cause a data processing system to:

receive a configuration model;

compute a variant for the configuration model that includes a non-linear function;

identify input/output pairs in the non-linear function of the variant;

execute a process on an external application for each input/output pair to produce an output value corresponding to each input of the input/output pairs;

compare the output value corresponding to each input of the input/output pairs with the output corresponding to each input of the input/output pairs; and

when the output value corresponding to each input of the input/output pairs is equal to the output corresponding to each input of the input/output pairs, store an indication that the variant is correct.

14. The non-transitory machine-readable medium of claim 13 , further encoded with executable instructions to, when the output value corresponding to each input of the input/output pairs is not equal to the output corresponding to each input of the input/output pairs, add one or more constraints to the configuration model.

15. The non-transitory machine-readable medium of claim 13 , further encoded with executable instructions to store an updated configuration model including the added constraints.

16. The non-transitory machine-readable medium of claim 13 , wherein identifying input/output pairs in the non-linear function of the variant is performed by a satisfiability modulo theories (SMT) solver.

17. The non-transitory machine-readable medium of claim 13 , wherein the non-linear function is represented in a satisfiability modulo theories solver as an uninterpreted function symbol.

18. The non-transitory machine-readable medium of claim 13 , further encoded with executable instructions to add additional constraints to the configuration model to limit a search space of a satisfiability modulo theories (SMT) computation.