Skip to content

Commit

Permalink
fromat and fixed tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@wanko
wanko committed May 16, 2024
1 parent ba9bf4b commit be68531
Show file tree
Hide file tree
Showing 5 changed files with 111 additions and 60 deletions.
26 changes: 15 additions & 11 deletions fclingo/__main__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -19,6 +18,7 @@
CSP = "__csp"
DEF = "__def"


class Statistic:
"""
Class for statistics of fclingo translation.
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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):
Expand Down Expand Up @@ -181,10 +185,10 @@ def main(self, control, 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

Expand All @@ -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)
Expand Down
46 changes: 37 additions & 9 deletions fclingo/parsing.py
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
"""
This module contains functions for parsing and normalizing constraints.
"""

import clingo
from clingo import ast

Expand Down Expand Up @@ -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))
36 changes: 17 additions & 19 deletions fclingo/translator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

AUX = "__aux"


class ConstraintAtom:
"""
Representation of a constraint atom.
Expand Down Expand Up @@ -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
)
Expand Down Expand Up @@ -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()
Expand All @@ -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 = []
Expand Down Expand Up @@ -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])
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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()
self._prg.cleanup()
15 changes: 8 additions & 7 deletions tests/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 = []
Expand Down
Loading

0 comments on commit be68531

Please sign in to comment.