diff --git a/.gitignore b/.gitignore index f927b1e6e..b642428d4 100644 --- a/.gitignore +++ b/.gitignore @@ -26,6 +26,9 @@ benchlog benchscores koat-examples benchmarks* +# Actually I find it kind of important to track benchmark results +# in git, to see how they are affected by changes in the codebase. +!benchmarks/ # hidden files .* @@ -40,6 +43,7 @@ build build-static bundle CMakeFiles +CMakeCache.txt compile_commands.json loat-static LoAT.* diff --git a/CMakeLists.txt b/CMakeLists.txt index a868b90d0..dfab90332 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,6 +34,7 @@ endif() add_compile_options(-Wall -Wextra -pedantic -Wno-unused-parameter) set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "${CMAKE_CXX_FLAGS_RELEASE} -g") +set(CMAKE_EXPORT_COMPILE_COMMANDS ON) message(STATUS "Build type: " ${CMAKE_BUILD_TYPE}) message(STATUS "Compiler flags:" ${CMAKE_CXX_COMPILE_FLAGS}) diff --git a/benchmarks/LIA-Lin.txt b/benchmarks/LIA-Lin.txt new file mode 100644 index 000000000..e4d39e7f8 --- /dev/null +++ b/benchmarks/LIA-Lin.txt @@ -0,0 +1,500 @@ +### Z3 ADCL +000 timeout timeout +001 timeout unknown +002 timeout unknown +003 timeout unknown +004 timeout unknown +005 timeout unknown +006 timeout unknown +007 sat unknown +008 timeout timeout +009 timeout unknown +010 sat unknown +011 sat unknown +012 timeout timeout +013 timeout timeout +014 timeout timeout +015 timeout unknown +016 timeout unknown +017 timeout unknown +018 timeout unknown +019 timeout unknown +020 timeout unknown +021 sat unknown +022 timeout unknown +023 sat unknown +024 timeout unknown +025 timeout timeout +026 timeout unknown +027 timeout unknown +028 sat unknown +029 timeout unknown +030 unsat unsat +031 unsat unsat +032 unsat unsat +033 unsat unsat +034 unsat unsat +035 unsat unsat +036 unsat unknown +037 unsat unsat +038 unsat unsat +039 unsat unsat +040 timeout timeout +041 timeout timeout +042 timeout timeout +043 timeout unsat +044 timeout unsat +045 timeout unsat +046 timeout unknown +047 timeout unsat +048 timeout timeout +049 timeout unknown +050 timeout unsat +051 timeout unsat +052 timeout unsat +053 timeout unsat +054 timeout unknown +055 timeout unknown +056 unsat unknown +057 timeout unsat +058 timeout unknown +059 timeout unsat +060 unsat unsat +061 unsat unsat +062 unsat unsat +063 unsat unsat +064 unsat unsat +065 timeout unsat +066 unsat unsat +067 unsat unsat +068 timeout unknown +069 timeout unsat +070 timeout timeout +071 unsat unsat +072 unsat unsat +073 sat timeout +074 timeout timeout +075 timeout unsat +076 timeout unsat +077 timeout unknown +078 timeout unknown +079 sat unknown +080 sat timeout +081 sat unknown +082 timeout unknown +083 unsat unsat +084 unsat unsat +085 sat unknown +086 unsat unsat +087 sat timeout +088 sat unknown +089 unsat unsat +090 timeout unknown +091 timeout unknown +092 unsat unsat +093 sat unknown +094 sat unknown +095 sat unknown +096 unsat timeout +097 timeout unknown +098 timeout unknown +099 timeout timeout +100 timeout unknown +101 timeout unknown +102 timeout timeout +103 timeout unknown +104 timeout unknown +105 timeout unknown +106 timeout timeout +107 timeout unknown +108 timeout unknown +109 timeout unknown +110 sat unknown +111 unsat unsat +112 sat unknown +113 sat timeout +114 sat timeout +115 sat unknown +116 unsat unsat +117 unsat unsat +118 sat unknown +119 unsat unsat +120 sat unknown +121 sat unknown +122 sat timeout +123 unsat unsat +124 sat timeout +125 timeout unknown +126 timeout unknown +127 timeout unknown +128 timeout unknown +129 sat timeout +130 unsat unsat +131 sat timeout +132 sat timeout +133 unsat unsat +134 timeout unknown +135 timeout timeout +136 timeout timeout +137 timeout timeout +138 timeout timeout +139 timeout timeout +140 timeout timeout +141 timeout timeout +142 timeout timeout +143 timeout timeout +144 timeout timeout +145 timeout timeout +146 timeout timeout +147 timeout timeout +148 timeout timeout +149 timeout timeout +150 timeout unknown +151 timeout timeout +152 timeout timeout +153 timeout timeout +154 timeout unsat +155 timeout timeout +156 timeout timeout +157 timeout timeout +158 timeout timeout +159 timeout timeout +160 timeout timeout +161 timeout timeout +162 timeout timeout +163 timeout timeout +164 timeout timeout +165 timeout timeout +166 timeout timeout +167 timeout timeout +168 timeout timeout +169 timeout timeout +170 sat timeout +171 sat timeout +172 sat timeout +173 sat timeout +174 sat unknown +175 unsat unsat +176 sat unknown +177 sat unknown +178 sat unknown +179 sat timeout +180 sat timeout +181 sat timeout +182 sat timeout +183 sat unknown +184 sat unknown +185 unsat unsat +186 sat unknown +187 unsat unsat +188 sat timeout +189 unsat timeout +190 sat timeout +191 sat timeout +192 sat timeout +193 sat timeout +194 sat timeout +195 sat timeout +196 sat timeout +197 unsat unsat +198 sat timeout +199 timeout timeout +200 unsat timeout +201 unsat unsat +202 timeout timeout +203 sat timeout +204 sat timeout +205 sat timeout +206 timeout timeout +207 timeout timeout +208 timeout timeout +209 timeout timeout +210 timeout timeout +211 timeout timeout +212 timeout timeout +213 timeout timeout +214 timeout timeout +215 timeout timeout +216 timeout timeout +217 timeout timeout +218 sat timeout +219 timeout timeout +220 timeout timeout +221 timeout timeout +222 timeout timeout +223 sat timeout +224 sat timeout +225 timeout timeout +226 timeout timeout +227 timeout timeout +228 sat timeout +229 timeout timeout +230 sat timeout +231 timeout timeout +232 sat timeout +233 timeout timeout +234 timeout timeout +235 timeout timeout +236 timeout timeout +237 timeout timeout +238 timeout timeout +239 timeout timeout +240 timeout timeout +241 timeout timeout +242 timeout timeout +243 timeout timeout +244 timeout timeout +245 timeout timeout +246 timeout timeout +247 timeout timeout +248 timeout timeout +249 timeout timeout +250 timeout timeout +251 timeout timeout +252 timeout timeout +253 timeout timeout +254 timeout timeout +255 timeout timeout +256 timeout timeout +257 timeout timeout +258 timeout timeout +259 timeout timeout +260 sat timeout +261 timeout unknown +262 unknown timeout +263 timeout unknown +264 timeout unknown +265 sat unknown +266 timeout unknown +267 timeout unknown +268 timeout unknown +269 timeout unknown +270 timeout unknown +271 timeout timeout +272 timeout timeout +273 timeout unknown +274 timeout unknown +275 timeout unknown +276 timeout timeout +277 timeout timeout +278 timeout timeout +279 timeout timeout +280 timeout unknown +281 timeout timeout +282 timeout timeout +283 timeout unknown +284 timeout timeout +285 timeout unknown +286 timeout unknown +287 timeout unknown +288 sat timeout +289 timeout unknown +290 sat unknown +291 sat unknown +292 timeout unknown +293 sat unknown +294 sat unknown +295 sat unknown +296 sat unknown +297 unsat unsat +298 timeout unknown +299 unsat unsat +300 sat unknown +301 sat unknown +302 timeout timeout +303 timeout unknown +304 timeout unknown +305 timeout unknown +306 sat unknown +307 sat unknown +308 sat unknown +309 sat unknown +310 sat unknown +311 sat unknown +312 timeout unknown +313 unsat unsat +314 sat unknown +315 sat unknown +316 unsat unsat +317 sat unknown +318 sat unknown +319 unsat unsat +320 sat unknown +321 unsat unsat +322 unsat unsat +323 sat unknown +324 sat timeout +325 sat unknown +326 unsat unsat +327 unsat unsat +328 unsat unsat +329 unsat unsat +330 unsat unsat +331 unsat unsat +332 unsat unsat +333 sat unknown +334 unsat unsat +335 unsat unsat +336 unsat unsat +337 unsat unsat +338 sat timeout +339 sat timeout +340 sat timeout +341 sat timeout +342 sat timeout +343 unsat timeout +344 sat timeout +345 unsat unsat +346 unsat unsat +347 unsat unsat +348 unsat unsat +349 unsat unsat +350 sat timeout +351 unsat unsat +352 unsat timeout +353 unsat unsat +354 unsat timeout +355 timeout unknown +356 timeout timeout +357 timeout timeout +358 timeout unsat +359 timeout timeout +360 timeout timeout +361 timeout timeout +362 timeout unsat +363 timeout timeout +364 timeout timeout +365 timeout timeout +366 timeout timeout +367 timeout timeout +368 timeout timeout +369 timeout timeout +370 timeout timeout +371 timeout timeout +372 timeout timeout +373 timeout timeout +374 timeout timeout +375 timeout timeout +376 timeout timeout +377 timeout timeout +378 timeout timeout +379 sat timeout +380 timeout timeout +381 timeout unsat +382 timeout timeout +383 timeout timeout +384 timeout timeout +385 timeout timeout +386 timeout unsat +387 timeout timeout +388 timeout timeout +389 timeout timeout +390 timeout timeout +391 timeout timeout +392 timeout timeout +393 timeout timeout +394 timeout timeout +395 unsat timeout +396 timeout timeout +397 timeout timeout +398 sat timeout +399 timeout timeout +400 timeout timeout +401 timeout unsat +402 timeout unsat +403 sat timeout +404 timeout timeout +405 timeout unsat +406 timeout timeout +407 timeout timeout +408 timeout timeout +409 sat unknown +410 sat unknown +411 sat unknown +412 sat unknown +413 sat unknown +414 sat unknown +415 sat unknown +416 sat unknown +417 sat unknown +418 sat unknown +419 sat unknown +420 sat unknown +421 sat unknown +422 sat unknown +423 sat unknown +424 sat unknown +425 sat unknown +426 sat unknown +427 sat unknown +428 sat unknown +429 timeout unknown +430 timeout unknown +431 timeout timeout +432 unsat timeout +433 timeout timeout +434 sat unknown +435 sat unknown +436 sat unknown +437 sat unknown +438 sat unknown +439 sat unknown +440 sat unknown +441 sat unknown +442 unsat timeout +443 sat unknown +444 sat unknown +445 sat unknown +446 timeout timeout +447 timeout timeout +448 timeout timeout +449 timeout timeout +450 timeout timeout +451 timeout timeout +452 timeout timeout +453 timeout timeout +454 timeout timeout +455 timeout timeout +456 timeout timeout +457 unsat timeout +458 timeout timeout +459 timeout timeout +460 timeout timeout +461 timeout unknown +462 timeout timeout +463 timeout timeout +464 timeout timeout +465 timeout timeout +466 timeout timeout +467 timeout timeout +468 timeout timeout +469 timeout timeout +470 timeout timeout +471 timeout timeout +472 timeout timeout +473 timeout timeout +474 unsat timeout +475 timeout unsat +476 timeout timeout +477 timeout timeout +478 timeout timeout +479 timeout timeout +480 timeout timeout +481 sat timeout +482 timeout timeout +483 timeout timeout +484 timeout timeout +485 timeout timeout +486 unsat timeout +487 sat timeout +488 timeout timeout +489 timeout timeout +490 timeout timeout +491 timeout timeout +492 timeout timeout +493 timeout timeout +494 timeout timeout +495 sat timeout +496 sat timeout +497 timeout timeout +498 timeout timeout \ No newline at end of file diff --git a/benchmarks/LIA.txt b/benchmarks/LIA.txt new file mode 100644 index 000000000..87608873f --- /dev/null +++ b/benchmarks/LIA.txt @@ -0,0 +1,456 @@ +### Z3 ADCL +000 sat timeout +001 sat timeout +002 sat timeout +003 sat timeout +004 sat timeout +005 sat timeout +006 sat timeout +007 sat timeout +008 sat timeout +009 sat timeout +010 sat timeout +011 sat timeout +012 sat timeout +013 sat timeout +014 timeout timeout +015 sat timeout +016 timeout timeout +017 sat timeout +018 timeout timeout +019 sat timeout +020 timeout timeout +021 sat unknown +022 sat timeout +023 sat timeout +024 timeout timeout +025 timeout timeout +026 timeout timeout +027 timeout timeout +028 timeout timeout +029 timeout timeout +030 timeout timeout +031 timeout timeout +032 timeout timeout +033 timeout timeout +034 timeout timeout +035 timeout timeout +036 timeout timeout +037 timeout timeout +038 timeout timeout +039 timeout timeout +040 timeout timeout +041 timeout timeout +042 timeout timeout +043 sat timeout +044 timeout timeout +045 timeout timeout +046 timeout timeout +047 timeout timeout +048 sat unknown +049 unsat timeout +050 timeout timeout +051 sat unknown +052 timeout timeout +053 timeout timeout +054 timeout timeout +055 timeout timeout +056 timeout timeout +057 timeout timeout +058 timeout timeout +059 sat timeout +060 unsat unsat +061 sat unknown +062 unsat unsat +063 unsat unsat +064 sat unknown +065 sat sat +066 sat timeout +067 unsat unsat +068 sat timeout +069 unsat unsat +070 sat timeout +071 sat unknown +072 unsat unsat +073 unsat unsat +074 sat timeout +075 unsat unsat +076 unsat timeout +077 unsat unsat +078 sat timeout +079 sat timeout +080 unsat timeout +081 unsat unsat +082 sat timeout +083 sat timeout +084 sat timeout +085 sat timeout +086 unsat timeout +087 timeout timeout +088 sat timeout +089 sat timeout +090 unsat timeout +091 sat timeout +092 timeout timeout +093 unsat timeout +094 timeout timeout +095 sat timeout +096 timeout unsat +097 timeout unsat +098 unsat timeout +099 sat timeout +100 sat timeout +101 timeout timeout +102 timeout timeout +103 unsat unsat +104 unsat unsat +105 unsat unsat +106 unsat unsat +107 sat timeout +108 sat timeout +109 unsat unsat +110 unsat unsat +111 unsat unsat +112 unsat unsat +113 unsat unsat +114 unsat unsat +115 sat unknown +116 sat unknown +117 sat timeout +118 sat unknown +119 timeout timeout +120 sat timeout +121 sat timeout +122 timeout timeout +123 timeout timeout +124 sat timeout +125 sat timeout +126 timeout timeout +127 sat timeout +128 sat unknown +129 sat timeout +130 timeout timeout +131 timeout timeout +132 timeout unknown +133 unsat timeout +134 unsat unsat +135 sat unknown +136 unsat unsat +137 unsat unsat +138 sat unknown +139 unsat timeout +140 sat unknown +141 unsat unsat +142 unsat unsat +143 sat unknown +144 sat unknown +145 unsat unsat +146 sat unknown +147 unsat unsat +148 unsat timeout +149 sat timeout +150 unsat unsat +151 sat timeout +152 unsat timeout +153 sat unknown +154 sat timeout +155 sat unknown +156 sat timeout +157 unsat timeout +158 unsat timeout +159 sat unknown +160 sat timeout +161 sat timeout +162 sat unknown +163 sat unknown +164 unsat timeout +165 unsat timeout +166 sat unknown +167 sat timeout +168 unsat timeout +169 timeout timeout +170 timeout timeout +171 timeout timeout +172 sat timeout +173 timeout timeout +174 timeout unknown +175 timeout timeout +176 timeout timeout +177 timeout timeout +178 sat timeout +179 timeout timeout +180 sat timeout +181 timeout timeout +182 sat timeout +183 timeout timeout +184 sat timeout +185 unknown timeout +186 sat unknown +187 timeout timeout +188 timeout timeout +189 timeout unknown +190 sat timeout +191 timeout timeout +192 sat timeout +193 sat timeout +194 timeout timeout +195 timeout timeout +196 timeout timeout +197 sat timeout +198 unsat unsat +199 unsat unsat +200 sat timeout +201 sat sat +202 sat unknown +203 unsat unsat +204 sat timeout +205 sat timeout +206 sat timeout +207 sat timeout +208 sat timeout +209 timeout timeout +210 sat timeout +211 unsat unsat +212 timeout timeout +213 sat timeout +214 timeout timeout +215 timeout timeout +216 sat timeout +217 timeout timeout +218 timeout timeout +219 sat timeout +220 timeout timeout +221 sat timeout +222 sat timeout +223 sat sat +224 sat timeout +225 timeout timeout +226 timeout timeout +227 sat timeout +228 sat timeout +229 sat timeout +230 sat timeout +231 sat timeout +232 sat sat +233 sat timeout +234 sat timeout +235 sat timeout +236 sat timeout +237 sat unknown +238 sat timeout +239 timeout timeout +240 timeout unknown +241 timeout unknown +242 timeout timeout +243 timeout timeout +244 sat timeout +245 unsat unsat +246 sat sat +247 unsat unsat +248 sat sat +249 unsat timeout +250 sat sat +251 sat sat +252 sat sat +253 unsat unsat +254 sat sat +255 sat sat +256 unsat unsat +257 sat timeout +258 sat sat +259 unsat unsat +260 sat sat +261 sat sat +262 sat unknown +263 unsat unsat +264 unsat unsat +265 timeout timeout +266 unsat timeout +267 timeout timeout +268 unsat unsat +269 sat sat +270 sat timeout +271 unsat unsat +272 sat unknown +273 unsat unsat +274 timeout timeout +275 unsat timeout +276 unsat timeout +277 unsat unsat +278 sat sat +279 unsat timeout +280 unsat timeout +281 timeout timeout +282 timeout timeout +283 unsat timeout +284 timeout timeout +285 timeout timeout +286 unsat timeout +287 timeout timeout +288 sat timeout +289 unsat timeout +290 timeout timeout +291 sat timeout +292 timeout timeout +293 sat timeout +294 timeout timeout +295 unsat timeout +296 timeout timeout +297 unsat timeout +298 timeout timeout +299 sat timeout +300 timeout timeout +301 unsat timeout +302 timeout timeout +303 timeout timeout +304 timeout timeout +305 unsat timeout +306 timeout timeout +307 unsat timeout +308 timeout timeout +309 timeout timeout +310 timeout timeout +311 timeout timeout +312 sat timeout +313 timeout timeout +314 unsat timeout +315 timeout timeout +316 timeout timeout +317 unsat timeout +318 sat timeout +319 unsat timeout +320 sat timeout +321 timeout timeout +322 timeout timeout +323 sat timeout +324 sat timeout +325 timeout timeout +326 unsat timeout +327 timeout timeout +328 unsat timeout +329 sat timeout +330 timeout timeout +331 timeout timeout +332 timeout timeout +333 unsat timeout +334 sat timeout +335 sat timeout +336 unsat unsat +337 sat timeout +338 unsat unsat +339 unsat unsat +340 sat timeout +341 sat timeout +342 unsat unsat +343 unsat timeout +344 unsat timeout +345 unsat unsat +346 sat timeout +347 sat timeout +348 sat timeout +349 unsat unsat +350 unsat unsat +351 unsat timeout +352 sat timeout +353 unsat timeout +354 unsat timeout +355 sat timeout +356 unsat timeout +357 timeout timeout +358 sat timeout +359 sat timeout +360 sat timeout +361 timeout timeout +362 sat timeout +363 sat timeout +364 unsat timeout +365 sat timeout +366 sat sat +367 sat sat +368 sat unknown +369 sat sat +370 sat sat +371 sat sat +372 sat sat +373 sat sat +374 sat sat +375 sat sat +376 sat sat +377 sat unknown +378 sat sat +379 sat sat +380 sat sat +381 sat sat +382 sat sat +383 sat sat +384 sat timeout +385 sat sat +386 sat timeout +387 unsat unsat +388 sat sat +389 unsat unsat +390 sat timeout +391 sat sat +392 sat sat +393 unsat timeout +394 sat timeout +395 sat timeout +396 sat sat +397 sat sat +398 sat timeout +399 unsat unsat +400 unsat timeout +401 sat timeout +402 timeout timeout +403 timeout timeout +404 sat timeout +405 timeout timeout +406 timeout timeout +407 sat timeout +408 sat timeout +409 unsat timeout +410 sat timeout +411 unsat timeout +412 sat timeout +413 sat sat +414 unsat timeout +415 sat timeout +416 sat timeout +417 sat timeout +418 sat sat +419 unsat timeout +420 sat timeout +421 sat timeout +422 unsat timeout +423 unsat unsat +424 sat timeout +425 sat timeout +426 unsat timeout +427 unsat unsat +428 sat timeout +429 unsat timeout +430 unsat timeout +431 unsat timeout +432 sat timeout +433 sat timeout +434 unsat timeout +435 sat timeout +436 unsat unsat +437 unsat timeout +438 timeout timeout +439 sat timeout +440 sat timeout +441 sat timeout +442 unsat unsat +443 sat timeout +444 unsat unsat +445 sat timeout +446 sat timeout +447 sat timeout +448 unsat timeout +449 sat timeout +450 timeout timeout +451 unsat timeout +452 unsat timeout +453 sat timeout +454 sat timeout diff --git a/benchmarks/comp23-LIA-nonlin.txt b/benchmarks/comp23-LIA-nonlin.txt new file mode 100644 index 000000000..4b1b5fadd --- /dev/null +++ b/benchmarks/comp23-LIA-nonlin.txt @@ -0,0 +1,427 @@ +### Z3 ADCL +000 sat timeout +001 sat timeout +002 sat timeout +003 sat timeout +004 unsat timeout +005 sat timeout +006 sat timeout +007 sat timeout +008 sat timeout +009 sat timeout +010 sat timeout +011 sat timeout +012 timeout timeout +013 timeout timeout +014 timeout timeout +015 timeout timeout +016 timeout timeout +017 timeout timeout +018 sat timeout +019 timeout timeout +020 sat timeout +021 timeout timeout +022 timeout timeout +023 timeout timeout +024 timeout timeout +025 timeout timeout +026 timeout timeout +027 timeout timeout +028 timeout timeout +029 timeout timeout +030 timeout timeout +031 timeout timeout +032 timeout timeout +033 timeout timeout +034 timeout timeout +035 timeout timeout +036 timeout timeout +037 timeout timeout +038 timeout timeout +039 timeout timeout +040 timeout timeout +041 timeout timeout +042 timeout timeout +043 timeout timeout +044 timeout timeout +045 timeout timeout +046 timeout timeout +047 timeout timeout +048 unsat unsat +049 unsat unsat +050 sat timeout +051 sat timeout +052 unsat unsat +053 sat unknown +054 sat timeout +055 sat unknown +056 unsat unsat +057 unsat timeout +058 sat timeout +059 sat timeout +060 sat timeout +061 sat timeout +062 sat timeout +063 timeout timeout +064 sat timeout +065 timeout timeout +066 timeout timeout +067 timeout timeout +068 sat timeout +069 unsat unsat +070 unsat unsat +071 unsat unsat +072 unsat unsat +073 sat timeout +074 sat timeout +075 sat timeout +076 sat timeout +077 sat timeout +078 timeout timeout +079 sat timeout +080 sat unknown +081 timeout timeout +082 sat timeout +083 timeout timeout +084 timeout timeout +085 timeout timeout +086 timeout timeout +087 timeout timeout +088 sat timeout +089 timeout timeout +090 timeout timeout +091 timeout timeout +092 timeout timeout +093 timeout timeout +094 sat timeout +095 sat timeout +096 sat timeout +097 sat timeout +098 sat timeout +099 unsat unsat +100 sat timeout +101 unsat unsat +102 unsat timeout +103 unsat timeout +104 unsat unsat +105 sat timeout +106 unsat timeout +107 sat timeout +108 unsat unsat +109 unsat unsat +110 sat timeout +111 unsat timeout +112 sat timeout +113 sat timeout +114 timeout timeout +115 timeout timeout +116 sat timeout +117 timeout timeout +118 timeout timeout +119 unsat timeout +120 timeout timeout +121 unsat timeout +122 timeout timeout +123 timeout timeout +124 unsat timeout +125 sat timeout +126 unsat unsat +127 sat timeout +128 sat timeout +129 unsat timeout +130 timeout timeout +131 sat timeout +132 timeout timeout +133 timeout timeout +134 timeout timeout +135 timeout timeout +136 timeout timeout +137 sat timeout +138 sat timeout +139 sat timeout +140 timeout timeout +141 timeout timeout +142 timeout timeout +143 sat timeout +144 timeout timeout +145 timeout timeout +146 sat timeout +147 timeout timeout +148 timeout timeout +149 timeout timeout +150 timeout timeout +151 sat timeout +152 sat timeout +153 sat timeout +154 sat timeout +155 timeout timeout +156 sat timeout +157 timeout timeout +158 unsat unsat +159 timeout timeout +160 sat timeout +161 sat timeout +162 sat timeout +163 timeout timeout +164 timeout timeout +165 timeout timeout +166 timeout timeout +167 timeout timeout +168 timeout timeout +169 sat timeout +170 sat timeout +171 unsat unsat +172 sat sat +173 sat sat +174 sat timeout +175 timeout timeout +176 sat timeout +177 sat timeout +178 timeout timeout +179 timeout timeout +180 timeout timeout +181 sat timeout +182 timeout timeout +183 timeout timeout +184 timeout timeout +185 sat sat +186 sat unknown +187 sat timeout +188 unsat timeout +189 unsat unsat +190 unsat unsat +191 unsat timeout +192 unsat unsat +193 unsat unsat +194 unsat unsat +195 unsat unsat +196 unsat timeout +197 sat sat +198 sat unknown +199 unsat unsat +200 sat sat +201 unsat unsat +202 unsat unsat +203 unsat unsat +204 unsat unsat +205 unsat unsat +206 unsat unsat +207 unsat unsat +208 sat unknown +209 sat sat +210 sat sat +211 sat sat +212 sat sat +213 unsat unsat +214 unsat timeout +215 timeout timeout +216 sat sat +217 unsat timeout +218 unsat unsat +219 sat sat +220 sat sat +221 sat timeout +222 sat timeout +223 sat timeout +224 unsat timeout +225 sat unknown +226 sat timeout +227 sat unknown +228 sat unknown +229 unsat unsat +230 sat timeout +231 unsat timeout +232 sat timeout +233 sat timeout +234 unsat timeout +235 unsat unsat +236 unsat timeout +237 unsat unsat +238 unsat unsat +239 sat timeout +240 sat timeout +241 sat timeout +242 sat timeout +243 sat unknown +244 sat timeout +245 sat timeout +246 sat timeout +247 unsat timeout +248 unsat unsat +249 unsat timeout +250 unsat timeout +251 unsat unsat +252 sat sat +253 unsat unsat +254 unsat timeout +255 unsat unsat +256 timeout timeout +257 sat unknown +258 sat unknown +259 timeout timeout +260 timeout timeout +261 unsat timeout +262 timeout timeout +263 timeout timeout +264 timeout timeout +265 timeout timeout +266 timeout timeout +267 timeout timeout +268 timeout timeout +269 unsat timeout +270 timeout timeout +271 timeout timeout +272 timeout timeout +273 sat timeout +274 unsat timeout +275 timeout timeout +276 timeout timeout +277 timeout timeout +278 timeout timeout +279 timeout timeout +280 timeout timeout +281 sat timeout +282 timeout timeout +283 unsat timeout +284 timeout timeout +285 timeout timeout +286 timeout timeout +287 timeout timeout +288 timeout timeout +289 sat unknown +290 sat timeout +291 timeout timeout +292 timeout timeout +293 timeout timeout +294 timeout timeout +295 timeout timeout +296 timeout timeout +297 timeout timeout +298 timeout timeout +299 timeout timeout +300 unsat timeout +301 timeout timeout +302 timeout timeout +303 timeout timeout +304 timeout timeout +305 timeout timeout +306 timeout timeout +307 timeout timeout +308 timeout timeout +309 timeout timeout +310 timeout timeout +311 timeout timeout +312 sat timeout +313 timeout timeout +314 timeout timeout +315 unsat timeout +316 timeout timeout +317 timeout timeout +318 unsat timeout +319 timeout timeout +320 timeout timeout +321 sat timeout +322 timeout timeout +323 timeout timeout +324 timeout timeout +325 timeout timeout +326 timeout timeout +327 sat unknown +328 timeout timeout +329 timeout timeout +330 timeout timeout +331 timeout timeout +332 timeout timeout +333 timeout timeout +334 timeout timeout +335 timeout timeout +336 unsat timeout +337 timeout timeout +338 unsat timeout +339 sat timeout +340 timeout timeout +341 timeout timeout +342 timeout timeout +343 sat timeout +344 timeout timeout +345 timeout timeout +346 unsat timeout +347 timeout timeout +348 timeout timeout +349 timeout timeout +350 timeout timeout +351 timeout timeout +352 timeout timeout +353 timeout timeout +354 timeout timeout +355 timeout timeout +356 timeout timeout +357 sat timeout +358 timeout timeout +359 timeout timeout +360 timeout timeout +361 timeout timeout +362 unsat timeout +363 timeout timeout +364 timeout timeout +365 sat unknown +366 sat unknown +367 unsat timeout +368 unsat unsat +369 sat unknown +370 sat unknown +371 unsat unsat +372 sat unknown +373 sat unknown +374 unsat timeout +375 sat unknown +376 timeout timeout +377 sat unknown +378 sat unknown +379 unsat timeout +380 sat sat +381 unsat unsat +382 sat unknown +383 unsat unsat +384 sat sat +385 sat sat +386 sat sat +387 sat sat +388 sat sat +389 sat unknown +390 sat sat +391 unsat unsat +392 unsat unsat +393 sat sat +394 sat sat +395 sat sat +396 sat timeout +397 sat timeout +398 sat timeout +399 sat timeout +400 sat timeout +401 sat unknown +402 sat sat +403 sat timeout +404 sat unknown +405 sat timeout +406 sat timeout +407 unsat timeout +408 sat sat +409 sat sat +410 sat unknown +411 sat timeout +412 sat unknown +413 sat unknown +414 sat timeout +415 sat timeout +416 timeout timeout +417 timeout timeout +418 sat unknown +419 timeout timeout +420 sat unknown +421 sat timeout +422 timeout timeout +423 timeout timeout +424 timeout timeout +425 timeout timeout diff --git a/benchmarks/review22.txt b/benchmarks/review22.txt new file mode 100644 index 000000000..3c710fcb1 --- /dev/null +++ b/benchmarks/review22.txt @@ -0,0 +1,18 @@ +### Z3 ADCL +087 timeout timeout +049 unsat timeout +119 timeout timeout +126 timeout timeout +130 timeout timeout +133 unsat timeout +139 unsat timeout +148 unsat timeout +152 unsat timeout +157 unsat timeout +158 unsat timeout +164 unsat timeout +165 unsat timeout +168 unsat timeout +249 unsat timeout +351 unsat timeout +442 unsat timeout diff --git a/run_benchmark.sh b/run_benchmark.sh new file mode 100755 index 000000000..9bdec3bb4 --- /dev/null +++ b/run_benchmark.sh @@ -0,0 +1,79 @@ +#!/bin/bash + +set -e + +# Switch working directory to the folder, where this script is laying around. +# That way all paths are guaranteed to be relative to the script location. +pushd $(dirname ${BASH_SOURCE[0]}) + +cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo +pushd build +make -j4 +popd + +# # gdb --args \ +# time ./build/loat-static \ +# --mode reachability \ +# --format horn \ +# --proof-level 0 \ +# "../chc-comp22-benchmarks/LIA/chc-LIA_076.smt2" +# # "../chc-comp23-benchmarks/LIA-nonlin/chc-LIA_075.smt2" +# # "../chc-comp22-benchmarks/LIA/chc-LIA_148_unknown.smt2" +# # "../chc-comp22-benchmarks/LIA/test3.smt2" + +# popd +# exit + +########################################################################## + +benchmark="LIA" + +printf "### %-7s %-7s %-7s \n" "Z3" "ADCL" "now" + +while IFS= read -r line +do + if [[ $line =~ ^#.*$ ]] || [[ "$line" = "" ]]; then + # skip comments and empty lines + continue + else + read idx z3_result adcl_result <<< "$line" + file="../chc-comp22-benchmarks/${benchmark}/chc-${benchmark}_${idx}.smt2" + # file="../chc-comp23-benchmarks/${benchmark}-nonlin/chc-${benchmark}_${idx}.smt2" + + # if true; then + # if [[ "$z3_result" == "unsat" ]] && [[ "$adcl_result" == "timeout" ]]; then + # if [[ "$z3_result" != "sat" ]] && [[ "$z3_result" != "timeout" ]]; then + # if [[ "$z3_result" != "timeout" ]]; then + if [[ "$z3_result" == "unsat" ]]; then + # if [[ "$adcl_result" == "unsat" ]]; then + set +e + result=$(timeout 20 ./build/loat-static --mode reachability --format horn --proof-level 0 "$file") + # result=$(timeout 5 z3 "$file") + exit_status=$? + set -e + + if [[ $exit_status -eq 0 ]]; then + result=$(echo "$result" | head -n 1) + # result="$result" + elif [ $exit_status -eq 124 ]; then + result="timeout" + else + result="error" + fi + + printf "$idx %-7s %-7s %-7s \n" $z3_result $adcl_result $result + + # else + # # if we skip an instance nevertheless include it in the output + # # so the log can easily be copied and saved as a whole + # printf "$idx %-7s %-7s %-7s \n" $z3_result $adcl_result $adcl_result + fi + + fi +# done < "./benchmarks/review23.txt" +done < "./benchmarks/${benchmark}.txt" +# done < "./benchmarks/comp23-${benchmark}-nonlin.txt" + +# "undo" pushd +popd + diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ce5e9a6f0..a3735f56a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -7,6 +7,7 @@ add_subdirectory(util) add_subdirectory(redundance) add_subdirectory(abmc) add_subdirectory(bmc) +add_subdirectory(nonlinear) target_sources(${EXECUTABLE} PRIVATE diff --git a/src/abmc/abmc.cpp b/src/abmc/abmc.cpp index 807135465..a86694891 100644 --- a/src/abmc/abmc.cpp +++ b/src/abmc/abmc.cpp @@ -341,7 +341,8 @@ void ABMC::analyze() { its.print(std::cout); } proof.majorProofStep("Initial ITS", ITSProof(), its); - const auto res{Preprocess::preprocess(its)}; + const auto res {Preprocess::preprocess(its)}; + const auto res{Preprocess::preprocess(its, false)}; if (res) { proof.concat(res.getProof()); if (Config::Analysis::log) { diff --git a/src/analysis/preprocessing.cpp b/src/analysis/preprocessing.cpp index 96cb2b1d1..fb2998daa 100644 --- a/src/analysis/preprocessing.cpp +++ b/src/analysis/preprocessing.cpp @@ -26,7 +26,16 @@ using namespace std; +// FIXME: for trivial ITS with no (reachable) initial locations or no (reachable) sinks, +// we should return SAT, but due to this preprocessing step we will throw an error instead. ResultViaSideEffects remove_irrelevant_clauses(ITSProblem &its, bool forward) { + if (its.getInitialTransitions().size() == 0) { + throw std::logic_error("remove_irrelevant_clauses: ITS has no initial transitions"); + } + if (its.getSinkTransitions().size() == 0) { + throw std::logic_error("remove_irrelevant_clauses: ITS has no sink transitions"); + } + std::unordered_set keep; std::stack todo; for (const auto x: forward ? its.getInitialTransitions() : its.getSinkTransitions()) { @@ -148,13 +157,18 @@ ResultViaSideEffects refine_dependency_graph(ITSProblem &its) { return res; } -ResultViaSideEffects Preprocess::preprocess(ITSProblem &its) { +ResultViaSideEffects Preprocess::preprocess(ITSProblem &its, bool incremental_mode) { ResultViaSideEffects res; ResultViaSideEffects sub_res; if (Config::Analysis::log) { std::cout << "starting preprocesing..." << std::endl; } - if (Config::Analysis::reachability()) { + if (Config::Analysis::reachability() && !incremental_mode) { + // In this preprocessing step we remove transitions that are not "forward reachable" + // from an initial location or "backward reachable" from a sink. Note, that this step + // is not valid if the ITS contains non-linear CHCs. For example, a sink appears to + // be unreachable if it is only reachable via a non-linear CHC (which are not accounted + // for in the dependency graph). if (Config::Analysis::log) { std::cout << "removing irrelevant clauses..." << std::endl; } @@ -166,17 +180,49 @@ ResultViaSideEffects Preprocess::preprocess(ITSProblem &its) { res.succeed(); res.majorProofStep("Removed Irrelevant Clauses", sub_res.getProof(), its); } - } - if (Config::Analysis::log) { - std::cout << "chaining linear paths..." << std::endl; - } - sub_res = chainLinearPaths(its); - if (Config::Analysis::log) { - std::cout << "finished chaining linear paths" << std::endl; - } - if (sub_res) { - res.succeed(); - res.majorProofStep("Chained Linear Paths", sub_res.getProof(), its); + + /* + Chaining linear paths is also problematic in incremental mode because + we remove the chained rules/facts, which cuts-off paths that might be + reachable via a non-linear rule. For example, consider the CHC problem: + + fib(1,1) + fib(2,1) + fib(a,c) /\ fib(b,d) /\ b=a+1 ==> f(b+1,c+d) + fib(5,5) ==> false + + The fact `fib(5,5)` is reachable so the problem should be UNSAT. + However, when we compute the resolvents of the non-linear clause with + all facts we get: + + fib(0,c) ==> fib(2,c+1) (R1) + fib(1,c) ==> fib(3,c+1) (R2) + fib(2,d) ==> fib(3,d+1) (R3) + fib(3,y) ==> fib(4,d+1) (R4) + + If we now chain linear paths we get: + + [fib(1,1), R2] = fib(3,2) + [fib(2,1), R3] = fib(3,2) + + [fib(3,2), R4] = fib(4,3) + + At this point we remove all facts except `fib(4,3)` because in the + linear context we can assume that all paths from these facts lead + to `fib(4,3)` anyway. However in the non-linear context we need to + keep `fib(3,2)` to derive `fib(5,5)`. + */ + if (Config::Analysis::log) { + std::cout << "chaining linear paths..." << std::endl; + } + sub_res = chainLinearPaths(its); + if (Config::Analysis::log) { + std::cout << "finished chaining linear paths" << std::endl; + } + if (sub_res) { + res.succeed(); + res.majorProofStep("Chained Linear Paths", sub_res.getProof(), its); + } } if (Config::Analysis::log) { std::cout << "preprocessing rules..." << std::endl; diff --git a/src/analysis/preprocessing.hpp b/src/analysis/preprocessing.hpp index bb02e875a..626f27d28 100644 --- a/src/analysis/preprocessing.hpp +++ b/src/analysis/preprocessing.hpp @@ -22,6 +22,6 @@ namespace Preprocess { - ResultViaSideEffects preprocess(ITSProblem &its); + ResultViaSideEffects preprocess(ITSProblem &its, bool incremental_mode); } diff --git a/src/analysis/reachability.cpp b/src/analysis/reachability.cpp index 2adcffb8d..f1876ccbd 100644 --- a/src/analysis/reachability.cpp +++ b/src/analysis/reachability.cpp @@ -1,4 +1,6 @@ #include "reachability.hpp" +#include "config.hpp" +#include "linearsolver.hpp" #include "preprocessing.hpp" #include "rulepreprocessing.hpp" #include "loopacceleration.hpp" @@ -111,10 +113,26 @@ ITSProof* ProvedUnsat::operator->() { return &proof; } -Reachability::Reachability(ITSProblem &chcs): +Reachability::Reachability(ITSProblem &chcs, bool incremental_mode): chcs(chcs), - drop(true) { + drop(true), + analysis_result(LinearSolver::Result::Pending), + incremental_mode(incremental_mode) { solver->enableModels(); + proof.majorProofStep("Initial ITS", ITSProof(), chcs); + if (Config::Analysis::log) { + std::cout << "Initial ITS" << std::endl; + ITSExport::printForProof(chcs, std::cout); + } + const auto res {Preprocess::preprocess(chcs, incremental_mode)}; + if (res) { + proof.concat(res.getProof()); + if (Config::Analysis::log) { + std::cout << "Simplified ITS" << std::endl; + ITSExport::printForProof(chcs, std::cout); + } + } + init(); } Step::Step(const TransIdx transition, const BoolExpr &sat, const Subs &var_renaming, const Rule &resolvent): @@ -227,10 +245,6 @@ void Reachability::update_cpx() { } Rule Reachability::compute_resolvent(const TransIdx idx, const BoolExpr &implicant) const { - static Rule dummy(top(), Subs()); - if (!Config::Analysis::complexity()) { - return dummy; - } auto resolvent = idx->withGuard(implicant); if (!trace.empty()) { resolvent = Chaining::chain(trace.back().resolvent, resolvent).first; @@ -322,6 +336,7 @@ void Reachability::print_state() { proof.storeSubProof(state_p); } +// TODO: do we need this function? ITS also has the function `getProgVars` now. void Reachability::init() { srand(42); for (const auto &x: chcs.getVars()) { @@ -329,9 +344,6 @@ void Reachability::init() { prog_vars.insert(x); } } - for (const auto &r: chcs.getAllTransitions()) { - last_orig_clause = std::max(last_orig_clause, r.getId()); - } } void Reachability::luby_next() { @@ -349,7 +361,7 @@ void Reachability::luby_next() { void Reachability::unsat() { const auto res = Config::Analysis::reachability() ? "unsat" : "NO"; - std::cout << res << std::endl << std::endl; + analysis_result = analysis_result_from(res); if (!Config::Analysis::log && Proof::disabled()) { return; } @@ -373,7 +385,7 @@ void Reachability::unsat() { } void Reachability::unknown() { - std::cout << "unknown" << std::endl << std::endl; + analysis_result = analysis_result_from("unknown"); if (!Config::Analysis::log && Proof::disabled()) { return; } @@ -470,15 +482,16 @@ TransIdx Reachability::add_learned_clause(const Rule &accel, const unsigned back const auto fst = trace.at(backlink).clause_idx; const auto last = trace.back().clause_idx; const auto loop_idx = chcs.addLearnedRule(accel, fst, last); + learned_clause_ids.insert(loop_idx->getId()); return loop_idx; } bool Reachability::is_learned_clause(const TransIdx idx) const { - return idx->getId() > last_orig_clause; + return learned_clause_ids.contains(idx->getId()); } bool Reachability::is_orig_clause(const TransIdx idx) const { - return idx->getId() <= last_orig_clause; + return !is_learned_clause(idx); } RuleResult Reachability::instantiate(const NumVar &n, const Rule &rule) const { @@ -541,7 +554,7 @@ std::unique_ptr Reachability::learn_clause(const Rule &rule, cons } if (accel_res.accel) { // acceleration succeeded, simplify the result - auto simplified = Preprocess::preprocessRule(accel_res.accel->rule); + auto simplified = Preprocess::preprocessRule(accel_res.accel->rule); if (simplified->getUpdate() != simp->getUpdate()) { // accelerated rule differs from the original one, update the result if (Config::Analysis::complexity()) { @@ -594,7 +607,7 @@ void Reachability::drop_until(const int new_size) { } } -std::unique_ptr Reachability::handle_loop(const unsigned backlink) { +std::unique_ptr Reachability::handle_loop(const unsigned backlink, LinearSolver::ConstraintTier max_constr_tier) { const auto lang {build_language(backlink)}; auto closure {lang}; redundancy->transitive_closure(closure); @@ -635,7 +648,18 @@ std::unique_ptr Reachability::handle_loop(const unsigned backlink } const auto accel_state {*state->succeeded()}; const auto learned_clauses {**accel_state}; + bool do_drop {drop || (backlink == trace.size() - 1 && learned_clauses.prefix <= 1 && learned_clauses.period == 1)}; + + // To respect `max_constraint_tier` we don't replace the recursive suffix with a + // learned clause if at least one of the learned clauses has a higher constraint tier + // then the maximum dictated by `max_constraint_tier` right now. + for (const auto idx: learned_clauses.res) { + if (constraint_tier_of(idx) > max_constr_tier) { + do_drop = false; + } + } + if (do_drop) { drop_until(backlink); } @@ -686,6 +710,24 @@ bool Reachability::try_to_finish() { return false; } +LinearSolver::Result Reachability::analysis_result_from(std::string res) const { + if (res == "sat") { + return LinearSolver::Result::Sat; + } else if (res == "unsat") { + return LinearSolver::Result::Unsat; + } else if (res == "unknown") { + return LinearSolver::Result::Unknown; + } else if (res == "pending") { + return LinearSolver::Result::Pending; + } else { + throw std::logic_error("undefined analysis result"); + } +} + +LinearSolver::Result Reachability::get_analysis_result() const { + return analysis_result; +} + unsigned Reachability::get_penalty(const TransIdx idx) const { const auto it {penalty.find(idx)}; if (it != penalty.end()) { @@ -699,26 +741,76 @@ void Reachability::bump_penalty(const TransIdx idx) { penalty.emplace(idx, 0).first->second++; } -void Reachability::analyze() { - proof.majorProofStep("Initial ITS", ITSProof(), chcs); - if (Config::Analysis::log) { - std::cout << "Initial ITS" << std::endl; - ITSExport::printForProof(chcs, std::cout); +/** + * The resolvent of the entire current trace represents a fact, + * that can be converted into a `Clause`. If the trace is empty, + * this function returns nullopt. + */ +const std::optional Reachability::trace_as_fact() { + if (trace.empty()) { + return {}; + } else { + const Step step = trace.back(); + return chcs.clauseFrom( + chcs.getInitialLocation(), + chcs.getRhsLoc(step.clause_idx), + step.resolvent + ); } - const auto res {Preprocess::preprocess(chcs)}; - if (res) { - proof.concat(res.getProof()); - if (Config::Analysis::log) { - std::cout << "Simplified ITS" << std::endl; - ITSExport::printForProof(chcs, std::cout); +} + +LinearSolver::ConstraintTier Reachability::constraint_tier_of(TransIdx rule) const { + if (rule->isLinear()) { + return LinearSolver::ConstraintTier::Linear; + } else if (rule->isPoly()) { + return LinearSolver::ConstraintTier::Polynomial; + } else { + return LinearSolver::ConstraintTier::Exponential; + } +} + +void Reachability::analyze() { + // First only derive "easy" to handle rules with linear guard. If that's not enough + // also try rules with polynomial guard. Otherwise also consider exponential + // (arbitrary) guards. + for (const auto tier: LinearSolver::constraint_tiers) { + derive_new_facts(tier); + + if (get_analysis_result() == LinearSolver::Result::Unsat) { + break; } } - init(); + + switch (get_analysis_result()) { + case LinearSolver::Result::Sat: + std::cout << "sat"; + break; + case LinearSolver::Result::Unsat: + std::cout << "unsat"; + break; + case LinearSolver::Result::Unknown: + std::cout << "unknown"; + break; + case LinearSolver::Result::Pending: + throw std::logic_error("exited main loop although analysis result is pending"); + } + + std::cout << std::endl << std::endl << std::endl; +} + +const std::set Reachability::derive_new_facts(LinearSolver::ConstraintTier max_constr_tier) { + luby_count = 0; + luby = {1,1}; + restart(); + + std::set derived_facts; + if (try_to_finish()) { - return; + return derived_facts; } blocked_clauses[0].clear(); do { + // QUESTION: still correct handling luby this way in incremental mode? ++luby_count; size_t next_restart = luby_unit * luby.second; std::unique_ptr state; @@ -729,7 +821,7 @@ void Reachability::analyze() { backlink = has_looping_suffix(*backlink - 1)) { auto step {trace[*backlink]}; auto simple_loop {*backlink == trace.size() - 1}; - state = handle_loop(*backlink); + state = handle_loop(*backlink, max_constr_tier); if (state->restart()) { break; } else if (state->covered()) { @@ -744,7 +836,7 @@ void Reachability::analyze() { proof.majorProofStep("Accelerate", (*state->succeeded())->getProof(), chcs); print_state(); if ((drop || simple_loop) && try_to_finish()) { - return; + return derived_facts; } } else if (state->dropped()) { if (simple_loop) { @@ -752,36 +844,40 @@ void Reachability::analyze() { } proof.majorProofStep("Accelerate and Drop", state->dropped()->get_proof(), chcs); print_state(); + break; } else if (state->unsat()) { proof.majorProofStep("Nonterm", **state->unsat(), chcs); proof.headline("Step with " + std::to_string(trace.back().clause_idx->getId())); print_state(); unsat(); - return; + + return derived_facts; } else if (state->unroll() && state->unroll()->acceleration_failed()) { - // stop searching for longer loops if the current one was already too complicated break; } } } if (luby_count >= next_restart || (state && state->restart()) || !check_consistency()) { if (Config::Analysis::log) std::cout << "restarting after " << luby_count << " iterations" << std::endl; - // restart - while (!trace.empty()) { - pop(); - } - luby_next(); - proof.headline("Restart"); + restart(); } + auto try_set = trace.empty() ? chcs.getInitialTransitions() : chcs.getSuccessors(trace.back().clause_idx); for (auto it = try_set.begin(); it != try_set.end();) { - if (is_learned_clause(*it) && locked.contains(*redundancy->get_language(*it))) { + // Only consider rules for "Step" whose guard has at most the constraint tier + // configured for the current run. For example if `max_constr_tier` is `Polynomial`, + // we only consider rules with `Linear` or `Polynomial` guard but ignore rules with + // `Exponential` guard. + if (constraint_tier_of(*it) > max_constr_tier) { + it = try_set.erase(it); + } else if (is_learned_clause(*it) && locked.contains(*redundancy->get_language(*it))) { it = try_set.erase(it); } else { ++it; } } + std::vector to_try(try_set.begin(), try_set.end()); std::sort(to_try.begin(), to_try.end(), [this](const TransIdx x, const TransIdx y){ const auto p1 {get_penalty(x)}; @@ -798,37 +894,98 @@ void Reachability::analyze() { const auto implicant {resolve(idx)}; solver->pop(); if (implicant && store_step(idx, *implicant)) { - proof.headline("Step with " + std::to_string(idx->getId())); - print_state(); - update_cpx(); - all_failed = false; - break; + // Additional redundnacy check: if resolvent of trace (after step) is + // syntactially equivalent (up to renaming) to an already derived fact, + // then backtrack and try a different step. + if (derived_facts.contains(trace_as_fact().value())) { + backtrack(); + } else { + proof.headline("Step with " + std::to_string(idx->getId())); + print_state(); + update_cpx(); + all_failed = false; + break; + } } else { bump_penalty(idx); } } if (trace.empty()) { - break; + // TODO: is this the only place where we break out of the main loop with SAT? + proof.headline("Accept"); + if (Config::Analysis::complexity()) { + proof.result(cpx.toString()); + proof.print(); + } else { + unknown(); + } + + return derived_facts; } else if (all_failed) { + // Using a crude (additional) redundancy criterion for facts here. We identify facts by the trace that lead to them. + // This is only sufficient because equivalent facts can have multiple traces. We don't need to memoize the entire + // trace structure. It's enough to store clause_idx/implicant for each trace step. + std::vector> trace_id; + for (const auto &step: trace) { + trace_id.push_back(std::make_pair( + step.clause_idx, + step.implicant + )); + } + + // Assume non-linear solver already nows about facts that are initially part of the CHC problem, + // so don't forward them eihter: + bool is_initial_fact = trace.size() == 1 && chcs.isInitialTransition(trace[0].clause_idx); + + if (!seen_traces.contains(trace_id) && !is_initial_fact) { + derived_facts.insert(trace_as_fact().value()); + seen_traces.insert(trace_id); + } + backtrack(); proof.headline("Backtrack"); print_state(); } else if (try_to_finish()) { // check whether a query is applicable after every step and, importantly, before acceleration (which might approximate) - return; + return derived_facts; } } while (true); - proof.headline("Accept"); - if (Config::Analysis::complexity()) { - proof.result(cpx.toString()); - proof.print(); - } else { - unknown(); +} + +void Reachability::restart() { + while (!trace.empty()) { + pop(); + } + luby_next(); + proof.headline("Restart"); + + analysis_result = LinearSolver::Result::Pending; +} + +void Reachability::add_clauses(const std::set &clauses) { + for (const auto &chc: clauses) { + if (chc.isLinear()) { + chcs.addClause(chc); + } else { + throw std::logic_error("Reachability::add_clauses: tried to add non-linear CHC"); + } + } + + // only start preprocessing again if at least one new clause was added. + if (!clauses.empty()) { + // TODO: are other preprocessing steps also unsound when in non-linear context? + const auto res {Preprocess::preprocess(chcs, incremental_mode)}; + if (res) { + proof.concat(res.getProof()); + if (Config::Analysis::log) { + std::cout << "Simplified ITS" << std::endl; + ITSExport::printForProof(chcs, std::cout); + } + } } - std::cout << std::endl; } void Reachability::analyze(ITSProblem &its) { - Reachability(its).analyze(); + Reachability(its, false).analyze(); } } diff --git a/src/analysis/reachability.hpp b/src/analysis/reachability.hpp index 3625b4516..5109633b5 100644 --- a/src/analysis/reachability.hpp +++ b/src/analysis/reachability.hpp @@ -1,6 +1,7 @@ #pragma once #include "itsproblem.hpp" +#include "linearsolver.hpp" #include "itsresult.hpp" #include "ruleresult.hpp" #include "redundanceviaautomata.hpp" @@ -155,7 +156,7 @@ class Restart final: public LearningState { std::optional restart() override; }; -class Reachability { +class Reachability : public ILinearSolver { ITSProblem &chcs; @@ -182,11 +183,6 @@ class Reachability { VarSet prog_vars {}; - /** - * clauses up to this one are original ones, all other clauses are learned - */ - unsigned last_orig_clause {0}; - std::pair luby {1,1}; unsigned luby_unit {10}; @@ -210,9 +206,6 @@ class Reachability { RuleResult instantiate(const NumVar &n, const Rule &rule) const; - /** - * initializes all data structures after preprocessing - */ void init(); /** @@ -268,7 +261,7 @@ class Reachability { /** * does everything that needs to be done if the trace has a looping suffix */ - std::unique_ptr handle_loop(const unsigned backlink); + std::unique_ptr handle_loop(const unsigned backlink, LinearSolver::ConstraintTier max_constr_tier); /** * @return the start position of the looping suffix of the trace, if any, or -1 @@ -311,12 +304,34 @@ class Reachability { bool try_to_finish(); - Reachability(ITSProblem &its); - void analyze(); + void restart(); + + LinearSolver::Result analysis_result = LinearSolver::Result::Pending; + + LinearSolver::Result analysis_result_from(std::string res) const; + + const bool incremental_mode; + + std::set>> seen_traces; + + const std::optional trace_as_fact(); + + std::set learned_clause_ids; + + LinearSolver::ConstraintTier constraint_tier_of(TransIdx rule) const; + public: + Reachability(ITSProblem &chcs, bool incremental_mode); + + LinearSolver::Result get_analysis_result() const override; + + void add_clauses(const std::set &chc) override; + + const std::set derive_new_facts(LinearSolver::ConstraintTier max_constr_type) override; + static void analyze(ITSProblem &its); }; diff --git a/src/bmc/bmc.cpp b/src/bmc/bmc.cpp index 179d4be4c..44d512523 100644 --- a/src/bmc/bmc.cpp +++ b/src/bmc/bmc.cpp @@ -38,7 +38,7 @@ void BMC::analyze() { its.print(std::cout); } proof.majorProofStep("Initial ITS", ITSProof(), its); - const auto res {Preprocess::preprocess(its)}; + const auto res {Preprocess::preprocess(its, false)}; if (res) { proof.concat(res.getProof()); if (Config::Analysis::log) { diff --git a/src/its/itsproblem.cpp b/src/its/itsproblem.cpp index 19ee5e3a2..1b159b0ca 100644 --- a/src/its/itsproblem.cpp +++ b/src/its/itsproblem.cpp @@ -17,8 +17,11 @@ #include "itsproblem.hpp" #include "export.hpp" +#include "expr.hpp" +#include "inttheory.hpp" #include "smtfactory.hpp" #include "chain.hpp" +#include using namespace std; @@ -239,3 +242,265 @@ linked_hash_set ITSProblem::refineDependencyGraph() { size_t ITSProblem::size() const { return graph.size(); } + +const std::vector ITSProblem::getProgVars() const { + std::vector prog_vars; + prog_vars.reserve(numProgVars.size() + boolProgVars.size()); + for (const auto &var: numProgVars) { + prog_vars.push_back(var); + } + for (const auto &var: boolProgVars) { + prog_vars.push_back(var); + } + return prog_vars; +} + +/** + * Note that `clauseFrom(TransIdx rule)` can only be used for rules that are stored + * in the ITS. Not to turn an entire trace into a clause, because `ITSProblem::getLhsLoc` + * and `ITSProblem::getRhsLoc` are only defined for rules that are actually in the ITS. + * Thus, here is a generalized version of `clauseFrom` that accepts the lhs/rhs location + * explicitly. + */ +const Clause ITSProblem::clauseFrom(const LocationIdx lhs_loc, const LocationIdx rhs_loc, const Rule& rule) const { + const auto prog_vars = getProgVars(); + const auto update = rule.getUpdate(); + + // First we eliminate the location variable from the guard. In the ITS context, + // the location variable encoded the lhs predicate. But in clauses the lhs + // predicate is carried explicitly. Thus, the location variable turns into + // a superfluous temporary variable in the constraint, which causes subsequent + // calls of Clause::resolutionWith to give different results even on same + // arguments. For example, computing the resolvent of + // + // (fact_F) i1=0 ==> F(y) + // (rule_F) i1=1 /\ F(x) ==> F(x) + // + // where `i1` is the location variable, gives: + // + // F(x) /\ i1=0 /\ i2=0 ==> F(x) + // + // because `i1` appeared in both clauses and had to be renamed in `fact_F` to + // make the variables in the clauses disjoint. If we do the same computation + // again we get: + // + // F(x) /\ i1=0 /\ i3=0 ==> F(x) + // + // with `i3` instead of `i2`, because new variables are created using a global + // counter and `i2` already exists. Thus, the resolvents are not syntactially + // equal, which leads to otherwise trivially detectable redundancy. + // + // To eliminate the location variable, we substitute `i1` with it's value to + // make the literate trivially true, which simplifies away when we later call + // `simplify()` on the guard, i.e. we substitute + // + // (i1=0 ==> F(y))[i1/0] + // = ( 0=0 ==> F(y)) + // = (true ==> F(y)) + // + const auto eliminate_loc_var = Subs::build(NumVar::loc_var, lhs_loc); + const auto guard_without_loc_var = rule.getGuard()->subs(eliminate_loc_var); + + // `update` might map vars to non-var compound expressions or literals. + // The `Clause` representation only allows variable arguments though for the + // RHS predicate. So we extract those expressions and put them back into the + // clause guard. This is a bit ad-hoc and also un-does work of the linear + // solver and the preprocessing, so it might be worth optimizing later. + std::vector guard_conj = { guard_without_loc_var }; + std::vector rhs_args; + for (const Var &var: prog_vars) { + if (!update.contains(var)) { + // If `var` is not contained in `update` it's implicitly mapped to itself, + // i.e. `update` does not change the value of `var`. Thus, we add `var` + // directly into `rhs_args`. + rhs_args.push_back(var); + } else { + const auto optional_var = expr::toVar(update.get(var)); + + if (optional_var.has_value()) { + rhs_args.push_back(optional_var.value()); + } else { + const auto new_var = expr::next(var); + rhs_args.push_back(new_var); + guard_conj.push_back(expr::mkEq(expr::toExpr(new_var), update.get(var))); + } + } + } + + const auto final_guard = BExpression::buildAnd(guard_conj)->simplify(); + const auto rhs_pred_name = getPrintableLocationName(rhs_loc); + + const std::optional rhs = rhs_loc == getSink() + ? std::optional() + : FunApp(rhs_pred_name, rhs_args); + + if (lhs_loc == getInitialLocation()) { + // rule is a linear CHC with no LHS predicates, ie a "fact" + return Clause({}, rhs, final_guard).normalize(); + } else { + // rule is a linear CHC with exactly one LHS predicates, ie a "rule" + const auto lhs_pred_name = getPrintableLocationName(lhs_loc); + return Clause({ FunApp(lhs_pred_name, prog_vars) }, rhs, final_guard).normalize(); + } +} + +/** + * Converts an ITS rule (identified by a TransIdx) back to Clause representation. + * This does not restore the original representation after parsing perfectly, + * since number and order of predicate arguments is lost. + */ +const Clause ITSProblem::clauseFrom(TransIdx rule) const { + const LocationIdx lhs_loc = getLhsLoc(rule); + const LocationIdx rhs_loc = getRhsLoc(rule); + return clauseFrom(lhs_loc, rhs_loc, *rule); +} + +/** + * Adds a linear clause to the ITS problem by converting it to an ITS rule. + * Throws an error if the given clause is non-linear. + */ +void ITSProblem::addClause(const Clause &initial_chc) { + if (!initial_chc.isLinear()) { + throw std::logic_error("Tried to add non-linear clause to ITS"); + } + + // need to make sure that predicate arguments are pairwise distinct before + // converting to Rule. TODO: skip this + Clause c = removeDuplicatePredicateArguments(initial_chc); + + // If the clause is linear, extract the single LHS predicate. Or in case there are zero + // LHS predicates, construct a dummy predicate with the initial ITS location as the + // predicate symbol. + const auto initial_loc_name = getPrintableLocationName(getInitialLocation()); + const FunApp lhs = c.lhs.size() == 1 ? *c.lhs.begin() : FunApp(initial_loc_name, {}); + + const std::vector rhs_args = c.rhs.has_value() + ? c.rhs.value().args + : std::vector(); + + Subs ren; + // replace the arguments of the body predicate with the corresponding program variables + unsigned bool_arg {0}; + unsigned int_arg {0}; + for (unsigned i = 0; i < lhs.args.size(); ++i) { + if (std::holds_alternative(lhs.args[i])) { + ren.put( + std::get(lhs.args[i]), + numProgVars[int_arg] + ); + ++int_arg; + } else { + ren.put( + std::get(lhs.args[i]), + std::get(expr::toExpr(boolProgVars[bool_arg])) + ); + ++bool_arg; + } + } + VarSet cVars; + for (const auto &var: rhs_args) { + cVars.insert(var); + } + c.guard->collectVars(cVars); + // replace all other variables from the clause with temporary variables + for (const auto &x: cVars) { + if (!ren.contains(x)) { + ren.put(x, expr::toExpr(expr::next(x))); + } + } + bool_arg = 0; + int_arg = 0; + Subs up; + for (unsigned i = 0; i < rhs_args.size(); ++i) { + if (std::holds_alternative(rhs_args[i])) { + up.put(numProgVars[int_arg], ren.get(std::get(rhs_args[i]))); + ++int_arg; + } else if (std::holds_alternative(rhs_args[i])) { + up.put(boolProgVars[bool_arg], ren.get(std::get(rhs_args[i]))); + ++bool_arg; + } else { + throw std::logic_error("unsupported theory in CHCParseVisitor"); + } + } + for (unsigned i = int_arg; i < numProgVars.size(); ++i) { + up.put(numProgVars[i], NumVar::next()); + } + for (unsigned i = bool_arg; i < boolProgVars.size(); ++i) { + up.put(boolProgVars[i], std::get(expr::toExpr(BoolVar::next()))); + } + + const auto lhs_loc = getLocationIdx(lhs.name); + const auto rhs_pred_name = c.rhs.has_value() ? c.rhs.value().name : "LoAT_sink"; + const auto rhs_loc = c.rhs.has_value() ? getLocationIdx(c.rhs.value().name) : getSink(); + + if (!rhs_loc.has_value()) { + throw std::logic_error("tried to add clause with unknown RHS predicate called " + rhs_pred_name); + } + if (!lhs_loc.has_value()) { + throw std::logic_error("tried to add clause with unknown LHS predicate called " + lhs.name); + } + + up.put(NumVar::loc_var, rhs_loc.value()); + const BoolExpr guard = c.guard->subs(ren)->simplify() & Rel::buildEq(NumVar::loc_var, lhs_loc.value()); + addRule(Rule(guard, up), lhs_loc.value()); +} + +/** + * Construct an ITS instance from a set of clauses. Non-linear clauses are ignored in the sense that + * they don't contribute ITS rules. However, predicates that only occur in non-linear rules are added + * as locations, because if we later add new rules to the ITS via `addClause` that are derived from + * non-linear clauses, we expect all locations to already be known. + */ +ITSPtr ITSProblem::fromClauses(const std::set& chcs) { + std::vector chc_vec(chcs.begin(), chcs.end()); + return fromClauses(chc_vec); +} +ITSPtr ITSProblem::fromClauses(const std::vector& chc_problem) { + ITSPtr its = std::make_shared(); + + const auto [max_int_arity, max_bool_arity] = maxArity(chc_problem); + + its->setInitialLocation(its->addNamedLocation("LoAT_init")); + // Collect all predicate that appear in `chc_problem`, add them as + // locations to the ITS : + std::map locations; + for (const auto &chc: chc_problem) { + if (chc.rhs.has_value()) { + const auto& rhs = chc.rhs.value(); + + bool location_already_added = its->getLocationIdx(rhs.name).has_value(); + if (!location_already_added) { + locations[rhs.name] = its->addNamedLocation(rhs.name); + } + } + + for (const auto &pred: chc.lhs) { + bool location_already_added = its->getLocationIdx(pred.name).has_value(); + if (!location_already_added) { + locations[pred.name] = its->addNamedLocation(pred.name); + } + } + } + + // Construct "normalized" vectors of bool/int program variables, + // because in ITS rules must all have the same argument vector. + std::vector int_vars; + for (unsigned i = 0; i < max_int_arity; ++i) { + int_vars.emplace_back(NumVar::nextProgVar()); + } + its->numProgVars = int_vars; + + std::vector bool_vars; + for (unsigned i = 0; i < max_bool_arity; ++i) { + bool_vars.emplace_back(BoolVar::nextProgVar()); + } + its->boolProgVars = bool_vars; + + for (const auto &chc: chc_problem) { + if (chc.isLinear()) { + its->addClause(chc); + } + } + + return its; +} diff --git a/src/its/itsproblem.hpp b/src/its/itsproblem.hpp index 7c81878f4..8f6441a23 100644 --- a/src/its/itsproblem.hpp +++ b/src/its/itsproblem.hpp @@ -18,6 +18,7 @@ #pragma once #include "rule.hpp" +#include "linearsolver.hpp" #include "dependencygraph.hpp" #include "types.hpp" #include "set.hpp" @@ -103,6 +104,23 @@ class ITSProblem { size_t size() const; + // TODO: these attributes should probably not be "so" public. They should only be initialized + // once after parsing and should not be mutated during analysis. But because the ITS instance is constructed + // incrementally, we can't pass these values into the constructor and having public getters+setters + // is no different from making the attributes public directly. + std::vector numProgVars; // TODO: clean up + std::vector boolProgVars; // TODO: clean up + const std::vector getProgVars() const; // TODO: clean up + + void addClause(const Clause &chc); + + const Clause clauseFrom(TransIdx trans_idx) const; + + const Clause clauseFrom(const LocationIdx lhs_loc, const LocationIdx rhs_loc, const Rule& rule) const; + + static std::shared_ptr fromClauses(const std::set& chc_problem); + static std::shared_ptr fromClauses(const std::vector& chc_problem); + protected: DG graph {}; diff --git a/src/lib/expr/boolexpr.hpp b/src/lib/expr/boolexpr.hpp index b7b9bf250..26daefd7d 100644 --- a/src/lib/expr/boolexpr.hpp +++ b/src/lib/expr/boolexpr.hpp @@ -12,6 +12,7 @@ #include #include #include +#include @@ -448,12 +449,10 @@ class BoolExpression: public std::enable_shared_from_this> std::optional elim; const auto vars {c->vars().template get()}; for (const auto &x: vars) { - if (x.isTempVar()) { - if (elim) { - return std::optional{}; - } else { - elim = x; - } + if (elim) { + return std::optional{}; + } else { + elim = x; } } return elim; @@ -520,9 +519,7 @@ class BoolExpression: public std::enable_shared_from_this> if (std::holds_alternative(lit)) { const auto &bool_lit {std::get(lit)}; const auto var {bool_lit.getBoolVar()}; - if (var.isTempVar()) { - res.put(var, bool_lit.isNegated() ? bot() : top()); - } + res.put(var, bool_lit.isNegated() ? bot() : top()); } } } diff --git a/src/lib/expr/expr.cpp b/src/lib/expr/expr.cpp index 3748336cd..2861c5e1a 100644 --- a/src/lib/expr/expr.cpp +++ b/src/lib/expr/expr.cpp @@ -14,6 +14,42 @@ bool isProgVar(const Var &var) { return !isTempVar(var); } +/** + * If the given expression is a simple (non-negated) variable, + * it is returned. For compound expressions, we return nullopt. + */ +const std::optional toVar(const ThExpr &expr) { + return std::visit(Overload{ + [](const Expr &num_expr) -> std::optional { + if (num_expr.isVar()) { + return Var(num_expr.toVar()); + } else { + return {}; + } + }, + [](const BoolExpr &bool_expr) -> std::optional { + if (bool_expr->isTheoryLit()) { + const auto theory_lit = bool_expr->getTheoryLit(); + + return std::visit(Overload{ + [](const BoolLit &lit) -> std::optional { + if (lit.isNegated()) { + return {}; + } else { + return Var(lit.getBoolVar()); + } + }, + [](const Rel &rel) -> std::optional { + return {}; + } + }, *theory_lit); + } else { + return {}; + } + } + }, expr); +} + Var next(const Var &var) { return std::visit(Overload{ [](const NumVar&) { diff --git a/src/lib/expr/expr.hpp b/src/lib/expr/expr.hpp index 43fa3a419..288806685 100644 --- a/src/lib/expr/expr.hpp +++ b/src/lib/expr/expr.hpp @@ -10,6 +10,8 @@ bool isTempVar(const Var &var); bool isProgVar(const Var &var); +const std::optional toVar(const ThExpr &expr); + Var next(const Var &var); ThExpr toExpr(const Var &var); diff --git a/src/lib/rule_simplifications/guardtoolbox.cpp b/src/lib/rule_simplifications/guardtoolbox.cpp index f603bf2c4..bfaca8456 100644 --- a/src/lib/rule_simplifications/guardtoolbox.cpp +++ b/src/lib/rule_simplifications/guardtoolbox.cpp @@ -16,6 +16,7 @@ */ #include "guardtoolbox.hpp" +#include "expr.hpp" #include "rule.hpp" #include "rel.hpp" #include "ruleresult.hpp" @@ -86,19 +87,43 @@ RuleResult GuardToolbox::propagateEqualities(const Rule &rule, SolvingLevel maxl return res; } - RuleResult GuardToolbox::propagateBooleanEqualities(const Rule &rule) { RuleResult res(rule); Proof subproof; Subs equiv; + + // If the value of program variables is implied by the guard, + // we remove them during propagating, which looses information. + // Thus we collect implied program variable equalities and re-add + // them to the guard at the end. + std::vector program_var_equalities; do { equiv = res->getGuard()->impliedEqualities(); + + // collect implied program variable equalities: + for (const auto &var: equiv.domain()) { + if (expr::isProgVar(var)) { + program_var_equalities.push_back( + expr::mkEq(expr::toExpr(var), equiv.get(var))->simplify() + ); + } + } + if (!equiv.empty()) { res = res->subs(equiv); subproof.append(stringstream() << "propagated equivalences: " << equiv << std::endl); } } while (!equiv.empty()); if (res) { + // re-add program variable equalities to guard: + program_var_equalities.push_back(res->getGuard()); + const auto new_guard = BExpression::buildAnd(program_var_equalities); + + if (rule.getGuard() == new_guard) { + return RuleResult(rule); + } + + res = res->withGuard(new_guard); res.ruleTransformationProof(rule, "Propagated Equivalences", *res); res.storeSubProof(subproof); } diff --git a/src/lib/rule_simplifications/rule.cpp b/src/lib/rule_simplifications/rule.cpp index 68110fab7..0201b2f0b 100644 --- a/src/lib/rule_simplifications/rule.cpp +++ b/src/lib/rule_simplifications/rule.cpp @@ -71,6 +71,10 @@ bool Rule::isPoly() const { return guard->isPoly() && update.isPoly(); } +bool Rule::isLinear() const { + return guard->isLinear() && update.isLinear(); +} + std::ostream& operator<<(std::ostream &s, const TransIdx &idx) { return s << idx->getId(); } diff --git a/src/lib/rule_simplifications/rule.hpp b/src/lib/rule_simplifications/rule.hpp index ac5c49518..6e7f03a1f 100644 --- a/src/lib/rule_simplifications/rule.hpp +++ b/src/lib/rule_simplifications/rule.hpp @@ -63,6 +63,8 @@ class Rule { bool isPoly() const; + bool isLinear() const; + unsigned getId() const; bool isDeterministic() const; diff --git a/src/lib/smt/z3.hpp b/src/lib/smt/z3.hpp index 49248b9c6..519a9c614 100644 --- a/src/lib/smt/z3.hpp +++ b/src/lib/smt/z3.hpp @@ -28,6 +28,10 @@ class Z3Base : public Smt { } SmtResult check() override { + // std::cerr << "==============================" << std::endl; + // // // std::cerr << solver << std::endl; + // std::cerr << "==============================" << std::endl; + switch (solver.check()) { case z3::unsat: return Unsat; case z3::unknown: return Unknown; diff --git a/src/main.cpp b/src/main.cpp index cf46a3bf6..ab8042d3c 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -18,6 +18,7 @@ #include "main.hpp" #include "itsparser.hpp" +#include "itsproblem.hpp" #include "parser.hpp" #include "chcparser.hpp" #include "cintparser.hpp" @@ -29,6 +30,7 @@ #include "abmc.hpp" #include "yices.hpp" #include "recurrence.hpp" +#include "nonlinear.hpp" #include "accelerationproblem.hpp" #include @@ -189,6 +191,8 @@ int main(int argc, char *argv[]) { } ITSPtr its; + std::vector clauses; + switch (Config::Input::format) { case Config::Input::Koat: its = parser::ITSParser::loadFromFile(filename); @@ -197,7 +201,7 @@ int main(int argc, char *argv[]) { its = sexpressionparser::Parser::loadFromFile(filename); break; case Config::Input::Horn: - its = hornParser::HornParser::loadFromFile(filename); + clauses = hornParser::HornParser::loadFromFile(filename); break; case Config::Input::C: its = cintParser::CIntParser::loadFromFile(filename); @@ -210,7 +214,12 @@ int main(int argc, char *argv[]) { yices::init(); switch (Config::Analysis::engine) { case Config::Analysis::ADCL: - reachability::Reachability::analyze(*its); + if (allLinear(clauses)) { + its = ITSProblem::fromClauses(clauses); + reachability::Reachability::analyze(*its); + } else { + NonLinearSolver::analyze(clauses); + } break; case Config::Analysis::BMC: BMC::analyze(*its); diff --git a/src/nonlinear/CMakeLists.txt b/src/nonlinear/CMakeLists.txt new file mode 100644 index 000000000..1350584e7 --- /dev/null +++ b/src/nonlinear/CMakeLists.txt @@ -0,0 +1,10 @@ +target_sources(${EXECUTABLE} + PRIVATE + nonlinear.hpp + nonlinear.cpp + clause.hpp + clause.cpp + linearsolver.hpp +) + +target_include_directories(${EXECUTABLE} PRIVATE ".") diff --git a/src/nonlinear/clause.cpp b/src/nonlinear/clause.cpp new file mode 100644 index 000000000..c83d916fe --- /dev/null +++ b/src/nonlinear/clause.cpp @@ -0,0 +1,637 @@ +#include "clause.hpp" +#include "boolexpr.hpp" +#include "expr.hpp" +#include "smtfactory.hpp" +#include "theory.hpp" +#include +#include +#include +#include + +/** + * TODO docs + */ +const Var varAt(const Var &var, const Subs &subs) { + if (!subs.contains(var)) { + return var; + } else { + const auto optional_var = expr::toVar(subs.get(var)); + + if (optional_var.has_value()) { + return optional_var.value(); + } else { + throw std::logic_error("Renaming contains non-variable expression"); + } + } +} + +/** + * Tries to compute a unifier for the two given predicates. Because predicate + * arguments are always simple variables (instead of expressions), the unifier + * is simply a variable renaming. If the predicates don't have the same + * predicate symbol or different arity or the argument types don't match, + * unification is not possible. For example: + * + * F(x,x) and G(y,z) are not unifiable + * F(x) and F(y,z) are not unifiable + * F(w,x) and F(y,z) returns { w -> y, x -> z } + * F(x,x) and F(y,z) returns { x -> y, z -> y } + * + * In practice we normalize all predicates to have the same arity with same argument + * types in the same order. So only differing predicate symbols should be a reason + * for two predicates to not be unifiable. But this is a non-local assumption (that might + * change) so for "local correctness" we also check arity and argument types. + */ +const std::optional computeUnifier(const FunApp &pred1, const FunApp &pred2) { + if (pred1.name == pred2.name) { + return computeUnifier(pred1.args, pred2.args); + } else { + return {}; + } +} +const std::optional computeUnifier(const std::vector &args1, const std::vector &args2) { + if (args1.size() == args2.size()) { + Subs subs; + + for (size_t i = 0; i < args1.size(); ++i) { + const Var var1 = args1[i]; + const Var var2 = args2[i]; + + if (subs.contains(var1)) { + // If `var1` is already contained in `subs`, then `pred1` must + // have `var1` multiple times as an argument. This is an implict + // equality. We assume at this point that this doesn't occur and + // that all equalities are explicitly mentioned in the constraint. + throw std::logic_error("computeUnifier: predicate has duplicate arguments"); + } else { + // QUESTION: I suspect some C++ template magic can make this prettier + bool both_nums = std::holds_alternative(var1) && + std::holds_alternative(var2); + bool both_bools = std::holds_alternative(var1) && + std::holds_alternative(var2); + + if (both_nums) { + subs.put(std::make_pair( + std::get(var1), + std::get(expr::toExpr(var2)) + )); + } else if (both_bools) { + subs.put(std::make_pair( + std::get(var1), + std::get(expr::toExpr(var2)) + )); + } else { + // argument types don't match ==> not unifiable + return {}; + } + } + } + + return subs; + } else { + return {}; + } +} + + +/** + * Apply `renaming` to all arguments of the predicate. + * Will throw an error if the renaming maps to compound expressions + * instead of variables. + */ +const FunApp FunApp::renameWith(const Subs &renaming) const { + std::vector args_renamed; + + for (const Var &var : args) { + const auto target_var = varAt(var, renaming); + args_renamed.push_back(target_var); + } + + return FunApp(name, args_renamed); +} + +/** + * Create a copy of predicate with argument vector replaced. + */ +const FunApp FunApp::withArgs(const std::vector new_args) const { + return FunApp(name, new_args); +} + +/** + * Collect set of variables used in predicate arguments. + */ +const VarSet FunApp::vars() const { + VarSet vs; + for (const auto &arg: args) { + vs.insert(arg); + } + return vs; +} + +/** + * Count number arguments with type integer valued arguments. + */ +unsigned long FunApp::intArity() const { + unsigned arity {0}; + for (const auto &arg: args) { + if (std::holds_alternative(arg)) { + arity++; + } + } + return arity; +} + +/** + * Count number arguments with type integer valued arguments. + */ +unsigned long FunApp::boolArity() const { + unsigned arity {0}; + for (const auto &arg: args) { + if (std::holds_alternative(arg)) { + arity++; + } + } + return arity; +} + +/** + * Apply `renaming` to all variables in the clause, i.e variables in the guard and the + * arguments of all predicates on both LHS and RHS. Will throw an error if the renaming + * maps to compound expressions + */ +const Clause Clause::renameWith(const Subs &renaming) const { + std::vector lhs_renamed; + for (const FunApp &pred : lhs) { + lhs_renamed.push_back(pred.renameWith(renaming)); + } + + // TODO: bottleneck applying large subsitution with 20_000 vars + if (renaming.size() > 15000) { + std::cout << "subs size: " << renaming.size() << std::endl; + std::cout << guard << std::endl; + } + const auto guard_renamed = guard->subs(renaming); + + if (rhs.has_value()) { + return Clause( + lhs_renamed, + rhs.value().renameWith(renaming), + guard_renamed + ); + } else { + return Clause(lhs_renamed, {}, guard_renamed); + } +} + +/** + * Collect set of variables used in predicate arguments and guard. + */ +const VarSet Clause::vars() const { + VarSet vs; + for (const auto &pred: lhs) { + vs.insertAll(pred.vars()); + } + if (rhs.has_value()) { + vs.insertAll(rhs.value().vars()); + } + guard->collectVars(vs); + return vs; +} + +const std::vector deletePredAt(const std::vector& preds, unsigned index) { + std::vector new_preds; + for (unsigned i=0; i G(x) + * chc : G(y) /\ G(z) /\ y < z ==> H(y,z) + * pred_index : ^--- points on first predicate (i.e. pred_index = 0) + * + * the returned resolvent should be + * + * G(y) /\ F(z) /\ y < z ==> H(y,z) + * + */ +const std::optional> Clause::resolutionWith(const Clause &chc, unsigned pred_index) const { + if (pred_index >= chc.lhs.size()) { + throw std::logic_error("Clause::resolutionWith: `pred_index` out-of-bounds"); + } + const auto& resolved_pred = chc.lhs.at(pred_index); + + // No resolvent if `this` is a query, ie has no RHS predicate. + if (this->isQuery()) { + return {}; + } + + // Make sure variables in `this` and `chc` are disjoint. + Subs renaming; + const VarSet this_vars {this->vars()}; + for (const auto &var: chc.vars()) { + if (this_vars.contains(var)) { + renaming.put(var, expr::toExpr(expr::next(var))); + } + } + const Clause this_with_disjoint_vars = this->renameWith(renaming); + + const auto unifier = computeUnifier(this_with_disjoint_vars.rhs.value(), resolved_pred); + + // If the predicates are not unifiable, we don't throw an error but return + // nullopt. That way the caller can filter out unifiable predicates using this + // function. We could throw an error here too, but that implies that we expect + // the caller to check unifiablility first and implementing that check would + // be redundant. On the other hand, choosing a literal from the LHS of `chc` + // is trivial, so we require the caller to do that correctly. + if (!unifier.has_value()) { + return {}; + } + + const Clause this_unified = this_with_disjoint_vars.renameWith(unifier.value()); + + // LHS of resolvent is the union of the renamed LHS of `this` ... + std::vector resolvent_lhs = this_unified.lhs; + // ... and the LHS of `chc` where `pred` is removed. + for (unsigned i=0; i, std::set> partitionByDegree(const std::set& chcs) { + std::set linear_chcs; + std::set non_linear_chcs; + + for (const Clause& chc: chcs) { + if (chc.isLinear()) { + linear_chcs.insert(chc); + } else { + non_linear_chcs.insert(chc); + } + } + + return std::make_tuple(linear_chcs, non_linear_chcs); +} + +/** + * Partition given `chcs` by their RHS predicate. Returns a map where the keys are RHS predicate names and + * values are the sets of clauses with that RHS predicate. The key is optional because clauses may have no + * RHS predicate (i.e. querys). + */ +const std::map, std::vector> partitionByRHS(const std::set& chcs) { + std::map, std::vector> partition; + + for (const auto& chc: chcs) { + std::optional> rhs_name; + if (chc.rhs.has_value()) { + rhs_name = chc.rhs.value().name; + } + + if (partition.contains(rhs_name)) { + std::vector& group = partition.at(chc.rhs->name); + group.push_back(chc); + } else { + partition.emplace(rhs_name, std::vector({ chc })); + } + } + + return partition; +} + +/** + * Filters facts from `chcs` and returns a tuple, where the first component contains all facts and + * the second component contains the remaining clauses. + */ +const std::tuple, std::set> partitionFacts(const std::set& chcs) { + std::set facts; + std::set non_facts; + + for (const auto& chc: chcs) { + if (chc.isFact()) { + facts.insert(chc); + } else { + non_facts.insert(chc); + } + } + + return std::make_tuple(facts, non_facts); +} + +/** + * Normalize variable names to detect syntactic equivalence of clauses up-to-renaming. + * + * For that the RHS predicate arguments are renamed to always have the indices 0,1,2,3,... + * For example + * + * i44 > i9 /\ b23 ==> F(i44,b23,i9) + * + * is renamed to + * + * i0 > i2 /\ b1 ==> F(i0,b1,i2) + * + * One exception is when a variable occurs multiple times in the arguments of the + * original RHS predicate. For example: + * + * i44 > i9 /\ b23 ==> F(i44,b23,i9,i44) + * + * is renamed to + * + * i0 > i2 /\ b1 ==> F(i0,b1,i2,i0) + * + * to preserve the implict equality. But this is not a problem to detect syntatic + * equivalence. + */ +const Clause Clause::normalize() const { + const auto& chc_uniq_args = removeDuplicatePredicateArguments(*this); + + if (!chc_uniq_args.rhs.has_value()) { + return chc_uniq_args; + } + const auto rhs = chc_uniq_args.rhs.value(); + + // construct a vector of variables with the same length as `rhs.args` + // and the same variable types in each position, except that the variable + // indices are simply: 0,1,2,3,etc. + std::vector target_args; + for (unsigned i=0; i < size(rhs.args); i++) { + const auto var = std::visit(Overload{ + [i](const NumVar&) { + return Var(NumVar(i)); + }, + [i](const BoolVar&) { + return Var(BoolVar(i)); + } + }, rhs.args[i]); + + target_args.push_back(var); + } + + const auto unifier = computeUnifier(rhs.args, target_args); + + if (unifier.has_value()) { + return chc_uniq_args.renameWith(unifier.value()); + } else { + // Variable vectors should always be unifiable unless the vectors have differnt length, + // but the vectors should have the same length by construction so this error should not + // occur. + throw std::logic_error("failed to unify variable vectors"); + } +} + +/** + * Returns true iff the clause has at most one LHS predicate. For example: + * + * F(x) /\ x > 1 ==> F(x) (linear) + * + * F(x) /\ x > 1 ==> false (linear) + * + * x > 1 ==> F(x) (linear) + * + * F(x) /\ G(x) ==> false (non-linear) + * + */ +bool Clause::isLinear() const { + return lhs.size() <= 1; +} + +/** + * Returns true iff the clause has a RHS predicte but no LHS predicates. For example: + * + * x > 0 ==> F(x) (fact) + * + * F(x) /\ x > 0 ==> F(x) (not fact) + * + * x > 0 ==> false (not fact) + * + */ +bool Clause::isFact() const { + return lhs.size() == 0 && rhs.has_value(); +} + +/** + * Returns true iff the clause has no RHS predicate. For example: + * + * F(x) /\ x > 1 ==> false (query) + * + * x > 1 ==> F(x) (not query) + * + */ +bool Clause::isQuery() const { + return !rhs.has_value(); +} + +/** + * Return first predicate with given `name` if it occurs on the LHS of the clause. + * Returns nullopt if there is no predicate with given `name`. + */ +std::optional Clause::indexOfLHSPred(const std::string name) const { + for (unsigned i=0; i maxArity(const std::vector& chc_problem) { + unsigned long max_int_arity {0}; + unsigned long max_bool_arity {0}; + + for (const auto &chc: chc_problem) { + if (chc.rhs.has_value()) { + const auto& rhs = chc.rhs.value(); + max_int_arity = std::max(max_int_arity, rhs.intArity()); + max_bool_arity = std::max(max_bool_arity, rhs.boolArity()); + } + + for (const auto &pred: chc.lhs) { + max_int_arity = std::max(max_int_arity, pred.intArity()); + max_bool_arity = std::max(max_bool_arity, pred.boolArity()); + } + } + + return std::pair(max_int_arity, max_bool_arity); +} + +/** + * If a predicate has duplicate arguments as in + * + * F(x,y,x) + * + * then this constitutes an implict equality. This function makes the equality + * explicit by moving it into the guard. + */ +const Clause removeDuplicatePredicateArguments(const Clause& chc) { + std::vector extra_conditions = { chc.guard }; + + std::vector new_lhs; + new_lhs.reserve(chc.lhs.size()); + for (const auto& pred: chc.lhs) { + std::vector new_args; + + for (const auto& arg: pred.args) { + if (std::find(new_args.begin(), new_args.end(), arg) != new_args.end()) { + auto fresh_var = expr::next(arg); + extra_conditions.push_back(expr::mkEq(expr::toExpr(arg), expr::toExpr(fresh_var))); + new_args.push_back(fresh_var); + } else { + new_args.push_back(arg); + } + } + + new_lhs.push_back(pred.withArgs(new_args)); + } + + std::unique_ptr new_rhs; + if (chc.rhs.has_value()) { + std::vector new_args; + + for (const auto& arg: chc.rhs.value().args) { + if (std::find(new_args.begin(), new_args.end(), arg) != new_args.end()) { + auto fresh_var = expr::next(arg); + extra_conditions.push_back(expr::mkEq(expr::toExpr(arg), expr::toExpr(fresh_var))); + new_args.push_back(fresh_var); + } else { + new_args.push_back(arg); + } + } + + new_rhs = std::make_unique( + chc.rhs.value().withArgs(new_args) + ); + } + + const auto new_guard = BExpression::buildAnd(extra_conditions)->simplify(); + return Clause(new_lhs, chc.rhs.has_value() ? *new_rhs : chc.rhs, new_guard); +} + +// QUESTION: does C++ have no iterable type of somehting so we can abstract over the collection type? +bool allLinear(const std::vector& chcs) { + for (const auto& chc: chcs) { + if (!chc.isLinear()) { + return false; + } + } + + return true; +} +bool allLinear(const std::set& chcs) { + chcs.begin(); + + for (const auto& chc: chcs) { + if (!chc.isLinear()) { + return false; + } + } + + return true; +} + +bool operator<(const FunApp &fun1, const FunApp &fun2) { + if (fun1.name < fun2.name) { + return true; + } else if (fun2.name < fun1.name) { + return false; + } else { + return fun1.args < fun2.args; + } +} + +bool operator<(const Clause &c1, const Clause &c2) { + if (c1.lhs < c2.lhs) { + return true; + } else if (c2.lhs < c1.lhs) { + return false; + } else if (c1.rhs < c2.rhs) { + return true; + } else if (c2.rhs < c1.rhs) { + return false; + } else if (c1.guard < c2.guard) { + return true; + } else if (c2.guard < c1.guard) { + return false; + } else { + return false; + } +} + +std::ostream &operator<<(std::ostream &s, const FunApp &fun) { + s << fun.name; + + if (fun.args.size() > 0) { + auto iter = fun.args.begin(); + + s << "(" << *iter; + iter++; + + while (iter < fun.args.end()) { + s << "," << *iter; + iter++; + } + + s << ")"; + } + + return s; +} + +std::ostream &operator<<(std::ostream &s, const Clause &chc) { + for (const FunApp &fun_app : chc.lhs) { + s << fun_app << " /\\ "; + } + + s << chc.guard << " ==> "; + + if (chc.rhs.has_value()) { + s << chc.rhs.value(); + } else { + s << "false"; + } + + return s; +} + +std::ostream& printSimple(std::ostream &s, const Clause &chc) { + for (const FunApp& pred: chc.lhs) { + s << pred.name << " /\\ "; + } + + s << "(...) ==> "; + + if (chc.rhs.has_value()) { + s << chc.rhs.value().name; + } else { + s << "false"; + } + + return s; +} diff --git a/src/nonlinear/clause.hpp b/src/nonlinear/clause.hpp new file mode 100644 index 000000000..3617508f2 --- /dev/null +++ b/src/nonlinear/clause.hpp @@ -0,0 +1,94 @@ +#include "theory.hpp" +#include + +class FunApp { + +public: + const std::string name; + const std::vector args; + + FunApp( + const std::string name, + const std::vector args + ): name(name), args(args) {} + + const FunApp renameWith(const Subs &renaming) const; + + const FunApp withArgs(const std::vector new_args) const; + + const VarSet vars() const; + + unsigned long intArity() const; + + unsigned long boolArity() const; +}; + +class Clause { + +public: + const std::vector lhs; + const std::optional rhs; + const BoolExpr guard; + + /** + * Constructor for a Constrained Horn Clause (CHC). For example: + * + * F(x1) /\ G(x2,x3) /\ (x1 < x2 /\ x2 < x3) ==> H(x1,x2,x3) + * + * ^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^ + * lhs guard rhs + * + * @param lhs - a set of predicates on the left-hand-side (LHS) of the implication. + * @param rhs - an optional predicate on the right-hand-side (RHS) of the implication. + * @param guard - a boolean expression describing the clause constraint. + */ + Clause( + const std::vector lhs, + const std::optional rhs, + const BoolExpr guard + ) : lhs(lhs), rhs(rhs), guard(guard) {} + + const Clause renameWith(const Subs &renaming) const; + + const std::optional> resolutionWith(const Clause &chc, unsigned pred_index) const; + + const Clause normalize() const; + + bool isLinear() const; + + bool isFact() const; + + bool isQuery() const; + + const VarSet vars() const; + + std::optional indexOfLHSPred(const std::basic_string name) const; +}; + +const Clause removeDuplicatePredicateArguments(const Clause& chc); + +const std::tuple, std::set> partitionByDegree(const std::set& chcs); + +const std::map, std::set> partitionFactsByRHS(const std::set& facts); + +const std::tuple, std::set> partitionFacts(const std::set& chcs); + +const std::map>, std::vector> partitionByRHS(const std::set& chcs); + +const std::optional computeUnifier(const FunApp &pred1, const FunApp &pred2); +const std::optional computeUnifier(const std::vector &args1, const std::vector &args2); + +const std::pair maxArity(const std::vector& chc_problem); + +bool allLinear(const std::vector& chcs); +bool allLinear(const std::set& chcs); + +// implement comparison operators so they can be stored in std::set +bool operator<(const Clause &c1, const Clause &c2); +bool operator<(const FunApp &fun1, const FunApp &fun2); + +std::ostream& operator<<(std::ostream &s, const FunApp &fun_app); + +std::ostream& operator<<(std::ostream &s, const Clause &chc); + +std::ostream& printSimple(std::ostream &s, const Clause &chc); diff --git a/src/nonlinear/linearsolver.hpp b/src/nonlinear/linearsolver.hpp new file mode 100644 index 000000000..6f05d888a --- /dev/null +++ b/src/nonlinear/linearsolver.hpp @@ -0,0 +1,72 @@ +#pragma once +#include "clause.hpp" + +namespace LinearSolver { + enum Result { Unsat, Sat, Unknown, Pending }; + enum ConstraintTier { Linear, Polynomial, Exponential }; + + /** + * Fixed list of all constraint tiers in order of solving difficulty. + */ + const std::vector constraint_tiers = { + LinearSolver::ConstraintTier::Linear, + LinearSolver::ConstraintTier::Polynomial, + LinearSolver::ConstraintTier::Exponential + }; +} + + +/** + * Any linear CHC solver that implements this interface (e.g. ADCL) is compatible with the + * non-linear CHC solver. The linear solver must also act as a data structure + * for the CHC problem. That is, it must store all available linear and non-linear + * clauses. That way the non-linear solver is not only independent of the linear solver + * but also the problem representation (e.g. ITS). + */ +class ILinearSolver { + +public: + + // virtual destructor + virtual ~ILinearSolver() {}; + + /** + * Let linear solver derive all (ideally non-redundant) facts it can derive with + * the current linear clause set. + * + * The argument `max_constr_tier` can be set to `Linear`, `Polynomial` or `Exponential`. + * Here "linear" does NOT refer the the plurality of left-hand-side predicates but the + * clause constraint. For example: + * + * - linear constraint : F(x) /\ 2*x=4 ==> F(x) + * - polynomial constraint : F(x) /\ x^2=4 ==> F(x) + * - exponential constraint : F(x) /\ 2^x=4 ==> F(x) + * + * If the argument is set to `Linear` the solver should only derive facts with linear + * constraint. If the argument is set to `Polynomial`, only polynomial facts should be + * derived. This includes linear facts, since linear constraints are also polynomial. + * Polynomial constraints are also exponential, so the argument `Exponential` instructs + * the solver to derive arbitrary constraints. + * + * The distinction is for optimization. Because the constraint tiers are successively + * harder to deal with for SMT solvers, we can first try to solve a CHC instance by only + * considering "easy" linear constraints and only consider harder polynomial and exponential + * constraints if necessary. + */ + virtual const std::set derive_new_facts( + LinearSolver::ConstraintTier max_constr_tier + ) = 0; + + /** + * Return current status of the solver. Status Unknown or Sat should be reset to + * Pending, when new clauses are added via `add_clauses`. The status Unsat should + * be considered final. + */ + virtual LinearSolver::Result get_analysis_result() const = 0; + + /** + * Adds new clauses to the solver in batch. The added clauses must be linear. + */ + virtual void add_clauses(const std::set &clauses) = 0; + +}; diff --git a/src/nonlinear/nonlinear.cpp b/src/nonlinear/nonlinear.cpp new file mode 100644 index 000000000..54c79d1e1 --- /dev/null +++ b/src/nonlinear/nonlinear.cpp @@ -0,0 +1,707 @@ +#include "nonlinear.hpp" +#include "boolexpr.hpp" +#include "itsproblem.hpp" +#include "reachability.hpp" +#include "linearsolver.hpp" +#include "smt.hpp" +#include "smtfactory.hpp" +#include "theory.hpp" +#include +#include + +// for debugging: activate logging only in this file +const bool dbg = false; + +bool has_entry(const std::set& chcs) { + for (const auto& chc: chcs) { + // Not necessarily a fact, because RHS predicate is not required. + // For example `true ==> false` is an entry but not a fact. + if (chc.lhs.empty()) { + return true; + } + } + return false; +} + +bool has_sink(const std::set& chcs) { + for (const auto& chc: chcs) { + if (!chc.rhs.has_value()) { + return true; + } + } + return false; +} + +bool is_trivially_sat(const std::set& chc_problem) { + // TODO: could check more generally: if no sink is reachable from an entry: + return chc_problem.empty() || !has_entry(chc_problem) || !has_sink(chc_problem); +} + +void NonLinearSolver::analyze(const std::vector& initial_chcs) { + const std::set chcs_preprocessed = presolve(normalize_all_preds(initial_chcs)); + + if (is_trivially_sat(chcs_preprocessed)) { + // If preprocessing manages to eliminate all clauses or at least all facts/queries + // we can terminate with SAT. + std::cout << "sat" << std::endl; + return; + } else if (allLinear(chcs_preprocessed)) { + ITSPtr its = ITSProblem::fromClauses(chcs_preprocessed); + reachability::Reachability::analyze(*its); + return; + } + + auto [linear_chcs, non_linear_chcs] = partitionByDegree(chcs_preprocessed); + + // Setup ITS and linear solver: + ITSPtr its = ITSProblem::fromClauses(chcs_preprocessed); + // TODO: why cant we give `linear_solver` the type `ILinearSolver` ? + auto linear_solver = reachability::Reachability(*its, true); + + // First only derive "easy" to handle rules with linear guard. If that's not enough + // also try rules with polynomial guard. Otherwise also consider exponential + // (arbitrary) guards. + for (const auto max_constraint_tier: LinearSolver::constraint_tiers) { + while (true) { + if (dbg || Config::Analysis::log) { + std::cout << "============= non-linear solver main loop =============" << std::endl; + } + + // Hand over to linear solver to derive new facts: + const auto& derived_facts = linear_solver.derive_new_facts(max_constraint_tier); + + // If the linear solver proved Unsat, we can terminate. Otherwise, we use the derived facts to in the next + // resolution round to derive more linear clauses, that we can feed back into the linear solver. Unless + // the set of derived facts is empty, then we have explored the entire search space and can also terminate: + const auto result = linear_solver.get_analysis_result(); + if (result == LinearSolver::Result::Unsat) { + break; + } else if ((result == LinearSolver::Result::Sat || result == LinearSolver::Result::Unknown) && derived_facts.empty()) { + break; + } + + // reduce number of facts by merging facts with the same RHS predicate: + std::set facts; + for (const auto& [_, fact_group]: partitionByRHS(derived_facts)) { + const auto& merged_fact = merge_facts(fact_group); + facts.insert(merged_fact); + } + if (dbg || Config::Analysis::log) { + std::cout + << "total new facts: " + << derived_facts.size() + << " / after merge: " + << facts.size() + << std::endl; + } + + // Do resolution with all combinations of facts and non-linear clauses to + // get every possible linear clause that we can derive in this iteration. + const auto resolvents = all_resolvents(non_linear_chcs, facts); + + // Add linear resolvents to linear solver and store non-linear resolvents for the next resolutions round: + const auto [linear_resolvents, non_linear_resolvents] = partitionByDegree(resolvents); + + // If there are no new linear resolvents the linear solver can't derive new facts + // in the next iteration, so we can exit here. This can happen if all linear resolvents + // had UNSAT constraints or the CHC problem contains only linear clauses (because all + // non-linear clauses got eliminated in the preprocessing step). + if (linear_resolvents.empty()) { + break; + } + + linear_solver.add_clauses(linear_resolvents); + non_linear_chcs.insert(non_linear_resolvents.begin(), non_linear_resolvents.end()); + } + + if (linear_solver.get_analysis_result() == LinearSolver::Result::Unsat) { + break; + } + } + + switch (linear_solver.get_analysis_result()) { + case LinearSolver::Result::Sat: + std::cout << "sat" << std::endl; + break; + case LinearSolver::Result::Unsat: + std::cout << "unsat" << std::endl; + break; + case LinearSolver::Result::Unknown: + std::cout << "unknown" << std::endl; + break; + case LinearSolver::Result::Pending: + throw std::logic_error("exited main loop, although linear solver is still pending"); + } +} + +/** + * Compute all resolvents of `non_linear_chcs` with `facts`, while trying to avoid redundant derivations. + * For example, let `F(1)` be the only fact and `chc` be `F(x) /\ F(y) /\ F(z) ==> G(x,y,z)` + * then a redundant derivation would be: + * + * F(x) /\ F(y) /\ F(z) ==> G(x,y,z) + * + * / \ + * + * F(x) /\ F(y) ==> G(x,y,1) F(x) /\ F(z) ==> G(x,1,z) + * + * | | + * + * F(x) ==> G(x,1,1) F(x) ==> G(x,1,1) + * + * The returned clause set should not contain any redundant clauses as long as the given + * `facts` and `non_linear_chcs` are not redundant. The returned clauses should also not + * include `non_linear_chcs` themselves and no facts (i.e. clauses with no LHS predicates). + */ +const std::set all_resolvents(const std::set& non_linear_chcs, const std::set& facts) { + std::set resolvents; + + unsigned redundant_resolvent_count = 0; + + if (dbg || Config::Analysis::log) { + std::cout + << "resolving " + << non_linear_chcs.size() + << " non-linear CHCs" + << std::endl; + } + + std::unique_ptr> solver {SmtFactory::solver()}; + + for (const auto& chc: non_linear_chcs) { + if (dbg || Config::Analysis::log) { + std::cout + << "resolving non-linear CHC with " + << chc.lhs.size() + << " LHS predicates with " + << facts.size() + << " facts" + << std::endl; + + printSimple(std::cout << "NL: ", chc) << std::endl; + } + + solver->push(); + solver->add(chc.guard); + all_resolvents_aux(chc, 0, facts, resolvents, redundant_resolvent_count, *solver); + solver->pop(); + } + + if (dbg || Config::Analysis::log) { + std::cout + << "computed " + << resolvents.size() + << " resolvents (" + << redundant_resolvent_count + << " redundant)" + << std::endl; + } + + // TODO: check comp23 069 + // for (const auto& res: resolvents) { + // const std::set lhs_unique(res.lhs.begin(), res.lhs.end()); + // int red_count = res.lhs.size() - lhs_unique.size(); + // if (red_count != 0) { + // std::cout << "redundant lhs preds: " << red_count << std::endl; + // } + // } + + return resolvents; +} +void all_resolvents_aux( + const Clause& chc, + unsigned pred_index, + const std::set& facts, + std::set& resolvents, + unsigned& redundant_resolvent_count, + Smt& solver +) { + // === Running example === + // `chc` : F(x) /\ F(y) /\ F(z) ==> G(x,y,z) + // `pred_index` : ^---- index on first LHS predicate of `chc` + // `facts` : [F(1), F(2)] + + if (pred_index >= chc.lhs.size() || chc.isLinear()) { + return; + } else { + // All resolvents that DO eliminate F(x) + for (const auto& fact: facts) { + // printSimple(std::cout << "fact: ", fact) << std::endl; + const auto optional_resolvent = fact.resolutionWith(chc, pred_index); + + if (optional_resolvent.has_value()) { + // const auto resolvent = optional_resolvent.value(); + const auto [resolvent, extra_constraints] = optional_resolvent.value(); + // for fact = F(1) : F(y) /\ F(z) ==> G(1,y,z) + // + // for fact = F(2) : F(y) /\ F(z) ==> G(2,y,z) + + if (resolvents.contains(resolvent)) { + // There are still many ways how we can get syntactically redundant resolvents. + // For example, with facts G,H and rules + // + // G /\ F ==> false + // H /\ F ==> false + // + // we derive `F ==> false` in two different ways. However, when we encouter a + // redundant resolvent we can prune the recursive call, because all following + // resolvents are also redundant. + redundant_resolvent_count++; + } else { + solver.push(); + solver.add(extra_constraints); + + // if (SmtFactory::check(resolvent.guard) == Sat) { + if (solver.check() == Sat) { + resolvents.insert(resolvent); + + all_resolvents_aux(resolvent, pred_index, facts, resolvents, redundant_resolvent_count, solver); + // for fact = F(1) : F(y) ==> G(1,y,1) + // F(y) ==> G(1,y,2) + // F(z) ==> G(1,1,z) + // F(z) ==> G(1,2,z) + // + // for fact = F(2) : F(y) ==> G(2,y,1) + // F(y) ==> G(2,y,2) + // F(z) ==> G(2,1,z) + // F(z) ==> G(2,2,z) + } + + solver.pop(); + } + } + } + + // All resolvents that DONT eliminate F(x) + all_resolvents_aux(chc, pred_index+1, facts, resolvents, redundant_resolvent_count, solver); + // F(x) /\ F(y) ==> G(x,y,1) + // F(x) /\ F(y) ==> G(x,y,2) + // + // F(x) /\ F(z) ==> G(x,1,z) + // F(x) ==> G(x,1,1) + // F(x) ==> G(x,1,2) + // + // F(x) /\ F(z) ==> G(x,2,z) + // F(x) ==> G(x,2,1) + // F(x) ==> G(x,2,2) + } +} + +const FunApp normalize_pred(unsigned int_var_count, unsigned bool_var_count, const FunApp &pred) { + std::vector int_args; + int_args.reserve(int_var_count); + std::vector bool_args; + bool_args.reserve(bool_var_count); + + for (const Var &arg: pred.args) { + if (std::holds_alternative(arg)) { + int_args.push_back(arg); + } else { + bool_args.push_back(arg); + } + } + + while (int_args.size() < int_var_count) { + int_args.push_back(NumVar::next()); + } + + while (bool_args.size() < bool_var_count) { + bool_args.push_back(BoolVar::next()); + } + + int_args.insert(int_args.end(), bool_args.begin(), bool_args.end()); + return FunApp(pred.name, int_args); +} + +/** + * Add and reorder int/bool arguments of each predicate in each clause in `chc_problem` until all + * of them have the same number of int/bool variables, that is: + * + * F(int_1, int_2, ..., int_n, bool_1, bool_2, ..., bool_m) + * + * This is necessary because the facts dervied by the linear solver (at least Reachability) have this shape. + * And to correctly resolve the facts with non-linear clauses, it's easier if all clauses have this shape to + * begin with. + */ +const std::vector normalize_all_preds(const std::vector& initial_chcs) { + std::vector chcs_normalized; + + auto [ max_int_arity, max_bool_arity ] = maxArity(initial_chcs); + + for (const auto& chc: initial_chcs) { + std::vector lhs_normalized; + + for (const FunApp &pred: chc.lhs) { + const auto pred_normalized = normalize_pred( + max_int_arity, + max_bool_arity, + pred + ); + lhs_normalized.push_back(pred_normalized); + } + + if (chc.rhs.has_value()) { + chcs_normalized.push_back(Clause( + lhs_normalized, + normalize_pred(max_int_arity, max_bool_arity, chc.rhs.value()), + chc.guard->simplify() + )); + } else { + chcs_normalized.push_back(Clause( + lhs_normalized, + {}, + chc.guard->simplify() + )); + } + } + + return chcs_normalized; +} + +/** + * Returns a clause in `chcs`, whose RHS predicate has the name `pred_name`, but only if + * this clause is the ONLY instance with this RHS predicate. For example, in the set of CHCs: + * + * (c1) F ==> G + * (c2) F ==> H + * (c3) G ==> H + * + * the predicate `G` occurs on the RHS of exactly one clause (namely c1), while the + * predicate `F` never occurs on the RHS and `H` occurs twice. Thus: + * + * unilaterally_resolvable_with(F, {c1,c2,c3}) == null + * unilaterally_resolvable_with(G, {c1,c2,c3}) == c1 + * unilaterally_resolvable_with(H, {c1,c2,c3}) == null + * + */ +const std::optional unilaterally_resolvable_with(const std::string& pred_name, const std::set& chcs) { + auto candidate = chcs.end(); // Initialize to end iterator, indicating no candidate found + + for (auto it = chcs.begin(); it != chcs.end(); ++it) { + if (it->rhs.has_value() && it->rhs.value().name == pred_name) { + if (candidate != chcs.end()) { + // Predicate occurs on RHS of multiple clauses. + return {}; + } else { + candidate = it; + } + } + } + + if (candidate != chcs.end()) { + return *candidate; + } else { + return {}; + } +} + +/** + * Compute resolvent of `left` and `right`. If the RHS predicate of `left` occurs + * multiple times on the LHS of `right`, then keep resolving until all predicates + * are eliminated. For example for + * + * (left) F ==> G + * (right) G /\ G ==> H + * + * we would resolve `left` with `right` twice, until `G` is completely eliminated. + */ +const Clause eliminate_pred(const Clause& left, const Clause& right) { + if (left.isQuery()) { + return right; + } + + const auto& left_pred = left.rhs.value(); + const auto& right_pred_index = right.indexOfLHSPred(left_pred.name); + + if (right_pred_index.has_value()) { + const auto [resolvent, _] = left.resolutionWith(right, right_pred_index.value()).value(); + return eliminate_pred(left, resolvent); + } else { + return right; + } +} + +/** + * Merges a collection of `facts` by building the disjunct of all constraints. + * For example, merging the facts: + * + * x=0 ==> F(x) + * + * y=1 ==> F(y) + * + * z>5 ==> F(z) + * + * results in: + * + * (x=0 \/ x=1 \/ x>5) ==> F(x) + * + * Notice, that the RHS predicates have to be unified for that. It's assumed that `facts`: + * + * 1) contains at least one item + * 2) contains only clauses that are indeed facts + * 3) all facts share the same RHS predicate + * + * Otherwise, this function throws an error. + */ +const Clause merge_facts(const std::vector facts) { + if (facts.size() == 0) { + throw std::logic_error("merge_facts: expect at least one fact"); + } + + std::unique_ptr fact_accum = std::make_unique(facts.at(0)); + + if (!fact_accum->isFact()) { + throw std::logic_error("merge_facts: got non-fact clause"); + } + + for (unsigned i=1; i < facts.size(); i++) { + const auto& fact_current = facts.at(i); + + if (!fact_current.isFact()) { + throw std::logic_error("merge_facts: got non-fact clause"); + } + + const auto& rhs_pred_accum = fact_accum->rhs.value(); + const auto& rhs_pred_current = fact_current.rhs.value(); + + if (rhs_pred_accum.name != rhs_pred_current.name) { + throw std::logic_error("merge_facts: all facts must have matching RHS"); + } + + const auto& unifier = computeUnifier(rhs_pred_current, rhs_pred_accum); + + if (!unifier.has_value()) { + throw std::logic_error("merge_facts: cannot unify RHS predicates"); + } + + const std::vector guards({ + fact_current.renameWith(unifier.value()).guard, + fact_accum->guard + }); + const auto& guard_disjunct = BExpression::buildOr(guards); + + fact_accum = std::make_unique( + Clause({}, rhs_pred_accum, guard_disjunct) + ); + } + + return *fact_accum; +} + +/** + * If a predicate only occurs on the RHS of a single CHC, then there is only one + * choice how to eliminate the predicate on the LHS of other CHCs. Thus, we can + * precompute all resolvents where one of parent clauses has a unique RHS. + * + * This reduces the number of clauses the CHC problem and has propagation effects. + * This can turn a non-linear CHC problem into a linear one, or even make it trivially + * UNSAT/SAT. For example, consider the non-linear CHC problem: + * + * (c1) X>0 ==> F(X) + * (c2) X<0 ==> G(X) + * (c3) F(X) /\ G(X) ==> H + * (c4) F(X) ==> H + * (c5) H ==> false + * + * The predicate `F(X)` occurs uniquely on the RHS of `c1` so we can precompute the + * resolvents of `c1` with any all clauses that have `F(X)` on the LHS (namely c3`, `c4`). + * We obtain: + * + * (c2) X<0 ==> G(X) + * (c1+c3) G(X) /\ X>0 ==> H + * (c1+c4) X>0 ==> H + * (c5) H ==> false + * + * Note that we can remove `c1` since it cannot be used for any future resolution steps + * anymore. Analogously, the predicate `G(X)` also occurs uniquely on the RHS of `c2`, + * so we eliminate `G(X)` as well: + * + * (c1+c2+c3) X<0 /\ X>0 ==> H + * (c1+c4) X>0 ==> H + * (c5) H ==> false + * + * The constraint of `c1+c2+c3` become UNSAT so this CHC can not be used in any + * reachability proof and we can remove it: + * + * (c1+c4) X>0 ==> H + * (c5) H ==> false + * + * Due to this removal the predicate `H` now also uccurs uniquely on the RHS of + * a CHC, so we can eliminate it as well: + * + * (c1+c4+c5) X>0 ==> false + * + * Thus, we are left with a trivial CHC problem. + */ +const std::set presolve(const std::vector& initial_chcs) { + // first collect all RHS predicates of all CHCs + std::set todo_rhs_preds; + for (const auto& chc: initial_chcs) { + if (chc.rhs.has_value()) { + todo_rhs_preds.insert(chc.rhs.value().name); + } + } + + std::set result_chcs(initial_chcs.begin(), initial_chcs.end()); + + // iterate over each RHS predicate and ... + while (!todo_rhs_preds.empty()) { + if (dbg || Config::Analysis::log) { + std::cout << "eliminating predicates: " << std::endl; + } + + for (const auto& pred: todo_rhs_preds) { + // ... check whether it occurs uniquely on the RHS of one CHC + const auto optional_uni_chc = unilaterally_resolvable_with(pred, result_chcs); + if (optional_uni_chc.has_value()) { + const Clause& uni_chc = optional_uni_chc.value(); + result_chcs.erase(uni_chc); + + if (dbg || Config::Analysis::log) { + std::cout << " - " << pred << std::endl; + } + + // An edge case to consider: if we have the clause set + // + // (c1) F ==> F + // (c2) F ==> false + // + // then `F` uniquely occurs on the RHS of `c1`. But after eliminating `c1` we get: + // + // (c1+c2) F ==> false + // + // We can't completely eliminate `F` because it also occurs on the LHS of `c1`. + // In fact, any clause that has `F` on the its LHS is "unreachable" so we can remove + // them all from the CHC problem. + if (uni_chc.indexOfLHSPred(pred).has_value()) { + std::set chcs_without_pred; + for (const Clause& chc: result_chcs) { + if (!chc.indexOfLHSPred(pred).has_value()) { + chcs_without_pred.insert(chc); + } + } + + result_chcs = chcs_without_pred; + } else { + std::set resolvents; + for (const Clause& chc: result_chcs) { + const Clause& resolvent = eliminate_pred(uni_chc, chc); + resolvents.insert(resolvent); + } + + result_chcs = resolvents; + } + } + } + + todo_rhs_preds.clear(); + + if (dbg || Config::Analysis::log) { + std::cout << "remove resolvents with UNSAT constraint: " << std::endl; + } + // Checking resolvents for satisfiability in a separate loop here, + // because it reduces the number of calls to the SMT solver. + std::set chcs_with_sat_guard; + for (const auto& chc: result_chcs) { + if (SmtFactory::check(chc.guard) == Sat) { + chcs_with_sat_guard.insert(chc); + } else if (chc.rhs.has_value()) { + // Assume we have the resolvents: + // + // (r1) F /\ (X>0 /\ X<0) ==> G + // (r2) F ==> G + // + // We can remove `r1` because the constraint is UNSAT. After that + // removal, `r2` is now unilaterally resolvable because we removed the + // only other clause, which had `G` as its RHS predicate. Thus, whenever + // we remove a resolvent, we add its RHS predicate into `rhs_preds` + // to re-check it in the next while-loop iteration. + todo_rhs_preds.insert(chc.rhs.value().name); + } + } + + // We can eliminate even more predicates by merging facts. For example, the + // facts: + // + // x=0 ==> F(x) + // + // x>0 ==> F(x) + // + // can be merged to: + // + // (x=0 \/ x>0) ==> F(x) + // + // This can make all facts unilaterally resolvable as long as the RHS predicate + // does not also occur on the RHS of a rule. + // + // Arguably, that just off-loads dealing with disjunctions to the linear solver. + // We also loose some CHC structure pushing disjunctions into the clause constraint. + // However, ADCL is designed to deal with disjunctions. And computing all resolvents + // in the non-linear solver is worst-case exponential in the number of LHS predicates, + // so it's probably worth it to eliminate as many LHS predicate as possible. + // + // For that we filter-out all the facts we currently have and partition them by their + // RHS predicates. Then we merge every group into a single fact. Notice, that we have + // to do this step repeatedly because some clauses might only later turn into facts. + // For example, here `G(x)` can not completely be merged into a single fact in the + // beginning: + // + // x=0 ==> F(x) + // + // x=1 ==> F(x) + // + // x=2 ==> G(x) + // + // F(x) ==> G(x) + // + // We merge all `F(x)` facts which makes the result unilaterally resolvable: + // + // (x=0 \/ x=1) ==> F(x) + // + // x=2 ==> G(x) + // + // F(x) /\ ==> G(x) + // + // We eliminate `F(x)` and get: + // + // x=2 ==> G(x) + // + // (x>0 \/ x=0) ==> G(x) + // + // Now, `G(x)` can be merged into a single fact: + // + // (x=0 \/ x=1 \/ x=2) ==> G(x) + // + const auto& [ facts, rest_chcs ] = partitionFacts(chcs_with_sat_guard); + result_chcs = rest_chcs; + for (const auto& [_, fact_group]: partitionByRHS(facts)) { + const Clause& merged_fact = merge_facts(fact_group); + + // If `fact_group.size() == 1` then `merge_facts` has nothing to merge and just + // returns the single fact unchanged. Thus, no facts where eliminated and nothing + // new became unilaterally resolvable. On the other hand, if `fact_group.size() > 1` + // then facts got eliminated, so the resulting clause might now be unilaterally + // resolvable and we add its RHS predicate back into `todo_rhs_preds`. + if (fact_group.size() > 1) { + todo_rhs_preds.insert(merged_fact.rhs.value().name); + } + + result_chcs.insert(merged_fact); + } + } + + if (dbg || Config::Analysis::log) { + std::cout << std::endl; + } + + // Use all facts and non-linear clauses that are already known at this point and + // do one round of resolution with them to derive all possible linear clauses that + // we can get at this point to give the linear solver as much information as possible + // for the first iteration. + const auto& [ linear_chcs, non_linear_chcs ] = partitionByDegree(result_chcs); + const auto& [ facts, _ ] = partitionFacts(linear_chcs); + std::set resolvents = all_resolvents(non_linear_chcs, facts); + result_chcs.insert(resolvents.begin(), resolvents.end()); + + return result_chcs; +} diff --git a/src/nonlinear/nonlinear.hpp b/src/nonlinear/nonlinear.hpp new file mode 100644 index 000000000..4b70306e0 --- /dev/null +++ b/src/nonlinear/nonlinear.hpp @@ -0,0 +1,34 @@ +#pragma once +#include "linearsolver.hpp" +#include "smt.hpp" + +class NonLinearSolver { + +private: + + // NonLinearSolver(); + +public: + + static void analyze(const std::vector& chcs); + +}; + +const std::set all_resolvents(const std::set& non_linear_chcs, const std::set& facts); + +void all_resolvents_aux( + const Clause& chc, + unsigned pred_index, + const std::set& facts, + std::set& resolvents, + unsigned& redundant_resolvent_count, + Smt& solver +); + +const Clause merge_facts(const std::vector facts); + +const std::vector normalize_all_preds(const std::vector& chc_problem); + +const std::optional unilaterally_resolvable_with(const FunApp& pred, const std::set& chcs); + +const std::set presolve(const std::vector& chc_problem); diff --git a/src/parser/chc/CHCParseVisitor.cpp b/src/parser/chc/CHCParseVisitor.cpp index e732dfcbd..b3bee80f8 100644 --- a/src/parser/chc/CHCParseVisitor.cpp +++ b/src/parser/chc/CHCParseVisitor.cpp @@ -1,6 +1,7 @@ #include "CHCParseVisitor.h" #include "boollit.hpp" #include "expr.hpp" +#include "clause.hpp" #include #include @@ -20,7 +21,7 @@ using lit_type = Res; using assert_type = Clause; using query_type = Clause; using symbol_type = std::string; -using tail_type = std::pair; +using tail_type = std::pair, BoolExpr>; using head_type = FunApp; using var_or_atom_type = std::variant; using boolop_type = BoolOp; @@ -32,19 +33,19 @@ Res::Res(const T &t): t(t) {} template Res::Res() {} -LocationIdx CHCParseVisitor::loc(const std::string &name) { - auto it = locations.find(name); - if (it == locations.end()) { - auto idx = its->addNamedLocation(name); - locations[name] = idx; - return idx; - } else { - return it->second; - } -} +// LocationIdx CHCParseVisitor::loc(const std::string &name) { +// auto it = locations.find(name); +// if (it == locations.end()) { +// auto idx = its->addNamedLocation(name); +// locations[name] = idx; +// return idx; +// } else { +// return it->second; +// } +// } antlrcpp::Any CHCParseVisitor::visitMain(CHCParser::MainContext *ctx) { - its->setInitialLocation(its->addNamedLocation("LoAT_init")); + // its->setInitialLocation(its->addNamedLocation("LoAT_init")); for (const auto &c: ctx->fun_decl()) { visit(c); } @@ -55,72 +56,24 @@ antlrcpp::Any CHCParseVisitor::visitMain(CHCParser::MainContext *ctx) { for (const auto &c: ctx->chc_query()) { clauses.push_back(any_cast(visit(c))); } - std::vector vars; - std::vector bvars; - for (unsigned i = 0; i < max_int_arity; ++i) { - vars.emplace_back(NumVar::nextProgVar()); - } - for (unsigned i = 0; i < max_bool_arity; ++i) { - bvars.emplace_back(BoolVar::nextProgVar()); - } - for (const Clause &c: clauses) { - Subs ren; - // replace the arguments of the body predicate with the corresponding program variables - unsigned bool_arg {0}; - unsigned int_arg {0}; - for (unsigned i = 0; i < c.lhs.args.size(); ++i) { - if (std::holds_alternative(c.lhs.args[i])) { - ren.put(std::get(c.lhs.args[i]), vars[int_arg]); - ++int_arg; - } else { - ren.put(std::get(c.lhs.args[i]), BExpression::buildTheoryLit(BoolLit(bvars[bool_arg]))); - ++bool_arg; - } - } - VarSet cVars; - for (const auto &var: c.rhs.args) { - cVars.insert(var); - } - c.guard->collectVars(cVars); - // replace all other variables from the clause with temporary variables - for (const auto &x: cVars) { - if (!ren.contains(x)) { - if (std::holds_alternative(x)) { - const auto &var = std::get(x); - ren.put(var, NumVar::next()); - } else if (std::holds_alternative(x)) { - const auto &var = std::get(x); - ren.put(var, BExpression::buildTheoryLit(BoolLit(BoolVar::next()))); - } else { - throw std::logic_error("unsupported theory in CHCParseVisitor"); - } - } - } - bool_arg = 0; - int_arg = 0; - Subs up; - for (unsigned i = 0; i < c.rhs.args.size(); ++i) { - if (std::holds_alternative(c.rhs.args[i])) { - up.put(vars[int_arg], ren.get(std::get(c.rhs.args[i]))); - ++int_arg; - } else if (std::holds_alternative(c.rhs.args[i])) { - up.put(bvars[bool_arg], ren.get(std::get(c.rhs.args[i]))); - ++bool_arg; - } else { - throw std::logic_error("unsupported theory in CHCParseVisitor"); - } - } - for (unsigned i = int_arg; i < max_int_arity; ++i) { - up.put(vars[i], NumVar::next()); - } - for (unsigned i = bool_arg; i < max_bool_arity; ++i) { - up.put(bvars[i], BExpression::buildTheoryLit(BoolLit(BoolVar::next()))); - } - up.put(NumVar::loc_var, c.rhs.loc); - const BoolExpr guard = c.guard->subs(ren)->simplify() & Rel::buildEq(NumVar::loc_var, c.lhs.loc); - its->addRule(Rule(guard, up), c.lhs.loc); - } - return its; + + // std::vector vars; + // for (unsigned i = 0; i < max_int_arity; ++i) { + // vars.emplace_back(NumVar::nextProgVar()); + // } + // its->numProgVars = vars; + + // std::vector bvars; + // for (unsigned i = 0; i < max_bool_arity; ++i) { + // bvars.emplace_back(BoolVar::nextProgVar()); + // } + // its->boolProgVars = bvars; + + // for (const Clause &c: clauses) { + // its->addClause(c); + // } + + return clauses; } std::string unescape(std::string name) { @@ -132,24 +85,25 @@ std::string unescape(std::string name) { } antlrcpp::Any CHCParseVisitor::visitFun_decl(CHCParser::Fun_declContext *ctx) { - unsigned long int_arity {0}; - unsigned long bool_arity {0}; - for (const auto &s: ctx->sort()) { - switch (std::any_cast(visit(s))) { - case Int: - ++int_arity; - break; - case Bool: - ++bool_arity; - break; - } - } - max_int_arity = std::max(max_int_arity, int_arity); - max_bool_arity = std::max(max_bool_arity, bool_arity); + // unsigned long int_arity {0}; + // unsigned long bool_arity {0}; + // for (const auto &s: ctx->sort()) { + // switch (std::any_cast(visit(s))) { + // case Int: + // ++int_arity; + // break; + // case Bool: + // ++bool_arity; + // break; + // } + // } + // max_int_arity = std::max(max_int_arity, int_arity); + // max_bool_arity = std::max(max_bool_arity, bool_arity); const auto name = any_cast(visit(ctx->symbol())); - const LocationIdx idx = its->addNamedLocation(name); - locations[name] = idx; - return idx; + // const LocationIdx idx = its->addNamedLocation(name); + // locations[name] = idx; + fun_names.insert(name); + return name; } antlrcpp::Any CHCParseVisitor::visitChc_assert(CHCParser::Chc_assertContext *ctx) { @@ -169,7 +123,7 @@ antlrcpp::Any CHCParseVisitor::visitChc_assert_head(CHCParser::Chc_assert_headCo antlrcpp::Any CHCParseVisitor::visitChc_assert_body(CHCParser::Chc_assert_bodyContext *ctx) { const auto lhs = any_cast(visit(ctx->chc_tail())); const auto rhs = any_cast(visit(ctx->chc_head())); - return Clause(lhs.first, rhs, lhs.second); + return Clause(lhs.first, rhs, lhs.second).normalize(); } antlrcpp::Any CHCParseVisitor::visitChc_head(CHCParser::Chc_headContext *ctx) { @@ -183,18 +137,18 @@ antlrcpp::Any CHCParseVisitor::visitChc_tail(CHCParser::Chc_tailContext *ctx) { guards.push_back(r.t); guards.insert(guards.end(), r.refinement.begin(), r.refinement.end()); } - std::optional lhs; + + std::vector predicates; for (const auto &c: ctx->var_or_atom()) { const auto v = any_cast(visit(c)); if (std::holds_alternative(v)) { guards.push_back(BExpression::buildTheoryLit(BoolLit(std::get(v)))); - } else if (lhs) { - throw std::invalid_argument("non-linear clause " + ctx->getText()); } else { - lhs = std::get(v); + predicates.push_back(std::get(v)); } } - return std::pair(lhs.value_or(FunApp(its->getInitialLocation(), {})), BExpression::buildAnd(guards)); + + return std::pair(predicates, BExpression::buildAnd(guards)); } antlrcpp::Any CHCParseVisitor::visitChc_query(CHCParser::Chc_queryContext *ctx) { @@ -203,7 +157,9 @@ antlrcpp::Any CHCParseVisitor::visitChc_query(CHCParser::Chc_queryContext *ctx) } const auto lhs = any_cast(visit(ctx->chc_tail())); vars.clear(); - return Clause(lhs.first, FunApp(its->getSink(), {}), lhs.second); + + // const auto sink_name = its->getLocationNames().at(its->getSink()); + return Clause(lhs.first, {}, lhs.second).normalize(); } antlrcpp::Any CHCParseVisitor::visitVar_decl(CHCParser::Var_declContext *ctx) { @@ -215,8 +171,9 @@ antlrcpp::Any CHCParseVisitor::visitVar_decl(CHCParser::Var_declContext *ctx) { antlrcpp::Any CHCParseVisitor::visitU_pred_atom(CHCParser::U_pred_atomContext *ctx) { const auto name = any_cast(visit(ctx->symbol())); - const std::optional loc = its->getLocationIdx(name); - if (!loc) { + // const std::optional loc = its->getLocationIdx(name); + // TODO: + if (!fun_names.contains(name)) { throw std::invalid_argument("undeclared function symbol " + name); } std::vector args; @@ -228,7 +185,7 @@ antlrcpp::Any CHCParseVisitor::visitU_pred_atom(CHCParser::U_pred_atomContext *c throw std::invalid_argument("arguments of predicate are not distinct"); } } - return FunApp(*loc, args); + return FunApp(name, args); } antlrcpp::Any CHCParseVisitor::visitI_formula(CHCParser::I_formulaContext *ctx) { @@ -575,9 +532,9 @@ antlrcpp::Any CHCParseVisitor::visitSort(CHCParser::SortContext *ctx) { antlrcpp::Any CHCParseVisitor::visitVar_or_atom(CHCParser::Var_or_atomContext *ctx) { if (ctx->var()) { - const std::optional loc = its->getLocationIdx(unescape(ctx->getText())); - if (loc) { - return std::variant(FunApp(*loc, {})); + const auto name = unescape(ctx->getText()); + if (fun_names.contains(name)) { // its->getLocationIdx(name).has_value()) { + return std::variant(FunApp(name, {})); } else { return std::variant(std::get(any_cast(visit(ctx->var())))); } diff --git a/src/parser/chc/CHCParseVisitor.h b/src/parser/chc/CHCParseVisitor.h index 22e408c8c..24fcd4c97 100644 --- a/src/parser/chc/CHCParseVisitor.h +++ b/src/parser/chc/CHCParseVisitor.h @@ -1,7 +1,7 @@ #pragma once -#include "itsproblem.hpp" #include "CHCVisitor.h" +#include "theory.hpp" template struct Res { @@ -50,37 +50,16 @@ enum Sort { Int, Bool }; -struct FunApp { - - LocationIdx loc; - std::vector args; - - FunApp(const LocationIdx loc, const std::vector args): loc(loc), args(args) {} - -}; - -struct Clause { - const FunApp lhs; - const FunApp rhs; - const BoolExpr guard; - - Clause(const FunApp &lhs, const FunApp &rhs, const BoolExpr &guard): lhs(lhs), rhs(rhs), guard(guard) {} - -}; - /** * This class provides an empty implementation of CHCVisitor, which can be * extended to create a visitor which only needs to handle a subset of the available methods. */ class CHCParseVisitor : public CHCVisitor { - ITSPtr its {std::make_shared()}; - std::unordered_map locations; - std::unordered_map vars; - unsigned long max_int_arity {0}; - unsigned long max_bool_arity {0}; + std::map vars; + std::set> fun_names; - LocationIdx loc(const std::string &name); + // LocationIdx loc(const std::string &name); Var var(const std::string &name, Sort sort); public: diff --git a/src/parser/chc/chcparser.cpp b/src/parser/chc/chcparser.cpp index 97bdf401c..19a9ac693 100644 --- a/src/parser/chc/chcparser.cpp +++ b/src/parser/chc/chcparser.cpp @@ -24,7 +24,7 @@ using namespace antlr4; using namespace hornParser; -ITSPtr HornParser::loadFromFile(const std::string &filename) { +std::vector HornParser::loadFromFile(const std::string &filename) { std::ifstream file(filename); if (!file.is_open()) { throw std::invalid_argument("Unable to open file: " + filename); @@ -39,6 +39,6 @@ ITSPtr HornParser::loadFromFile(const std::string &filename) { if (parser.getNumberOfSyntaxErrors() > 0) { throw std::invalid_argument("parsing failed"); } else { - return any_cast(vis.visit(ctx)); + return any_cast>(vis.visit(ctx)); } } diff --git a/src/parser/chc/chcparser.hpp b/src/parser/chc/chcparser.hpp index db0645def..ce1955191 100644 --- a/src/parser/chc/chcparser.hpp +++ b/src/parser/chc/chcparser.hpp @@ -13,7 +13,7 @@ class HornParser { * @param path The file to load * @return The resulting ITSProblem (a FileError is thrown if parsing fails) */ - static ITSPtr loadFromFile(const std::string &path); + static std::vector loadFromFile(const std::string &path); }; diff --git a/test_data_lialin.txt b/test_data_lialin.txt new file mode 100644 index 000000000..62bb8f19f --- /dev/null +++ b/test_data_lialin.txt @@ -0,0 +1,175 @@ +032 unsat +034 unsat +038 unsat +043 unsat +044 unsat +045 unsat +047 unsat +050 unsat +052 unsat +053 unsat +057 unsat +059 unsat +083 unsat +084 unsat +089 unsat +119 unsat +130 unsat +133 unsat +154 unsat +297 unsat +299 unsat +316 unsat +185 unsat +187 unsat +175 unsat +402 unsat +321 unsat +319 unsat +331 unsat +329 unsat +330 unsat +328 unsat +322 unsat +336 unsat +332 unsat +335 unsat +327 unsat +401 unsat +334 unsat +358 unsat +362 unsat +386 unsat +381 unsat +348 unsat +197 unsat +037 unsat +111 unsat +036 unknown +242 unknown +179 unknown +199 unknown +172 unknown +170 unknown +323 unknown +214 unknown +182 unknown +006 unknown +015 unknown +018 unknown +020 unknown +022 unknown +026 unknown +029 unknown +090 unknown +091 unknown +103 unknown +104 unknown +105 unknown +107 unknown +108 unknown +125 unknown +126 unknown +127 unknown +461 unknown +000 unknown +001 unknown +002 unknown +003 unknown +004 unknown +005 unknown +010 unknown +014 unknown +021 unknown +023 unknown +079 unknown +081 unknown +085 unknown +094 unknown +095 unknown +097 unknown +112 unknown +115 unknown +118 unknown +120 unknown +128 unknown +134 unknown +290 unknown +291 unknown +293 unknown +294 unknown +295 unknown +296 unknown +298 unknown +300 unknown +301 unknown +303 unknown +304 unknown +305 unknown +306 unknown +307 unknown +308 unknown +309 unknown +310 unknown +311 unknown +409 unknown +410 unknown +411 unknown +412 unknown +413 unknown +414 unknown +415 unknown +416 unknown +417 unknown +418 unknown +419 unknown +420 unknown +421 unknown +422 unknown +423 unknown +424 unknown +425 unknown +426 unknown +427 unknown +428 unknown +429 unknown +430 unknown +431 unknown +434 unknown +435 unknown +436 unknown +437 unknown +438 unknown +439 unknown +440 unknown +441 unknown +443 unknown +444 unknown +445 unknown +178 unknown +183 unknown +177 unknown +184 unknown +176 unknown +186 unknown +173 unknown +320 unknown +016 unknown +150 unknown +009 unknown +333 unknown +325 unknown +180 unknown +181 unknown +240 unknown +171 unknown +208 unknown +215 unknown +257 unknown +240 unknown +207 unknown +241 unknown +210 unknown +231 unknown +248 unknown +243 unknown