You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
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.
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:
We want to evaluate a rational division in a model, completely unrelated to any pushed assertions.
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:
Stacktrace:
The term
(/ x 2)
that is used for the model evaluation can be printed asEPS 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?
The text was updated successfully, but these errors were encountered: