Model evaluation for rational theory crashes in MatchError

[kfriedberger]

The JavaSMT developers are currently trying to improve their support for Rational theory with the SMT solver Princess (see https://github.com/sosy-lab/java-smt/pull/257). There are some smaller issues in Princess (version 2023-06-19) that block us from a good integration.

The following issue appeared in model evaluation:

Description:

We want to evaluate a rational division in a model, completely unrelated to any pushed assertions.

(declare-fun x () Real)
(assert (true))
(check-sat) // --> SAT
(evaluate-model (/ x 2)) 

The division in the last line is a rational division, not the integer-based one. The result is not relevant for us and can be any arbitrary value, except a crashing program :-)

Code / Junit test:

  private SimpleAPI api;

  @Before
  public void init() {
    Debug.enableAllAssertions(true);
    api = SimpleAPI.apply(
        SimpleAPI.apply$default$1(),
        SimpleAPI.apply$default$2(),
        SimpleAPI.apply$default$3(),
        SimpleAPI.apply$default$4(),
        SimpleAPI.apply$default$5(),
        SimpleAPI.apply$default$6(),
        SimpleAPI.apply$default$7(),
        SimpleAPI.apply$default$8(),
        SimpleAPI.apply$default$9(),
        SimpleAPI.apply$default$10(),
        SimpleAPI.apply$default$11()
    );
  }

  @Test
  public void testRationalEvaluation2() {
    ITerm num2 = Rationals$.MODULE$.int2ring(new IIntLit(IdealInt.apply(2)));
    ITerm x = api.createConstant("x", Rationals$.MODULE$.dom());
    Value result = api.checkSat(true); // --> we have not added any constraints, so this is SAT
    PartialModel model = api.partialModel();
    Option<IExpression> eval = model.evalExpression(Rationals$.MODULE$.div(x, num2)); // --> CRASH
    System.out.println(eval); // -> Some(0) would be nice to receive
  }
}

Stacktrace:

scala.MatchError: _0 (of class ap.parser.ISortedVariable)
	at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:134)
	at ap.api.PartialModel$Evaluator$.postVisit(PartialModel.scala:114)
	at ap.parser.CollectingVisitor.visit(InputAbsyVisitor.scala:169)
	at ap.api.PartialModel$Evaluator$.apply(PartialModel.scala:116)
	at ap.api.PartialModel.evalExpression(PartialModel.scala:59)
	at ... <insert code position from above>

The term (/ x 2) that is used for the model evaluation can be printed as EPS Rat. EX (((Rat_denom = _0) & ((_0 + -1) >= 0)) & (mul(_0, _1[Rat]) = mul(x, Rat_frac(1, 2)))). I assume that the symbol _0 comes from this notation.

@pruemmer Could you take a look?

[daniel-raffler]

This actually seems to be the Rational version of https://github.com/uuverifiers/princess/issues/17. Here the Epsilon term is created indirectly by the division:

  
  test("epsilon rational") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import ap.theories.rationals.Rationals._
      import p._;

      val x = createConstant("x", dom)
      val f = div(x, int(2))

      // We now have:
      // f = EPS Rat. EX (((Rat_denom = _0) & ((_0 + -1) >= 0)) & (mul(_0, _1[Rat]) = mul(x, Rat_frac(1, 2))))

      checkSat(true)
      assertResult(1: ITerm)(partialModel.evalToTerm(f))
    }
  }

[kfriedberger]

Are there any news on that issue?

[pruemmer]

I had some time over Christmas to rework the solver for rational numbers; does this problem still occur when using the latest master?

[daniel-raffler]

Thanks, this solved the issue!