mirror of
https://github.com/Z3Prover/z3
synced 2026-01-20 17:14:43 +00:00
31cbb4b144
* add examples * add lattice refutation solver class * store partial order in vector * capture partial order relations * begin with the incremental reachability data structure * implement data structure for incremental reachability * fix bug in subset propagation * add trace * only propagate if new value was added * begin implementing bitvector variant of reachability matrix * fix path creation and cycle detection * fix bug * make conflict triggering more conservative * check if theory vars are in bounds * add cycle detection (including equality propagation) * add examples * remove example * remove traces * remove sln file |
||
|---|---|---|
| .. | ||
| c | ||
| c++ | ||
| dotnet | ||
| java | ||
| maxsat | ||
| ml | ||
| python | ||
| SMT-LIB2 | ||
| tptp | ||
| userPropagator | ||
| CMakeLists.txt | ||