@@ -58,8 +58,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
5858 */
5959 private fun appendTableDefinitions (smt : SMTLib ) {
6060 for (table in schema.tables) {
61- val sanitizedTableName = convertToAscii(table.id.name)
62- val dataTypeName = " ${StringUtils .capitalization(sanitizedTableName )} Row"
61+ val smtTableName = convertToAscii(table.id.name)
62+ val dataTypeName = " ${StringUtils .capitalization(smtTableName )} Row"
6363
6464 // Declare datatype for the table
6565 smt.addNode(
@@ -68,7 +68,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
6868
6969 // Declare constants for each row
7070 for (i in 1 .. numberOfRows) {
71- smt.addNode(DeclareConstSMTNode (" ${sanitizedTableName .lowercase()}$i " , dataTypeName))
71+ smt.addNode(DeclareConstSMTNode (" ${smtTableName .lowercase()}$i " , dataTypeName))
7272 }
7373 }
7474 }
@@ -92,10 +92,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
9292 * @param table The table for which unique constraints are added.
9393 */
9494 private fun appendUniqueConstraints (smt : SMTLib , table : TableDto ) {
95- val tableName = convertToAscii(table.id.name).lowercase()
95+ val smtTableName = convertToAscii(table.id.name).lowercase()
9696 for (column in table.columns) {
9797 if (column.unique) {
98- val nodes = assertForDistinctField(convertToAscii(column.name), tableName )
98+ val nodes = assertForDistinctField(convertToAscii(column.name), smtTableName )
9999 smt.addNodes(nodes)
100100 }
101101 }
@@ -168,7 +168,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
168168
169169 private fun appendBooleanConstraints (smt : SMTLib ) {
170170 for (table in schema.tables) {
171- val tableName = convertToAscii(table.id.name).lowercase()
171+ val smtTableName = convertToAscii(table.id.name).lowercase()
172172 for (column in table.columns) {
173173 if (column.type.equals(" BOOLEAN" , ignoreCase = true )) {
174174 val columnName = convertToAscii(column.name).uppercase()
@@ -177,12 +177,12 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
177177 AssertSMTNode (
178178 OrAssertion (
179179 listOf (
180- EqualsAssertion (listOf (" ($columnName $tableName $i )" , " \" true\" " )),
181- EqualsAssertion (listOf (" ($columnName $tableName $i )" , " \" True\" " )),
182- EqualsAssertion (listOf (" ($columnName $tableName $i )" , " \" TRUE\" " )),
183- EqualsAssertion (listOf (" ($columnName $tableName $i )" , " \" false\" " )),
184- EqualsAssertion (listOf (" ($columnName $tableName $i )" , " \" False\" " )),
185- EqualsAssertion (listOf (" ($columnName $tableName $i )" , " \" FALSE\" " ))
180+ EqualsAssertion (listOf (" ($columnName $smtTableName $i )" , " \" true\" " )),
181+ EqualsAssertion (listOf (" ($columnName $smtTableName $i )" , " \" True\" " )),
182+ EqualsAssertion (listOf (" ($columnName $smtTableName $i )" , " \" TRUE\" " )),
183+ EqualsAssertion (listOf (" ($columnName $smtTableName $i )" , " \" false\" " )),
184+ EqualsAssertion (listOf (" ($columnName $smtTableName $i )" , " \" False\" " )),
185+ EqualsAssertion (listOf (" ($columnName $smtTableName $i )" , " \" FALSE\" " ))
186186 )
187187 )
188188 )
@@ -195,7 +195,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
195195
196196 private fun appendTimestampConstraints (smt : SMTLib ) {
197197 for (table in schema.tables) {
198- val tableName = convertToAscii(table.id.name).lowercase()
198+ val smtTableName = convertToAscii(table.id.name).lowercase()
199199 for (column in table.columns) {
200200 if (column.type.equals(" TIMESTAMP" , ignoreCase = true )) {
201201 val columnName = convertToAscii(column.name).uppercase()
@@ -206,15 +206,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
206206 smt.addNode(
207207 AssertSMTNode (
208208 GreaterThanOrEqualsAssertion (
209- " ($columnName $tableName $i )" ,
209+ " ($columnName $smtTableName $i )" ,
210210 lowerBound.toString()
211211 )
212212 )
213213 )
214214 smt.addNode(
215215 AssertSMTNode (
216216 LessThanOrEqualsAssertion (
217- " ($columnName $tableName $i )" ,
217+ " ($columnName $smtTableName $i )" ,
218218 upperBound.toString()
219219 )
220220 )
@@ -233,11 +233,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
233233 * @param table The table for which primary key constraints are added.
234234 */
235235 private fun appendPrimaryKeyConstraints (smt : SMTLib , table : TableDto ) {
236- val tableName = convertToAscii(table.id.name).lowercase()
236+ val smtTableName = convertToAscii(table.id.name).lowercase()
237237 val primaryKeys = table.columns.filter { it.primaryKey }
238238
239239 for (primaryKey in primaryKeys) {
240- val nodes = assertForDistinctField(convertToAscii(primaryKey.name), tableName )
240+ val nodes = assertForDistinctField(convertToAscii(primaryKey.name), smtTableName )
241241 smt.addNodes(nodes)
242242 }
243243 }
@@ -249,7 +249,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
249249 * @param tableName The name of the table.
250250 * @return A list of SMT nodes representing distinct assertions.
251251 */
252- private fun assertForDistinctField (pkSelector : String , tableName : String ): List <SMTNode > {
252+ private fun assertForDistinctField (pkSelector : String , t st : String ): List <SMTNode > {
253253 val nodes = mutableListOf<AssertSMTNode >()
254254 for (i in 1 .. numberOfRows) {
255255 for (j in i + 1 .. numberOfRows) {
0 commit comments