search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

Fixes several model printing bugs (and more) #584

Closed quickbeam123 closed 1 week ago

quickbeam123 commented 1 month ago

Quite a few changes in FiniteModelBuilder and around with the ultimate aim of Vampire being able to correctly model-check all finite models it generates.

This PR achieves this goal for inputs in CNF and under fde=none:erd=off:updr=off:bce=off - (This means we verify models we output, but so far only for strategies which don't manipulate the signature or eliminate things.)

The next step will be to support undoing these elimination operations and making the model work for the original input (and to do the corresponding operations also for saturations, where we will simply dump the definitions of the eliminated symbols to document how one could recover a model, if they had one.)

MichaelRawson commented 1 month ago

I've mostly just asked for some explanatory comments...once you've done what you are willing to do go ahead and merge.