RULE-BASED METHOD FOR PROVING UNSATISFIABLE CONDITIONS IN A MIXED NUMERIC AND STRING SOLVER

摘要

A method includes, by computing devices, analyzing numeric and string constraints associated with a software module that includes numeric and string variables and operations applying to specific variables for numeric or string results. The numeric constraints apply to specific numeric variables. The string constraints apply to specific string variables. The method further includes determining an over-approximated constraint from the numeric constraints or operations, representing the over-approximated constraint and string constraints with finite state machines, representing the numeric constraints with an equation, determining whether a solution does not exist for the combination of the variables that satisfies the over-approximated constraint, the numeric constraints, and the string constraints using operations, and terminating attempts to solve for the variables based on the determination whether the solution does not exist. The over-approximated constraint includes a superset of the numeric constraints or operations and applies to specific string variables.