search

ths-rwth / smtrat

http://smtrat.github.io/
Other
52 stars 13 forks source link

Support for mod in QF_NIA #3

Open Heizmann opened 8 years ago

Heizmann commented 8 years ago

I just applied to most recent version 8dd6e395ee125d6c95f86a70ba9a1b65b9a22516 of smtrat to the attached script and obtained the following error message.

ERROR smtrat.parser: Failed to call "mod" with arguments [2: v_~a102_3_const_-1782958188*v_~a16_3_const_1604997482, 14999]:
        Arithmetic: mod should be called with a variable as first argument.
        Bitvector: Invalid operator "mod".
        Core: Arguments are expected to be formulas, but argument 1 is not: "v_~a102_3_const_-1782958188*v_~a16_3_const_1604997482".
        Uninterpreted: Invalid operator "mod".
Heizmann commented 2 years ago

Many thanks! I did not yet try your new tool, but I probably will. It seems that NIA logics become more and more important for us.

derjasper commented 2 years ago

It seems that this issue has been closed wrongly. Sorry for the confusion!

We still do not support mod yet.

Heizmann commented 2 years ago

Oh no, that's a pity! For checking satisfiabilty, you could support (mod a b) by replacing this term internally with a fresh constant symbol x_remainder and asserting additionally a=x_divisor*b+x_remainder ∧ 0<=x_remainder ∧x_remainder<b where x_divisor is also a fresh constant symbol.

I am however familiar with the problem that people that don't know the architecture of our tool tell me that I could support xyz very easily. ;-)