You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We rely on specific SMT Solvers to parse and dump SMT2 formulas. Some solvers don't offer these API calls, while those that do print formulas arbitrarily for dump calls. Additionally, some solvers (e.g. Vampire) can only be used via SMT2 files.
Having a solver-independent String SMT2 parser that translates SMT2 files into their respective API calls for all supporting SMT solvers would allow us more freedom when choosing a solver.
Similarly, supporting solver-independent composing of SMT2 formulas allows us to easily share generated SMT2 files/Strings, even with solvers that don't offer an API.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
We rely on specific SMT Solvers to parse and dump SMT2 formulas. Some solvers don't offer these API calls, while those that do print formulas arbitrarily for dump calls. Additionally, some solvers (e.g. Vampire) can only be used via SMT2 files.
Having a solver-independent String SMT2 parser that translates SMT2 files into their respective API calls for all supporting SMT solvers would allow us more freedom when choosing a solver.
Similarly, supporting solver-independent composing of SMT2 formulas allows us to easily share generated SMT2 files/Strings, even with solvers that don't offer an API.
Beta Was this translation helpful? Give feedback.
All reactions