Merge pull request #42 from pysmt/annotations_and_unsat_cores

Annotations and unsat cores

docs/CHANGES.rst

@@ -21,7 +21,8 @@ Backwards Incompatible Changes:
 
 * Expressions: Added Min/Max operators.
 
-* SMT-LIB: Substantially improved parser performances.
+* SMT-LIB: Substantially improved parser performances. Added explicit
+  Annotations object to deal with SMT-LIB Annotations.
 
 
 0.2.2 2015-02-07 -- BDDs

pysmt/smtlib/annotations.py

@@ -0,0 +1,115 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+
+
+class Annotations(object):
+    """Handles and stores (key,value) annotations for formulae"""
+
+    def __init__(self, initial_annotations=None):
+        if initial_annotations is not None:
+            self._annotations = initial_annotations
+        else:
+            self._annotations = {}
+
+
+    def add(self, formula, annotation, value=None):
+        """Adds an annotation for the given formula, possibly with the
+        specified value"""
+        term_annotations = self._annotations.setdefault(formula, {})
+        values = term_annotations.setdefault(annotation, set())
+        if value is not None:
+            values.add(value)
+
+
+    def remove(self, formula):
+        """Removes all the annotations for the given formula"""
+        if formula in self._annotations:
+            del self._annotations[formula]
+
+
+    def remove_annotation(self, formula, annotation):
+        """Removes the given annotation for the given formula"""
+        if formula in self._annotations:
+            if annotation in self._annotations[formula]:
+                del self._annotations[formula][annotation]
+
+
+    def remove_value(self, formula, annotation, value):
+        """Removes the given annotation for the given formula"""
+        if formula in self._annotations:
+            if annotation in self._annotations[formula]:
+                d = self._annotations[formula][annotation]
+                if value in d:
+                    d.remove(value)
+
+
+    def has_annotation(self, formula, annotation, value=None):
+        """Returns True iff the given formula has the given annotation. If
+        Value is specified, True is returned only if the value is
+        matching.
+        """
+        if formula in self._annotations:
+            if annotation in self._annotations[formula]:
+                if value is None:
+                    return True
+                else:
+                    return (value in self._annotations[formula][annotation])
+        return False
+
+
+    def annotations(self, formula):
+        """Returns a dictionary containing all the annotations for the given
+        formula as keys and the respective values. None is returned if
+        formula has no annotations.
+        """
+        try:
+            return self._annotations[formula]
+        except KeyError:
+            return None
+
+
+    def all_annotated_formulae(self, annotation, value=None):
+        """Returns the set of all the formulae having the given annotation
+        key. If Value is specified, only the formula having the
+        specified value are returned.
+        """
+        res = []
+        for f,amap in self._annotations.iteritems():
+            if annotation in amap:
+                if value is None:
+                    res.append(f)
+                else:
+                    if value in amap[annotation]:
+                        res.append(f)
+        return set(res)
+
+
+    def __contains__(self, formula):
+        """Checks if formula has at least one annotation"""
+        return formula in self._annotations
+
+    def __str__(self):
+        res = ["Annotations: {"]
+        for t, m in self._annotations.iteritems():
+            res.append(str(t) + " -> ")
+            for a, lst in m.iteritems():
+                res.append(":" + str(a) + "{")
+                for v in lst:
+                    res.append(str(v) + ", ")
+                res.append("} ")
+        return "".join(res + ["}"])

pysmt/smtlib/parser.py

@@ -26,6 +26,7 @@
 from pysmt.logics import get_logic_by_name, UndefinedLogicError
 from pysmt.exceptions import UnknownSmtLibCommandError
 from pysmt.smtlib.script import SmtLibCommand, SmtLibScript
+from pysmt.smtlib.annotations import Annotations
 
 
 def get_formula(script_stream, environment=None):
@@ -77,7 +78,7 @@ class SmtLibExecutionCache(object):
     def __init__(self):
         self.keys = {}
         self.definitions = {}
-        self.annotations = {}
+        self.annotations = Annotations()
 
     def bind(self, name, value):
         """Binds a symbol in this environment"""
@@ -193,14 +194,24 @@ class SmtLibParser(object):
 
     def __init__(self, environment=None):
         self.pysmt_env = get_env() if environment is None else environment
-        self._current_env = self.pysmt_env
-        self.cache = SmtLibExecutionCache()
+
+        # Placeholders for fields filled by self._reset
+        self._current_env = None
+        self.cache = None
         self.logic = None
 
         # Special tokens appearing in expressions
         self.parentheses = set(["(", ")"])
         self.specials = set(["let", "!", "exists", "forall"])
 
+
+
+    def _reset(self):
+        """Resets the parser to the initial state"""
+        self.cache = SmtLibExecutionCache()
+        self.logic = None
+        self._current_env = self.pysmt_env
+
         mgr = self.pysmt_env.formula_manager
         self.cache.update({'+':mgr.Plus,
                            '-':self._minus_or_uminus,
@@ -295,17 +306,20 @@ def atom(self, token, mgr):
         """
         res = self.cache.get(token)
         if res is None:
-            # This is a numerical constant
-            if "." in token:
-                res = mgr.Real(Fraction(token))
-            else:
-                iterm = int(token)
-                # We found an integer, depending on the logic this can be
-                # an Int or a Real
-                if self.logic is None or self.logic.theory.integer_arithmetic:
-                    res = mgr.Int(iterm)
+            try:
+                # This is a numerical constant
+                if "." in token:
+                    res = mgr.Real(Fraction(token))
                 else:
-                    res = mgr.Real(iterm)
+                    iterm = int(token)
+                    # We found an integer, depending on the logic this can be
+                    # an Int or a Real
+                    if self.logic is None or self.logic.theory.integer_arithmetic:
+                        res = mgr.Int(iterm)
+                    else:
+                        res = mgr.Real(iterm)
+            except ValueError:
+                res = token
             self.cache.bind(token, res)
         return res
 
@@ -360,22 +374,26 @@ def _handle_quantifier(self, fun, vrs, body):
         return fun(vrs, body)
 
 
-    def _handle_annotation(self, pyterm, attrs):
+    def _handle_annotation(self, pyterm, *attrs):
         """
         This method is invoked when we finish parsing an annotated expression
         """
-        pyterm_annotations = self.cache.annotations.setdefault(pyterm, {})
 
         # Iterate on elements.
         i = 0
         while i < len(attrs):
             if i+1 < len(attrs) and str(attrs[i+1])[0] != ":" :
-                key, value = attrs[i], attrs[i+1]
+                key, value = str(attrs[i]), str(attrs[i+1])
+                if key[0] != ":":
+                    raise SyntaxError("Annotations keys should start with colon")
+                self.cache.annotations.add(pyterm, key[1:], value)
                 i += 2
             else:
-                key, value = attrs[i], True
+                key = str(attrs[i])
+                if key[0] != ":":
+                    raise SyntaxError("Annotations keys should start with colon")
+                self.cache.annotations.add(pyterm, key[1:])
                 i += 1
-            pyterm_annotations[key] = value
 
         return pyterm
 
@@ -475,9 +493,11 @@ def get_script(self, script):
         """
         Takes a file object and returns a SmtLibScript object representing the file
         """
+        self._reset() # prepare the parser
         res = SmtLibScript()
         for cmd in self.get_command_generator(script):
             res.add_command(cmd)
+        res.annotations = self.cache.annotations
         return res
 
     def get_command_generator(self, script):

pysmt/smtlib/script.py

@@ -105,6 +105,7 @@ def serialize_to_string(self):
 class SmtLibScript(object):
 
     def __init__(self):
+        self.annotations = None
         self.commands = []
 
     def add(self, name, args):