java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Published 20 hours ago • verified publisher icon sosy-lab

Declare a new Sort with JavaSMT

Open ghost opened this issue 2 years ago • 2 comments

hello, is it possible with javaSMT to declare a new Sort like in SMTLIB ? for example : (declare-sort Auto 0)

ghost avatar Jun 24 '22 20:06 ghost

No. JavaSMT does currently not support user-defined sorts.

UPDATE: see below,

kfriedberger avatar Jun 25 '22 08:06 kfriedberger

We support enumeration sort (bounded domain sort) since #303.

More generic datatype sorts (like simple tuples or more advanced structures like lists and trees) are not yet supported, because of:

  • low priority and missing demand.
  • model evaluation and presentation is unclear.
  • representation of operators is unclear.

kfriedberger avatar Nov 26 '23 11:11 kfriedberger