diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 10:07:12 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 10:07:19 +0200 |
commit | fb746fdd4e60e7d166b0fa1e5788bea925d22ee7 (patch) | |
tree | 1a8b8dc8c2b4f57352ab10365e2b2765c06285c9 /test/regress | |
parent | 60f6d09d7ad9e37f5a23e6a2b0e47a7b0e47df81 (diff) |
Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Enable redundant ITE branch elimination in quantifiers rewriter.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/quantifiers/006-cbqi-ite.smt2 | 299 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 |
2 files changed, 301 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/006-cbqi-ite.smt2 b/test/regress/regress0/quantifiers/006-cbqi-ite.smt2 new file mode 100644 index 000000000..bfa3ef22b --- /dev/null +++ b/test/regress/regress0/quantifiers/006-cbqi-ite.smt2 @@ -0,0 +1,299 @@ +(set-logic LIA) +(set-info :status unsat) +(declare-fun W_S2_V6 () Bool) +(declare-fun W_S2_V4 () Bool) +(declare-fun W_S2_V2 () Bool) +(declare-fun W_S2_V3 () Bool) +(declare-fun W_S2_V1 () Bool) +(declare-fun W_S1_V6 () Bool) +(declare-fun W_S1_V5 () Bool) +(declare-fun W_S1_V2 () Bool) +(declare-fun W_S1_V3 () Bool) +(declare-fun W_S1_V1 () Bool) +(declare-fun R_S1_V1 () Bool) +(declare-fun R_S2_V6 () Bool) +(declare-fun R_S2_V4 () Bool) +(declare-fun R_S2_V5 () Bool) +(declare-fun R_S2_V2 () Bool) +(declare-fun R_S2_V3 () Bool) +(declare-fun R_S2_V1 () Bool) +(declare-fun R_E1_V6 () Bool) +(declare-fun R_E1_V4 () Bool) +(declare-fun R_E1_V5 () Bool) +(declare-fun R_E1_V2 () Bool) +(declare-fun R_E1_V3 () Bool) +(declare-fun R_E1_V1 () Bool) +(declare-fun DISJ_W_S2_R_E1 () Bool) +(declare-fun DISJ_W_S2_R_S2 () Bool) +(declare-fun R_S1_V6 () Bool) +(declare-fun R_S1_V4 () Bool) +(declare-fun R_S1_V5 () Bool) +(declare-fun R_S1_V2 () Bool) +(declare-fun R_S1_V3 () Bool) +(declare-fun DISJ_W_S2_R_S1 () Bool) +(declare-fun DISJ_W_S1_W_S2 () Bool) +(declare-fun DISJ_W_S1_R_E1 () Bool) +(declare-fun DISJ_W_S1_R_S2 () Bool) +(declare-fun DISJ_W_S1_R_S1 () Bool) +(declare-fun W_S2_V5 () Bool) +(declare-fun W_S1_V4 () Bool) +(assert + (let + (($x1615 + (forall + ((V1_0 Int) (V3_0 Int) + (V2_0 Int) (V5_0 Int) + (V4_0 Int) (V6_0 Int) + (MW_S1_V1 Bool) (MW_S1_V3 Bool) + (MW_S1_V2 Bool) (MW_S1_V5 Bool) + (MW_S1_V4 Bool) (MW_S1_V6 Bool) + (MW_S2_V1 Bool) (MW_S2_V3 Bool) + (MW_S2_V2 Bool) (MW_S2_V5 Bool) + (MW_S2_V4 Bool) (MW_S2_V6 Bool) + (S1_V1_!158 Int) (S1_V1_!171 Int) + (S2_V5_!167 Int) (S2_V5_!180 Int) + (S1_V3_!159 Int) (S1_V3_!172 Int) + (S1_V2_!160 Int) (S1_V2_!173 Int) + (E1_!157 Int) (E1_!170 Int) + (E1_!183 Int) (S2_V4_!168 Int) + (S2_V4_!181 Int) (S2_V6_!169 Int) + (S2_V6_!182 Int) (S1_V5_!161 Int) + (S1_V5_!174 Int) (S2_V1_!164 Int) + (S2_V1_!177 Int) (S1_V4_!162 Int) + (S1_V4_!175 Int) (S2_V3_!165 Int) + (S2_V3_!178 Int) (S2_V2_!166 Int) + (S2_V2_!179 Int) (S1_V6_!163 Int) + (S1_V6_!176 Int)) + (let ((?x1431 (ite MW_S1_V6 S1_V6_!176 V6_0))) + (let ((?x1432 (ite MW_S2_V6 S2_V6_!182 ?x1431))) + (let ((?x1433 (ite MW_S1_V6 S1_V6_!163 V6_0))) + (let ((?x1434 (ite MW_S2_V6 S2_V6_!169 ?x1433))) + (let (($x1435 (= ?x1434 ?x1432))) + (let ((?x1436 (ite MW_S1_V4 S1_V4_!175 V4_0))) + (let ((?x1437 (ite MW_S2_V4 S2_V4_!181 ?x1436))) + (let ((?x1438 (ite MW_S1_V4 S1_V4_!162 V4_0))) + (let ((?x1439 (ite MW_S2_V4 S2_V4_!168 ?x1438))) + (let (($x1440 (= ?x1439 ?x1437))) + (let ((?x1441 (ite MW_S1_V5 S1_V5_!174 V5_0))) + (let ((?x1442 (ite MW_S2_V5 S2_V5_!180 ?x1441))) + (let ((?x1444 (ite MW_S1_V5 S1_V5_!161 V5_0))) + (let ((?x1445 (ite MW_S2_V5 S2_V5_!167 ?x1444))) + (let (($x1446 (= ?x1445 ?x1442))) + (let ((?x1447 (ite MW_S1_V2 S1_V2_!173 V2_0))) + (let ((?x1448 (ite MW_S2_V2 S2_V2_!179 ?x1447))) + (let ((?x1449 (ite MW_S1_V2 S1_V2_!160 V2_0))) + (let ((?x1450 (ite MW_S2_V2 S2_V2_!166 ?x1449))) + (let (($x1451 (= ?x1450 ?x1448))) + (let ((?x1467 (ite MW_S1_V3 S1_V3_!159 V3_0))) + (let ((?x1468 (+ 1 ?x1467))) + (let ((?x1458 (ite MW_S2_V3 S2_V3_!165 ?x1468))) + (let + (($x1459 + (= ?x1458 + (+ (ite MW_S2_V3 S2_V3_!178 (ite MW_S1_V3 S1_V3_!172 V3_0)) ?x1448 + (* (- 1) E1_!183))))) + (let ((?x1460 (ite MW_S1_V1 S1_V1_!171 E1_!170))) + (let ((?x1487 (ite MW_S2_V1 S2_V1_!177 ?x1460))) + (let ((?x1453 (ite MW_S1_V1 S1_V1_!158 E1_!157))) + (let ((?x1489 (ite MW_S2_V1 S2_V1_!164 ?x1453))) + (let (($x1289 (= ?x1489 ?x1487))) + (let ((?x1455 (+ (- 1) ?x1448))) + (let (($x1376 (>= ?x1487 ?x1455))) + (let (($x1377 (<= V2_0 E1_!170))) + (let (($x1379 (not $x1377))) + (let ((?x1380 (+ (- 1) ?x1450))) + (let (($x1381 (>= ?x1489 ?x1380))) + (let (($x1479 (<= V2_0 E1_!157))) + (let (($x1456 (not $x1479))) + (let (($x1499 (and $x1456 $x1381 $x1379 $x1376))) + (let (($x1500 (not $x1499))) + (let (($x1502 (not MW_S2_V6))) + (let (($x1503 (or $x1502 W_S2_V6))) + (let (($x1504 (not MW_S2_V4))) + (let (($x1505 (or $x1504 W_S2_V4))) + (let (($x1508 (not MW_S2_V2))) + (let (($x1509 (or $x1508 W_S2_V2))) + (let (($x1510 (not MW_S2_V3))) + (let (($x1511 (or $x1510 W_S2_V3))) + (let (($x1512 (not MW_S2_V1))) + (let (($x1513 (or $x1512 W_S2_V1))) + (let (($x1514 (not MW_S1_V6))) + (let (($x1515 (or $x1514 W_S1_V6))) + (let (($x1518 (not MW_S1_V5))) + (let (($x1519 (or $x1518 W_S1_V5))) + (let (($x1520 (not MW_S1_V2))) + (let (($x1521 (or $x1520 W_S1_V2))) + (let (($x1522 (not MW_S1_V3))) + (let (($x1523 (or $x1522 W_S1_V3))) + (let (($x1524 (not MW_S1_V1))) + (let (($x1525 (or $x1524 W_S1_V1))) + (let (($x1527 (= S1_V6_!176 S1_V6_!163))) + (let (($x1528 (= E1_!170 E1_!157))) + (let (($x228 (not R_S1_V1))) + (let (($x1529 (or $x228 $x1528))) + (let (($x1530 (not $x1529))) + (let (($x1531 (or $x1530 $x1527))) + (let (($x1532 (= S2_V2_!179 S2_V2_!166))) + (let (($x1533 (= ?x1431 ?x1433))) + (let (($x253 (not R_S2_V6))) + (let (($x1534 (or $x253 $x1533))) + (let (($x1535 (= ?x1436 ?x1438))) + (let (($x251 (not R_S2_V4))) + (let (($x1536 (or $x251 $x1535))) + (let (($x1537 (= ?x1441 ?x1444))) + (let (($x249 (not R_S2_V5))) + (let (($x1538 (or $x249 $x1537))) + (let (($x1539 (= ?x1447 ?x1449))) + (let (($x247 (not R_S2_V2))) + (let (($x1540 (or $x247 $x1539))) + (let ((?x1462 (ite MW_S1_V3 S1_V3_!172 V3_0))) + (let (($x1541 (= ?x1462 ?x1468))) + (let (($x245 (not R_S2_V3))) + (let (($x1542 (or $x245 $x1541))) + (let (($x1543 (= ?x1460 ?x1453))) + (let (($x243 (not R_S2_V1))) + (let (($x1544 (or $x243 $x1543))) + (let (($x1545 (and $x1544 $x1542 $x1540 $x1538 $x1536 $x1534))) + (let (($x1546 (not $x1545))) + (let (($x1547 (or $x1546 $x1532))) + (let (($x1548 (= S2_V3_!165 S2_V3_!178))) + (let (($x1549 (= ?x1433 ?x1431))) + (let (($x1550 (or $x253 $x1549))) + (let (($x1551 (= ?x1438 ?x1436))) + (let (($x1552 (or $x251 $x1551))) + (let (($x1553 (= ?x1444 ?x1441))) + (let (($x1554 (or $x249 $x1553))) + (let (($x1555 (= ?x1449 ?x1447))) + (let (($x1556 (or $x247 $x1555))) + (let ((?x1557 (+ (- 1) ?x1462))) + (let (($x1558 (= ?x1467 ?x1557))) + (let (($x1559 (or $x245 $x1558))) + (let (($x1560 (= ?x1453 ?x1460))) + (let (($x1561 (or $x243 $x1560))) + (let (($x1562 (and $x1561 $x1559 $x1556 $x1554 $x1552 $x1550))) + (let (($x1563 (not $x1562))) + (let (($x1564 (or $x1563 $x1548))) + (let (($x1565 (= S1_V4_!175 S1_V4_!162))) + (let (($x1566 (or $x1530 $x1565))) + (let (($x1567 (= S2_V1_!177 S2_V1_!164))) + (let (($x1568 (or $x1546 $x1567))) + (let (($x1569 (= S1_V5_!174 S1_V5_!161))) + (let (($x1570 (or $x1530 $x1569))) + (let (($x1571 (= S2_V6_!182 S2_V6_!169))) + (let (($x1572 (or $x1546 $x1571))) + (let (($x1573 (= S2_V4_!168 S2_V4_!181))) + (let (($x1574 (or $x1563 $x1573))) + (let (($x1575 (= E1_!170 E1_!183))) + (let (($x1576 (= V6_0 ?x1432))) + (let (($x177 (not R_E1_V6))) + (let (($x1577 (or $x177 $x1576))) + (let (($x1578 (= V4_0 ?x1437))) + (let (($x175 (not R_E1_V4))) + (let (($x1579 (or $x175 $x1578))) + (let (($x1580 (= V5_0 ?x1442))) + (let (($x173 (not R_E1_V5))) + (let (($x1581 (or $x173 $x1580))) + (let (($x1582 (= V2_0 ?x1448))) + (let (($x171 (not R_E1_V2))) + (let (($x1583 (or $x171 $x1582))) + (let ((?x1463 (ite MW_S2_V3 S2_V3_!178 ?x1462))) + (let (($x1584 (= V3_0 ?x1463))) + (let (($x169 (not R_E1_V3))) + (let (($x1585 (or $x169 $x1584))) + (let ((?x1586 (+ 1 ?x1487))) + (let (($x1587 (= V1_0 ?x1586))) + (let (($x167 (not R_E1_V1))) + (let (($x1588 (or $x167 $x1587))) + (let (($x1589 (and $x1588 $x1585 $x1583 $x1581 $x1579 $x1577))) + (let (($x1590 (not $x1589))) + (let (($x1591 (or $x1590 $x1575))) + (let (($x1592 (= E1_!157 E1_!183))) + (let (($x1593 (or $x1590 $x1592))) + (let (($x1594 (= E1_!157 E1_!170))) + (let (($x1595 (= S1_V2_!173 S1_V2_!160))) + (let (($x1596 (or $x1530 $x1595))) + (let (($x1597 (= S1_V3_!159 S1_V3_!172))) + (let (($x1598 (or $x228 $x1594))) + (let (($x1599 (not $x1598))) + (let (($x1600 (or $x1599 $x1597))) + (let (($x1601 (= S2_V5_!180 S2_V5_!167))) + (let (($x1602 (or $x1546 $x1601))) + (let (($x1603 (= S1_V1_!158 S1_V1_!171))) + (let (($x1604 (or $x1599 $x1603))) + (let + (($x1612 + (and $x1604 $x1602 $x1600 $x1596 $x1594 $x1593 $x1591 $x1574 $x1572 + $x1570 $x1568 $x1566 $x1564 $x1547 $x1531 $x1525 $x1523 $x1521 $x1519 + $x1515 $x1513 $x1511 $x1509 $x1505 $x1503))) + (let (($x1613 (not $x1612))) + (or $x1613 $x1500 (and $x1289 $x1459 $x1451 $x1446 $x1440 $x1435))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (let (($x103 (and W_S2_V6 R_E1_V6))) + (let (($x102 (and W_S2_V4 R_E1_V4))) + (let (($x100 (and W_S2_V2 R_E1_V2))) + (let (($x99 (and W_S2_V3 R_E1_V3))) + (let (($x98 (and W_S2_V1 R_E1_V1))) + (let (($x128 (or $x98 $x99 $x100 R_E1_V5 $x102 $x103))) + (let (($x129 (not $x128))) + (let (($x130 (= DISJ_W_S2_R_E1 $x129))) + (let (($x93 (and W_S2_V6 R_S2_V6))) + (let (($x92 (and W_S2_V4 R_S2_V4))) + (let (($x90 (and W_S2_V2 R_S2_V2))) + (let (($x89 (and W_S2_V3 R_S2_V3))) + (let (($x88 (and W_S2_V1 R_S2_V1))) + (let (($x125 (or $x88 $x89 $x90 R_S2_V5 $x92 $x93))) + (let (($x126 (not $x125))) + (let (($x127 (= DISJ_W_S2_R_S2 $x126))) + (let (($x83 (and W_S2_V6 R_S1_V6))) + (let (($x82 (and W_S2_V4 R_S1_V4))) + (let (($x80 (and W_S2_V2 R_S1_V2))) + (let (($x79 (and W_S2_V3 R_S1_V3))) + (let (($x78 (and W_S2_V1 R_S1_V1))) + (let (($x122 (or $x78 $x79 $x80 R_S1_V5 $x82 $x83))) + (let (($x123 (not $x122))) + (let (($x124 (= DISJ_W_S2_R_S1 $x123))) + (let (($x73 (and W_S1_V6 W_S2_V6))) + (let (($x68 (and W_S1_V2 W_S2_V2))) + (let (($x66 (and W_S1_V3 W_S2_V3))) + (let (($x64 (and W_S1_V1 W_S2_V1))) + (let (($x119 (or $x64 $x66 $x68 W_S1_V5 W_S2_V4 $x73))) + (let (($x120 (not $x119))) + (let (($x121 (= DISJ_W_S1_W_S2 $x120))) + (let (($x58 (and W_S1_V6 R_E1_V6))) + (let (($x54 (and W_S1_V5 R_E1_V5))) + (let (($x52 (and W_S1_V2 R_E1_V2))) + (let (($x50 (and W_S1_V3 R_E1_V3))) + (let (($x48 (and W_S1_V1 R_E1_V1))) + (let (($x116 (or $x48 $x50 $x52 $x54 R_E1_V4 $x58))) + (let (($x117 (not $x116))) + (let (($x118 (= DISJ_W_S1_R_E1 $x117))) + (let (($x42 (and W_S1_V6 R_S2_V6))) + (let (($x38 (and W_S1_V5 R_S2_V5))) + (let (($x36 (and W_S1_V2 R_S2_V2))) + (let (($x34 (and W_S1_V3 R_S2_V3))) + (let (($x32 (and W_S1_V1 R_S2_V1))) + (let (($x113 (or $x32 $x34 $x36 $x38 R_S2_V4 $x42))) + (let (($x114 (not $x113))) + (let (($x115 (= DISJ_W_S1_R_S2 $x114))) + (let (($x26 (and W_S1_V6 R_S1_V6))) + (let (($x21 (and W_S1_V5 R_S1_V5))) + (let (($x18 (and W_S1_V2 R_S1_V2))) + (let (($x15 (and W_S1_V3 R_S1_V3))) + (let (($x12 (and W_S1_V1 R_S1_V1))) + (let (($x110 (or $x12 $x15 $x18 $x21 R_S1_V4 $x26))) + (let (($x111 (not $x110))) + (let (($x112 (= DISJ_W_S1_R_S1 $x111))) + (and W_S1_V4 W_S2_V5 $x112 $x115 $x118 $x121 $x124 $x127 $x130 $x1615)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(assert + (let (($x1192 (not W_S2_V2))) + (let (($x1189 (not W_S2_V3))) + (let (($x1186 (not W_S2_V1))) + (let (($x1091 (not W_S1_V2))) + (let (($x1078 (not W_S1_V1))) + (let (($x245 (not R_S2_V3))) + (let (($x167 (not R_E1_V1))) + (let + (($x1647 + (and $x167 $x245 $x1078 $x1091 $x1186 $x1189 $x1192 DISJ_W_S1_R_E1 + DISJ_W_S2_R_E1))) (not $x1647)))))))))) +(check-sat) + diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 092c1548f..60b10666e 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -53,7 +53,8 @@ TESTS = \ nested-delta.smt2 \ nested-inf.smt2 \ RND-small.smt2 \ - clock-10.smt2 + clock-10.smt2 \ + 006-cbqi-ite.smt2 |