From 401e0eb398c5f265424033a930c7749ac47b4a81 Mon Sep 17 00:00:00 2001
From: Angello Astorga <aastorg2@illinois.edu>
Date: Mon, 29 Nov 2021 19:26:30 -0500
Subject: [PATCH] multiply variable by itself instead of using power function
---
firstpass_learner.py | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/firstpass_learner.py b/firstpass_learner.py
index 5693951..9877be7 100644
--- a/firstpass_learner.py
+++ b/firstpass_learner.py
@@ -22,7 +22,7 @@ def l1_norm(*exprs) -> z3.ExprRef:
return z3.Sum(*(abs_expr(expr) for expr in exprs))
def l2_norm(*exprs) -> z3.ExprRef:
- return z3.Sum(*(expr**2 for expr in exprs))
+ return z3.Sum(*(expr*expr for expr in exprs))
def max_expr(*exprs) -> z3.ExprRef:
m = exprs[0]
@@ -99,7 +99,7 @@ class FirstpassLearner(Z3LearnerBase):
print("(unsat)")
return None
else:
- print("(unknown)")
+ print("(unknown) or timeout!")
return None
--
GitLab