mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
18155 commits 23 branches 48 tags 157 MiB
Commit graph

18155 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
e18bc46de1 Move on_scope_exit to util.h 2022-10-07 14:23:26 +02:00
Jakob Rath
dcd6c01a90 revive polynomial superposition (wip) 2022-10-07 10:34:07 +02:00
Jakob Rath
155b746e03 side lemmas 2022-10-07 10:18:29 +02:00
Jakob Rath
bef1be8cb5 should not happen anymore 2022-10-07 10:11:00 +02:00
Jakob Rath
af368b39c9 less output 2022-10-07 10:10:44 +02:00
Jakob Rath
f184545aca Debug dlist insertion 
Found because of assertion failure in
test_polysat::test_fixed_point_arith_div_mul_inverse()
 2022-10-05 17:24:28 +02:00
Jakob Rath
e58815884f Remove debugging leftover 2022-10-04 17:10:10 +02:00
Jakob Rath
dc9373dcbd Change old solver::propagate method 2022-10-04 17:09:09 +02:00
Jakob Rath
a0fe568561 Another possible case for subsumption 2022-10-04 14:13:51 +02:00
Jakob Rath
e18dfb2253 revert_bool_decision 2022-10-04 14:13:39 +02:00
Jakob Rath
ad5c4145c1 pop non-asserting lemmas 2022-10-04 14:10:54 +02:00
Jakob Rath
46c69766d1 output 2022-10-04 14:09:57 +02:00
Jakob Rath
9cc9d1fac4 count 2022-10-04 14:08:44 +02:00
Jakob Rath
3d27ec41d0 Bring back boolean decisions (wip) 
The backtracking code doesn't know about boolean decisions yet
 2022-10-03 18:36:16 +02:00
Jakob Rath
811843cf45 Fix interval check 2022-10-03 15:35:07 +02:00
Jakob Rath
e09cf4faa5 Remove broken method 2022-10-03 11:05:07 +02:00
Jakob Rath
6caa3ba1b7 Skip redundant intervals in viable::resolve (disabled for now) 2022-10-03 11:03:05 +02:00
Jakob Rath
0b560e5117 Improve sharing 2022-10-03 10:57:56 +02:00
Jakob Rath
cd2d197bb9 Add compact version of std::all_of 2022-10-03 10:55:13 +02:00
Jakob Rath
0bea276e82 Add dll_iterator 2022-10-03 10:54:24 +02:00
Jakob Rath
05442e8788 lemma_invariant 2022-09-30 13:12:47 +02:00
Jakob Rath
5e54cd3e44 Add basic support for not, or, xor, nand, nor via rewriting 2022-09-30 13:02:32 +02:00
Jakob Rath
9b907d709f minor 2022-09-29 18:25:28 +02:00
Jakob Rath
8242069ba6 One more case for ule_constraint::is_always_false 2022-09-29 18:22:31 +02:00
Jakob Rath
6218931dde We only need one of is_true/is_false 2022-09-29 17:19:47 +02:00
Jakob Rath
79c82a3d97 update ule_constraint::is_currently_true 2022-09-29 17:02:30 +02:00
Jakob Rath
8d803a1266 Move unfinished make_asserting code 2022-09-28 19:19:33 +02:00
Jakob Rath
0dae3bad6a Fix subsumption terminology 2022-09-28 15:35:05 +02:00
Jakob Rath
7be82a36f2 Recognize x != k among new literals in lemma 2022-09-28 15:16:05 +02:00
Jakob Rath
6715058876 Simplify equations into canonical form 
Also simplify constraints that are always false due to parity
 2022-09-28 13:22:17 +02:00
Jakob Rath
480ba01cb0 Log ule rewrites 2022-09-28 11:01:23 +02:00
Jakob Rath
e08e124790 Expand always-false check 2022-09-28 10:57:40 +02:00
Jakob Rath
27b31c88d2 re-enable ule rewrite 2022-09-28 10:53:55 +02:00
Jakob Rath
d09e3eaa37 Update notes 2022-09-27 18:00:30 +02:00
Jakob Rath
0f993e3977 New constraints need to be eval'd 2022-09-27 17:56:26 +02:00
Jakob Rath
602a9e3914 test_l4b for another always-false constraint 2022-09-27 17:55:29 +02:00
Jakob Rath
74d8497ed9 Fix subsumption for unilinear case 2022-09-27 17:53:45 +02:00
Jakob Rath
1df749ad33 Merge branch 'master' into polysat 2022-09-23 17:14:26 +02:00
Jakob Rath
67c778a6da unit test notes 2022-09-23 16:53:07 +02:00
Jakob Rath
49590e0e01 Conflict from viable_fallback also depends on the current assignment 2022-09-23 16:45:56 +02:00
Jakob Rath
4e4b4fdd06 subsumption notes 2022-09-23 16:45:23 +02:00
Jakob Rath
3c60c418e7 fix assertion 2022-09-23 16:15:38 +02:00
Jakob Rath
0a0953ae78 Reduce log output 2022-09-23 16:12:39 +02:00
Jakob Rath
8ed6938cbe remove/update comment 2022-09-23 16:06:14 +02:00
Jakob Rath
4312611bd6 nicer lit_pp 2022-09-23 16:06:14 +02:00
Jakob Rath
a4f0e3a228 Add level to conflict 
- reset conflict at correct level when popping user scopes
- functions as flag when handling inconsistent input (e.g., opposite literals)
- now all constraints in the conflict core should have bvalue == l_true
 2022-09-23 16:06:14 +02:00
Jakob Rath
86d00b536a move todo notes to cpp file 2022-09-23 15:45:53 +02:00
Nikolaj Bjorner
4c6d7158cb extended debugging for sat.euf 2022-09-22 17:05:32 -05:00
Nikolaj Bjorner
c24d445886 fix #6355 
conversion from AIG to expressions should always use the optimized conversion function.

the aig-tactic should throttle regarding output bloat from AIG.
If the expression after AIG simpification, for whatever reason, is bloated the rewrite does not take place.
 2022-09-22 17:05:32 -05:00
gmh5225
b0d0c36b11
Add option 'MSVC_STATIC' (#6358) 
* Add option 'MSVC_STATIC'

* Update CMakeLists.txt

* Update CMakeLists.txt

* Upload msvc-static-build.yml
 2022-09-22 15:55:40 -05:00