|
29 | 29 | import ap.parser.SMTParser2InputAbsy.SMTType;
|
30 | 30 | import ap.terfor.ConstantTerm;
|
31 | 31 | import ap.terfor.preds.Predicate;
|
32 |
| -import ap.theories.ExtArray; |
| 32 | +import ap.theories.ExtArray.ArraySort; |
33 | 33 | import ap.theories.bitvectors.ModuloArithmetic;
|
34 | 34 | import ap.theories.rationals.Fractions.FractionSort$;
|
35 | 35 | import ap.types.Sort;
|
@@ -532,9 +532,9 @@ private static FormulaType<?> getFormulaTypeFromSort(final Sort sort) {
|
532 | 532 | return FormulaType.IntegerType;
|
533 | 533 | } else if (sort instanceof FractionSort$) {
|
534 | 534 | return FormulaType.RationalType;
|
535 |
| - } else if (sort instanceof ExtArray.ArraySort) { |
536 |
| - Seq<Sort> indexSorts = ((ExtArray.ArraySort) sort).theory().indexSorts(); |
537 |
| - Sort elementSort = ((ExtArray.ArraySort) sort).theory().objSort(); |
| 535 | + } else if (sort instanceof ArraySort) { |
| 536 | + Seq<Sort> indexSorts = ((ArraySort) sort).theory().indexSorts(); |
| 537 | + Sort elementSort = ((ArraySort) sort).theory().objSort(); |
538 | 538 | assert indexSorts.iterator().size() == 1 : "unexpected index type in Array type:" + sort;
|
539 | 539 | // assert indexSorts.size() == 1; // TODO Eclipse does not like simpler code.
|
540 | 540 | return FormulaType.getArrayType(
|
@@ -598,20 +598,20 @@ public IFunction declareFun(String name, Sort returnType, List<Sort> args) {
|
598 | 598 |
|
599 | 599 | public ITerm makeSelect(ITerm array, ITerm index) {
|
600 | 600 | List<ITerm> args = ImmutableList.of(array, index);
|
601 |
| - ExtArray.ArraySort arraySort = (ExtArray.ArraySort) Sort$.MODULE$.sortOf(array); |
| 601 | + ArraySort arraySort = (ArraySort) Sort$.MODULE$.sortOf(array); |
602 | 602 | return new IFunApp(arraySort.theory().select(), toSeq(args));
|
603 | 603 | }
|
604 | 604 |
|
605 | 605 | public ITerm makeStore(ITerm array, ITerm index, ITerm value) {
|
606 | 606 | List<ITerm> args = ImmutableList.of(array, index, value);
|
607 |
| - ExtArray.ArraySort arraySort = (ExtArray.ArraySort) Sort$.MODULE$.sortOf(array); |
| 607 | + ArraySort arraySort = (ArraySort) Sort$.MODULE$.sortOf(array); |
608 | 608 | return new IFunApp(arraySort.theory().store(), toSeq(args));
|
609 | 609 | }
|
610 | 610 |
|
611 | 611 | public boolean hasArrayType(IExpression exp) {
|
612 | 612 | if (exp instanceof ITerm) {
|
613 | 613 | final ITerm t = (ITerm) exp;
|
614 |
| - return Sort$.MODULE$.sortOf(t) instanceof ExtArray.ArraySort; |
| 614 | + return Sort$.MODULE$.sortOf(t) instanceof ArraySort; |
615 | 615 | } else {
|
616 | 616 | return false;
|
617 | 617 | }
|
|
0 commit comments