search

usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Opensmt rejects non-linear integer arithmetic too eagerly #655

Open aehyvari opened 11 months ago

aehyvari commented 11 months ago

Opensmt throws a LANonLinearException on this instance. It'd be nice if it didn't. Maybe we should somehow tell ArithLogic when it is parsing a define-fun to ignore the nonlinearities.

(set-logic QF_LIA)
(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
(assert (= (uninterp_mul 1 2)))
(check-sat)
(exit)
blishko commented 11 months ago

I think this is not going to be easy in the current implementation. The code of ArithLogic assumes we do not create nonlinear expressions.

I see two ways forward here, both of which would be good to have, eventually. One is a change in the frontend, which would use a new term data structure that would follow closely the term grammar of SMT-LIB, and we would translate that to PTRef during some internalization process. Second change is to actually start supporting nonlinear arithmetic, at least in the term representation.

blishko commented 1 month ago

We talked with @BritikovKI about this and I think we should start supporting nonlinear arithmetic expressions inArithLogic. It would be a good step towards nonlinear arithmetic solver.