search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
363 stars 45 forks source link

Rename smt status enum #466

Open ahmed-irfan opened 9 months ago

ahmed-irfan commented 9 months ago

Towards fixing #418

Reason for the change:

STATUS_INTERRUPTED is a defined in windows, and we are using it in the smt_status_t enum. This PR renames the symbols used in the smt_status_t enum.

coveralls commented 9 months ago

Coverage Status

coverage: 65.098%. remained the same when pulling 9859cb95a70d4510648bb13c121be61c46fe8116 on rename-smt-status-enum into 95f13c6777b9c262dc13aebd908aa52fda0892d2 on master.

markpmitchell commented 9 months ago

At some point, we might consider prefixing all constants exposed as part of the API with YICES_, matching the function names.

FWIW,

-- Mark Mitchell

On Oct 9, 2023, at 9:23 AM, Ahmed @.***> wrote:

Towards fixing #418 https://github.com/SRI-CSL/yices2/issues/418 Reason for the change:

STATUS_INTERRUPTED is a defined in windows, and we are using it in the smt_status_t enum. This PR renames the symbols used in the smt_status_t enum.

You can view, comment on, or merge this pull request online at:

https://github.com/SRI-CSL/yices2/pull/466

Commit Summary

7ce891a https://github.com/SRI-CSL/yices2/pull/466/commits/7ce891ab9cafe048e2dd4eb77d76dd854551bc32 rename smt_status enum 90a2aeb https://github.com/SRI-CSL/yices2/pull/466/commits/90a2aebfd90e941b24cb9adeab4fa96901d4c43f update manual 9859cb9 https://github.com/SRI-CSL/yices2/pull/466/commits/9859cb95a70d4510648bb13c121be61c46fe8116 update html doc File Changes (66 files https://github.com/SRI-CSL/yices2/pull/466/files) M doc/manual/manual.tex https://github.com/SRI-CSL/yices2/pull/466/files#diff-c5084727efc62c6113e6fdfe7a8a9a6e9d96fe3f079f4301f4918ece904d6367 (18) M doc/sphinx/source/_static/example1.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-307489a7ec730c6dc5975e0feb6106bcd2f561c1d5a07c5b220f64130127c51e (14) M doc/sphinx/source/_static/example1b.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-577c7975239b2cbaec98f262c7298a411d8bfc7d39ca81cf36607b34f83c5b60 (14) M doc/sphinx/source/api-types.rst https://github.com/SRI-CSL/yices2/pull/466/files#diff-396c6ac70749fd25fd50eda8a58c95efebb64e7e062c97f625f5d5126ffb194b (36) M doc/sphinx/source/basic-usage.rst https://github.com/SRI-CSL/yices2/pull/466/files#diff-479e36c7ff8143cc907d5140d2ad06fc60fafb6fc9f6375ad3298ccc8c33da82 (24) M doc/sphinx/source/context-operations.rst https://github.com/SRI-CSL/yices2/pull/466/files#diff-384189121b92eb6419cfeb7206f29f2d8fd092152088bccf457877888e1eec33 (130) M doc/sphinx/source/formula-operations.rst https://github.com/SRI-CSL/yices2/pull/466/files#diff-7c62417c9aec5d1810e6c6e0cb83ac17cea7faa0c72e9a9f55a19f827d485019 (10) M doc/sphinx/source/model-operations.rst https://github.com/SRI-CSL/yices2/pull/466/files#diff-aa93e720059a3a09854ed8afc8ad28bc343e7205f112d65e7b3990c338c0bd78 (6) M examples/check_formula_examples.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-133525f0980759fb2b6d042f74b420245797569f6b6212df3215b662e1087f1f (4) M examples/check_formula_examples_mt.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-32113bed829ec1f0caf5bd35674b80bce047975adc93d6c924b2f27f6cd6ac6e (4) M examples/example1.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-ef81e73136a8f751b843d499906b36f60033e114e7d9d11198c89398416013d4 (14) M examples/example1b.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-4f733a156b4d6acf4f40a1eea613ba4a2989b67b083a8e4466e44ea6a32f8cd5 (14) M examples/example1c.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-f771493c0d09216fbd55df4df2910e79501c09d82d0e51b2758bcd0ecc75e7a6 (14) M examples/example2.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-6a06bd7828dde6dba5f24f99cc9f30c643ce99531b644cf938eed8baa298d81a (14) M examples/example2b.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-2024e31e52c83f6e002dc3104e69a4974e3955defa17987a46e54b01f550eb49 (14) M examples/example2c.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-ec39c5105fa6f66128ff46d5a457280e1db09353f6f4e067ff7e077bf06223be (14) M examples/example2d.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-081cff0de96de79191ea280bd340b5d6d7a52ffc2cc834ee60ce70fe846e5fbe (14) M examples/example2e.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-70c2ed73a10956c09b865337c762f4341ad667a53a74f34ad770094bb7b33d23 (14) M examples/example_mcsat.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-64c49436c15ecb32df06f64f2bfd5fe1b30939e4bbb1de7e16130bf2f1a3606a (4) M examples/example_unsat_core.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-a3e736b5d8acaa124d78b9974b43617e7d95acd00a5638fcc3bfe0d853fee80b (8) M examples/export_to_dimacs_example.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-7ca2133c4d0065365c1715eeca1effc16da5ce3f6f88eb0d5bb7310f7c4e22b5 (4) M examples/export_to_dimacs_example_mt.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-cea7913f87aa334e520ecabe91a9df156ac6e3f43ef817e41220a4a6b89fc5b1 (4) M examples/like_issue233.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-910da3b91764c537f8d5424a8a919ce4708d797f2aea4aa395ff76ab8fa1fd0f (18) M examples/like_test02m.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-5e6d8d00a8e00d9a6d47487703661aff94f164f8faa1eb677e57a79b0bd89181 (26) M examples/test_check_with_model.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-3ef969fb00c96e1ed71d522c7614fbd0107c3dc9bf7bdc2fad3e45f52b24409a (12) M src/api/yices_api.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-f906bec767cff61c3540feb869f23557387588c90fc81d70ec613380280fec22 (268) M src/context/context.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-c9b6890d96d0da48760cd80cdf7403f6f7708c26be7a57bcdeaca98f1644cabe (20) M src/context/context.h https://github.com/SRI-CSL/yices2/pull/466/files#diff-c0ae5ddf3dfec92232e908f7212e66c37d73fbd18ea7784518298624f6c5386f (36) M src/context/context_solver.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-dabda8f4cc4800d3fd61747aef3588aee59907fa67b8a2324214956e5b1c99e2 (74) M src/exists_forall/efsolver.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-1f99214bd5729a79d6c2df4b0a446de9f1008837a1439c81ed4c7717031061e4 (88) M src/frontend/common/assumptions_and_core.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-ba255e393d66e0bf49e3732eb3faa23c7c0cdce2e4de70030d6f63a0b18ed5fd (2) M src/frontend/smt2/smt2_commands.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-a10105cce9050820d0a3bb888cf7a32a9a67528624dc4ffd79904e991f2a11cc (270) M src/frontend/yices/yices_reval.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-fff88f4f282fc9b7575f2a880f556db24aec56804ad39e983e59b3da603bddb3 (140) M src/frontend/yices_smt.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-1cf027faa06edb8c9dc4407c1f516e42e123ba93673d8b800bfc5485d0ca0882 (6) M src/frontend/yices_smtcomp.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-799f906b1646ed16d6c44395023eadb41cd17df176fa97223f356471e86b76ad (10) M src/include/yices.h https://github.com/SRI-CSL/yices2/pull/466/files#diff-913e4fd2b4876d7ec940efff1f976e43bcda5dca0067fcf03967be33a1295ed9 (120) M src/include/yices_types.h https://github.com/SRI-CSL/yices2/pull/466/files#diff-568871607b523aa15c2c53076965871130ee4c3ebe40ba075a8a0cf9c57b52af (14) M src/mcsat/bv/bv_explainer.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-d63d1ece21e4aad4b8f55b730dda95ff38fd97cde2be0be7d1b00e290976e955 (2) M src/mcsat/bv/bv_utils.h https://github.com/SRI-CSL/yices2/pull/466/files#diff-d3682148e957b5e09844b226c38624ee264e56c412706f87a49b16635fa6a28c (2) M src/mcsat/bv/explain/full_bv_sat.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-717403654fe4eeb9fdb5baa35b3ec97a658c4dd27df7cbf0362bffbd231a1b41 (2) M src/mcsat/conflict.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-3d807b6c205dd07ba9403dc0054dd1bbc1904ebb1c16153226f17cdd6befdef8 (2) M src/mcsat/no_mcsat.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-b1c2f5b0e68ceae5864bbde25d91f0914e38ea4efc7b781f3cf7b67acd987397 (2) M src/mcsat/solver.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-9beddeebb3753d511c9f74a6cac286af71b99af654e1bbac026f53de0eefcd47 (32) M src/solvers/cdcl/delegate.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-2c431d949f7f554999f3ea0118ac6f545dae511aeee2c8a358233f6bc71a65ff (32) M src/solvers/cdcl/delegate.h https://github.com/SRI-CSL/yices2/pull/466/files#diff-c079197953d09f897556ade0816eeeb69457730c6add16a6f96ebe47523e0018 (8) M src/solvers/cdcl/smt_core.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-73b6e8d1166540c30d143e2dc9fe24ee2209e0be989e425ffcf3867a60ba43d6 (90) M src/solvers/cdcl/smt_core.h https://github.com/SRI-CSL/yices2/pull/466/files#diff-e7e153387576074aa22957370a371961b1fcc2eea8f1b29d48582da36a4000d6 (36) M src/solvers/cdcl/smt_core_printer.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-dd59275593c2c264545239f9a1caff9c52c7a2f2125ee496bcb8500ed0ceca31 (4) M src/solvers/quant/quant_solver.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-30be464f04fd6f7b6db7ea951a89436b593026983d0dc6a76589edc26f289365 (8) M tests/api/balanced_arith_buffers.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-2708c41722de12450b4246003e20c2c305b0d634a14b889ca63d6e8beaea23f9 (4) M tests/api/mcsat_preprocessor.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-3afe39c3107924e6cc0cc664f376b46e10862fd184051bc6fa69acddc4440ac5 (2) M tests/api/model_eval.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-9a8f039916a1d20654bbbda6e051e3cfca1f41c41b63d36a7791a8c82e5e8402 (2) M tests/api/mpq_aux.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-be92cebc34e7a0f92cb5adcfb7286684efe0967b0b65dfab706ad0be1d01eea2 (2) M tests/api/nra_plugin_explain.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-7b1d86a8e0cbc6190178e1a99df2e38c0fb11599dfe6ceb746c1db835e8e5366 (4) M tests/api/nra_plugin_explain_2.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-ec56ca653e2e4ae3a938113fe5ae4e10fb827a903cf70bc7b4e7414f9e19e76f (2) M tests/api/rationals.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-6332075ef8666b17313f96f35db9c89ee4d1e3c491710b54528fb369b7cc5b8c (2) M tests/api/rba_buffer_terms.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-6281ec06838bdc53766efcb95072eeb930878079df364dac0b405cd961883a24 (2) M tests/api/term_utils.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-9a557a9a9b4ac142f154e517479c3d717e6c3c288ca7a069f2b440af280bf653 (2) M tests/api/uf_plugin.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-9138e0a943dc50211e8c0a5b9939d4e6e6a36721f3139473e9887436b4d53e19 (2) M tests/unit/sudoku.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-230c88b4ae92e187c70d2cd571f49041cae8918292ffe7d7da23a3c311c7e5aa (2) M tests/unit/test_check_formulas.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-38fe4c5c4786f05844c4ff091353cfc7b9c453174fc1b428339fd32d32a25aaa (4) M tests/unit/test_core2.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-39a2a20e1bbec5e10817665165aa62f6221e28771166412322bf1ca7ce52cbf9 (18) M tests/unit/test_core3.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-75a6f0d5d261c4ba234a50192f725678b8fc6fd858f55c6e775b9d18556dfd94 (18) M tests/unit/test_export_formulas.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-2d427b072c1e6fbb4b82604de9ba0f6a1942416f54a4b4a9c37f480204dd73a5 (4) M tests/unit/test_gate_manager.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-b8bd2792b8bcd130d087064332c36ca0dd70700593cf14c6b35409f9836da614 (10) M tests/unit/test_mcsat.c https://github.com/SRI-CSL/yices2/pull/466/files#diff-f87981d8b4d819914f97fa94920118cacbddbf375520153464b94ad1ea40a036 (4) Patch Links:

https://github.com/SRI-CSL/yices2/pull/466.patch https://github.com/SRI-CSL/yices2/pull/466.diff — Reply to this email directly, view it on GitHub https://github.com/SRI-CSL/yices2/pull/466, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVS3HQUIOVR7DBN23RNHDX6QQH7AVCNFSM6AAAAAA5ZBU6JWVHI2DSMVQWIX3LMV43ASLTON2WKOZRHEZTGNBRG42DMNI. You are receiving this because you are subscribed to this thread.

ahmed-irfan commented 9 months ago

At some point, we might consider prefixing all constants exposed as part of the API with YICES_, matching the function names. FWIW, …

+1 That's a good point.