mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
19422 commits 49 branches 53 tags 182 MiB
Commit graph

1794 commits

Author SHA1 Message Date
Lev Nachmanson
73224adc48 cleanup 2023-03-08 10:27:05 -08:00
Lev Nachmanson
377ceba6d5 rm lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
6132bf93f7 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
bfe73c01a6 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
1da4c018e4 rm lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
62bd3bd1e6 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
5f03c93270 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
9a7c99da33 rm lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
c251151d66 rm_lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
25f103db1a rm_lp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
527f0d1242 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
a38be43264 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
97c1ba4641 rm get_column_in_lu_mode 2023-03-08 10:27:05 -08:00
Lev Nachmanson
ea16f6608c before rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
92fe8c5968 restore the previous state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-03 18:30:17 -08:00
Lev Nachmanson
ff1dc0424c rm lp_solver 2023-03-03 16:32:49 -08:00
Lev Nachmanson
2dd30fa350 rm lp_primal_simplex 2023-03-03 15:44:50 -08:00
Lev Nachmanson
8989e10e71 rm lp_dual_simplex 2023-03-03 15:41:30 -08:00
Lev Nachmanson
d2e8297d41 remove includes of lp_dual_simplex 2023-03-03 15:38:47 -08:00
Lev Nachmanson
2ec09944d7 removals 2023-03-03 15:32:44 -08:00
Lev Nachmanson
8db2f1409b lp_dual_simplex.cpp removed from CMakeLists.txt 2023-03-03 15:27:57 -08:00
Lev Nachmanson
cd24c99739 remove a lp_primal_simplex.cpp from CMakeLists 2023-03-03 15:26:06 -08:00
Lev Nachmanson
f986ac6a75 remove mps_reader 2023-03-03 14:50:10 -08:00
Nikolaj Bjorner
5974a2dc58 remove m_b from lar_core_solver 
the column vector is pure overhead for the way the lar solver uses lp.
Some other solver modules use column vectors b and integrate with the lp_core_solver_base. The interaction model should be reviewed.
Unused solvers should be removed to make it easier to maintain this code.
 2023-02-28 17:40:08 -08:00
Nikolaj Bjorner
7c08e53e94 fixes for #6590 2023-02-15 15:11:44 -08:00
Nikolaj Bjorner
8ce0c56ff5 fix #6590 2023-02-15 08:36:01 -08:00
Nikolaj Bjorner
a976b781a0 fix #6585 2023-02-14 15:33:17 -08:00
Nikolaj Bjorner
3dc91de531 fix #6582 2023-02-13 13:21:30 -08:00
Jakob Rath
d69155b9e9
Shared features from polysat branch (#6567) 
* Allow setting default debug action

* Fix dlist and add iterator

* Add var_queue iterator

* Add some helpers

* rational: machine_div2k and pseudo_inverse

* Basic support for non-copyable types in map

* tbv helpers

* pdd updates

* Remove duplicate functions

gcc doesn't like having both versions
 2023-02-03 13:08:47 -08:00
Nikolaj Bjorner
741634b703 compiler warning fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:26:51 -08:00
Nikolaj Bjorner
682e868129 initialize field 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner
0f86a00229 use setter method to easier track updates to settings. 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner
304b316314 move bounded division lemmas to nla solver/ nla_divisions. 2023-01-30 11:11:04 -08:00
Nikolaj Bjorner
03ca330926 fix division filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 08:23:17 -08:00
Nikolaj Bjorner
2c4a9c2f5c fix division filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 08:20:26 -08:00
Nikolaj Bjorner
8e37e2f913 handle non-linear division axioms, consolidate backtracking state in nla_core 
this update enables new incremental linear axioms based on division terms.
It also consolidates some of the backtracking state in nla_core / emons to use stack traces instead of custom backtracking state.
 2023-01-29 17:22:57 -08:00
Nikolaj Bjorner
8ea49eed8e convert reduce-args to a simplifier 
- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
  - allow multiple defs to be added with same pool of removed formulas
  - fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-
 2023-01-28 20:12:14 -08:00
Nikolaj Bjorner
fb1f4f3a2c add pragma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-27 18:03:06 -08:00
Nikolaj Bjorner
91d6082f2f Move modular interval to interval directory 2023-01-27 17:55:36 -08:00
Nikolaj Bjorner
ae24b73b19 bugfixes to incremental linearization for expanding power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-26 21:19:45 -08:00
Nikolaj Bjorner
8be43ca68b reshuffle pre-conditions for powers 2023-01-25 13:51:19 -08:00
Nikolaj Bjorner
e41dd91893 add module for handling axioms for powers 2023-01-25 13:34:13 -08:00
Nikolaj Bjorner
2ae476416c initial outline of exponentiation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-23 17:38:34 -08:00
Nikolaj Bjorner
d9f9cceea4 use intervals for tracking bounds on arithmetic variables 
leverage interval propagation for bounds.
merge functionality with propagate-ineqs tactic
remove the new propagate-bounds tactic and instead use propagate-ineqs
 2023-01-23 14:13:03 -08:00
Nikolaj Bjorner
eb751bec4c fix riscv/aarch/powerpc build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 23:57:59 -08:00
Nikolaj Bjorner
806a4772bc revert effect of filtering unsupported 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-20 17:28:24 -08:00
Nikolaj Bjorner
fcea32344e add missing tactic descriptions, add rewrite for tamagochi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 13:32:26 -08:00
Nikolaj Bjorner
380c701cbe restore debug clang/gcc build 2023-01-04 15:01:40 -08:00
Nikolaj Bjorner
ef10119005 #6429 fixes 2023-01-04 13:05:45 -08:00
Nuno Lopes
a2cc504d4a remove a couple more std::endl 2023-01-03 09:49:58 +00:00