Model generation support for SatML #829

Halbaroth · 2023-09-21T08:54:29Z

This PR includes two things:

A refactoring of the way AE prints models.
A support of the model generation for SatML.
I cannot separate them as the support for model generation in SatML has been done after the refactoring in the OptimAE branch.

IMPORTANT: This PR has to been merged before OptimAE.

I also disable some tests as the printers change a bit but the models (with FunSAT) are still valid. I am preparing another PR rebase on this one that fix printers and test the support of model generation with SatML.

bclement-ocp · 2023-09-21T09:34:05Z

Thanks for splitting the PR up — I will take a look at this one in the afternoon.

(We could split up further by merging the refactoring first as well — but this is at a size and scope that is manageable on its own now I think)

src/lib/frontend/frontend.ml

src/lib/frontend/models.ml

src/lib/frontend/models.mli

src/lib/util/printer.ml

src/lib/reasoners/fun_sat.ml

bclement-ocp

There are a couple minor cleanups to do, and some other things we may want to change later (e.g. the use of a reference for the last env), but I think we should merge with only the minor cleanups for now so that we can move on.

src/bin/common/solving_loop.ml

src/lib/frontend/frontend.ml

src/lib/frontend/models.ml

src/lib/frontend/models.mli

src/lib/reasoners/satml_frontend.ml

src/lib/reasoners/satml.ml

src/lib/reasoners/theory.mli

src/lib/util/printer.ml

src/lib/frontend/models.mli

Halbaroth · 2023-09-22T13:04:27Z

There are a couple minor cleanups to do, and some other things we may want to change later (e.g. the use of a reference for the last env), but I think we should merge with only the minor cleanups for now so that we can move on.

Seems good to mean as we have another PR to fix and test the feature #832

Halbaroth · 2023-09-25T09:58:13Z

I think we can merge this PR. The PR #832 fixes almost everything but we have to merge #836 and #835 in order to pass the CI on it.

bclement-ocp · 2023-09-25T10:15:14Z

Is #836 really needed? PROXY variables shouldn't end up in models, unless I am mistaken.

If #832 is ready and working we should merge #832 into this PR, then merge both into next at once.

Halbaroth · 2023-09-25T10:35:57Z

Is #836 really needed? PROXY variables shouldn't end up in models, unless I am mistaken.

They do :/ I will check why they leak.

If #832 is ready and working we should merge #832 into this PR, then merge both into next at once.

Ok

…_split

- add a data-structure for models, - save the strucutre in the SAT's env - print the models in the Frontend module

Some tests about models failed in the OptimAE PR. This commit allows to tag tests in `tests/` with `fail` tag which means the test is supposed to fail.

I also remove the mention about the different kind of formats used to print models. Indeed, we use only the SMT-LIB format and the Why3 format is slightly different but probably outdated.

Some cram tests are not valid anymore as we don't need to select the SAT solver Tableaux while generating models.

The dump-models option have been broken by the refactoring in OptimAE. I restore this feature.

Return the appropriate environment in the Frontend module to retrieve the model with `(get-model)` as we did in the PR OCamlPro#789.

This commit restore the feature of the PR OCamlPro#838 as the location of code moved after the refactoring of model generation in OptimAE.

Halbaroth · 2023-09-26T15:32:07Z

The CI will fail because FunSAT failed to produce a complete model for the first check-sat in bool1.smt2. SatML manages to produce a complete model in this case but the expected output has to be the some for both solvers. I will fix the issue with FunSAT in another PR.

Halbaroth · 2023-09-26T15:33:26Z

I forgot to add the support for String.starts_with in the compat module! This feature is not present in old stdlib. I'll do it right now.

You did it!

bclement-ocp

A couple very minor things to fix and we should be good to go 🎉

src/bin/common/solving_loop.ml

src/lib/frontend/frontend.ml

tests/dune.inc

src/lib/structures/symbols.ml

Symbol names prefixed with a dot or @ shouldn't never be printed in models as they cannot be declared by the user. This behaviour is SMT-LIB compliant.

This reverts commit 9507d63.

Prevent to test models with other solvers as we cannot guarantee they will produce exactly the same model. We have to modify gentest to manage several expected files while testing models.

Halbaroth · 2023-09-27T13:01:30Z

I removed tests for other solvers. I will modify gentest script later to manage tests with several expected outputs but I have more urgent stuff to do now and this PR should be merge as soon as possible.

bclement-ocp

LGTM 🎉

Now only check-all-sat and OptimAE itself remain?

Halbaroth · 2023-09-27T13:17:34Z

Yes! I'm working on CheckAllSat.

Prior to c1e4387 (OCamlPro#829) we did not have model generation in the default solver, and model generation required to use the Tableaux solver, so we used the Tableaux solver when testing models. Since the default solver now supports model generation, we should use it to test model generation instead, since the models generated by both solvers can be different and most users will use the default solver rather than the Tableaux solver. Unfortunately, this causes some tests using `get-assignment` to fail (see OCamlPro#937).

Prior to c1e4387 (#829) we did not have model generation in the default solver, and model generation required to use the Tableaux solver, so we used the Tableaux solver when testing models. Since the default solver now supports model generation, we should use it to test model generation instead, since the models generated by both solvers can be different and most users will use the default solver rather than the Tableaux solver. Unfortunately, this causes some tests using `get-assignment` to fail (see #937).

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)

Halbaroth added the enhancement label Sep 21, 2023

Halbaroth marked this pull request as ready for review September 21, 2023 09:25

Halbaroth commented Sep 21, 2023

View reviewed changes

Halbaroth mentioned this pull request Sep 21, 2023

Fix model generation with SatML #832

Closed

bclement-ocp mentioned this pull request Sep 21, 2023

Bubble decision of printing models upwards #833

Closed

bclement-ocp requested changes Sep 21, 2023

View reviewed changes

Halbaroth mentioned this pull request Sep 22, 2023

Printing unknown reason #834

Closed

Halbaroth force-pushed the satml-model branch from f764ed4 to 8a00a07 Compare September 22, 2023 13:41

Halbaroth force-pushed the satml-model branch from 028bb58 to bbac2d7 Compare September 25, 2023 10:55

Halbaroth requested a review from bclement-ocp September 26, 2023 14:23

iguerNL and others added 15 commits September 26, 2023 17:19

Theory: harden 'compute_concrete_model' function

914d283

Push the test 'get_case_split_policy() == origin' into Theory.do_case…

982bb92

…_split

CS: functions return all the env instead of just 'gamma_finite'.

de26aae

Fun_sat: refactor the way models are handled/printed

fed58a7

- add a data-structure for models, - save the strucutre in the SAT's env - print the models in the Frontend module

satML: add missing case-split strategies

7447ca3

satML: implement models generation.

0c37f66

Make model tests negative

1ace3d9

Some tests about models failed in the OptimAE PR. This commit allows to tag tests in `tests/` with `fail` tag which means the test is supposed to fail.

Reindent

3ac006b

Update documentation about output_concrete_model

4b03759

I also remove the mention about the different kind of formats used to print models. Indeed, we use only the SMT-LIB format and the Why3 format is slightly different but probably outdated.

Document the timeout_reason ADT

0251733

poetry

9496cf6

Restore the comment about reinit_cpt

115a16a

Fix spelling

986321d

Remainder to the issue 834

b39ecb8

Simplify get-model processing

9507d63

Halbaroth added 5 commits September 26, 2023 17:19

Remove deprecated cram tests

afb8e44

Some cram tests are not valid anymore as we don't need to select the SAT solver Tableaux while generating models.

Test models with all the SAT solvers

e0c9b34

Restoring dump-models option

b45ee04

The dump-models option have been broken by the refactoring in OptimAE. I restore this feature.

Use the right post-solve SAT environment for models

a155756

Return the appropriate environment in the Frontend module to retrieve the model with `(get-model)` as we did in the PR OCamlPro#789.

Print dump models on the channel models

709dc42

This commit restore the feature of the PR OCamlPro#838 as the location of code moved after the refactoring of model generation in OptimAE.

Halbaroth force-pushed the satml-model branch from bbac2d7 to 91b110d Compare September 26, 2023 15:29

bclement-ocp mentioned this pull request Sep 26, 2023

Ensure that internal AC symbols do not end up in models #810

Closed

bclement-ocp requested changes Sep 26, 2023

View reviewed changes

Halbaroth mentioned this pull request Sep 26, 2023

Support of get-info SMT2 command #837

Merged

Halbaroth added 2 commits September 26, 2023 18:27

Prevent printing internal names in models

cd998e7

Symbol names prefixed with a dot or @ shouldn't never be printed in models as they cannot be declared by the user. This behaviour is SMT-LIB compliant.

Promote tests

819935b

Halbaroth force-pushed the satml-model branch from 346378c to d4301df Compare September 26, 2023 16:28

Halbaroth added 3 commits September 26, 2023 18:28

Revert "Simplify get-model processing"

a6caf6a

This reverts commit 9507d63.

Review changes

d4301df

Test only models with FunSAT

3299ff7

Prevent to test models with other solvers as we cannot guarantee they will produce exactly the same model. We have to modify gentest to manage several expected files while testing models.

Halbaroth requested a review from bclement-ocp September 27, 2023 13:01

bclement-ocp approved these changes Sep 27, 2023

View reviewed changes

Halbaroth merged commit c1e4387 into OCamlPro:next Sep 27, 2023
14 checks passed

bclement-ocp mentioned this pull request Nov 16, 2023

Use default solver for testing models #938

Merged

bclement-ocp mentioned this pull request Nov 17, 2023

Timeouts are broken #946

Closed

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

Model generation support for SatML #829

Model generation support for SatML #829

Halbaroth commented Sep 21, 2023 •

edited

Loading

bclement-ocp commented Sep 21, 2023 •

edited

Loading

bclement-ocp left a comment

Halbaroth commented Sep 22, 2023

Halbaroth commented Sep 25, 2023

bclement-ocp commented Sep 25, 2023

Halbaroth commented Sep 25, 2023

Halbaroth commented Sep 26, 2023

Halbaroth commented Sep 26, 2023 •

edited

Loading

bclement-ocp left a comment

Halbaroth commented Sep 27, 2023

bclement-ocp left a comment

Halbaroth commented Sep 27, 2023

Model generation support for SatML #829

Model generation support for SatML #829

Conversation

Halbaroth commented Sep 21, 2023 • edited Loading

bclement-ocp commented Sep 21, 2023 • edited Loading

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Sep 22, 2023

Halbaroth commented Sep 25, 2023

bclement-ocp commented Sep 25, 2023

Halbaroth commented Sep 25, 2023

Halbaroth commented Sep 26, 2023

Halbaroth commented Sep 26, 2023 • edited Loading

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Sep 27, 2023

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Sep 27, 2023

Halbaroth commented Sep 21, 2023 •

edited

Loading

bclement-ocp commented Sep 21, 2023 •

edited

Loading

Halbaroth commented Sep 26, 2023 •

edited

Loading