Sort.sortOf returns the wrong type

[daniel-raffler]

Hello,
it seems that Sort.sortOf sometimes returns Integer, even when the term should have type Rational. Here are a few examples I've found:

import ap.SimpleAPI
import ap.parameters.GlobalSettings
import ap.types.Sort
import ap.util.Debug
import org.scalatest.funsuite.AnyFunSuite

class SortOfBug extends AnyFunSuite {
  import ap.parser.IExpression.{Sort => _, _}
  import ap.theories.rationals.Rationals._;

  val withAssertions = false;

  test("plus") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      val a = createConstant("a", dom)
      val b = createConstant("b", dom)
      val f1 = a + b
      printf("%s :: %s\n", f1, Sort.sortOf(f1)) // Says Int, but should be Rational

      assertResult(dom)(Sort.sortOf(f1))
    }
  }

  test("mul") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      val a = createConstant("a", dom)
      val b = int(2) // frac(2,1) works
      val f1 = mul(a, b)
      printf("%s :: %s\n", f1, Sort.sortOf(f1)) // Says Int, but should be Rational

      assertResult(dom)(Sort.sortOf(f1))
    }
  }

  test("nested mul/plus") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      val a = createConstant("a", dom)
      val b = createConstant("b", dom)
      val f1 = a + b

      val c = createBooleanVariable("c")
      val d = frac(2, 1)
      val f2 = ite(c, f1, d)
      printf("%s :: %s\n", f2, Sort.sortOf(f2)) // Says Int, but should be Rational

      assertResult(dom)(Sort.sortOf(f2))
    }
  }
}

There might be other instances like div that just didn't show up in our tests.

Is this something that could be fixed?

[daniel-raffler]

One more variant of this:

  test("mul") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      val a = createConstant("a", dom)
      val b = int(0)
      val f1 = mul(a, b)
      printf("%s :: %s\n", f1, Sort.sortOf(f1))

      assertResult(dom)(Sort.sortOf(f1))
    }
  }

Here f1 is simplified even further and we get IIntLit 0 instead of just ITimes k a.

[pruemmer]

This can be fixed, but requires some reorganization of the theory of rationals; I won't have time for doing anything about this problem right away.

[daniel-raffler]

This can be fixed, but requires some reorganization of the theory of rationals; I won't have time for doing anything about this problem right away.

Thanks for the updates! We do have a workaround for the issue, so this isn't too pressing.

When you have time, could you maybe release a new version (to Maven) of Princess and Ostrich with the latest bug fixes?

[pruemmer]

That's an excellent idea ;-) I have just released versions 2024-11-08 (Princess) and 1.4.1 (Ostrich)!

[pruemmer]

This should all be working now:
https://github.com/uuverifiers/princess/blob/master/src/test/scala/ap/theories/rationals/RatTypes.scala

[daniel-raffler]

Yes, it's working now. Thanks for your help!