No undefined symbols in finite models.

[MichaelRawson]

Refer to GEG001+1. When producing a finite model, we report that some atoms are 'undefined in model', which I assume is a SAT/SMT don't-care. Geoff asks what this means, so I guess we should read the spec and work out what we're supposed to do with these: just pick an arbitrary value?

[easychair]

Choose a designated constant in the finite model, call it geoff, and say the value is geoff instead of "undefined". If the model does not have don't care elements, don't use geoff. I am sure there will be no more questions :) Andrei

…

On Wed, 16 Aug 2023 at 15:20, Michael Rawson ***@***.***> wrote: Refer to GEG001+1 <https://www.tptp.org/CASC/29/WWWFiles/Results/FNQ/Vampire-SAT---4.8/GEG001+1>. When producing a finite model, we report that some atoms are 'undefined in model', which I assume is a SAT/SMT don't-care. Geoff asks what this means, so I guess we should read the spec and work out what we're supposed to do with these: just pick an arbitrary value? — Reply to this email directly, view it on GitHub <#477>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BNZ3DCAYHZBSUVCCETXVTCLJANCNFSM6AAAAAA3SRBIXY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>