| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | check.py | 23 from syntax import (true_term, false_term, boolT, mk_var, mk_word32, mk_word8, namespace
|
| H A D | debug.py | 155 assert r in [syntax.true_term, syntax.false_term], r
369 assert v in [syntax.true_term, syntax.false_term]
|
| H A D | logic.py | 11 from syntax import true_term, false_term, mk_num namespace
337 return false_term
503 return false_term
640 elif node.kind == 'Cond' and node.cond == false_term:
1029 elif c == syntax.false_term:
1611 if vals[1] in [syntax.true_term, syntax.false_term]:
1615 elif vals[0] == syntax.false_term:
|
| H A D | loop_bounds.py | 6 from syntax import mk_not, true_term, false_term, mk_implies, Expr, Type, unspecified_precond_term,mk_and namespace
|
| H A D | problem.py | 9 from syntax import (Expr, mk_var, Node, true_term, false_term, namespace
702 true_term, false_term]:
|
| H A D | rep_graph.py | 10 from syntax import (true_term, false_term, boolT, mk_and, mk_not, mk_implies, namespace
208 elif pc[0] == 'Bool' and pc[1] == false_term:
259 return syntax.false_term
293 return Hyp ('PCImp', vis, ('Bool', false_term))
662 if pc == false_term:
663 return [(c, false_term, {}) for c in node.get_conts()]
668 (node.right, false_term, env)]
1048 return false_term
|
| H A D | search.py | 17 foldr1, boolT, word32T, word8T, builtinTs, true_term, false_term,
209 test_expr = false_term
282 test_expr = false_term
479 assert b in [false_term, true_term]
552 result = {True: true_term, False: false_term}[result]
555 result = {True: true_term, False: false_term}[result]
558 result = {True: true_term, False: false_term}[result]
562 result = {True: true_term, False: false_term}[result]
601 assert x in [syntax.true_term, syntax.false_term]
602 if x == syntax.false_term
[all...] |
| H A D | solver.py | 177 from syntax import (Expr, fresh_name, builtinTs, true_term, false_term, namespace
1955 pc_envs = [(pc, env) for (pc, env) in pc_envs if pc != false_term]
1957 path_cond = false_term
2015 return false_term
2028 elif b == syntax.false_term:
2106 false_vals = [x for (x, v) in vals if v == syntax.false_term]
2120 if v == syntax.false_term:
2162 if fun.nodes[n].cond != syntax.false_term]
2188 assert solv.check_hyp (false_term, {}, force_solv = fs) == 'sat'
2195 assert solv.check_hyp (false_term, {}, mode
[all...] |
| H A D | stack_logic.py | 913 res = rep.test_hyp_whyps (syntax.false_term, assns, model = m)
|
| H A D | syntax.py | 1100 false_term = Expr ('Op', boolT, name = 'False', vals = []) variable
|
| H A D | trace_refute.py | 269 return rep.test_hyp_whyps (syntax.false_term, hs)
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | elf_correlate.py | 14 from graph_refine.syntax import true_term, false_term, mk_not namespace
|