Merge pull request #44 from pysmt/cone_walker

Get free Variables

docs/CHANGES.rst

@@ -1,14 +1,23 @@
 Change Log
 ==========
 
+0.2.4 XXXXXXXX  -- YYYY
+-----------------------
+
+General:
+
+* Iterative implementation of FNode.get_free_variables().
+  This also deprecates FNode.get_dependencies().
+
+
 0.2.3 2015-03-12 -- Logics Refactoring
 --------------------------------------
 
 General:
 
 * install.py: script to automate the installation of supported
-  solvers. 
-  
+  solvers.
+
 * get_logic() Oracle: Detects the logic used in a formula. This can now be used in the shortcuts (_is_sat()_, _is_unsat()_, _is_valid()_, and
   _get_model()_) by choosing the special logic pysmt.logics.AUTO.
 
@@ -24,7 +33,7 @@ General:
 * The default logic for Factory.get_solver() is now the most generic
   *quantifier free* logic supported by pySMT (currently,
   QF_UFLIRA). The factory not provides a way to change this default.
-  
+
 * Removed option _quantified_ from all shortcuts.
 
 

pysmt/environment.py

@@ -46,6 +46,7 @@ def __init__(self):
         self._serializer = pysmt.printers.HRSerializer(self)
         self._qfo = pysmt.oracles.QuantifierOracle(self)
         self._theoryo = pysmt.oracles.TheoryOracle(self)
+        self._fvo = pysmt.oracles.FreeVarsOracle(self)
 
         self._factory = None
         # Configurations
@@ -86,6 +87,11 @@ def theoryo(self):
         """ Get the Theory Oracle """
         return self._theoryo
 
+    @property
+    def fvo(self):
+        """ Get the FreeVars Oracle """
+        return self._fvo
+
     def add_dynamic_walker_function(self, nodetype, walker, function):
         """Dynamically bind the given function to the walker for the nodetype.
 

pysmt/fnode.py

@@ -16,11 +16,10 @@
 #   limitations under the License.
 #
 """FNode are the building blocks of formulae."""
-
 import collections
 
 import shortcuts
-from pysmt.operators import ALL_TYPES, QUANTIFIERS, CONSTANTS
+from pysmt.operators import CONSTANTS
 from pysmt.operators import (FORALL, EXISTS, AND, OR, NOT, IMPLIES, IFF,
                              SYMBOL, FUNCTION,
                              REAL_CONSTANT, BOOL_CONSTANT, INT_CONSTANT,
@@ -29,15 +28,11 @@
                              ITE,
                              TOREAL)
 from pysmt.typing import BOOL, REAL, INT, PYSMT_TYPES
+from pysmt.decorators import deprecated
 
 FNodeContent = collections.namedtuple("FNodeContent",
                                       ["node_type", "args", "payload"])
 
-# Operators for which Args is an FNode (used by compute_dependencies
-DEPENDENCIES_SIMPLE_ARGS = (set(ALL_TYPES) - \
-                            (set([SYMBOL, FUNCTION]) | QUANTIFIERS | CONSTANTS))
-
-
 class FNode(object):
     r"""FNode represent the basic structure for representing a formula.
 
@@ -55,7 +50,6 @@ class FNode(object):
 
     def __init__(self, content):
         self._content = content
-        self._dependencies = None
         return
 
     # __eq__ and __hash__ are left as default
@@ -70,43 +64,16 @@ def args(self):
     def arg(self, idx):
         return self._content.args[idx]
 
-
+    @deprecated("get_free_variables")
     def get_dependencies(self):
-        if self._dependencies is None:
-            self._dependencies = self._compute_dependencies()
-        return self._dependencies
-
-    def _compute_dependencies(self):
-        if self.node_type() in DEPENDENCIES_SIMPLE_ARGS:
-            res = set()
-            for s in self.get_sons():
-                res.update(s.get_dependencies())
-            return res
-
-        elif self.node_type() in QUANTIFIERS:
-            return self.arg(0).get_dependencies().difference(self._content.payload)
-
-        elif self.node_type() == SYMBOL:
-            return frozenset([self])
-
-        elif self.node_type() in CONSTANTS:
-            return frozenset()
-
-        elif self.node_type() == FUNCTION:
-            res = set([self._content.payload])
-            for p in self.args():
-                res.update(p.get_dependencies())
-            return res
-
-        else:
-            assert False
-        return
+        return self.get_free_variables()
 
+    def get_free_variables(self):
+        return shortcuts.get_free_variables(self)
 
     def get_sons(self):
         return self.args()
 
-
     def simplify(self):
         return shortcuts.simplify(self)
 

pysmt/oracles.py

@@ -20,6 +20,7 @@
 
  * QuantifierOracle says whether a formula is quantifier free
  * TheoryOracle says which logic is used in the formula.
+ * FreeVarsOracle says which variables are free in the formula
 """
 
 import pysmt.walkers as walkers
@@ -168,10 +169,72 @@ def get_theory(self, formula):
         """Returns the thoery for the formula."""
         return self.walk(formula)
 
-
 # EOC TheoryOracle
 
 
+# Operators for which Args is an FNode
+DEPENDENCIES_SIMPLE_ARGS = (set(op.ALL_TYPES) - \
+                           (set([op.SYMBOL, op.FUNCTION]) | op.QUANTIFIERS | op.CONSTANTS))
+
+class FreeVarsOracle(pysmt.walkers.DagWalker):
+    def __init__(self, env=None):
+        pysmt.walkers.DagWalker.__init__(self, env=env)
+
+        # Clear the mapping function
+        self.functions.clear()
+
+        # We have only few categories for this walker.
+        #
+        # - Simple Args simply need to combine the cone/dependencies
+        #   of the children.
+        # - Quantifiers need to exclude bounded variables
+        # - Constants have no impact
+        #
+        for elem in op.ALL_TYPES:
+            if elem in DEPENDENCIES_SIMPLE_ARGS:
+                self.functions[elem] = self.walk_simple_args
+            elif elem in op.QUANTIFIERS:
+                self.functions[elem] = self.walk_quantifier
+            elif elem in op.CONSTANTS:
+                self.functions[elem] = self.walk_constant
+            else:
+                self.functions[elem] = self.walk_error
+
+        # These are the only 2 cases that can introduce elements.
+        self.functions[op.SYMBOL] = self.walk_symbol
+        self.functions[op.FUNCTION] = self.walk_function
+
+        # Check that no operator in undefined
+        assert self.is_complete(verbose=True)
+
+
+    def get_free_variables(self, formula):
+        """Returns the set of Symbols appearing free in the formula."""
+        return self.walk(formula)
+
+    def walk_simple_args(self, formula, args):
+        res = set()
+        for arg in args:
+            res.update(arg)
+        return frozenset(res)
+
+    def walk_quantifier(self, formula, args):
+        return args[0].difference(formula.quantifier_vars())
+
+    def walk_symbol(self, formula, args):
+        return frozenset([formula])
+
+    def walk_constant(self, formula, args):
+        return frozenset()
+
+    def walk_function(self, formula, args):
+        res = set([formula.function_name()])
+        for arg in args:
+            res.update(arg)
+        return frozenset(res)
+
+# EOC FreeVarsOracle
+
 def get_logic(formula, env=None):
     if env is None:
         env = pysmt.shortcuts.get_env()

pysmt/shortcuts.py

@@ -81,6 +81,10 @@ def serialize(formula, threshold=None):
     return get_env().serializer.serialize(formula,
                                           threshold=threshold)
 
+def get_free_variables(formula):
+    """Returns the simplified version of the formula."""
+    return get_env().fvo.get_free_variables(formula)
+
 ##### Nodes Creation #####
 
 def ForAll(variables, formula):

pysmt/simplifier.py

@@ -248,7 +248,7 @@ def walk_forall(self, formula, args):
         assert len(args) == 1
         sf = args[0]
 
-        varset = set(formula.quantifier_vars()).intersection(sf.get_dependencies())
+        varset = set(formula.quantifier_vars()).intersection(sf.get_free_variables())
 
         if len(varset) == 0:
             return sf
@@ -260,7 +260,7 @@ def walk_exists(self, formula, args):
         assert len(args) == 1
         sf = args[0]
 
-        varset = set(formula.quantifier_vars()).intersection(sf.get_dependencies())
+        varset = set(formula.quantifier_vars()).intersection(sf.get_free_variables())
 
         if len(varset) == 0:
             return sf

pysmt/smtlib/printers.py

@@ -173,7 +173,7 @@ def _push_with_children_to_stack(self, formula, **kwargs):
     def printer(self, f):
         self.openings = 0
         self.name_seed = 0
-        self.names = set(x.symbol_name() for x in f.get_dependencies())
+        self.names = set(x.symbol_name() for x in f.get_free_variables())
 
         key = self.walk(f)
         self.write(key)

pysmt/smtlib/script.py

@@ -200,7 +200,7 @@ def smtlibscript_from_formula(formula):
     script.add(name=smtcmd.SET_LOGIC,
                args=[UFLIRA])
 
-    deps = formula.get_dependencies()
+    deps = formula.get_free_variables()
     # Declare all variables
     for symbol in deps:
         assert symbol.is_symbol()

pysmt/smtlib/solver.py

@@ -72,7 +72,7 @@ def reset_assertions(self):
         return
 
     def add_assertion(self, formula, named=None):
-        deps = formula.get_dependencies()
+        deps = formula.get_free_variables()
         for d in deps:
             if d not in self.declared_vars:
                 self._declare_variable(d)

pysmt/substituter.py

@@ -79,7 +79,7 @@ def _push_with_children_to_stack(self, formula, **kwargs):
                 # we do not consider this substitution in the body of
                 # the quantifier.
                 if all(m not in formula.quantifier_vars()
-                       for m in k.get_dependencies()):
+                       for m in k.get_free_variables()):
                     new_subs[k] = v
 
             # 2. We apply the substitution on the quantifier body with