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.

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

VAMPIRE: Fix lower bound structure #31

Open
ArenBabikian opened this issue Apr 1, 2019 · 3 comments
Open

VAMPIRE: Fix lower bound structure #31

ArenBabikian opened this issue Apr 1, 2019 · 3 comments
Assignees

Comments

@ArenBabikian
Copy link
Collaborator

No description provided.

@ArenBabikian
Copy link
Collaborator Author

ArenBabikian commented Apr 4, 2019

Mentioning a constant (ex. o1) in the input file triggers the solver to necessarily create it as a node in the generated finite model. This is problematic because currently, we are mentioning the list of constants for the scope minimum and maximum (ex. MinScope = (object <=> o1..o3), MaxSope = (object <=>o1..o6) ).
In this example, the solver will attempt to find finite models with 6 nodes because 6 constants are mentioned. These nodes may not all be objects because the scope minimum and maximum formula structure is logically correct, however, if the solver cannot handle finite models with 6 nodes (ex. timeout or memory limit reached), then no models at all will be generated.

@ArenBabikian
Copy link
Collaborator Author

The solution to this issue may rely in tweaking the solver itself (ex. through command line parameters, maybe).

@ArenBabikian
Copy link
Collaborator Author

A possibility would be to introduce model elements as skolem constants.

ArenBabikian added a commit that referenced this issue Jun 8, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant