added prover script

1 files changed, 0 insertions, 53 deletions

diff --git a/parser.py b/parser.py
deleted file mode 100644
index e66f9d2..0000000
--- a/parser.py
+++ /dev/null
@@ -1,53 +0,0 @@
-
-class Concrete:
-   def __init__(self, val): self.val = val
-   def __str__(self): return str(self.val)
-
-class Symbolic:
-   def __init__(self, id): self.id = id
-   def __str__(self): return f"x_{self.id}"
-
-class TermAdd:
-   def __init__(self, a, b): self.a, self.b = a, b
-   def __str__(self): return f"(+ {self.a} {self.b})"
-
-class TermMul:
-   def __init__(self, a, b): self.a, self.b = a, b
-   def __str__(self): return f"(* {self.a} {self.b})"
-
-class TermReLU:
-   def __init__(self, a): self.a = a
-   def __str__(self): return f"(ite (> {self.a} 0) {self.a} 0)"
-
-def generate_z3(net_a_str, net_b_str, epsilon=1e-5):
-   context = {
-       'Concrete': Concrete,
-       'Symbolic': Symbolic,
-       'TermAdd': TermAdd,
-       'TermMul': TermMul,
-       'TermReLU': TermReLU
-   }
-
-   try:
-       tree_a = eval(net_a_str, context)
-       tree_b = eval(net_b_str, context)
-   except Exception as e:
-       print(f"; Error parsing Inpla output: {e}")
-       return
-
-   print("(declare-const x_0 Real)") 
-   print("(declare-const x_1 Real)")
-
-   print(f"(define-fun net_a () Real {tree_a})")
-   print(f"(define-fun net_b () Real {tree_b})")
-
-   print(f"(assert (> (abs (- net_a net_b)) {epsilon:.10f}))")
-   
-   print("(check-sat)")
-   print("(get-model)")
-
-if __name__ == "__main__":
-   output_net_a = "TermAdd(TermMul(Symbolic(0), Concrete(2)), Concrete(3))" # 2x + 3
-   output_net_b = "TermAdd(Concrete(3), TermMul(Concrete(2), Symbolic(0)))" # 3 + 2x
-   
-   generate_z3(output_net_a, output_net_b)