Lines Matching refs:smt_expr
291 def mk_smt_expr (smt_expr, typ):
292 return Expr ('SMTExpr', typ, val = smt_expr)
303 def smt_expr (expr, env, solv):
307 ex = smt_expr (v, env, solv)
332 vs = [smt_expr (v, env, solv) for v in expr.vals]
337 v = smt_expr (v, env, solv)
343 return smt_expr (expr, env, solv)
361 p_s = smt_expr (p, env, solv)
365 [p, dom] = [smt_expr (e, env, solv) for e in expr.vals]
374 m_s = smt_expr (m, env, solv)
375 p_s = smt_expr (p, env, solv)
376 v_s = smt_expr (v, env, solv)
381 m_s = smt_expr (m, env, solv)
382 p_s = smt_expr (p, env, solv)
385 (x, y) = [smt_expr (e, env, solv) for e in expr.vals]
393 (x, y) = [smt_expr (e, env, solv) for e in expr.vals]
397 [sp1, st1, sp2, st2] = [smt_expr (e, env, solv)
411 sp1 = smt_expr (sp1, env, solv)
412 sp2 = smt_expr (sp2, env, solv)
415 (sw, x, y) = [smt_expr (e, env, solv) for e in expr.vals]
421 vals = [smt_expr (e, env, solv) for e in expr.vals]
432 trace ('Env miss for %s in smt_expr' % expr.name)
515 s = smt_expr (expr, env, solv)
914 smt = smt_expr (val, env, self)
1291 goal = smt_expr (syntax.mk_not (hyp), env, self)
1572 hyp = smt_expr (hyp, env, self)
1600 fact = smt_expr (fact, env, self)
1687 r_addr_s = smt_expr (r_addr, {}, None)
1718 ass_s = smt_expr (ass, None, None)
1722 ass_s = smt_expr (ass, None, None)
1776 sp_smt = smt_expr (sp, env, self)
1822 smt_expr = mk_smt_expr (sexpr, typ)
1823 v = self.add_def ('query_' + s, smt_expr, {})
1904 hyps = [(smt_expr (hyp, env, self), tag) for (hyp, tag) in hyps]
1925 pc_str = smt_expr (pc, env, solv)
1967 s = smt_expr (hyp, env, solv)
1976 s = smt_expr (hyp, env, solv)
2086 return ['(= %s %s)' % (flat_s_expression (x), smt_expr (v, {}, solv))