uuverifiers
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.
