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
In presence of the flag, the custom statements maximize, minimize and get-objectives should be available as SMT-LIB statements and Alt-Ergo may perform extra works to fulfill these objectives. In the current implementation, the FunSAT solver doesn't support optimization and we don't plan to support it in future. Thus, in the presence of --optimize, the binary should select the CDCL-Tableaux solver and produce a warning in presence of --sat-solver Tableaux or --sat-solver Tableaux-CDCL options.
In absence of the flag, the name maximize and minimize are not reserved and get-objectives should produce a SMT-LIB error.
The text was updated successfully, but these errors were encountered:
This flag should behave as follow:
maximize
,minimize
andget-objectives
should be available as SMT-LIB statements and Alt-Ergo may perform extra works to fulfill these objectives. In the current implementation, theFunSAT
solver doesn't support optimization and we don't plan to support it in future. Thus, in the presence of--optimize
, the binary should select theCDCL-Tableaux
solver and produce a warning in presence of--sat-solver Tableaux
or--sat-solver Tableaux-CDCL
options.maximize
andminimize
are not reserved andget-objectives
should produce a SMT-LIB error.The text was updated successfully, but these errors were encountered: