builtins for z3 theories

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
This commit is contained in:
Pierre Crégut 2018-10-26 14:43:20 +02:00
parent 75df78f5f2
commit 4b2b6fafbe
9 changed files with 311 additions and 73 deletions

View File

@ -170,7 +170,8 @@ class TestTypeChecker(base.TestCase):
self.world['t2'] = t2
self.rules = ast.parse(
'l(2). l(3). p(x) :- l(x). q(x,x) :- m(x). '
'm("a"). k(x) :- t2:f(x). r(y) :- q(x,y).')
'm("a"). k(x) :- t2:f(x). r(y) :- q(x,y). '
's(x) :- l(y),builtin:plus(y, 2, x).')
for rule in self.rules:
t1.insert(rule)
for rule in ast.parse("f(3)."):
@ -192,12 +193,21 @@ class TestTypeChecker(base.TestCase):
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_type_environment()
env = tc.type_env
self.assertEqual(4, len(env.keys()))
self.assertEqual(5, len(env.keys()))
for variables in six.itervalues(env):
for (v, cell) in six.iteritems(variables):
self.assertIn(v, [u'x', u'y'])
self.assertEqual(mkc(None, False), cell)
def test_reset_polymorphic_calls(self):
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_type_environment()
env = tc.type_env_builtins
rule = self.rules[7]
typ = mkc(None, False)
self.assertEqual(5, len(env.keys()))
self.assertEqual({1: [typ, typ, typ]}, env[rule.id])
def test_type_facts(self):
tc = typechecker.Typechecker([self.t1], self.world)
tc.reset_types()
@ -225,10 +235,14 @@ class TestTypeChecker(base.TestCase):
def test_type_all(self):
tc = typechecker.Typechecker([self.t1], self.world)
tc.type_all()
type_env = tc.type_all()
smap = self.t1.schema.map
self.assertEqual('Int', smap['p'][0]['type']) # propagation of l
self.assertEqual('Str', smap['q'][0]['type']) # propagation of m
self.assertEqual('Str', smap['q'][1]['type'])
self.assertEqual('Str', smap['r'][0]['type'])
self.assertEqual('Scalar', smap['k'][0]['type']) # prop of ext table
self.assertEqual('Int', smap['s'][0]['type']) # through builtins
rule = self.rules[7]
typ = mkc('Int', False)
self.assertEqual([typ, typ, typ], type_env[rule.id][1])

View File

@ -252,6 +252,17 @@ class TestZ3Context(base.TestCase):
context.declare_tables()
return (context, t1, rule)
def init_one_builtin(self, body, typ, arity):
context = z3theory.Z3Context()
world = {}
t1 = z3theory.Z3Theory('t1', theories=world)
world['t1'] = t1
context.register(t1)
rule = ast.parse('p(x) :- ' + body + '.')[0]
t1.schema.map['p'] = [mkc(typ)]
context.declare_tables()
return (context, t1, rule, {0: [mkc(typ)] * arity})
def init_one_theory(self, prog):
context = z3theory.Z3Context()
world = {}
@ -265,7 +276,7 @@ class TestZ3Context(base.TestCase):
@mockz3
def test_compile_atoms(self):
(context, t1, rule) = self.init_one_rule()
result = context.compile_atoms(t1, rule.head, rule.body)
result = context.compile_atoms({}, t1, rule.head, rule.body)
self.assertEqual(3, len(result))
(vars, head, body) = result
self.assertEqual(2, len(vars))
@ -284,10 +295,45 @@ class TestZ3Context(base.TestCase):
self.assertEqual(z3.Z3_OP_UNINTERPRETED,
body[1].children()[1].decl().kind())
@mockz3
def test_compile_binop_builtin(self):
tests = [('plus', 'bvadd'), ('minus', 'bvsub'), ('mul', 'bvmul'),
('and', 'bvand'), ('or', 'bvor')]
for (datalogName, z3Name) in tests:
(context, t1, rule, env) = self.init_one_builtin(
'builtin:' + datalogName + '(2, 3, x)', 'Int', 3)
result = context.compile_atoms(env, t1, rule.head, rule.body)
(_, _, body) = result
# two literals in the body
self.assertEqual(1, len(body))
# First body literal is l
eqExpr = body[0]
self.assertEqual('=', eqExpr.decl().name())
right = eqExpr.children()[0]
self.assertEqual(z3Name, right.decl().name())
self.assertEqual(2, right.children()[0].as_long())
self.assertEqual(3, right.children()[1].as_long())
@mockz3
def test_compile_builtin_tests(self):
tests = [('gt', 'bvsgt'), ('lt', 'bvslt'), ('gteq', 'bvsge'),
('lteq', 'bvsle'), ('equal', '=')]
for (datalogName, z3Name) in tests:
(context, t1, rule, env) = self.init_one_builtin(
'builtin:' + datalogName + '(2, x)', 'Int', 2)
result = context.compile_atoms(env, t1, rule.head, rule.body)
(_, _, body) = result
# two literals in the body
self.assertEqual(1, len(body))
# First body literal is l
testExpr = body[0]
self.assertEqual(z3Name, testExpr.decl().name())
self.assertEqual(2, testExpr.children()[0].as_long())
@mockz3
def test_compile_rule(self):
(context, t1, rule) = self.init_one_rule()
context.compile_rule(t1, rule)
context.compile_rule({}, t1, rule)
result = context.context._rules[0] # pylint: disable=E1101
self.assertEqual('forall', result.decl().name())
self.assertEqual('=>', result.children()[2].decl().name())
@ -306,14 +352,14 @@ class TestZ3Context(base.TestCase):
context = self.init_three_theories()
context.declare_tables()
context.declare_external_tables()
context.compile_theory(context.z3theories['t1'])
context.compile_theory({}, context.z3theories['t1'])
rules = context.context._rules # pylint: disable=E1101
self.assertEqual(3, len(rules))
@mockz3
def test_compile_all(self):
context = self.init_three_theories()
context.compile_all()
context.compile_all({})
rules = context.context._rules # pylint: disable=E1101
rels = context.context._relations # pylint: disable=E1101
self.assertEqual(4, len(rules))
@ -412,8 +458,8 @@ class TestTypeConstraints(base.TestCase):
@mockz3
def test_compile_all_ok(self):
context = self.init_two_theories('p("a"). p(x) :- t2:p(x).')
context.typecheck()
context.compile_all()
env = context.typecheck()
context.compile_all(env)
rules = context.context._rules # pylint: disable=E1101
self.assertEqual(2, len(rules))
@ -427,7 +473,7 @@ class TestTypeConstraints(base.TestCase):
def test_compile_fails_values(self):
context = self.init_two_theories('p("c"). p(x) :- t2:p(x).')
# Type-check succeeds
context.typecheck()
env = context.typecheck()
# But we are caught when trying to convert 'c' as a 'Small' value
self.assertRaises(exception.PolicyRuntimeException,
context.compile_all)
context.compile_all, env)

View File

@ -85,9 +85,15 @@ class ExprRef(object):
return repr(self._decl) + repr(self.args)
class BoolRef(ExprRef):
def __init__(self, decl, args):
super(BoolRef, self).__init__(decl, args)
pass
class BitVecRef(ExprRef):
def __init__(self, decl, val, sort):
super(BitVecRef, self).__init__(decl, [])
def __init__(self, decl, args, sort, val=None):
super(BitVecRef, self).__init__(decl, args)
self.val = val
self.sort = sort
@ -97,16 +103,50 @@ class BitVecRef(ExprRef):
def size(self):
return self.sort.size()
def __add__(self, b):
return BitVecRef(FuncDeclRef('bvadd', 1028), [self, b], self.sort)
def __sub__(self, b):
return BitVecRef(FuncDeclRef('bvsub', 1029), [self, b], self.sort)
def __mul__(self, b):
return BitVecRef(FuncDeclRef('bvmul', 1030), [self, b], self.sort)
def __or__(self, b):
return BitVecRef(FuncDeclRef('bvor', 1050), [self, b], self.sort)
def __and__(self, b):
return BitVecRef(FuncDeclRef('bvand', 1049), [self, b], self.sort)
def __not__(self, b):
return BitVecRef(FuncDeclRef('bvnot', 1051), [self, b], self.sort)
def __lt__(self, b):
return BoolRef(FuncDeclRef('bvslt', 1046), [self, b])
def __le__(self, b):
return BoolRef(FuncDeclRef('bvsle', 1042), [self, b])
def __gt__(self, b):
return BoolRef(FuncDeclRef('bvsgt', 1048), [self, b])
def __ge__(self, b):
return BoolRef(FuncDeclRef('bvsge', 1044), [self, b])
def __eq__(self, b):
return BoolRef(FuncDeclRef('=', 258), [self, b])
def __ne__(self, b):
return BoolRef(FuncDeclRef('distinct', 259), [self, b])
def __repr__(self):
return "bv({})".format(self.val)
return (
"bv({})".format(self.val) if self.val is not None
else super(BitVecRef, self).__repr__())
def BitVecVal(v, s):
return BitVecRef(FuncDeclRef('bv', Z3_OP_BNUM), v, s)
class BoolRef(ExprRef):
pass
return BitVecRef(FuncDeclRef('bv', Z3_OP_BNUM), [], s, v)
def BoolVal(val):

View File

@ -64,6 +64,7 @@ import six
from congress import data_types
from congress.datalog import compile as ast
from congress import exception
from congress.z3 import z3builtins
MYPY = False
# pylint: disable = ungrouped-imports
@ -76,12 +77,13 @@ if MYPY:
CELLTYPE = TypedDict(
'CELLTYPE', {'nullable': bool, 'type': Optional[str]})
GEN_TYPE_ENV = Dict[str, Dict[int, List[CELLTYPE]]]
LOG = logging.getLogger(__name__)
def min_type(name1, name2, strict):
# type: (str, str, boolean) -> Optional[str]
# type: (str, str, bool) -> Optional[str]
"""Given two type names, gives back the most precise one or None.
If one of the type is more precise than the other, give it back otherwise
@ -108,6 +110,7 @@ class Typechecker(object):
self.work = False
self.once = False
self.type_env = {} # type: Dict[str, Dict[str, CELLTYPE]]
self.type_env_builtins = {} # type: GEN_TYPE_ENV
def constrain_type(self, cell, typ):
# type: (CELLTYPE, str) -> None
@ -129,7 +132,7 @@ class Typechecker(object):
self.work = True
def type_cells(self, cell1, cell2, strict):
# type: (CELLTYPE, Union[str, CELLTYPE]) -> Optional[str]
# type: (CELLTYPE, Union[str, CELLTYPE], bool) -> Optional[str]
"""Propagates type constraints between two type cells
Updates work if a change has been made.
@ -156,18 +159,19 @@ class Typechecker(object):
if typ1 is None and typ2 is not None:
cell1['type'] = typ2
self.work = True
elif typ1 is not None and typ2 is None:
cell2['type'] = typ1
self.work = True
elif typ1 is not None: # then typ2 is not None too
if typ1 != typ2:
typ3 = min_type(typ1, typ2, strict)
if typ3 is not None:
cell1['type'] = typ3
cell2['type'] = typ3
self.work = True
else:
return "{} != {}".format(typ1, typ2)
elif typ1 is not None:
if typ2 is None:
cell2['type'] = typ1
self.work = True
else: # then typ2 is not None too
if typ1 != typ2:
typ3 = min_type(typ1, typ2, strict)
if typ3 is not None:
cell1['type'] = typ3
cell2['type'] = typ3
self.work = True
else:
return "{} != {}".format(typ1, typ2)
# else: two unresolved constraints, we do nothing
return None
@ -189,6 +193,32 @@ class Typechecker(object):
def reset_type_environment(self):
"""Reset the type environment for all variables in rules"""
def builtin_type_env(atom):
"""Generates the type of a builtin.
The builtin can be polymorphic
For a fixed type, we must tell if the type is nullable.
Nullable types must begin with character @.
"""
tablename = atom.table.table
builtin = z3builtins.BUILTINS.get(tablename)
if builtin is None:
raise exception.PolicyRuntimeException(
'Unknown builtin {}'.format(tablename))
typ_vars = [
{'type': None, 'nullable': False}
for _ in range(builtin.ty_vars)]
def cell(t):
return (
{'type': arg[1:], 'nullable': True}
if arg[0] == '@'
else {'type': arg, 'nullable': False})
return [
typ_vars[arg] if isinstance(arg, int) else cell(arg)
for arg in builtin.args
]
self.type_env = {
rule.id: {
variable.name: {'type': None, 'nullable': False}
@ -198,6 +228,16 @@ class Typechecker(object):
for ruleset in theory.rules.rules.values()
for rule in ruleset
}
self.type_env_builtins = {
rule.id: {
pos: builtin_type_env(atom)
for (pos, atom) in enumerate(rule.body)
if atom.table.service == 'builtin'
}
for theory in self.theories
for ruleset in theory.rules.rules.values()
for rule in ruleset
}
def reset_types(self):
"""Set all types in theory to typechecks to bottom"""
@ -227,18 +267,23 @@ class Typechecker(object):
"""One type iteration over a single rule"""
LOG.debug("Type rule %s", rule.id)
var_types = self.type_env[rule.id]
builtin_types = self.type_env_builtins[rule.id]
def type_atom(atom):
# type: (ast.Literal) -> None
def type_atom(atom, pos):
# type: (ast.Literal, int) -> None
"""Type iteration for a single atom"""
table = atom.table
svc = theory.name if table.service is None else table.service
tablename = table.table
if svc == 'builtin':
raise exception.PolicyRuntimeException(
'typing Z3 theories with builtin not supported yet')
strict = svc not in self.theorynames
tbl_schema = self.world[svc].schema.map[tablename]
if pos == -1:
raise exception.PolicyRuntimeException(
'builtin not authorized in rule head')
strict = False
tbl_schema = builtin_types.get(pos, []) # type: List[CELLTYPE]
else:
strict = svc not in self.theorynames
tbl_schema = self.world[svc].schema.map[tablename]
for (arg, typ_col) in six.moves.zip(atom.arguments, tbl_schema):
if isinstance(arg, ast.Variable):
typ_var = var_types[arg.name]
@ -252,11 +297,12 @@ class Typechecker(object):
elif isinstance(arg, ast.ObjectConstant) and self.once:
self.type_constant(arg.name, typ_col)
for atom in rule.body:
type_atom(atom)
type_atom(rule.head)
for (pos, atom) in enumerate(rule.body):
type_atom(atom, pos)
type_atom(rule.head, -1)
def type_all(self):
# type: () -> GEN_TYPE_ENV
"""Iterative typechecker"""
self.reset_types()
self.reset_type_environment()
@ -273,3 +319,4 @@ class Typechecker(object):
for rule in ruleset:
self.type_rule(theory, rule)
self.once = False
return self.type_env_builtins

53
congress/z3/z3builtins.py Normal file
View File

@ -0,0 +1,53 @@
# Copyright (c) 2018 Orange. All rights reserved.
#
# Licensed under the Apache License, Version 2.0 (the "License"); you may
# not use this file except in compliance with the License. You may obtain
# a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
# License for the specific language governing permissions and limitations
# under the License.
#
import collections
# BuiltinPred describes a builtin predicate
#
# @param ty_vars: the number of generic type variables
# @param args: an array describing the type of each argument of the predicate.
# It is a string for standard type and an integer for type variables in
# the range 0, ty_vars - 1.
# @param z3: a function generating the z3 code from an array coding the
# z3 arguments
BuiltinPred = collections.namedtuple(
'BuiltinPred',
['args', 'ty_vars', 'z3'])
# Warning: the z3 code operates on syntax and builds syntax. It does not
# perform an operation on the fly. This is a clever trick of z3 library
# but may puzzle the casual reader.
BUILTINS = {
# Bit arithmetic
"and": BuiltinPred(
ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x & y)),
"or": BuiltinPred(
ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x | y)),
"bnot": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: y == ~x)),
# Arithmetic (limited as it may render z3 slow in some modes)
"plus": BuiltinPred(
ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x + y)),
"minus": BuiltinPred(
ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x - y)),
"mul": BuiltinPred(
ty_vars=1, args=[0, 0, 0], z3=(lambda x, y, z: z == x * y)),
# Comparisons
"lt": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x < y)),
"lteq": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x <= y)),
"equal": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x == y)),
"gteq": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x >= y)),
"gt": BuiltinPred(ty_vars=1, args=[0, 0], z3=(lambda x, y: x > y)),
}

View File

@ -30,6 +30,7 @@ from congress.datalog import ruleset
from congress.datalog import unify
from congress import exception
from congress.z3 import typechecker
from congress.z3 import z3builtins
from congress.z3 import z3types
# pylint: disable = ungrouped-imports
@ -37,7 +38,8 @@ MYPY = False
if MYPY:
# pylint: disable = unused-import
from congress.datalog import topdown # noqa
from typing import Dict, Callable, Union, List, Any, Tuple # noqa
from mypy_extensions import TypedDict # noqa
from typing import Dict, Callable, Optional, Union, List, Any, Tuple # noqa
import z3 # noqa
Z3_RESULT = Tuple[Union[bool, List[List[z3.ExprRef]]],
List[ast.Variable],
@ -219,16 +221,16 @@ class Z3Context(object):
# There is no reset on Z3 context. Replace with a new one.
self.context = Z3OPT.Fixedpoint()
self.context.set(**Z3_ENGINE_OPTIONS)
self.typecheck()
self.compile_all()
type_env = self.typecheck()
self.compile_all(type_env)
self.synchronize_external()
z3query = self.compile_query(theory, query)
self.context.query(z3query)
z3answer = self.context.get_answer()
answer = z3types.z3_to_array(z3answer)
typ_args = theory.schema.types(query.table.table)
variables = []
translators = []
variables = [] # type: List[ast.Variable]
translators = [] # type: List[z3types.Z3Type]
for arg, typ_arg in six.moves.zip(query.arguments, typ_args):
if isinstance(arg, ast.Variable) and arg not in variables:
translators.append(
@ -286,7 +288,8 @@ class Z3Context(object):
"""Declares the table of a litteral if necessary"""
service = lit.table.service
table = lit.table.table
if service is not None and service not in self.z3theories:
if (service is not None and service != 'builtin' and
service not in self.z3theories):
self.externals.add((service, table))
for theory in six.itervalues(self.z3theories):
for rules in six.itervalues(theory.rules.rules):
@ -312,6 +315,7 @@ class Z3Context(object):
self.context.fact(z3fact)
def compile_atoms(self,
type_env,
theory, # type: Z3Theory
head, # type: ast.Literal
body # type: List[ast.Literal]
@ -340,20 +344,26 @@ class Z3Context(object):
raise exception.PolicyException(
"Expr {} not handled by Z3".format(expr))
def compile_atom(literal):
def compile_atom(literal, pos=-1):
"""Compiles an atom in Z3"""
name = literal.table.table
svc = literal.table.service
if svc == 'builtin':
raise exception.PolicyException(
"Builtins not handled by Z3 yet")
lit_theory = theory if svc is None else self.theories[svc]
translators = [
self.type_registry.get_translator(str(arg_type.type))
for arg_type in lit_theory.schema.types(name)]
fullname = lit_theory.name + ":" + name
translators = [
self.type_registry.get_translator(str(arg_type['type']))
for arg_type in type_env[pos]
]
fullname = 'builtin:'+name
else:
lit_theory = theory if svc is None else self.theories[svc]
translators = [
self.type_registry.get_translator(str(arg_type.type))
for arg_type in lit_theory.schema.types(name)]
fullname = lit_theory.name + ":" + name
try:
z3func = self.relations[fullname]
z3func = (
z3builtins.BUILTINS[name].z3 if svc == 'builtin'
else self.relations[fullname])
z3args = (compile_expr(arg, tr)
for (arg, tr) in six.moves.zip(literal.arguments,
translators))
@ -365,20 +375,20 @@ class Z3Context(object):
"Z3: Relation %s not registered" % fullname)
z3head = compile_atom(head)
z3body = [compile_atom(atom) for atom in body]
z3body = [compile_atom(atom, pos) for (pos, atom) in enumerate(body)]
# We give back variables explicitely and do not rely on declare_var and
# abstract. Otherwise rules are cluttered with useless variables.
return (z3vars, z3head, z3body)
def compile_rule(self, theory, rule):
# type: (Z3Theory, ast.Rule) -> None
def compile_rule(self, type_env, theory, rule):
# type: (typechecker.GEN_TYPE_ENV, Z3Theory, ast.Rule) -> None
"""compiles a single rule
:param theory: the theory containing the rule
:param rule: the rule to compile.
"""
z3vars, z3head, z3body = self.compile_atoms(theory, rule.head,
rule.body)
z3vars, z3head, z3body = self.compile_atoms(
type_env.get(rule.id, {}), theory, rule.head, rule.body)
term1 = (z3head if z3body == []
else Z3OPT.Implies(Z3OPT.And(*z3body), z3head))
term2 = term1 if z3vars == [] else Z3OPT.ForAll(z3vars, term1)
@ -392,11 +402,11 @@ class Z3Context(object):
:param litteral: the query
:returns: an existentially quantified litteral in Z3 format.
"""
z3vars, z3head, _ = self.compile_atoms(theory, literal, [])
z3vars, z3head, _ = self.compile_atoms({}, theory, literal, [])
return z3head if z3vars == [] else Z3OPT.Exists(z3vars, z3head)
def compile_theory(self, theory):
# type: (Z3Theory) -> None
def compile_theory(self, type_env, theory):
# type: (typechecker.GEN_TYPE_ENV, Z3Theory) -> None
"""Compiles all the rules of a theory
:param theory: theory to compile. Will be marked clean after.
@ -404,24 +414,24 @@ class Z3Context(object):
self.compile_facts(theory)
for rules in six.itervalues(theory.rules.rules):
for rule in rules:
self.compile_rule(theory, rule)
self.compile_rule(type_env, theory, rule)
theory.dirty = False
def compile_all(self):
def compile_all(self, type_env):
"""Compile all Z3 theories"""
self.relations = {}
self.externals.clear()
self.declare_tables()
self.declare_external_tables()
for theory in six.itervalues(self.z3theories):
self.compile_theory(theory)
self.compile_theory(type_env, theory)
self.last_compiled = time.time()
def typecheck(self):
"""Typechecker for rules defined"""
typer = typechecker.Typechecker(
self.z3theories.values(), self.theories)
typer.type_all()
return typer.type_all()
def inject(self, theoryname, tablename):
# type: (str, str) -> None

View File

@ -45,7 +45,7 @@ class Z3Type(object):
@abc.abstractmethod
def to_z3(self, val, strict=False):
# type: (Any) -> z3.ExprRef
# type: (Any, bool) -> z3.ExprRef
"""Transforms a value from OpenStack in a Z3 value"""
raise NotImplementedError

View File

@ -503,12 +503,32 @@ Z3 imposes a different set of restrictions on the Datalog language. First
it lifts the recursivity restriction of the internal engine and supports
stratified negation.
But z3 policies do not support the set of builtins of regular policies. Some
builtins will be supported in the future.
But z3 policies do not support the set of builtins of regular policies.
Supported builtins are:
============== =======================================================
Builtins Description
============== =======================================================
lt(x, y) True if x < y
lteq(x, y) True if x <= y
equal(x, y) True if x == y
gt(x, y) True if x > y
gteq(x, y) True if x >= y
plus(x, y, z) z = x + y
minus(x, y, z) z = x - y
mul(x, y, z) z = x * y
or(x, y, z) z = x | y (bitwise or)
and(x, y, z) z = x & y (bitwise and)
bnot(x, y) y = ~x (bitwise not)
============== =======================================================
As for regular theories, all builtins are referenced in rules using the
prefix *builtin:*.
Z3 is a typed Datalog engine. Although the type-checking engine silently
infer types, it may refuse some policies that mix columns of different
types.
types. Internally Z3 codes everything as bitvectors and the integer type
is in fact a 32 bitvector type.
3. Multiple Policies
====================

View File

@ -0,0 +1,8 @@
---
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).