Skip to content

Commit

Permalink
fix: add support for Rational type in Princess.
Browse files Browse the repository at this point in the history
We do not yet add support for building queries (see #257 for that),
but only add a minimal capacity for getting the type from parsed formulas containing rational symbols.
  • Loading branch information
kfriedberger committed Jul 4, 2022
1 parent fb56765 commit a6a34b4
Showing 1 changed file with 3 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
import ap.terfor.preds.Predicate;
import ap.theories.ExtArray;
import ap.theories.bitvectors.ModuloArithmetic;
import ap.theories.rationals.Fractions.FractionSort$;
import ap.types.Sort;
import ap.types.Sort$;
import ap.types.Sort.MultipleValueBool$;
Expand Down Expand Up @@ -528,6 +529,8 @@ private static FormulaType<?> getFormulaTypeFromSort(final Sort sort) {
return FormulaType.BooleanType;
} else if (sort == PrincessEnvironment.INTEGER_SORT) {
return FormulaType.IntegerType;
} else if (sort instanceof FractionSort$) {
return FormulaType.RationalType;
} else if (sort instanceof ExtArray.ArraySort) {
Seq<Sort> indexSorts = ((ExtArray.ArraySort) sort).theory().indexSorts();
Sort elementSort = ((ExtArray.ArraySort) sort).theory().objSort();
Expand Down

0 comments on commit a6a34b4

Please sign in to comment.