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

NRA completeness regression (diverges with logic set) #292

Closed
maurobringolf opened this issue Aug 27, 2021 · 0 comments · Fixed by cvc5/cvc5#8233
Closed

NRA completeness regression (diverges with logic set) #292

maurobringolf opened this issue Aug 27, 2021 · 0 comments · Fixed by cvc5/cvc5#8233
Assignees
@ajreynol
Labels
performance
Projects
Non-linear Arithmetic Challenge Problems

Comments

@maurobringolf
Copy link

Commit: 1639655ca7b8f0f18145fdbb515253810b119d08

Another small NRA regression, decidable by --sygus-inst but not by forcing the logic. Possibly related to https://github.com/cvc5/cvc5/issues/6798.

$ cvc5 -q unknown.smt2
unknown
$ cvc5 -q --sygus-inst unknown.smt2
sat
$ cvc4-1.8 -q unknown.smt2
sat
$ time cvc5 --force-logic=NRA unknown.smt2
^Ccvc5 interrupted by user.
real    1m7.944s
user    1m7.907s
sys     0m0.020s
$ cat unknown.smt2
(declare-const x Real)
(declare-const u Real)
(declare-const v Real)
(assert (exists ((t Real)) (and (>= x (- 1.0)) (not (or (< t 0.0) (= t (* u t v)))))))
(check-sat)
@ajreynol ajreynol self-assigned this Sep 30, 2021
@ajreynol ajreynol transferred this issue from cvc5/cvc5 Oct 15, 2021
@ajreynol ajreynol mentioned this issue Mar 4, 2022
Merged
Non-linear Arithmetic Challenge Problems automation moved this from To do to Done Mar 5, 2022
nafur pushed a commit to cvc5/cvc5 that referenced this issue Mar 5, 2022
@ajreynol
Enable NL tangent planes by default (#8233)
e099e59 
Fixes cvc5/cvc5-projects#215
Fixes cvc5/cvc5-projects#291
Fixes cvc5/cvc5-projects#292
Fixes cvc5/cvc5-projects#294
Fixes cvc5/cvc5-projects#297

Previously the concern was that this would interfere with e.g. quantifiers + non-linear. However, our strategy is now fair wrt other theories as we send lemmas at LAST_CALL effort, and is properly restricted by the nl-ext mode.

Moreover, this option increases our ability to solve problems (instead of saying "unknown") significantly, even for quantified logics like UFNIA.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ajreynol ajreynol

Labels
performance
Projects
Non-linear Arithmetic Challenge Problems
Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Enable NL tangent planes by default ajreynol/CVC4
2 participants
@ajreynol @maurobringolf