Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Opensmt rejects non-linear integer arithmetic too eagerly #655

Open
aehyvari opened this issue Dec 18, 2023 · 2 comments · May be fixed by #790
Open

Opensmt rejects non-linear integer arithmetic too eagerly #655

aehyvari opened this issue Dec 18, 2023 · 2 comments · May be fixed by #790
Assignees
@BritikovKI

Comments

@aehyvari
Copy link
Member

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
Copy link
Member

blishko commented Dec 22, 2023

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
Copy link
Member

blishko commented Oct 18, 2024

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.

@blishko blishko pinned this issue Oct 18, 2024
@BritikovKI BritikovKI linked a pull request Nov 4, 2024 that will close this issue
Nonlin LA preds #790
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@BritikovKI BritikovKI

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Nonlin LA preds usi-verification-and-security/opensmt
3 participants
@aehyvari @blishko @BritikovKI