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

[kfriedberger]

The JavaSMT developers are currently trying to improve their support for Rational theory with the SMT solver Princess (see sosy-lab/java-smt#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 😢 , 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.

[kfriedberger]

Are there any news on that issue?

[pruemmer]

This should be fixed on the master now.