smt2_translator: added smt2_assert and smt2_or to smt_helper. refactored other smt2_helpers to work with multiple arguments

1 files changed, 26 insertions, 6 deletions

diff --git a/miasm2/expression/smt2_helper.py b/miasm2/expression/smt2_helper.py
index f7737116..53d323e8 100644
--- a/miasm2/expression/smt2_helper.py
+++ b/miasm2/expression/smt2_helper.py
@@ -23,11 +23,22 @@ def smt2_implies(a, b):
     return "(=> {} {})".format(a, b)
 
 
-def smt2_and(a, b):
+def smt2_and(*args):
     """
-    Conjunction: a and b
+    Conjunction: a and b and c ...
     """
-    return "(and {} {})".format(a, b)
+    # transform args into strings
+    args = [str(arg) for arg in args]
+    return "(and {})".format(' '.join(args))
+
+
+def smt2_or(*args):
+    """
+    Disjunction: a or b or c ...
+    """
+    # transform args into strings
+    args = [str(arg) for arg in args]
+    return "(or {})".format(' '.join(args))
 
 
 def smt2_ite(cond, a, b):
@@ -37,11 +48,20 @@ def smt2_ite(cond, a, b):
     return "(ite {} {} {})".format(cond, a, b)
 
 
-def smt2_distinct(a, b):
+def smt2_distinct(*args):
+    """
+    Distinction: a != b != c != ...
+    """
+    # transform args into strings
+    args = [str(arg) for arg in args]
+    return "(distinct {})".format(' '.join(args))
+
+
+def smt2_assert(expr):
     """
-    Distinction: a != b
+    Assertion that @expr holds
     """
-    return "(distinct {} {})".format(a, b)
+    return "(assert {})".format(expr)
 
 
 # definitions