Add real to int conversions #614
Conversation
|
@shaobo-he Thanks for the contribution. Before accepting this PR, we need to add the new operator also to all other solvers supporting QF_LIRA (mathsat, CVC4 and yices), otherwise the tests will fail. (note that in your test you specified UFLIRA, instead, you should specify QF_LIRA to target the right fragment and enable all relevant solvers). Also, other changes are needed, particularly adding examples of RealToInt in tests/examples.py and adding the walk_realtoint to all the walkers (simplifier, rewritings and oracles). Are you willing to continue the work in this direction? We can of course help you and guide you in this. |
pysmt/test/test_lira.py
Outdated
| Equals(RealToInt(Real(1)), Int(1))) | ||
| check = And(check, | ||
| Equals(RealToInt(ToReal(b)), b)) | ||
| for sname in get_env().factory.all_solvers(logic=UFLIRA): |
There was a problem hiding this comment.
the logic here should be 'QF_LIRA' to enable all the relevant solvers.
There was a problem hiding this comment.
It seems QF_LIRA is not defined in pysmt.logics. Should I define it?
|
Another minor point: |
|
How about me making as many changes as I can and then you can take over to finish it if necessary? Hopefully you don't have to do a lot. |
Specifically, three operations are added, RealToInt -- The SMT `to_int` function Ceiling -- Equivalent to the Racket `ceiling` function Truncate -- Equivalent to the Racket `truncate` function
|
Hi, @mikand. I updated this PR. Please take a look at it again and let me know if it needs any changes. |
|
Hi @shaobo-he, thanks for this work and sorry for the latency! I am unconvinced of the addition of UF_NIRA though: UF_NIRA also contains non-linear terms and mod operators (http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_NIA) that are currently not supported, so I am not comfortable in adding the theory to z3 just for the sake of having the Floor operator implemented. Also, note that the logic addition code is incomplete: you also need to extend the TheoryOracle in oracles.py to produce non-linearity when it encounters a Floor. Let me think a bit more on this, but maybe the right way to proceed is to add the mod operator together with the floor to fulfill the requirements of QF_NIA and have a clean implementation of the whole logic? @marcogario any comment or feedback is welcome. |
|
Thank you for your feedback.
So the changes in https://github.com/pysmt/pysmt/pull/614/files#diff-03f2e786a2b9045a041adfab13dde3a5R244-R249 are not enough? Could you give me some pointers about what should I do here? |
|
Hello, @mikand. I'm sorry to bother you again. I was wondering if there's any feedback or decision on this PR. I'd like to see this PR merged so that I can start to work on adding operations of floating-point theory otherwise there'll be conflicts. |
| def walk_realtoint(self, formula, args, **kwargs): | ||
| #pylint: disable=unused-argument | ||
| """Extends the Theory with NIRA.""" | ||
| theory_out = args[0].set_nira() # This makes a copy of args[0] |
There was a problem hiding this comment.
This seems problematic. The output should extend the input with nonlinearity as well as integer arithmetic.
Specifically, three operations are added,
RealToInt -- The SMT
to_intfunctionCeiling -- Equivalent to the Racket
ceilingfunctionTruncate -- Equivalent to the Racket
truncatefunction