Merge pull request #427 from pysmt/typeoracle_constants

TypesOracle: Fix handling of constants

pysmt/oracles.py

@@ -444,7 +444,8 @@ def expand_types(self, types):
         return expanded
 
     @walkers.handles(set(op.ALL_TYPES) - \
-                     set([op.SYMBOL, op.FUNCTION, op.QUANTIFIERS]))
+                     set([op.SYMBOL, op.FUNCTION]) -\
+                     op.QUANTIFIERS - op.CONSTANTS)
     def walk_combine(self, formula, args, **kwargs):
         #pylint: disable=unused-argument
         res = set()
@@ -466,6 +467,10 @@ def walk_quantifier(self, formula, args, **kwargs):
         return frozenset([x.symbol_type()
                           for x in formula.quantifier_vars()]) | args[0]
 
+    @walkers.handles(op.CONSTANTS)
+    def walk_constant(self, formula, args, **kwargs):
+        return frozenset([formula.constant_type()])
+
 # EOC TypesOracle
 
 

pysmt/test/test_oracles.py

@@ -20,7 +20,7 @@
 from pysmt.test.examples import get_example_formulae
 from pysmt.test import TestCase, main
 from pysmt.oracles import get_logic
-from pysmt.typing import BOOL, Type
+from pysmt.typing import BOOL, Type, INT
 
 
 class TestOracles(TestCase):
@@ -121,6 +121,11 @@ def test_types_oracle(self):
         self.assertTrue(idx_US < idx_BUSBBS)
         self.assertTrue(idx_BBS < idx_BUSBBS)
 
+    def test_type_oracles_constants(self):
+        mgr = self.env.formula_manager
+        f = mgr.Plus(mgr.Int(5), mgr.Int(6))
+        types_all = self.env.typeso.get_types(f)
+        self.assertEqual(types_all, [INT])
 
 if __name__ == '__main__':
     main()