Repository: pysmt/pysmt

Issue:
`get_atoms()` crashes with boolean-typed arrays
There is a bug in `get_atoms()` when boolean arrays are involved.

Consider the following code:
```python
from pysmt.shortcuts import *

a = Symbol("a", ArrayType(INT, BOOL))
x = Symbol("x", INT)
p = Symbol("p", BOOL)

phi = And(Iff(Select(a, x), p), GT(x, Int(1)))

print(phi.get_atoms())
```

The current master crashes with 
```
Traceback (most recent call last):
  File "bugo.py", line 9, in <module>
    print(phi.get_atoms())
  File "/home/amicheli/work/code/pysmt/pysmt/fnode.py", line 118, in get_atoms
    return _env().ao.get_atoms(self)
  File "/home/amicheli/work/code/pysmt/pysmt/oracles.py", line 396, in get_atoms
    return self.walk(formula)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 106, in walk
    res = self.iter_walk(formula, **kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 98, in iter_walk
    self._process_stack(**kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 91, in _process_stack
    self._compute_node_result(formula, **kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 75, in _compute_node_result
    self.memoization[key] = f(formula, args=args, **kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/oracles.py", line 403, in walk_bool_op
    return frozenset(x for a in args for x in a)
  File "/home/amicheli/work/code/pysmt/pysmt/oracles.py", line 403, in <genexpr>
    return frozenset(x for a in args for x in a)
TypeError: 'NoneType' object is not iterable
```

the expected behavior is to return the set `{p, a[x], x>1}`

Thanks to Gianluca Redondi for signaling the issue.


Discussion:

Patch:
diff --git a/pysmt/oracles.py b/pysmt/oracles.py
index 36b8b12..5cae510 100644
--- a/pysmt/oracles.py
+++ b/pysmt/oracles.py
@@ -389,6 +389,7 @@ class AtomsOracle(walkers.DagWalker):
     # - ITE terms
     # - Symbols
     # - Constants
+    # - Array select, e.g. a[x] because such term could be of Boolean type
     #
 
     def get_atoms(self, formula):
@@ -406,11 +407,17 @@ class AtomsOracle(walkers.DagWalker):
         #pylint: disable=unused-argument
         return frozenset([formula])
 
-    @walkers.handles(op.THEORY_OPERATORS)
+    @walkers.handles(op.THEORY_OPERATORS - {op.ARRAY_SELECT})
     def walk_theory_op(self, formula, **kwargs):
         #pylint: disable=unused-argument
         return None
 
+    def walk_array_select(self, formula, **kwargs):
+        #pylint: disable=unused-argument
+        if self.env.stc.get_type(formula).is_bool_type():
+            return frozenset([formula])
+        return None
+
     @walkers.handles(op.CONSTANTS)
     def walk_constant(self, formula, **kwargs):
         #pylint: disable=unused-argument


Test patch:
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 29985f8..d894eaa 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -544,6 +544,20 @@ class TestRegressions(TestCase):
         f = get_formula_strict(cStringIO(smt_script))
         self.assertSat(f, solver_name='yices')
 
+    def test_get_atoms_array_select(self):
+        a = Symbol("a", ArrayType(INT, BOOL))
+        x = Symbol("x", INT)
+        p = Symbol("p", BOOL)
+
+        phi = And(Iff(Select(a, x), p), Equals(x, Int(1)))
+
+        atoms = phi.get_atoms()
+
+        self.assertEqual(len(atoms), 3)
+        self.assertIn(Select(a, x), atoms)
+        self.assertIn(p, atoms)
+        self.assertIn(Equals(x, Int(1)), atoms)
+
 
 if __name__ == "__main__":
     main()