Repository: pysmt/pysmt

Issue:
issue in processing arguments for ExactlyOne()
Hi, 

I noticed that instantiating shortcuts.ExactlyOne() throws e.g.

TypeError: list() takes at most 1 argument (3 given)

at formula.py, line 480. I believe args shouldn't be unpacked in the list constructor. 

Martin

Discussion:

Patch:
diff --git a/pysmt/formula.py b/pysmt/formula.py
index 0a4dcd3..4fdcbfe 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -477,7 +477,7 @@ class FormulaManager(object):
            A -> !(B \/ C)
            B -> !(C)
         """
-        args = list(*args)
+        args = self._polymorph_args_to_tuple(args)
         return self.And(self.Or(*args),
                         self.AtMostOne(*args))
 


Test patch:
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 0ddbec4..924328a 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -494,6 +494,16 @@ class TestFormulaManager(TestCase):
         self.assertEqual(c, self.mgr.Bool(False),
                          "ExactlyOne should not allow 2 symbols to be True")
 
+        s1 = self.mgr.Symbol("x")
+        s2 = self.mgr.Symbol("x")
+        f1 = self.mgr.ExactlyOne((s for s in [s1,s2]))
+        f2 = self.mgr.ExactlyOne([s1,s2])
+        f3 = self.mgr.ExactlyOne(s1,s2)
+
+        self.assertEqual(f1,f2)
+        self.assertEqual(f2,f3)
+
+
     @skipIfNoSolverForLogic(QF_BOOL)
     def test_exactly_one_is_sat(self):
         symbols = [ self.mgr.Symbol("s%d"%i, BOOL) for i in range(5) ]
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 2fecd04..67bfc3d 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -311,6 +311,14 @@ class TestRegressions(TestCase):
         close_l = get_closer_smtlib_logic(logics.BOOL)
         self.assertEqual(close_l, logics.LRA)
 
+    def test_exactly_one_unpacking(self):
+        s1,s2 = Symbol("x"), Symbol("y")
+        f1 = ExactlyOne((s for s in [s1,s2]))
+        f2 = ExactlyOne([s1,s2])
+        f3 = ExactlyOne(s1,s2)
+
+        self.assertEqual(f1,f2)
+        self.assertEqual(f2,f3)
 
 if __name__ == "__main__":
     main()