summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xsrc/theory/rewriter/compiler.py172
-rw-r--r--src/theory/rewriter/node.py56
-rw-r--r--src/theory/rewriter/parser.py19
-rw-r--r--src/theory/rewriter/rules/basic.rules79
4 files changed, 246 insertions, 80 deletions
diff --git a/src/theory/rewriter/compiler.py b/src/theory/rewriter/compiler.py
index 20e34f7b1..0e8e98315 100755
--- a/src/theory/rewriter/compiler.py
+++ b/src/theory/rewriter/compiler.py
@@ -32,6 +32,8 @@ op_to_kind = {
Op.BVUREM: 'BITVECTOR_UREM_TOTAL',
Op.BVSMOD: 'BITVECTOR_SMOD',
Op.BVSHL: 'BITVECTOR_SHL',
+ Op.BVLSHR: 'BITVECTOR_LSHR',
+ Op.BVASHR: 'BITVECTOR_ASHR',
Op.ROTATE_LEFT: 'BITVECTOR_ROTATE_LEFT',
Op.ROTATE_RIGHT: 'BITVECTOR_ROTATE_RIGHT',
Op.BVNOT: 'BITVECTOR_NOT',
@@ -58,11 +60,14 @@ op_to_kind = {
op_to_const_eval = {
Op.BVSHL: '({}.leftShift({}))',
+ Op.EXTRACT: '({2}.extract({0}, {1}))',
Op.BVNOT: '(~{})',
Op.PLUS: '({} + {})',
Op.MINUS: '({} - {})',
+ Op.LT: '({} < {})',
Op.GEQ: '({} >= {})',
Op.NOT: '(!{})',
+ Op.AND: '({} && {})',
Op.EQ: '({} == {})',
}
@@ -104,6 +109,8 @@ op_to_nindex = {
Op.BVUREM: 0,
Op.BVSMOD: 0,
Op.BVSHL: 0,
+ Op.BVLSHR: 0,
+ Op.BVASHR: 0,
Op.ROTATE_LEFT: 1,
Op.ROTATE_RIGHT: 1,
Op.BVNOT: 0,
@@ -140,11 +147,16 @@ def mk_simple_block(cfg, next_block, instr):
def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs):
- def expr_to_ir(const_checks, next_block, expr, node, vars_seen, in_loop=False):
+ def expr_to_ir(const_checks,
+ next_block,
+ expr,
+ node,
+ vars_seen,
+ in_loop=False):
if isinstance(expr, Var):
if expr.name in vars_seen:
- return mk_simple_block(cfg, next_block,
- Assert(Fn(Op.EQ, [expr, node]), in_loop))
+ return mk_simple_block(
+ cfg, next_block, Assert(Fn(Op.EQ, [expr, node]), in_loop))
else:
if expr.sort is not None and expr.sort.base == BaseSort.BitVec:
width = expr.sort.children[0]
@@ -164,20 +176,41 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs):
elif expr.sort.const:
if isinstance(expr, Fn) and expr.op == Op.BVCONST:
- # bvval =
+ # bvval =
# next_block = mk_simple_block(
# cfg, next_block,
# Assert(
# Fn(Op.EQ,
# [Fn(Op.GET_KIND, [node]),
# KindConst(expr.op)]), in_loop))
- return mk_simple_block(
+
+ if isinstance(expr.children[0],
+ Var) and expr.children[0] not in vars_seen:
+ next_block = mk_simple_block(
+ cfg, next_block,
+ Assign(expr.children[0], Fn(Op.BV_SIZE, [node])))
+
+ next_block = expr_to_ir(const_checks, next_block,
+ expr.children[0],
+ Fn(Op.BV_SIZE,
+ [node]), vars_seen, in_loop)
+
+ if isinstance(expr.children[1],
+ Var) and expr.children[1] not in vars_seen:
+ next_block = expr_to_ir(const_checks, next_block,
+ expr.children[1],
+ Fn(Op.BV_SIZE,
+ [node]), vars_seen, in_loop)
+
+ next_block = mk_simple_block(
cfg, next_block,
Assert(
Fn(Op.EQ,
[Fn(Op.GET_KIND, [node]),
KindConst(expr.op)]), in_loop))
+ return next_block
+
# TODO: node.sort should not be None
instr = None
if node.sort and node.sort.const:
@@ -185,19 +218,27 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs):
else:
instr = Fn(Op.EQ, [node, Fn(Op.MK_CONST, [expr])])
- return mk_simple_block(
- cfg, next_block,
- Assert(instr, in_loop))
+ return mk_simple_block(cfg, next_block, Assert(instr, in_loop))
elif isinstance(expr, Fn):
if expr.op in commutative_ops:
- nlist_children = [child for child in expr.children if child.sort.base != BaseSort.List]
- loop_idxs = [Var(fresh_name('loopi'), Sort(BaseSort.Int, [], True)) for _ in nlist_children]
+ nlist_children = [
+ child for child in expr.children
+ if child.sort.base != BaseSort.List
+ ]
+ loop_idxs = [
+ Var(fresh_name('loopi'), Sort(BaseSort.Int, [], True))
+ for _ in nlist_children
+ ]
# Assign the remainder of the list
if len(nlist_children) != len(expr.children):
- list_child = next(child for child in expr.children if child.sort.base == BaseSort.List)
- next_block = mk_simple_block(cfg, next_block, Assign(list_child, Fn(Op.GET_CHILDREN, [node] + loop_idxs)))
+ list_child = next(child for child in expr.children
+ if child.sort.base == BaseSort.List)
+ next_block = mk_simple_block(
+ cfg, next_block,
+ Assign(list_child,
+ Fn(Op.GET_CHILDREN, [node] + loop_idxs)))
for i, child in reversed(list(enumerate(nlist_children))):
sub_expr_vars_seen = vars_seen.copy()
@@ -205,18 +246,22 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs):
sub_expr_vars_seen |= collect_vars(child2)
loop_idx = loop_idxs[i]
- loop_var = Var(fresh_name('loopv'), child.sort)
- next_block = expr_to_ir(const_checks, next_block, child, loop_var, sub_expr_vars_seen, True)
- next_block = mk_simple_block(cfg, next_block, Assign(loop_var, Fn(
- Op.GET_CHILD,
- [node, loop_idx])))
+ loop_var_sort = Sort(child.sort.base, child.sort.children)
+ loop_var = Var(fresh_name('loopv'), loop_var_sort)
+ next_block = expr_to_ir(const_checks, next_block, child,
+ loop_var, sub_expr_vars_seen, True)
+ next_block = mk_simple_block(
+ cfg, next_block,
+ Assign(loop_var, Fn(Op.GET_CHILD, [node, loop_idx])))
for j in range(i):
- check = Fn(Op.NOT, [Fn(Op.EQ, [loop_idx, loop_idxs[j]])])
+ check = Fn(Op.NOT,
+ [Fn(Op.EQ, [loop_idx, loop_idxs[j]])])
# Use infer types
check.sort = Sort(BaseSort.Bool, [], True)
check.children[0].sort = Sort(BaseSort.Bool, [], True)
- next_block = mk_simple_block(cfg, next_block, Assert(check, True))
+ next_block = mk_simple_block(cfg, next_block,
+ Assert(check, True))
loop_block = fresh_name('loop')
cfg[loop_block] = CFGLoop(loop_idx, node, next_block)
@@ -234,17 +279,16 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs):
else:
child_node = Fn(
Op.GET_CHILD,
- [node,
- IntConst(i - op_to_nindex[expr.op])])
- next_block = expr_to_ir(const_checks, next_block, child, child_node,
- sub_expr_vars_seen, in_loop)
+ [node, IntConst(i - op_to_nindex[expr.op])])
+ next_block = expr_to_ir(const_checks, next_block, child,
+ child_node, sub_expr_vars_seen,
+ in_loop)
return mk_simple_block(
cfg, next_block,
Assert(
- Fn(Op.EQ,
- [Fn(Op.GET_KIND, [node]),
- KindConst(expr.op)]), in_loop))
+ Fn(Op.EQ, [Fn(Op.GET_KIND, [node]),
+ KindConst(expr.op)]), in_loop))
elif isinstance(expr, BVConst):
assert False
@@ -269,9 +313,10 @@ def rule_to_in_ir(cfg, out_block, node_var, rvars, lhs):
vars_seen = set()
const_check_block = fresh_name('block')
const_checks = []
- entry = expr_to_ir(const_checks, const_check_block, lhs, node_var, vars_seen)
+ entry = expr_to_ir(const_checks, const_check_block, lhs, node_var,
+ vars_seen)
cfg[const_check_block] = CFGNode(const_checks,
- [CFGEdge(BoolConst(True), out_block)])
+ [CFGEdge(BoolConst(True), out_block)])
return entry
@@ -298,16 +343,19 @@ def rule_to_out_expr(cfg, next_block, res, expr):
cfg[cond_block] = CFGNode([], edges)
return cond_block
elif expr.op == Op.FAIL:
- return mk_simple_block(cfg, next_block, Assert(BoolConst(False), False))
+ return mk_simple_block(cfg, next_block,
+ Assert(BoolConst(False), False))
elif expr.op == Op.LET:
next_block = rule_to_out_expr(cfg, next_block, res,
expr.children[2])
- next_block = rule_to_out_expr(cfg, next_block, expr.children[0],
+ next_block = rule_to_out_expr(cfg, next_block,
+ expr.children[0],
expr.children[1])
return next_block
elif expr.op == Op.BVCONST:
new_vars = [
- Var(fresh_name('__v'), child.sort) for child in expr.children
+ Var(fresh_name('__v'), child.sort)
+ for child in expr.children
]
bvc = Fn(Op.BVCONST, new_vars)
bvc.sort = expr.sort
@@ -330,14 +378,18 @@ def rule_to_out_expr(cfg, next_block, res, expr):
return next_block
else:
new_vars = [
- Var(fresh_name('__v'), child.sort) for child in expr.children
+ Var(fresh_name('__v'), child.sort)
+ for child in expr.children
]
assign = None
if expr.sort.const:
fn = Fn(expr.op, new_vars)
fn.sort = expr.sort
- assign = Assign(res, fn)
+ if res.sort and res.sort.const:
+ assign = Assign(res, fn)
+ else:
+ assign = Assign(res, Fn(Op.MK_CONST, [fn]))
else:
# If we have a non-constant expression with constant arguments,
# we have to cast the constant arguments to terms
@@ -347,6 +399,7 @@ def rule_to_out_expr(cfg, next_block, res, expr):
new_args.append(Fn(Op.MK_CONST, [new_var]))
else:
new_args.append(new_var)
+
assign = Assign(
res, Fn(Op.MK_NODE, [KindConst(expr.op)] + new_args))
@@ -366,8 +419,8 @@ def rule_to_out_expr(cfg, next_block, res, expr):
res.sort = Sort(BaseSort.Bool, [])
assign = Assign(res, expr)
if next_block:
- cfg[assign_block] = CFGNode([assign],
- [CFGEdge(BoolConst(True), next_block)])
+ cfg[assign_block] = CFGNode(
+ [assign], [CFGEdge(BoolConst(True), next_block)])
else:
assign.expr = Fn(Op.MK_CONST, [assign.expr])
cfg[assign_block] = CFGNode([assign], [])
@@ -377,8 +430,8 @@ def rule_to_out_expr(cfg, next_block, res, expr):
res.sort = Sort(BaseSort.Int, [], True)
assign = Assign(res, expr)
if next_block:
- cfg[assign_block] = CFGNode([assign],
- [CFGEdge(BoolConst(True), next_block)])
+ cfg[assign_block] = CFGNode(
+ [assign], [CFGEdge(BoolConst(True), next_block)])
else:
cfg[assign_block] = CFGNode([assign], [])
return assign_block
@@ -387,8 +440,8 @@ def rule_to_out_expr(cfg, next_block, res, expr):
assign = Assign(res, expr)
res.sort = expr.sort
if next_block:
- cfg[assign_block] = CFGNode([assign],
- [CFGEdge(BoolConst(True), next_block)])
+ cfg[assign_block] = CFGNode(
+ [assign], [CFGEdge(BoolConst(True), next_block)])
else:
cfg[assign_block] = CFGNode([assign], [])
return assign_block
@@ -414,16 +467,38 @@ def expr_to_code(expr):
return 'nm->mkConst({})'.format(', '.join(args))
elif expr.op == Op.MK_NODE:
kind = expr.children[0].val
- if op_to_nindex[kind] != 0:
- op = 'bv::utils::mkIndexedOp({})'.format(', '.join(args[:op_to_nindex[kind] + 1]))
- return 'nm->mkNode({})'.format(', '.join([op] + args[op_to_nindex[kind] + 1:]))
+
+ list_arg = None
+ for child in expr.children:
+ if child.sort and child.sort.base == BaseSort.List:
+ list_arg = child.sort
+ break
+
+ arg_str = None
+ if list_arg:
+ vec = fresh_name('__vec')
+ arg_str = '{}, '.format(args[0])
+ arg_str += '[&](){{ std::vector<Node> {0}; {1}; return {0}; }}()'.format(
+ vec, ';'.join(
+ ('{}.push_back({})'.format(vec, arg)
+ if child.sort and child.sort.base != BaseSort.List
+ else '{0}.insert({0}.end(), {1}.begin(), {1}.end())'.
+ format(vec, arg))
+ for arg, child in zip(args[1:], expr.children[1:])))
+ elif op_to_nindex[kind] != 0:
+ op = 'bv::utils::mkIndexedOp({})'.format(', '.join(
+ args[:op_to_nindex[kind] + 1]))
+ arg_str = ', '.join([op] + args[op_to_nindex[kind] + 1:])
else:
- return 'nm->mkNode({})'.format(', '.join(args))
+ arg_str = ', '.join(args)
+
+ return 'nm->mkNode({})'.format(arg_str)
elif expr.op == Op.GET_CHILD:
return '{}[{}]'.format(args[0], args[1])
elif expr.op == Op.GET_CHILDREN:
cond = ' && '.join('i != {}'.format(arg) for arg in args[1:])
- return 'bv::utils::getChildren({}, [&](size_t i) {{ return {}; }})'.format(args[0], cond)
+ return 'bv::utils::getChildren({}, [&](size_t i) {{ return {}; }})'.format(
+ args[0], cond)
elif expr.op == Op.GET_INDEX:
return 'bv::utils::getIndex({}, {})'.format(args[0], args[1])
elif expr.sort and expr.sort.const:
@@ -465,9 +540,8 @@ def ir_to_code(match_instrs):
expr_to_code(instr.expr)))
elif isinstance(instr, Assert):
exit = 'continue' if instr.in_loop else 'return RewriteResponse(REWRITE_DONE, __node, RewriteRule::NONE)'
- code.append(
- 'if (!({})) {};'
- .format(expr_to_code(instr.expr), exit))
+ code.append('if (!({})) {};'.format(expr_to_code(instr.expr),
+ exit))
return '\n'.join(code)
@@ -478,7 +552,9 @@ def cfg_to_code(block, cfg):
return """
for ({} = 0; {} < {}.getNumChildren(); {}++) {{
{}
- }}""".format(cfg[block].loop_var, cfg[block].loop_var, cfg[block].domain, cfg[block].loop_var, body)
+ }}""".format(cfg[block].loop_var, cfg[block].loop_var,
+ expr_to_code(cfg[block].domain), cfg[block].loop_var,
+ body)
else:
result = ir_to_code(cfg[block].instrs)
first_edge = True
diff --git a/src/theory/rewriter/node.py b/src/theory/rewriter/node.py
index 8a69b3896..09ccd47ac 100644
--- a/src/theory/rewriter/node.py
+++ b/src/theory/rewriter/node.py
@@ -31,6 +31,8 @@ class Op(Enum):
# Bit-vector shifts
BVSHL = auto()
+ BVLSHR = auto()
+ BVASHR = auto()
ROTATE_LEFT = auto()
ROTATE_RIGHT = auto()
@@ -69,6 +71,7 @@ class Op(Enum):
PLUS = auto()
MINUS = auto()
MULT = auto()
+ LT = auto()
GEQ = auto()
###########################################################################
@@ -89,6 +92,7 @@ class Op(Enum):
MK_NODE = auto()
MK_CONST = auto()
BV_SIZE = auto()
+ APPEND = auto()
###########################################################################
# Language operators
@@ -102,8 +106,9 @@ class Op(Enum):
LET = auto()
FAIL = auto()
-commutative_ops = set([Op.AND, Op.XOR, Op.EQ])
-nary_ops = set([Op.AND])
+
+commutative_ops = set([Op.BVADD, Op.BVXOR, Op.AND, Op.XOR, Op.EQ])
+nary_ops = set([Op.BVADD, Op.AND])
class BaseSort(Enum):
@@ -247,9 +252,8 @@ class Sort(Node):
def __repr__(self):
return '({} {}{})'.format(
- self.base, ' '.join(
- str(child)
- for child in self.children), ' :const' if self.const else '')
+ self.base, ' '.join(str(child) for child in self.children),
+ ' :const' if self.const else '')
def collect_vars(node):
@@ -294,6 +298,16 @@ def unify_types(t1, t2):
return t1
+def are_types_compatible(t1, t2):
+ if t1.base == t2.base:
+ return True
+ if t1.base == BaseSort.List:
+ return are_types_compatible(t1.children[0], t2)
+ elif t2.base == BaseSort.List:
+ return are_types_compatible(t1, t2.children[0])
+ return False
+
+
def infer_types(context, node):
if node.sort:
return
@@ -323,14 +337,21 @@ def infer_types(context, node):
assert node.children[0].sort.base == BaseSort.BitVec
assert node.children[0].sort == node.children[1].sort
sort = Sort(BaseSort.Bool, [])
- elif node.op in [
- Op.BVREDAND, Op.BVREDOR
- ]:
+ elif node.op in [Op.BVREDAND, Op.BVREDOR]:
assert node.children[0].sort.base == BaseSort.BitVec
sort = Sort(BaseSort.Bool, [])
- elif node.op in [Op.BVADD, Op.BVSUB, Op.BVSDIV, Op.BVUDIV, Op.BVSREM, Op.BVUREM, Op.BVSMOD, Op.BVSHL, Op.BVAND, Op.BVOR, Op.BVXOR, Op.BVNAND, Op.BVNOR, Op.BVXNOR]:
- assert node.children[0].sort.base == BaseSort.BitVec
- assert node.children[0].sort == node.children[1].sort
+ elif node.op in [
+ Op.BVADD, Op.BVSUB, Op.BVSDIV, Op.BVUDIV, Op.BVSREM, Op.BVUREM,
+ Op.BVSMOD, Op.BVSHL, Op.BVLSHR, Op.BVASHR, Op.BVAND, Op.BVOR,
+ Op.BVXOR, Op.BVNAND, Op.BVNOR, Op.BVXNOR
+ ]:
+ assert node.children[0].sort.base == BaseSort.BitVec or (
+ node.children[0].sort.base == BaseSort.List
+ and node.children[0].sort.children[0].base == BaseSort.BitVec)
+ arg_sort = node.children[0].sort
+ assert all(
+ are_types_compatible(arg_sort, child.sort)
+ for child in node.children)
sort = Sort(BaseSort.BitVec, [node.children[0].sort.children[0]])
elif node.op in [Op.ROTATE_LEFT, Op.ROTATE_RIGHT]:
assert node.children[0].sort.base == BaseSort.Int
@@ -367,8 +388,10 @@ def infer_types(context, node):
assert node.children[1].sort.base == BaseSort.Int
assert node.children[2].sort.base == BaseSort.BitVec
sort = Sort(BaseSort.BitVec, [
- Fn(Op.PLUS, [Fn(Op.MINUS,
- [node.children[0], node.children[1]]), IntConst(1)])
+ Fn(Op.PLUS, [
+ Fn(Op.MINUS, [node.children[0], node.children[1]]),
+ IntConst(1)
+ ])
])
elif node.op in [Op.BVNEG, Op.BVNOT]:
assert node.children[0].sort.base == BaseSort.BitVec
@@ -410,7 +433,7 @@ def infer_types(context, node):
assert node.children[0].sort.base == BaseSort.Int
assert node.children[1].sort.base == BaseSort.Int
sort = Sort(BaseSort.Int, [])
- elif node.op in [Op.GEQ]:
+ elif node.op in [Op.LT, Op.GEQ]:
assert node.children[0].sort.base == BaseSort.Int
assert node.children[1].sort.base == BaseSort.Int
sort = Sort(BaseSort.Bool, [])
@@ -419,7 +442,10 @@ def infer_types(context, node):
assert node.children[1].sort.base == BaseSort.Bool
sort = Sort(BaseSort.Bool, [])
elif node.op in [Op.AND]:
- assert all(child.sort.base == BaseSort.Bool or (child.sort.base == BaseSort.List and child.sort.children[0].base == BaseSort.Bool) for child in node.children)
+ assert all(child.sort.base == BaseSort.Bool or (
+ child.sort.base == BaseSort.List
+ and child.sort.children[0].base == BaseSort.Bool)
+ for child in node.children)
# TODO: Check that list is used correctly
sort = Sort(BaseSort.Bool, [])
elif node.op == Op.FAIL:
diff --git a/src/theory/rewriter/parser.py b/src/theory/rewriter/parser.py
index f6a4673de..7bfeeb5f4 100644
--- a/src/theory/rewriter/parser.py
+++ b/src/theory/rewriter/parser.py
@@ -23,6 +23,8 @@ symbol_to_op = {
'bvurem': Op.BVUREM,
'bvsmod': Op.BVSMOD,
'bvshl': Op.BVSHL,
+ 'bvlshr': Op.BVLSHR,
+ 'bvashr': Op.BVASHR,
'rotate_left': Op.ROTATE_LEFT,
'rotate_right': Op.ROTATE_RIGHT,
'bvnot': Op.BVNOT,
@@ -45,6 +47,7 @@ symbol_to_op = {
'xor': Op.XOR,
'+': Op.PLUS,
'-': Op.MINUS,
+ '<': Op.LT,
'>=': Op.GEQ,
'=': Op.EQ,
'ite': Op.ITE,
@@ -60,14 +63,16 @@ def symbol():
special_chars = '=' + '_' + '+' + '-' + '<' + '>'
return pp.Word(pp.alphas + special_chars, pp.alphanums + special_chars)
+
def mk_let(let):
body = let[-1]
for binding in reversed(let[0:-1]):
body = Fn(Op.LET, [binding[0], binding[1], body])
return body
+
def mk_case(cases):
- if cases[-1].op != Op.CASE:
+ if not isinstance(cases[-1], Fn) or cases[-1].op != Op.CASE:
cases[-1] = Fn(Op.CASE, [BoolConst(True), cases[-1]])
else:
cases.append(Fn(Op.CASE, [BoolConst(True), Fn(Op.FAIL, [])]))
@@ -99,11 +104,11 @@ def expr():
).setParseAction(lambda s, l, t: Fn(symbol_to_op[t[0]], t[1:]))
# Let bindings
- binding = (pp.Suppress('(') + var + expr + pp.Suppress(')')
- ).setParseAction(lambda s, l, t: (t[0], t[1]))
+ binding = (pp.Suppress('(') + var + expr +
+ pp.Suppress(')')).setParseAction(lambda s, l, t: (t[0], t[1]))
let = (pp.Suppress('(') + pp.Keyword('let') + pp.Suppress('(') +
- pp.OneOrMore(binding) + pp.Suppress(')') + expr + pp.Suppress(')')
- ).setParseAction(lambda s, l, t: mk_let(t[1:]))
+ pp.OneOrMore(binding) + pp.Suppress(')') + expr +
+ pp.Suppress(')')).setParseAction(lambda s, l, t: mk_let(t[1:]))
# Conditionals
case = (pp.Suppress('(') + expr + expr + pp.Suppress(')')
@@ -139,9 +144,11 @@ def process_var_decl(name, sort, attrs):
def attrs():
return pp.Keyword(':list') | pp.Keyword(':const')
+
def var_decl():
return (pp.Suppress('(') + symbol() + sort() + pp.ZeroOrMore(attrs()) +
- pp.Suppress(')')).setParseAction(lambda s, l, t: process_var_decl(t[0], t[1], t[2:]))
+ pp.Suppress(')')).setParseAction(
+ lambda s, l, t: process_var_decl(t[0], t[1], t[2:]))
def var_list():
diff --git a/src/theory/rewriter/rules/basic.rules b/src/theory/rewriter/rules/basic.rules
index 19a712c97..0d39f8050 100644
--- a/src/theory/rewriter/rules/basic.rules
+++ b/src/theory/rewriter/rules/basic.rules
@@ -31,6 +31,13 @@
((_ extract i j) (bvnot x))
(bvnot ((_ extract i j) x)))
+(define-rule ExtractSignExtend ((i Int :const) (j Int :const) (k Int :const) (n Int :const) (x (_ BitVec n)))
+ ((_ extract i j) ((_ sign_extend k) x))
+ (cond
+ ((< i n) ((_ extract i j) x))
+ ((and (< j n) (>= i n)) ((_ sign_extend (+ (- i n) 1)) ((_ extract (- n 1) j) x)))
+ (true ((_ repeat (+ (- i j) 1)) ((_ extract (- n 1) (- n 1)) x)))))
+
/******************************************************************************
* Operator Elimination
******************************************************************************/
@@ -167,25 +174,21 @@
* Simplification
******************************************************************************/
-/*
(define-rule BvIteConstCond ((m Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
(bvite (_ bv m 1) x y)
(cond
((= m 1) x)
y))
-*/
(define-rule BvIteEqualChildren ((c (_ BitVec 1)) (x (_ BitVec m)))
(bvite c x x)
x)
-/*
-(define-rule BvIteConstChildren ((n Int) (m Int) (x (_ BitVec o)))
+(define-rule BvIteConstChildren ((n Int :const) (m Int :const) (x (_ BitVec o)))
(bvite x (_ bv n 1) (_ bv m 1))
(cond
((and (= n 1) (= m 0)) x)
- (bvnot x)))
-*/
+ (true (bvnot x))))
(define-rule BvIteEqualCondThen ((c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
(bvite c (bvite c x y) z)
@@ -211,10 +214,11 @@
(bvite c0 x (bvite c1 y x))
(bvite (bvand (bvnot c0) c1) y x))
-/*
-(define-rule BvComp ((n Int) (x (_ BitVec 1)))
+(define-rule BvComp ((n Int :const) (x (_ BitVec 1)))
(bvcomp (_ bv n 1) x)
- (ite (= n 0) (bvnot x) x))
+ (cond
+ ((= n 0) (bvnot x))
+ x))
(define-rule ShlByConst ((n Int :const) (m Int :const) (x (_ BitVec m)))
(bvshl x (_ bv n m))
@@ -222,13 +226,20 @@
((= n 0) x)
((>= n m) (_ bv 0 m))
(concat ((_ extract (- m (+ n 1)) 0) x) (_ bv 0 n))))
-*/
/*
+(define-rule XorOne ((n Int :const) (xs (_ BitVec n) :list))
+ (bvxor (bvnot (_ bv 0 n)) xs)
+ (bvxor xs))
+*/
+
+(define-rule XorZero ((n Int :const) (xs (_ BitVec n) :list))
+ (bvxor (_ bv 0 n) xs)
+ (bvxor xs))
+
(define-rule NotXor ((x (_ BitVec n)) (xs (_ BitVec n) :list))
(bvnot (bvxor x xs))
(bvxor (bvnot x) xs))
-*/
(define-rule NotIdemp ((x (_ BitVec n)))
(bvnot (bvnot x))
@@ -250,11 +261,31 @@
(bvsle x x)
true)
+(define-rule ZeroUlt ((n Int :const) (x (_ BitVec n)))
+ (bvult (_ bv 0 n) x)
+ (not (= (_ bv 0 n) x)))
+
+(define-rule UltZero ((n Int :const) (x (_ BitVec n)))
+ (bvult x (_ bv 0 n))
+ false)
+
+(define-rule UltOne ((n Int :const) (x (_ BitVec n)))
+ (bvult x (_ bv 1 n))
+ (= x (_ bv 0 n)))
+
+(define-rule SltZero ((n Int :const) (x (_ BitVec n)))
+ (bvslt x (_ bv 0 n))
+ (= ((_ extract (- n 1) (- n 1)) x) (_ bv 1 1)))
+
/* Note: Duplicate of LtSelfUlt */
(define-rule UltSelf ((x (_ BitVec n)))
(bvult x x)
false)
+(define-rule UleZero ((n Int :const) (x (_ BitVec n)))
+ (bvule x (_ bv 0 n))
+ (= x (_ bv 0 n)))
+
/* Note: Duplicate of LteSelfUle */
(define-rule UleSelf ((x (_ BitVec n)))
(bvule x x)
@@ -290,10 +321,26 @@
(bvudiv x (_ bv 1 n))
x)
+(define-rule UremOne ((n Int :const) (x (_ BitVec n)))
+ (bvudiv x (_ bv 1 n))
+ (_ bv 0 n))
+
(define-rule UremSelf ((n Int :const) (x (_ BitVec n)))
(bvudiv x x)
(_ bv 0 n))
+(define-rule ShiftZeroShl ((n Int :const) (x (_ BitVec n)))
+ (bvshl (_ bv 0 n) x)
+ (_ bv 0 n))
+
+(define-rule ShiftZeroLshr ((n Int :const) (x (_ BitVec n)))
+ (bvlshr (_ bv 0 n) x)
+ (_ bv 0 n))
+
+(define-rule ShiftZeroAshr ((n Int :const) (x (_ BitVec n)))
+ (bvashr (_ bv 0 n) x)
+ (_ bv 0 n))
+
(define-rule MergeSignExtendSign ((i Int :const) (j Int :const) (n Int :const) (x (_ BitVec n)))
((_ sign_extend i) ((_ sign_extend j) x))
((_ sign_extend (+ i j)) x))
@@ -304,6 +351,16 @@
((= j 0) ((_ sign_extend i) x))
(true ((_ zero_extend (+ i j)) x))))
+(define-rule ZeroExtendEqConst ((i Int :const) (n Int :const) (m Int :const) (x (_ BitVec n)))
+ (= ((_ zero_extend i) x) (_ bv m n))
+ (cond
+ ((= ((_ extract (- (+ n m) 1) n) (_ bv m n)) (_ bv 0 n)) (= x ((_ extract (- n 1) 0) (_ bv m n))))
+ false))
+
+(define-rule UltPlusOne ( (n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
+ (bvult x (bvadd y (_ bv 1 n)))
+ (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n))))))
+
/******************************************************************************
* Experimental
******************************************************************************/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback