Princess does not support Real values in arrays

[daniel-raffler]

Hello everyone,
Princess seems to crash whenever I try to create an array with Real numbers as index or element type. Here is an smt file that will trigger the issue:

(declare-const empty (Array Int Real))
(declare-const array (Array Int Real))

(assert (= array ((as array (Array Int Real)) 0.0)))
(assert (= (select array 4) 0.1))

(check-sat)
(get-model)

When I run it with princess 2024-01-12 I get this output:

daniel@ZenBook:~/Downloads/princess-bin-2024-01-12$ ./princess -logo +incremental ~/array.smt2 
OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release.
Loading /home/daniel/array.smt2 ...
error
Universal quantifiers over fractions/rationals are currently not supported

This seems to be a regression as the same code still worked with the previous release:

daniel@ZenBook:~/Downloads/princess-bin-2023-06-19$ ./princess -logo +incremental ~/array.smt2 
OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release.
Loading /home/daniel/array.smt2 ...
sat
(model
  (define-fun array () (Array Int Real) (store ((as const (Array Int Real)) (/ 11 10)) 4 (/ 1 10)))
)

Is this something that could be fixed for the latest princess version?

[daniel-raffler]

The crash occurs when the array is first created, and it can also be triggered through the API:

import ap.SimpleAPI
import ap.theories.arrays.{ExtArray}
import ap.theories.rationals.Rationals.dom
import ap.types.Sort
import org.scalatest.funsuite.AnyFunSuite

class RationalArrays extends AnyFunSuite {
  test("Array(Int, Int)") {
    SimpleAPI.withProver(enableAssert = true) { p =>
      var array = ExtArray(Seq(Sort.Integer), Sort.Integer)
    }
  }

  test("Array(Int, Real)") {
    SimpleAPI.withProver(enableAssert = true) { p =>
      var array = ExtArray(Seq(Sort.Integer), dom)
    }
  }

  test("Array(Real, Int)") {
    SimpleAPI.withProver(enableAssert = true) { p =>
      var array = ExtArray(Seq(dom), Sort.Integer)
    }
  }

  test("Array(Real, Real)") {
    SimpleAPI.withProver(enableAssert = true) { p =>
      var array = ExtArray(Seq(dom), dom)
    }
  }
}

Here everything except test("Array(Int, Int)") crashes for me. The stacktrace looks like this:

Universal quantifiers over fractions/rationals are currently not supported
java.lang.Exception: Universal quantifiers over fractions/rationals are currently not supported
	at ap.theories.rationals.Fractions$IncompletenessChecker$.postVisit(Fractions.scala:336)
	at ap.theories.rationals.Fractions$IncompletenessChecker$.postVisit(Fractions.scala:325)
	at ap.parser.CollectingVisitor.visitWithoutResult(InputAbsyVisitor.scala:190)
	at ap.theories.rationals.Fractions.iPreprocess(Fractions.scala:279)
	at ap.theories.Theory$.$anonfun$iPreprocess$1(Theory.scala:135)
	at scala.collection.immutable.List.foldRight(List.scala:353)
	at scala.collection.IterableOnceOps.$colon$bslash(IterableOnce.scala:761)
	at scala.collection.IterableOnceOps.$colon$bslash$(IterableOnce.scala:761)
	at scala.collection.AbstractIterable.$colon$bslash(Iterable.scala:935)
	at ap.theories.Theory$.iPreprocess(Theory.scala:135)
	at ap.parser.Preprocessing$.$anonfun$apply$3(Preprocessing.scala:99)
	at scala.collection.immutable.List.map(List.scala:247)
	at ap.parser.Preprocessing$.apply(Preprocessing.scala:98)
	at ap.theories.Theory$.genAxioms(Theory.scala:101)
	at ap.theories.arrays.ExtArray.<init>(ExtArray.scala:610)
	at ap.theories.arrays.ExtArray$.$anonfun$apply$1(ExtArray.scala:74)
	at scala.collection.mutable.HashMap.getOrElseUpdate(HashMap.scala:469)
	at ap.theories.arrays.ExtArray$.apply(ExtArray.scala:74)
	at RationalArrays.$anonfun$new$4(RationalArrays.scala:16)
	at RationalArrays.$anonfun$new$4$adapted(RationalArrays.scala:15)
	at ap.api.SimpleAPI$.withProver(SimpleAPI.scala:178)
	at RationalArrays.$anonfun$new$3(RationalArrays.scala:15)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
	at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
	at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
	at org.scalatest.Transformer.apply(Transformer.scala:22)
	at org.scalatest.Transformer.apply(Transformer.scala:20)
	at org.scalatest.funsuite.AnyFunSuiteLike$$anon$1.apply(AnyFunSuiteLike.scala:226)
	at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
	at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
	at org.scalatest.funsuite.AnyFunSuite.withFixture(AnyFunSuite.scala:1564)
	at org.scalatest.funsuite.AnyFunSuiteLike.invokeWithFixture$1(AnyFunSuiteLike.scala:224)
	at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$runTest$1(AnyFunSuiteLike.scala:236)
	at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTest(AnyFunSuiteLike.scala:236)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTest$(AnyFunSuiteLike.scala:218)
	at org.scalatest.funsuite.AnyFunSuite.runTest(AnyFunSuite.scala:1564)
	at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$runTests$1(AnyFunSuiteLike.scala:269)
	at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
	at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
	at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTests(AnyFunSuiteLike.scala:269)
	at org.scalatest.funsuite.AnyFunSuiteLike.runTests$(AnyFunSuiteLike.scala:268)
	at org.scalatest.funsuite.AnyFunSuite.runTests(AnyFunSuite.scala:1564)
	at org.scalatest.Suite.run(Suite.scala:1114)
	at org.scalatest.Suite.run$(Suite.scala:1096)
	at org.scalatest.funsuite.AnyFunSuite.org$scalatest$funsuite$AnyFunSuiteLike$$super$run(AnyFunSuite.scala:1564)
	at org.scalatest.funsuite.AnyFunSuiteLike.$anonfun$run$1(AnyFunSuiteLike.scala:273)
	at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
	at org.scalatest.funsuite.AnyFunSuiteLike.run(AnyFunSuiteLike.scala:273)
	at org.scalatest.funsuite.AnyFunSuiteLike.run$(AnyFunSuiteLike.scala:272)
	at org.scalatest.funsuite.AnyFunSuite.run(AnyFunSuite.scala:1564)
	at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:47)
	at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1321)
	at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1315)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1315)
	at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:992)
	at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:970)
	at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1481)
	at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:970)
	at org.scalatest.tools.Runner$.run(Runner.scala:798)
	at org.scalatest.tools.Runner.run(Runner.scala)
	at org.jetbrains.plugins.scala.testingSupport.scalaTest.ScalaTestRunner.runScalaTest2or3(ScalaTestRunner.java:43)
	at org.jetbrains.plugins.scala.testingSupport.scalaTest.ScalaTestRunner.main(ScalaTestRunner.java:26)

[pruemmer]

Our checks were a bit too strict here. In the latest commit, this should work again!

[daniel-raffler]

Thanks! It's working for me now.