Smtlib mode mechanism #971

Stevendeo · 2023-11-23T16:35:01Z

As discussed in #936 , there is currently no mechanism to check whether an option can be updated or not given the analysis context. The standard describes the different configuration in which each option can be updated or not, and even more.

This PR adds a mode mechanism and implements a check on different instructions (set-logic, set-option, etc.).

bclement-ocp

Looks reasonable; the tests for calling (get-model) before (check-sat) should not be removed.

bclement-ocp · 2023-11-24T07:46:41Z

tests/cram.t/run.t

  (error "Model generation disabled (try --produce-models)")

 The messages above mention `--produce-models`, but we can also use
 `set-option`.

-  $ echo '(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 --continue-on-error


Hm, these should have been broken since the switch to Dolmen as default frontend, are they skipped somehow?

Anyways, this is no longer the same test as before, and the existing test (adding (set-logic)) should still be valid. This is also true for the next test below; please do not remove them.

are they skipped

No they are not skipped, they just result in an error; why do you think they should have been broken?

the existing test (adding (set-logic)) should still be valid

I am not sure which test you are referring to. (set-logic ALL)(get-model) is invalid, as (get-model) can only be called in Sat mode which happens after a check-sat; or did I miss something?

Or are you saying we want this test to show that alt-ergo will fail on bad smt files? This sounds relevant.

No they are not skipped, they just result in an error; why do you think they should have been broken?

I thought that (get-model) would have returned an error about set-logic not being present rather than an error about the model not being here, but it looks like Dolmen does not complain about a missing set-logic for get-model.

Or are you saying we want this test to show that alt-ergo will fail on bad smt files? This sounds relevant.

Yes, that was what the test was doing (although the error was different; it was "No model produced" and now it should be "Invalid command in start mode").

(Now thinking that we should probably also have a test for (set-logic ALL)(assert false)(check-sat)(get-model) for the "No model produced" error, I don't think we have that one)

I thought that (get-model) would have returned an error about set-logic not being present rather than an error about the model not being here, but it looks like Dolmen does not complain about a missing set-logic for get-model.

Not by default indeed. The situation is that, the dolmen functions to typecheck things would raise a missing set-logic error if called, but in the case of get-model, nothing needs to be typed. For that, dolmen has a Flow module, whose role is to check that the statements respect the smtlib constraints, see Gbury/dolmen#135

Ah! Interesting! I thought for a moment that we could maybe use that in this PR, but it looks like it is not designed to be extensible — it doesn't look like we can access the current mode from the state, or otherwise configure custom mode-specific filters (e.g. for custom options that can only be set in start mode), is that correct?

That's correct currently, but I'd accept a PR to make it extensible.

OK. I think if Dolmen already had everything we needed it would have made sense to use that, but given that we would need to modify the Flow module to suit our needs and that we have an already working implementation inside Alt-Ergo in this PR, I am fine with either solution.

(Now thinking that we should probably also have a test for (set-logic ALL)(assert false)(check-sat)(get-model) for the "No model produced" error, I don't think we have that one)

This would return a different error: after check-sat we would be in Unsat mode, which is an invalid mode for get-model

Another error is fine; what I meant is that this is a common scenario that should fail and that (I believe) we don't test.

bclement-ocp · 2023-11-24T07:54:05Z

src/lib/frontend/d_state_option.ml

@@ -106,6 +133,6 @@ let options_requiring_initialization = [

 let init st =
  List.fold_left
-    (fun st (module S : S) -> S.reset st)
+    (fun st (module S : S) -> S.set (S.get (S.reset st)) st)


Nit: set (get (reset x)) is confusing to read. Maybe reset should be called clear?

src/bin/common/solving_loop.ml

bclement-ocp

Please restore the tests for the "No model produced" error that you removed, as I asked in the previous round of review.

Stevendeo · 2023-11-27T10:50:48Z

Please restore the tests for the "No model produced" error that you removed, as I asked in the previous round of review.

For some reason my comments were pending; you should see them now

bclement-ocp · 2023-11-27T11:04:27Z

tests/smtlib/testfile-steps-bound1.dolmen.err.expected

@@ -0,0 +1 @@
+(error "Invalid action during mode Util.Assert: Set option steps_bound")


"mode Util.Assert" is not very nice; if that's what @@deriving show does we should write our own printer instead.

bclement-ocp

LGTM; just two small typos I missed on first read.

src/bin/common/solving_loop.ml

src/lib/structures/errors.ml

Co-authored-by: Basile Clément <[email protected]>

CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)

Stevendeo requested review from bclement-ocp, Halbaroth and hra687261 and removed request for bclement-ocp and Halbaroth November 23, 2023 16:36

bclement-ocp requested changes Nov 24, 2023

View reviewed changes

Stevendeo force-pushed the immutable-options branch from 4d7dc46 to 145fef2 Compare November 24, 2023 09:16

Stevendeo requested a review from bclement-ocp November 24, 2023 09:37

bclement-ocp requested changes Nov 24, 2023

View reviewed changes

Stevendeo force-pushed the immutable-options branch from 2200443 to d14ddf7 Compare November 27, 2023 10:56

bclement-ocp reviewed Nov 27, 2023

View reviewed changes

Stevendeo requested a review from bclement-ocp November 27, 2023 14:58

bclement-ocp approved these changes Nov 27, 2023

View reviewed changes

src/bin/common/solving_loop.ml Outdated Show resolved Hide resolved

src/lib/structures/errors.ml Outdated Show resolved Hide resolved

Stevendeo force-pushed the immutable-options branch from be59a8d to c3493ef Compare November 28, 2023 12:55

Stevendeo and others added 13 commits November 28, 2023 14:35

SAT Mode manager

8577adb

Update modes in solving_loop

53fa605

Restricting instruction invocation to their specific modes

ddb4216

Relaxing when not in SMTLIB2

5d6e1fe

Update tests

9a4d5ab

Rebase artifact

4427014

Update tests

1dbf420

Poetry

ca70715

Update src/bin/common/solving_loop.ml

22d1636

Co-authored-by: Basile Clément <[email protected]>

Reset to clear

b794900

Update tests

3c85785

Poetry

c086f7f

Update tests

e2b428e

Stevendeo and others added 2 commits November 28, 2023 14:35

Apply suggestions from code review

6cc3f7e

Co-authored-by: Basile Clément <[email protected]>

Update tests

fe9e4a4

Stevendeo force-pushed the immutable-options branch from 5259187 to fe9e4a4 Compare November 28, 2023 13:35

Halbaroth enabled auto-merge (squash) November 28, 2023 13:39

Halbaroth merged commit 7bddee4 into OCamlPro:next Nov 28, 2023
14 checks passed

bclement-ocp mentioned this pull request Sep 24, 2024

[new release] alt-ergo (4 packages) (2.6.0) ocaml/opam-repository#26609

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Smtlib mode mechanism #971

Smtlib mode mechanism #971

Stevendeo commented Nov 23, 2023

bclement-ocp left a comment

bclement-ocp Nov 24, 2023

Stevendeo Nov 24, 2023

Stevendeo Nov 24, 2023

bclement-ocp Nov 27, 2023

Gbury Nov 27, 2023

bclement-ocp Nov 27, 2023

Gbury Nov 27, 2023

bclement-ocp Nov 27, 2023

Stevendeo Nov 27, 2023

bclement-ocp Nov 27, 2023

bclement-ocp Nov 24, 2023

bclement-ocp left a comment

Stevendeo commented Nov 27, 2023

bclement-ocp Nov 27, 2023

bclement-ocp left a comment

		@@ -0,0 +1 @@
		(error "Invalid action during mode Util.Assert: Set option steps_bound")

Smtlib mode mechanism #971

Smtlib mode mechanism #971

Conversation

Stevendeo commented Nov 23, 2023

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

Stevendeo commented Nov 27, 2023

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment