3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 00:35:47 +00:00

Commit graph

  • 0108a86490 fix the build slack Lev Nachmanson 2025-05-08 17:28:34 -07:00
  • 7da06df64f restore lar_solver::add_named_var Lev Nachmanson 2025-05-08 17:18:41 -07:00
  • 935f076a05 continue PIMPL refactor in lar_solver Lev Nachmanson 2025-05-08 16:45:00 -07:00
  • a51239c641 update namespace, hoist exported functions outside of embedded namespace master Nikolaj Bjorner 2025-05-07 15:57:47 -07:00
  • 644118660f list euf dependency in api cmakefile Nikolaj Bjorner 2025-05-07 15:47:03 -07:00
  • eca5cd1841 mark virtual methods as override Nikolaj Bjorner 2025-05-07 15:24:20 -07:00
  • 9a299eb9ff move mam to euf Nikolaj Bjorner 2025-05-07 14:38:59 -07:00
  • d4f45e1528 implement imp of lar_solver as lar_solver::imp Lev Nachmanson 2025-05-07 13:53:28 -07:00
  • 97c6074156 remove a function from lar_solver Lev Nachmanson 2025-05-07 13:33:46 -07:00
  • 67652dd8eb test Lev Nachmanson 2025-05-07 13:14:23 -07:00
  • 5487c5a963 shuffle more functionality from lar_solver.h to lar_solver::imp Lev Nachmanson 2025-05-07 12:59:49 -07:00
  • 32e8697abd
    Merge 78c5800a99 into 0e4c033e30 mikulas-patocka 2025-05-07 13:32:05 +08:00
  • fdcde925d6 apply the slack idea in a loop Lev Nachmanson 2025-05-05 16:21:37 -07:00
  • 0e4c033e30 fix #7639 Nikolaj Bjorner 2025-05-03 11:06:25 -07:00
  • 4bedb5f8fc fix #7638 Nikolaj Bjorner 2025-05-03 11:04:41 -07:00
  • d413468dce slack Lev Nachmanson 2025-05-02 12:10:29 -07:00
  • dd211bade9 filter out terms that are not solved Nikolaj Bjorner 2025-04-30 09:40:45 -07:00
  • f89e133d52
    revert the behavior of add_zero_assumption (#7631) Lev Nachmanson 2025-04-28 16:07:46 -07:00
  • 6af61fa0f4 remove experiment Nikolaj Bjorner 2025-04-28 10:00:02 -07:00
  • b502126ebc fix #7634 Nikolaj Bjorner 2025-04-27 23:57:57 -07:00
  • 24090fc48c move flush smc to first use Nikolaj Bjorner 2025-04-27 11:44:45 -07:00
  • a626cd0fed flush smc before use in model construction Nikolaj Bjorner 2025-04-27 11:18:18 -07:00
  • 71b5e44058 #7596 - flush smc before copy Nikolaj Bjorner 2025-04-27 10:36:27 -07:00
  • 7a302239c2 fix #7630 Nikolaj Bjorner 2025-04-26 11:40:48 -07:00
  • d581dc1db4 #7630 propagate parameters on lazy tactics Nikolaj Bjorner 2025-04-26 11:22:16 -07:00
  • 322e4441b3 Fix conversion of signed 1-bit BV to FP Fixes https://github.com/AliveToolkit/alive2/issues/1193 Nuno Lopes 2025-04-25 12:38:00 +01:00
  • 792ffeeda7 fix latent sign bug Nikolaj Bjorner 2025-04-23 17:22:57 -07:00
  • fe1fff3b7e add scaffolding for experiments with slack Nikolaj Bjorner 2025-04-23 17:07:50 -07:00
  • 12ccf59ab9 rename fields to compile on c++ platforms Nikolaj Bjorner 2025-04-23 17:06:15 -07:00
  • e41acd7b50 convert m_r_upper and m_r_lower bounds to plain vectors Nikolaj Bjorner 2025-04-23 16:33:38 -07:00
  • fae60946bf consolidate some bounds references Nikolaj Bjorner 2025-04-23 15:45:44 -07:00
  • f6fbeda9d7 fix #7629 Nikolaj Bjorner 2025-04-23 15:22:44 -07:00
  • 7641393f8a use inlined functions Nikolaj Bjorner 2025-04-23 14:28:31 -07:00
  • 5cc57b8958 coalesce updates to bounds Nikolaj Bjorner 2025-04-23 14:05:17 -07:00
  • 7168589dd1 revert the behavior of add_zero_assumption add_zero_assumption Lev Nachmanson 2025-04-23 12:21:00 -07:00
  • 579ba8bd70 add power axioms to arith_solver Nikolaj Bjorner 2025-04-23 10:48:29 -07:00
  • d73d104ded remove overwriting x,y,rval Nikolaj Bjorner 2025-04-23 09:17:12 -07:00
  • ff920ba51b handle root expressions, and checking exponentiation with nlsat Nikolaj Bjorner 2025-04-22 13:47:38 -07:00
  • 2fe2735b5e
    Replace _DEBUG with Z3DEBUG (#7628) Carson Radtke 2025-04-22 15:39:01 -05:00
  • 30ec308c57
    Replace _DEBUG with Z3DEBUG Carson Radtke 2025-04-22 14:07:00 -05:00
  • a1673f2bdd fallback to Gomory cuts and gcd conflicts if dio fails Lev Nachmanson 2025-04-21 17:10:32 -07:00
  • 78c5800a99
    Merge branch 'master' into ctrl-c-races Nikolaj Bjorner 2025-04-19 13:58:13 -07:00
  • cc1bb0a255 remove superfluous makefile Nikolaj Bjorner 2025-04-19 13:56:30 -07:00
  • 17cac7d87c provide shortcut to command-line version to retrieve parameters Nikolaj Bjorner 2025-04-19 13:51:08 -07:00
  • 6e88d91214 add badge for ocaml cmake Nikolaj Bjorner 2025-04-19 13:46:40 -07:00
  • 3761dd869a address build warning with overloaded virtual operators Nikolaj Bjorner 2025-04-19 13:42:08 -07:00
  • f7aec02503
    WIP: Migrating OCaml binding to CMake (#7254) Shiwei Weng 翁士伟 2025-04-19 16:41:27 -04:00
  • 4237ebd027 Bypass @rpath in building sanity check. Weng Shiwei 2025-04-19 14:56:49 -04:00
  • ac10869fff Fix mac linking once more. Weng Shiwei 2025-04-19 04:30:53 -04:00
  • ab9f3307d6 change the default of running dio to true, and running gcd to false, remove branching in dio Lev Nachmanson 2025-04-18 18:07:59 -07:00
  • dbde713eb3 remove testing code in is_big_term_on_no_term Lev Nachmanson 2025-04-09 19:24:59 -07:00
  • 1131d5294d fix a bug in tracking the changes in dio Lev Nachmanson 2025-04-09 15:56:44 -07:00
  • d289495ca4 allow gcd when dio ignores some terms Lev Nachmanson 2025-04-09 10:23:55 -07:00
  • 17af18fe31 make gcd call in dio optional Lev Nachmanson 2025-04-08 16:10:17 -07:00
  • 436eefbce2 always remove the tightened term Lev Nachmanson 2025-04-08 10:47:51 -07:00
  • dc7185d0a4 change the name of m_changed_columns to m_changed_f_columns Lev Nachmanson 2025-04-08 07:07:00 -07:00
  • 32e77d8214 typo Lev Nachmanson 2025-04-08 06:18:57 -07:00
  • cb1818f4b8 reject more terms with big numbers Lev Nachmanson 2025-04-07 11:49:39 -07:00
  • 1cde40bddb dio_calls_period=4 Lev Nachmanson 2025-04-05 10:27:49 -07:00
  • 87e2ce8948 Update lp_settings.h - m_dio_calls_period = 4 Lev Nachmanson 2025-04-05 10:26:35 -07:00
  • 59edb81f86 Update lp_settings.cpp Lev Nachmanson 2025-04-05 10:25:39 -07:00
  • 8db9f52386 add parameter m_dio_calls_period Lev Nachmanson 2025-04-04 19:56:13 -07:00
  • ae97ee09d9 throttle dio Lev Nachmanson 2025-04-04 13:34:16 -07:00
  • 972f80188a throttle dio for big numbers Lev Nachmanson 2025-04-04 08:51:35 -07:00
  • 3e49d9fcfe reuse dio branch Lev Nachmanson 2025-04-03 09:47:02 -07:00
  • 699e55ac8c change the default of running dio to true, and running gcd to false, remove branching in dio dio Lev Nachmanson 2025-04-18 18:07:59 -07:00
  • eac9908550
    Add workflow using matrix. Weng Shiwei 2025-04-18 12:41:58 -04:00
  • e31e9819b1
    Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling (#7619) mikulas-patocka 2025-04-18 19:34:54 +02:00
  • ed5dd26bb7 remove non-working ts mcp server, settle with python variant Nikolaj Bjorner 2025-04-18 10:10:12 -07:00
  • 741cb5c3b5 minimal z3 MCP server Nikolaj Bjorner 2025-04-18 10:00:04 -07:00
  • a405046161
    Try github action for ocaml. Weng Shiwei 2025-04-18 03:18:53 -04:00
  • bf21d02df5
    Keep ml_example.ml in the src. Weng Shiwei 2025-04-18 02:10:52 -04:00
  • 7943538744
    Keep z3.ml and z3.mli in the src but specify the generated file in the bin. Weng Shiwei 2025-04-17 21:56:51 -04:00
  • 7a78bd4a6b
    Remove including AddOCaml. Weng Shiwei 2025-04-17 21:53:43 -04:00
  • f63c9e366f disable assignment for param_descrs Nikolaj Bjorner 2025-04-17 17:29:09 -07:00
  • 3f73c8b18f stab at SMTLIB REL mcp server Nikolaj Bjorner 2025-04-17 17:23:09 -07:00
  • 755f57931b fix #7622 Nikolaj Bjorner 2025-04-17 11:05:49 -07:00
  • b03efc7c00
    Resume working on this PR. Weng Shiwei 2025-04-17 03:08:26 -04:00
  • 81f10912ae remove unused bdd based variable elimination Nikolaj Bjorner 2025-04-14 16:07:41 -07:00
  • e41090df83 fix #7602 Nikolaj Bjorner 2025-04-14 15:38:22 -07:00
  • 8035edbe65 remove lp_assert Nikolaj Bjorner 2025-04-14 11:10:26 -07:00
  • 1510b3112e fix build warnings Nikolaj Bjorner 2025-04-14 10:33:14 -07:00
  • 5ad79f2864
    Add Iterators as acceptable arguments to functions (#7620) Kyle Bloom 2025-04-12 18:32:56 +01:00
  • 8f05d2e3cb Add Iterators as acceptable arguments to functions Kyle Bloom 2025-04-12 15:34:30 +01:00
  • 6ecc7a2dd4
    Fix a race condition in scoped_timer::finalize (#7618) mikulas-patocka 2025-04-11 09:08:27 +02:00
  • a83efa68eb spacing Nikolaj Bjorner 2025-04-09 20:23:51 -07:00
  • 8138829231 fix #7616 Nikolaj Bjorner 2025-04-09 20:23:26 -07:00
  • 36a0006f59 remove testing code in is_big_term_on_no_term Lev Nachmanson 2025-04-09 19:24:59 -07:00
  • 97bb449a24 fix a bug in tracking the changes in dio Lev Nachmanson 2025-04-09 15:56:44 -07:00
  • 7e88064da9 allow gcd when dio ignores some terms Lev Nachmanson 2025-04-09 10:23:55 -07:00
  • b5821f6e5e Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling Mikulas Patocka 2025-04-09 19:03:26 +02:00
  • b007eb30ab Fix a race condition in scoped_timer::finalize Mikulas Patocka 2025-04-09 18:46:10 +02:00
  • bcd615f3c5 Make Ctrl-C handling thread-safe (#7603) Mikulas Patocka 2025-04-09 18:29:08 +02:00
  • 7ee3415150 make gcd call in dio optional Lev Nachmanson 2025-04-08 16:10:17 -07:00
  • d792840739
    Add Z3_is_recursive_datatype_sort to the API (#7615) Josh Berdine 2025-04-08 22:36:57 +01:00
  • 019da2308e always remove the tightened term Lev Nachmanson 2025-04-08 10:47:51 -07:00
  • 386c331eb9 Add Z3_is_recursive_datatype_sort to the API Josh Berdine 2025-04-08 16:50:59 +01:00
  • dd1b2a294f change the name of m_changed_columns to m_changed_f_columns Lev Nachmanson 2025-04-08 07:07:00 -07:00
  • 0011deea5c typo Lev Nachmanson 2025-04-08 06:18:57 -07:00
  • df10608db8 reject more terms with big numbers Lev Nachmanson 2025-04-07 11:49:39 -07:00