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

Not_found exception while printing models #854

Closed
bclement-ocp opened this issue Oct 3, 2023 · 0 comments · Fixed by #855
Closed

Not_found exception while printing models #854

bclement-ocp opened this issue Oct 3, 2023 · 0 comments · Fixed by #855
Assignees
@bclement-ocp
Labels
bug models This issue is related to model generation.

Comments

@bclement-ocp
Copy link
Collaborator 

$ alt-ergo --produce-models unexpected_Not_found.smt2
; File "unexpected_Not_found.smt2", line 20, characters 1-12: I don't know (0.0277) (4 steps) (goal g_1)

unknown
(
  (define-fun intrefqtmk ((arg_0 Int)) intref Fatal error: exception Not_found
$ cat unexpected_Not_found.smt2
(set-logic ALL)
(set-info :smt-lib-version 2.6)
(declare-sort intref 0)
(declare-fun intrefqtmk (Int) intref)
(declare-fun a () Int)
(define-fun aqtunused () intref (intrefqtmk a))
(declare-fun a1 () Int)
(assert (not (and (<= 5 a1) (<= a1 15))))
(check-sat)
(get-model)

Initially reported by Claude Marché using Alt-Ergo 2.5.1, still present in next currently
@bclement-ocp bclement-ocp added bug models This issue is related to model generation. labels Oct 3, 2023
@bclement-ocp bclement-ocp self-assigned this Oct 3, 2023
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Oct 3, 2023
@bclement-ocp
Treat missing values in models as abstract
8a436c3 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

Fixes OCamlPro#854
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Oct 3, 2023
@bclement-ocp
Treat missing values in models as abstract
8b3d668 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

Note that this bug affects version 2.5.1, and we changed the way
abstract values are printed since the release. The patch is written to
be easy to backport.

Fixes OCamlPro#854
@bclement-ocp bclement-ocp mentioned this issue Oct 3, 2023
Merged
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Oct 3, 2023
@bclement-ocp
Treat missing values in models as abstract
58ae06c 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

This is backported from 8b3d668 for branch 2.5.x.

Fixes OCamlPro#854
bclement-ocp added a commit that referenced this issue Oct 4, 2023
@bclement-ocp
Treat missing values in models as abstract (#855)
a0575d2 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

Note that this bug affects version 2.5.1, and we changed the way
abstract values are printed since the release. The patch is written to
be easy to backport.

Fixes #854
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Oct 4, 2023
@bclement-ocp
Treat missing values in models as abstract
f0fbede 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

This is backported from a0575d2 for branch 2.5.x.

Fixes OCamlPro#854
@bclement-ocp bclement-ocp mentioned this issue Oct 4, 2023
Merged
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Oct 4, 2023
@bclement-ocp
Treat missing values in models as abstract
4d1b51d 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

This is backported from a0575d2 for branch 2.5.x.

Fixes OCamlPro#854
Halbaroth pushed a commit that referenced this issue Oct 4, 2023
@bclement-ocp
Treat missing values in models as abstract (#860)
ec74b44 
When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

This is backported from a0575d2 for branch 2.5.x.

Fixes #854
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bclement-ocp bclement-ocp

Labels
bug models This issue is related to model generation.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Treat missing values in models as abstract bclement-ocp/alt-ergo
1 participant
@bclement-ocp