4b2b6fafbe
Adds basic comparison, arithmetic and bit arithmetic to Z3 theories. Builtins depend on the kind of theory in use. Z3 builtins are the only polymorphic predicates of the engine. Change-Id: Icb68c71ec29604638282a34d34ce06f1e1d69275 Implements: blueprint alternative-engine-z3
9 lines
246 B
YAML
9 lines
246 B
YAML
---
|
|
prelude: >
|
|
features:
|
|
- |
|
|
Built-ins have been added to z3 policies. Available builtins cover
|
|
comparisons (equal, less than, greater than), basic arithmetic (plus,
|
|
minus, mul) and bitwise operations (and, or, not on bitvectors).
|
|
|