(code: str)
| 62 | return execution_globals |
| 63 | |
| 64 | def execute_code_in_process(code: str): |
| 65 | import z3 |
| 66 | import sympy |
| 67 | import math |
| 68 | import itertools |
| 69 | from fractions import Fraction |
| 70 | |
| 71 | execution_globals = prepare_execution_globals() |
| 72 | |
| 73 | # Add Z3 specific functions |
| 74 | z3_whitelist = set(dir(z3)) |
| 75 | execution_globals.update({name: getattr(z3, name) for name in z3_whitelist}) |
| 76 | |
| 77 | # Add SymPy specific functions |
| 78 | sympy_whitelist = set(dir(sympy)) |
| 79 | execution_globals.update({name: getattr(sympy, name) for name in sympy_whitelist}) |
| 80 | |
| 81 | # Ensure key Z3 and SymPy components are available |
| 82 | execution_globals.update({ |
| 83 | 'z3': z3, |
| 84 | 'sympy': sympy, |
| 85 | 'Solver': z3.Solver, |
| 86 | 'solver': z3.Solver, |
| 87 | 'Optimize': z3.Optimize, |
| 88 | 'sat': z3.sat, |
| 89 | 'unsat': z3.unsat, |
| 90 | 'unknown': z3.unknown, |
| 91 | 'Real': z3.Real, |
| 92 | 'Int': z3.Int, |
| 93 | 'Bool': z3.Bool, |
| 94 | 'And': z3.And, |
| 95 | 'Or': z3.Or, |
| 96 | 'Not': z3.Not, |
| 97 | 'Implies': z3.Implies, |
| 98 | 'If': z3.If, |
| 99 | 'Sum': z3.Sum, |
| 100 | 'ForAll': z3.ForAll, |
| 101 | 'Exists': z3.Exists, |
| 102 | 'model': z3.Model, |
| 103 | 'Symbol': sympy.Symbol, |
| 104 | 'solve': sympy.solve, |
| 105 | 'simplify': sympy.simplify, |
| 106 | 'expand': sympy.expand, |
| 107 | 'factor': sympy.factor, |
| 108 | 'diff': sympy.diff, |
| 109 | 'integrate': sympy.integrate, |
| 110 | 'limit': sympy.limit, |
| 111 | 'series': sympy.series, |
| 112 | }) |
| 113 | |
| 114 | # Add custom functions |
| 115 | def as_numerical(x): |
| 116 | if z3.is_expr(x): |
| 117 | if z3.is_int_value(x) or z3.is_rational_value(x): |
| 118 | return float(x.as_decimal(20)) |
| 119 | elif z3.is_algebraic_value(x): |
| 120 | return x.approx(20) |
| 121 | return float(x) |
nothing calls this directly
no test coverage detected