New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rename smt status enum #466

Draft

ahmed-irfan wants to merge 3 commits into master from rename-smt-status-enum

Contributor

ahmed-irfan commented Oct 9, 2023

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.

ahmed-irfan added 3 commits

October 7, 2023 22:59


          rename smt_status enum

7ce891a


          update manual

90a2aeb


          update html doc

9859cb9

ahmed-irfan requested a review from disteph

October 9, 2023 16:23

coveralls commented Oct 9, 2023

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

Contributor

markpmitchell commented Oct 9, 2023 via email

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 <#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: #466 Commit Summary 7ce891a <7ce891a> rename smt_status enum 90a2aeb <90a2aeb> update manual 9859cb9 <9859cb9> 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 <#466>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKVS3HQUIOVR7DBN23RNHDX6QQH7AVCNFSM6AAAAAA5ZBU6JWVHI2DSMVQWIX3LMV43ASLTON2WKOZRHEZTGNBRG42DMNI>. You are receiving this because you are subscribed to this thread.

Contributor Author

ahmed-irfan commented Oct 9, 2023

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.

ahmed-irfan added this to the Yices 2.7 milestone

disteph approved these changes

View reviewed changes

Contributor

disteph left a comment

Looks good to me. That should go in the next non-backward compatible release though.

ahmed-irfan modified the milestones: Yices 2.7, Yices 2.8

ahmed-irfan self-assigned this

ahmed-irfan mentioned this pull request

hack: undef status_interrupted to fix windows build #467

Merged

ahmed-irfan marked this pull request as draft

October 10, 2023 18:45

ahmed-irfan modified the milestones: Yices 2.8, Yices 2.7

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment