Model evaluation for rational theory is incomplete and does not simplify terms

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:

(declare-fun x () Real) (assert (= x 2)) (check-sat) // --> SAT (evaluate-model (+ 2 x)) // --> no result available :cry: , expected result would be 4

Code / Junit test:

Comparing Integer and Rational theory shows that the model evaluation for Integer theory is more advanced than Rational theory.

  private SimpleAPI api;

  @Before
  public void init() {
    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 testIntegerEvaluation() {
    ITerm num2 = new IIntLit(IdealInt.apply(2));
    ITerm x = api.createConstant("x", Sort.Integer$.MODULE$);
    IFormula eq = num2.$eq$eq$eq(x);
    api.addAssertion(eq);
    Value result = api.checkSat(true); // --> SAT
    PartialModel model = api.partialModel();
    Option<IExpression> eval = model.evalExpression(num2.$plus(x));
    System.out.println(eval); // -> Some(4) :-) GOOD BEHAVIOUR
  }

  @Test
  public void testRationalEvaluation() {
    ITerm num2 = Rationals$.MODULE$.int2ring(new IIntLit(IdealInt.apply(2)));
    ITerm x = api.createConstant("x", Rationals$.MODULE$.dom());
    IFormula eq = num2.$eq$eq$eq(x);
    api.addAssertion(eq);
    Value result = api.checkSat(true); // --> SAT
    PartialModel model = api.partialModel();
    Option<IExpression> eval = model.evalExpression(num2.$plus(x));
    System.out.println(eval); // -> None :-( BAD BEHAVIOUR
  }

Wanted behaviour:

Princess should also provide a model evaluation and term simplification for Rational theory, such that the result from above is available.

uuverifiers / princess