From 20f2249b77e7e42be5fcfc6bd7dd5be222060c79 Mon Sep 17 00:00:00 2001 From: wanko Date: Tue, 14 May 2024 13:01:25 +0200 Subject: [PATCH 1/3] add statistics --- fclingo/__main__.py | 35 ++++++++++++++++++++++++++++++++--- fclingo/translator.py | 3 ++- 2 files changed, 34 insertions(+), 4 deletions(-) diff --git a/fclingo/__main__.py b/fclingo/__main__.py index 7e6c297..38e7a8b 100644 --- a/fclingo/__main__.py +++ b/fclingo/__main__.py @@ -3,12 +3,14 @@ """ import sys +import time import clingo from clingcon import ClingconTheory from clingo.ast import ProgramBuilder, parse_files, Location, Position, Rule from fclingo import THEORY +from fclingo import translator from fclingo.parsing import HeadBodyTransformer from fclingo.translator import AUX, Translator @@ -17,6 +19,18 @@ 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 + + class AppConfig: """ Class for application specific options. @@ -40,6 +54,7 @@ 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.stats = Statistic() self._theory = ClingconTheory() self._answer = 0 @@ -129,6 +144,14 @@ def register_options(self, options): 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 constraints added"] = self.stats.constraints_added + fclingo["Number of rules added"] = self.stats.rules_added return True def _read(self, path): @@ -142,7 +165,6 @@ 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)) @@ -150,6 +172,7 @@ def main(self, control, files): if not files: files = ["-"] + start = time.time() with ProgramBuilder(control) as bld: hbt = HeadBodyTransformer() parse_files( @@ -160,14 +183,20 @@ def main(self, control, files): loc = Location(pos, pos) for rule in hbt.rules_to_add: 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(): diff --git a/fclingo/translator.py b/fclingo/translator.py index e7c09f7..9f59f68 100644 --- a/fclingo/translator.py +++ b/fclingo/translator.py @@ -173,9 +173,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() From ba9bf4bb869f1e57c9f0cc8ed8e9af6fc478b537 Mon Sep 17 00:00:00 2001 From: wanko Date: Thu, 16 May 2024 12:15:16 +0200 Subject: [PATCH 2/3] add statistiscs --- fclingo/__main__.py | 2 ++ fclingo/translator.py | 3 +++ 2 files changed, 5 insertions(+) diff --git a/fclingo/__main__.py b/fclingo/__main__.py index 38e7a8b..ccb17c8 100644 --- a/fclingo/__main__.py +++ b/fclingo/__main__.py @@ -29,6 +29,7 @@ def __init__(self): self.translate_program = 0 self.constraints_added = 0 self.rules_added = 0 + self.variables_added = 0 class AppConfig: @@ -150,6 +151,7 @@ def _on_statistics(self, step, akku): 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 diff --git a/fclingo/translator.py b/fclingo/translator.py index 9f59f68..3a60673 100644 --- a/fclingo/translator.py +++ b/fclingo/translator.py @@ -231,10 +231,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() @@ -256,6 +258,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 = [] From be68531d618de0fd904d77a4e38d9f3c4e49c871 Mon Sep 17 00:00:00 2001 From: wanko Date: Thu, 16 May 2024 12:21:07 +0200 Subject: [PATCH 3/3] fromat and fixed tests --- fclingo/__main__.py | 26 +++++++++++++---------- fclingo/parsing.py | 46 +++++++++++++++++++++++++++++++++-------- fclingo/translator.py | 36 +++++++++++++++----------------- tests/__init__.py | 15 +++++++------- tests/test_htc.py | 48 ++++++++++++++++++++++++++++++------------- 5 files changed, 111 insertions(+), 60 deletions(-) diff --git a/fclingo/__main__.py b/fclingo/__main__.py index ccb17c8..9e6ebff 100644 --- a/fclingo/__main__.py +++ b/fclingo/__main__.py @@ -7,10 +7,9 @@ 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 translator +from fclingo import THEORY, translator from fclingo.parsing import HeadBodyTransformer from fclingo.translator import AUX, Translator @@ -19,6 +18,7 @@ CSP = "__csp" DEF = "__def" + class Statistic: """ Class for statistics of fclingo translation. @@ -54,7 +54,9 @@ 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 @@ -80,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) @@ -107,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 @@ -140,7 +144,7 @@ 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): @@ -181,10 +185,10 @@ def main(self, control, files): files, lambda stm: bld.add(hbt.visit(stm)), ) - pos = Position('', 1, 1) + pos = Position("", 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 @@ -195,7 +199,7 @@ def main(self, control, files): translator = Translator(control, self.config, self.stats) translator.translate(control.theory_atoms) end = time.time() - self.stats.translate_program = end -start + self.stats.translate_program = end - start self._theory.prepare(control) control.solve(on_model=self.on_model, on_statistics=self._on_statistics) diff --git a/fclingo/parsing.py b/fclingo/parsing.py index 25627ff..014fd38 100644 --- a/fclingo/parsing.py +++ b/fclingo/parsing.py @@ -1,6 +1,7 @@ """ This module contains functions for parsing and normalizing constraints. """ + import clingo from clingo import ast @@ -138,7 +139,7 @@ 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: @@ -146,23 +147,50 @@ def visit_Rule(self,rule): 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)) diff --git a/fclingo/translator.py b/fclingo/translator.py index 3a60673..9de5241 100644 --- a/fclingo/translator.py +++ b/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 ) @@ -231,12 +229,12 @@ def _add_auxvar(self): clingo.TheoryTermType.Function, ) self._auxvars += 1 - self._stats.variables_added+=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 + self._stats.constraints_added += 1 if symbol: return backend.add_atom(symbol) return backend.add_atom() @@ -258,7 +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 + self._stats.rules_added += 1 backend.add_rule(head, body, choice) if self._config.print_trans: head_atoms = [] @@ -292,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]) @@ -464,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, @@ -657,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) @@ -690,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) @@ -719,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() \ No newline at end of file + self._prg.cleanup() diff --git a/tests/__init__.py b/tests/__init__.py index 1d80c68..9b0d065 100644 --- a/tests/__init__.py +++ b/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('', 1, 1) + pos = Position("", 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 = [] diff --git a/tests/test_htc.py b/tests/test_htc.py index 8963dff..3d143fd 100644 --- a/tests/test_htc.py +++ b/tests/test_htc.py @@ -232,7 +232,7 @@ def test_defined(self): -10, 10, ), - [["b",("x", 0)]], + [["b", ("x", 0)]], ) self.assertEqual( solve( @@ -242,7 +242,7 @@ def test_defined(self): -10, 10, ), - [["b",("x", 0)]], + [["b", ("x", 0)]], ) self.assertEqual( solve( @@ -252,7 +252,7 @@ def test_defined(self): -10, 10, ), - [[("x", 0),("y", 0)]], + [[("x", 0), ("y", 0)]], ) self.assertEqual( solve( @@ -263,7 +263,7 @@ def test_defined(self): -10, 10, ), - [["b",("x",2),("y",2)]], + [["b", ("x", 2), ("y", 2)]], ) def test_multiset(self): @@ -639,7 +639,7 @@ def test_choice_sum(self): -10, 10, ), - [['a', ('x', 4)]], + [["a", ("x", 4)]], ) self.assertEqual( solve( @@ -660,7 +660,15 @@ def test_choice_sum(self): -2, 2, ), - [['a', ('x', 2), ('y', 0)], ['a', 'b', ('x', 0), ('y', 2)], ['a', 'b', ('x', 0), ('y', 2)], ['a', 'b', ('x', 1), ('y', 1)], ['a', 'b', ('x', 2), ('y', 0)], ['a', 'b', ('x', 2), ('y', 0)], ['b', ('x', 0), ('y', 2)]], + [ + ["a", ("x", 2), ("y", 0)], + ["a", "b", ("x", 0), ("y", 2)], + ["a", "b", ("x", 0), ("y", 2)], + ["a", "b", ("x", 1), ("y", 1)], + ["a", "b", ("x", 2), ("y", 0)], + ["a", "b", ("x", 2), ("y", 0)], + ["b", ("x", 0), ("y", 2)], + ], ) self.assertEqual( solve( @@ -670,7 +678,7 @@ def test_choice_sum(self): -10, 10, ), - [['a', ('x', 8)]], + [["a", ("x", 8)]], ) self.assertEqual( solve( @@ -681,7 +689,7 @@ def test_choice_sum(self): -2, 2, ), - [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 2), ('x(2)', 2)]], + [["a(1)", "a(2)", "r(1)", "r(2)", ("x(1)", 2), ("x(2)", 2)]], ) self.assertEqual( solve( @@ -692,7 +700,10 @@ def test_choice_sum(self): -4, 4, ), - [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 4), ('x(2)', 4)], ['a(1)', 'r(1)', ('x(1)', 4), ('x(2)', 0)]], + [ + ["a(1)", "a(2)", "r(1)", "r(2)", ("x(1)", 4), ("x(2)", 4)], + ["a(1)", "r(1)", ("x(1)", 4), ("x(2)", 0)], + ], ) def test_choice_sus(self): @@ -714,7 +725,7 @@ def test_choice_sus(self): -10, 10, ), - [['a', ('x', 4)]], + [["a", ("x", 4)]], ) self.assertEqual( solve( @@ -735,7 +746,13 @@ def test_choice_sus(self): -2, 2, ), - [['a', ('x', 2), ('y', 0)], ['a', 'b', ('x', 0), ('y', 2)], ['a', 'b', ('x', 1), ('y', 1)], ['a', 'b', ('x', 2), ('y', 0)], ['b', ('x', 0), ('y', 2)]], + [ + ["a", ("x", 2), ("y", 0)], + ["a", "b", ("x", 0), ("y", 2)], + ["a", "b", ("x", 1), ("y", 1)], + ["a", "b", ("x", 2), ("y", 0)], + ["b", ("x", 0), ("y", 2)], + ], ) self.assertEqual( solve( @@ -745,7 +762,7 @@ def test_choice_sus(self): -10, 10, ), - [['a', ('x', 8)]], + [["a", ("x", 8)]], ) self.assertEqual( solve( @@ -756,7 +773,7 @@ def test_choice_sus(self): -2, 2, ), - [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 2), ('x(2)', 2)]], + [["a(1)", "a(2)", "r(1)", "r(2)", ("x(1)", 2), ("x(2)", 2)]], ) self.assertEqual( solve( @@ -767,7 +784,10 @@ def test_choice_sus(self): -4, 4, ), - [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 4), ('x(2)', 4)], ['a(1)', 'r(1)', ('x(1)', 4), ('x(2)', 0)]], + [ + ["a(1)", "a(2)", "r(1)", "r(2)", ("x(1)", 4), ("x(2)", 4)], + ["a(1)", "r(1)", ("x(1)", 4), ("x(2)", 0)], + ], ) def test_taxes(self):