| 摘要 |
PROBLEM TO BE SOLVED: To provide a system and a method for discriminating a "DON'T CARE" variable in a programming code.SOLUTION: A method includes the steps of: obtaining a SMT formula having a plurality of a SMT (satisfiability problem modulo theory) variables from a programming code; obtaining a simplified SMT formula including a plurality of simplified SMT valuables from the SMT formula; obtaining a SAT formula including a plurality of SAT variables from the simplified SMT formula; determining which is a "DON'T CARE" variable among the plurality of a SMT variables by the simplified SMT formula; and determining which is a "DON'T CARE" variable among the plurality of SMT variables by the simplified SAT formula.SELECTED DRAWING: Figure 1 |
