Wanko/statistics

fclingo/__main__.py

@@ -3,12 +3,13 @@
 """
 
 import sys
+import time
 
 import clingo
 from clingcon import ClingconTheory
-from clingo.ast import ProgramBuilder, parse_files, Location, Position, Rule
+from clingo.ast import Location, Position, ProgramBuilder, Rule, parse_files
 
-from fclingo import THEORY
+from fclingo import THEORY, translator
 from fclingo.parsing import HeadBodyTransformer
 from fclingo.translator import AUX, Translator
 
@@ -17,6 +18,20 @@
 CSP = "__csp"
 DEF = "__def"
 
+
+class Statistic:
+    """
+    Class for statistics of fclingo translation.
+    """
+
+    def __init__(self):
+        self.rewrite_ast = 0
+        self.translate_program = 0
+        self.constraints_added = 0
+        self.rules_added = 0
+        self.variables_added = 0
+
+
 class AppConfig:
     """
     Class for application specific options.
@@ -39,7 +54,10 @@ class FclingoApp(clingo.Application):
     def __init__(self):
         self.program_name = "fclingo"
         self.version = "0.1"
-        self.config = AppConfig(MIN_INT,MAX_INT,clingo.Flag(False),clingo.Flag(False), DEF)
+        self.config = AppConfig(
+            MIN_INT, MAX_INT, clingo.Flag(False), clingo.Flag(False), DEF
+        )
+        self.stats = Statistic()
         self._theory = ClingconTheory()
         self._answer = 0
 
@@ -64,7 +82,9 @@ def print_model(self, model, printer):
             for assignment in model.symbols(theory=True)
             if assignment.name == CSP
             and len(assignment.arguments) == 2
-            and model.contains(clingo.Function(self.config.defined, [assignment.arguments[0]]))
+            and model.contains(
+                clingo.Function(self.config.defined, [assignment.arguments[0]])
+            )
             and not assignment.arguments[0].name == AUX
         ]
         shown.extend(valuation)
@@ -91,8 +111,8 @@ def print_model(self, model, printer):
 
     def _flag_str(self, flag):
         return "yes" if flag else "no"
-    
-    def _parse_defined_predicate(self,name):
+
+    def _parse_defined_predicate(self, name):
         if name[0].islower() and name.contains("[a-zA-Z0-9]+"):
             self.config.defined = name
             return True
@@ -124,11 +144,20 @@ def register_options(self, options):
             group,
             "defined-predicate",
             "Name of the defined predicate [{}]".format(self.config.defined),
-            self._parse_defined_predicate
+            self._parse_defined_predicate,
         )
 
     def _on_statistics(self, step, akku):
         self._theory.on_statistics(step, akku)
+        akku["fclingo"] = {}
+        fclingo = akku["fclingo"]
+        fclingo["Translation time in seconds"] = {}
+        translation = fclingo["Translation time in seconds"]
+        translation["AST rewriting"] = self.stats.rewrite_ast
+        translation["Translation"] = self.stats.translate_program
+        fclingo["Number of variables added"] = self.stats.variables_added
+        fclingo["Number of constraints added"] = self.stats.constraints_added
+        fclingo["Number of rules added"] = self.stats.rules_added
         return True
 
     def _read(self, path):
@@ -142,32 +171,38 @@ def main(self, control, files):
         Entry point of the application registering the propagator and
         implementing the standard ground and solve functionality.
         """
-
         self._theory.register(control)
         self._theory.configure("max-int", str(self.config.max_int))
         self._theory.configure("min-int", str(self.config.min_int))
 
         if not files:
             files = ["-"]
 
+        start = time.time()
         with ProgramBuilder(control) as bld:
             hbt = HeadBodyTransformer()
             parse_files(
                 files,
                 lambda stm: bld.add(hbt.visit(stm)),
             )
-            pos = Position('<string>', 1, 1)
+            pos = Position("<string>", 1, 1)
             loc = Location(pos, pos)
             for rule in hbt.rules_to_add:
-                bld.add(Rule(loc,rule[0],rule[1]))
+                bld.add(Rule(loc, rule[0], rule[1]))
+        end = time.time()
+        self.stats.rewrite_ast = end - start
 
         control.add("base", [], THEORY)
         control.ground([("base", [])])
-        translator = Translator(control, self.config)
+
+        start = time.time()
+        translator = Translator(control, self.config, self.stats)
         translator.translate(control.theory_atoms)
+        end = time.time()
+        self.stats.translate_program = end - start
 
         self._theory.prepare(control)
-        control.solve(on_model=self.on_model, on_statistics=self._theory.on_statistics)
+        control.solve(on_model=self.on_model, on_statistics=self._on_statistics)
 
 
 def main():

fclingo/parsing.py

@@ -1,6 +1,7 @@
 """
 This module contains functions for parsing and normalizing constraints.
 """
+
 import clingo
 from clingo import ast
 
@@ -138,31 +139,58 @@ def visit_TheoryAtom(self, atom, in_lit=False):
             )
         return atom
 
-    def visit_Rule(self,rule):
+    def visit_Rule(self, rule):
         head = rule.head
         location = head.location
         if head.ast_type == ast.ASTType.TheoryAtom:
             new_elements = []
             for element in head.elements:
                 term = element.terms[0]
                 condition = element.condition
-                if term.ast_type == ast.ASTType.TheoryUnparsedTerm and "::" in str(term):
+                if term.ast_type == ast.ASTType.TheoryUnparsedTerm and "::" in str(
+                    term
+                ):
                     unparsed_terms = term.elements[:-1]
                     choice_atom = term.elements[-1].term
-                    assert "::" == term.elements[-1].operators[0] and choice_atom.ast_type in [ast.ASTType.TheoryFunction, ast.ASTType.SymbolicTerm] and len(element.terms) == 1
+                    assert (
+                        "::" == term.elements[-1].operators[0]
+                        and choice_atom.ast_type
+                        in [ast.ASTType.TheoryFunction, ast.ASTType.SymbolicTerm]
+                        and len(element.terms) == 1
+                    )
                     if choice_atom.ast_type == ast.ASTType.TheoryFunction:
-                        choice_atom = ast.Literal(location,0,ast.SymbolicAtom(ast.Function(location,choice_atom.name,choice_atom.arguments,0)))
+                        choice_atom = ast.Literal(
+                            location,
+                            0,
+                            ast.SymbolicAtom(
+                                ast.Function(
+                                    location, choice_atom.name, choice_atom.arguments, 0
+                                )
+                            ),
+                        )
                     else:
-                        choice_atom = ast.Literal(location,0,ast.SymbolicAtom(choice_atom))
-                    choice = ast.Aggregate(location, None, [ast.ConditionalLiteral(location,choice_atom,[])], None)                    
+                        choice_atom = ast.Literal(
+                            location, 0, ast.SymbolicAtom(choice_atom)
+                        )
+                    choice = ast.Aggregate(
+                        location,
+                        None,
+                        [ast.ConditionalLiteral(location, choice_atom, [])],
+                        None,
+                    )
                     body = []
                     body.extend(rule.body)
                     body.extend(condition)
-                    self.rules_to_add.append((choice,body))
+                    self.rules_to_add.append((choice, body))
                     new_element_condition = [choice_atom]
                     new_element_condition.extend(condition)
-                    new_elements.append(ast.TheoryAtomElement([ast.TheoryUnparsedTerm(location,unparsed_terms)],new_element_condition))
+                    new_elements.append(
+                        ast.TheoryAtomElement(
+                            [ast.TheoryUnparsedTerm(location, unparsed_terms)],
+                            new_element_condition,
+                        )
+                    )
                 else:
                     new_elements.append(element)
-            rule.head.elements=new_elements
+            rule.head.elements = new_elements
         return rule.update(**self.visit_children(rule))

fclingo/translator.py

@@ -10,6 +10,7 @@
 
 AUX = "__aux"
 
+
 class ConstraintAtom:
     """
     Representation of a constraint atom.
@@ -145,23 +146,20 @@ def copy(term):
 
     def __eq__(self, another_term):
         if not isinstance(another_term, ConstraintTerm):
-            raise TypeError('Can only compare two ConstraintTerms')   
+            raise TypeError("Can only compare two ConstraintTerms")
         return str(self) == str(another_term)
-    
+
     def __hash__(self):
         return hash(str(self))
 
+
 ONE = ConstraintTerm(None, 1, None, clingo.TheoryTermType.Number)
 ZERO = ConstraintTerm(None, 0, None, clingo.TheoryTermType.Number)
-SUM_TERM_HEAD = ConstraintTerm(
-    "__sum" + HEAD, None, [], clingo.TheoryTermType.Function
-)
+SUM_TERM_HEAD = ConstraintTerm("__sum" + HEAD, None, [], clingo.TheoryTermType.Function)
 FSUM_TERM_HEAD = ConstraintTerm(
     PREFIX + "sum" + HEAD, None, [], clingo.TheoryTermType.Function
 )
-SUM_TERM_BODY = ConstraintTerm(
-    "__sum" + BODY, None, [], clingo.TheoryTermType.Function
-)
+SUM_TERM_BODY = ConstraintTerm("__sum" + BODY, None, [], clingo.TheoryTermType.Function)
 FSUM_TERM_BODY = ConstraintTerm(
     PREFIX + "sum" + BODY, None, [], clingo.TheoryTermType.Function
 )
@@ -173,9 +171,10 @@ class Translator:
     including assignments and conditionals into a Clingcon program.
     """
 
-    def __init__(self, prg, config):
+    def __init__(self, prg, config, stats):
         self._prg = prg
         self._config = config
+        self._stats = stats
         self._defined = {}
         self._auxvars = 0
         self._sum_constraints = set()
@@ -230,10 +229,12 @@ def _add_auxvar(self):
             clingo.TheoryTermType.Function,
         )
         self._auxvars += 1
+        self._stats.variables_added += 1
         return var
 
     def _add_atom(self, symbol=None):
         with self._prg.backend() as backend:
+            self._stats.constraints_added += 1
             if symbol:
                 return backend.add_atom(symbol)
             return backend.add_atom()
@@ -255,6 +256,7 @@ def _search_atom(self, lit):
 
     def _add_rule(self, head, body, choice=False):
         with self._prg.backend() as backend:
+            self._stats.rules_added += 1
             backend.add_rule(head, body, choice)
         if self._config.print_trans:
             head_atoms = []
@@ -288,7 +290,9 @@ def _add_defined(self, var, reason=None):
 
     def _define_variables(self, atom):
         assert (
-            match(atom.term, PREFIX + "sum" + HEAD, 0) or match(atom.term, PREFIX + "sus" + HEAD, 0) or match(atom.term, "__sum" + HEAD, 0)
+            match(atom.term, PREFIX + "sum" + HEAD, 0)
+            or match(atom.term, PREFIX + "sus" + HEAD, 0)
+            or match(atom.term, "__sum" + HEAD, 0)
         ) and not self.conditional(atom)
         for var in self.vars(atom.guard[1]):
             self._add_defined(var, [atom.literal])
@@ -460,9 +464,7 @@ def _translate_max(self, atom):
         elif ">" in rel:
             rel = rel.replace(">", "<")
         type_term = ConstraintTerm(
-            PREFIX + "min" + BODY
-            if BODY in atom.term.name
-            else PREFIX + "min" + HEAD,
+            PREFIX + "min" + BODY if BODY in atom.term.name else PREFIX + "min" + HEAD,
             None,
             [],
             clingo.TheoryTermType.Function,
@@ -653,7 +655,7 @@ def _translate_constraint(self, atom):
             assert len(atom.elements) == 1 and not self.conditional(atom)
             var = self.vars(atom.elements[0].terms[0]).pop()
             def_lit = self._add_defined(var)
-            self._add_rule([atom.literal],[def_lit])
+            self._add_rule([atom.literal], [def_lit])
         elif (
             (
                 match(atom.term, PREFIX + "sum" + BODY, 0)
@@ -686,10 +688,10 @@ def _translate_constraints(self, theory_atoms):
         for atom in theory_atoms:
             self._translate_constraint(atom)
 
-    def _prepare_theory_atoms(self,theory_atoms):
+    def _prepare_theory_atoms(self, theory_atoms):
         atoms = []
         for atom in theory_atoms:
-            ca =  ConstraintAtom.copy(atom)
+            ca = ConstraintAtom.copy(atom)
             if (
                 match(ca.term, PREFIX + "sum" + BODY, 0)
                 or match(ca.term, PREFIX + "sum" + HEAD, 0)
@@ -715,4 +717,4 @@ def translate(self, theory_atoms):
         theory_atoms = self._prepare_theory_atoms(theory_atoms)
         self._translate_constraints(theory_atoms)
         self._fix_undefined()
-        self._prg.cleanup()
+        self._prg.cleanup()

tests/__init__.py

@@ -7,12 +7,12 @@
 from clingo.ast import Location, Position, ProgramBuilder, Rule, parse_string
 
 from fclingo import THEORY, Translator
-from fclingo.__main__ import CSP, DEF
+from fclingo.__main__ import CSP, DEF, Statistic
 from fclingo.parsing import HeadBodyTransformer
 
 
 class Config:
-    def __init__(self, max_int, min_int, print_trans ,defined) -> None:
+    def __init__(self, max_int, min_int, print_trans, defined) -> None:
         self.max_int = max_int
         self.min_int = min_int
         self.print_trans = print_trans
@@ -69,16 +69,17 @@ def solve(self, s):
             hbt = HeadBodyTransformer()
             parse_string(
                 s,
-                lambda ast: bld.add(hbt.visit(ast))
-                ,
+                lambda ast: bld.add(hbt.visit(ast)),
             )
-            pos = Position('<string>', 1, 1)
+            pos = Position("<string>", 1, 1)
             loc = Location(pos, pos)
             for rule in hbt.rules_to_add:
-                bld.add(Rule(loc,rule[0],rule[1]))
+                bld.add(Rule(loc, rule[0], rule[1]))
 
         self.prg.ground([("base", [])])
-        translator = Translator(self.prg, Config(self.maxint, self.minint, False, DEF))
+        translator = Translator(
+            self.prg, Config(self.maxint, self.minint, False, DEF), Statistic()
+        )
         translator.translate(self.prg.theory_atoms)
 
         ret = []