deepxube.logic.logic_utils

  1from typing import List, Set, Tuple, Dict
  2from deepxube.logic.logic_objects import Clause, Literal, Atom
  3from deepxube.utils import misc_utils
  4import re
  5
  6
  7def parse_literal(lit_str: str) -> Literal:
  8    # check for negation
  9    not_match = re.match(r"\s*not\s+(.*)", lit_str)
 10    positive: bool
 11    if not_match is None:
 12        positive = True
 13    else:
 14        positive = False
 15        lit_str = not_match.group(1).strip()
 16
 17    # parse literal
 18    lit_str = misc_utils.remove_all_whitespace(lit_str)
 19    match = re.match(r"([^(]+)(\((.*)\))?", lit_str)
 20    assert match is not None
 21    pred_name: str = match.group(1)
 22    pred_args: Tuple[str, ...]
 23    if match.group(3) is not None:
 24        pred_args = tuple([x.strip() for x in match.group(3).split(",")])
 25    else:
 26        pred_args = tuple()
 27
 28    # TODO, better way to handle directions?
 29    directions = ["in"] * len(pred_args)
 30
 31    literal: Literal = Literal(pred_name, pred_args, tuple(directions), positive=positive)
 32    return literal
 33
 34
 35def replace_anon_vars(lit: Literal, all_lits: List[Literal]) -> Literal:
 36    all_args: Set[str] = set()
 37    for lit2 in [lit] + all_lits:
 38        all_args.update(lit2.arguments)
 39
 40    args_new: List[str] = []
 41    for arg in lit.arguments:
 42        if arg == "_":
 43            arg_new: str = "V0"
 44            arg_new_idx: int = 0
 45            while arg_new in all_args:
 46                arg_new_idx += 1
 47                arg_new = f"V{arg_new_idx}"
 48            all_args.add(arg_new)
 49
 50            args_new.append(arg_new)
 51        else:
 52            args_new.append(arg)
 53
 54    lit_ret: Literal = Literal(lit.predicate, tuple(args_new), lit.directions, positive=lit.positive)
 55    return lit_ret
 56
 57
 58def parse_clause(constr_str: str) -> Tuple[Clause, Dict[str, List[str]]]:
 59    head_str, body_str = constr_str.split(":-")
 60    head_lit = parse_literal(head_str)
 61
 62    # lits
 63    body_lit_strs: Tuple[str, ...] = tuple(re.findall(r"[^,]+\([^)]+\)|^\s*[^,]+|[^,)]+\s*$", body_str))
 64    body_lits: List[Literal] = []
 65    for body_lit_str in body_lit_strs:
 66        body_lit = parse_literal(body_lit_str)
 67        body_lits.append(body_lit)
 68
 69    # subs forbid
 70    subs_forbid: Dict[str, List[str]] = dict()
 71    sub_forbid_strs = re.findall(r"\s*([^,]+)\s*!\s*=\s*([^,]+)\s*", body_str)
 72    for v1, v2 in sub_forbid_strs:
 73        v1 = v1.strip()
 74        v2 = v2.strip()
 75        if v1 not in subs_forbid:
 76            subs_forbid[v1] = []
 77        if v2 not in subs_forbid:
 78            subs_forbid[v2] = []
 79
 80        subs_forbid[v1].append(v2)
 81        subs_forbid[v2].append(v1)
 82
 83    head_lit = replace_anon_vars(head_lit, [head_lit] + body_lits)
 84    for idx, body_lit in enumerate(body_lits):
 85        body_lits[idx] = replace_anon_vars(body_lit, [head_lit] + body_lits)
 86
 87    clause: Clause = Clause(head_lit, tuple(body_lits))
 88    return clause, subs_forbid
 89
 90
 91def copy_clause_with_new_head(clause: Clause, head_name_new: str) -> Clause:
 92    assert clause.head.positive, "Head should be positive"
 93    clause_new = Clause(Literal(head_name_new, clause.head.arguments, clause.head.directions,
 94                                positive=clause.head.positive), clause.body)
 95
 96    return clause_new
 97
 98
 99def atom_to_str(atom: Atom) -> str:
100    return f"{atom[0]}({','.join(atom[1:])})"