Commit 9814e6c4 authored by Ing. Martin Svatoš's avatar Ing. Martin Svatoš
Browse files

base camp

parents
import itertools
import pycosat
import time
from collections import defaultdict
from typing import List
from logic import *
'''
This file contains subsumption engine (based on pycosat).
'''
def addSpecialSymbol(literal: Literal) -> Literal:
prefix = "~~" if literal.positive else "~~!"
predicate = Predicate(prefix + literal.atom.predicate.name, literal.atom.predicate.arity)
return Literal(Atom(predicate, literal.atom.terms), positive=True)
def addExactlyOneHoldConstraint(constraints: List[List[int]], variables: Iterable[int]) -> None:
constraints.append([variable for variable in variables])
for i, j in itertools.combinations(variables, r=2):
constraints.append([-i, -j])
def findPycosatSubstitutions(allSolutions: bool, query: Iterable[Literal], world: Iterable[Literal]) -> List[Dict[Variable, Term]]:
# general case
start = time.time()
# encode to CSP
# encode instance
literalsPerPredicate: Dict[Predicate, Set[Literal]] = defaultdict(set)
totalVars = 0
terms: Iterable[Term] = unionSets(set(literal.atom.terms) for literal in world)
universalDomain: Set[Variable] = set()
def varCounter():
nonlocal totalVars
totalVars += 1
return totalVars
assignments: Dict['var', Dict['term', int]] = defaultdict(lambda: defaultdict(varCounter)) # id of var->term, i.e. assignment[var][term] returns id of propositional variable
for literal in world:
literalsPerPredicate[literal.getPredicate()].add(literal)
if not literal.positive:
raise ValueError("Only non-negated literals are allowed for the world variable.")
constraints: List[List[int]] = []
for literal in query:
if literal.isGround():
if (literal.positive and literal not in world) or ((not literal.positive) and literal.negation() in world):
return [] # if a query's l is ground but is not in the world, then the query cannot subsume the world (similarly for negative literal)
continue
if not literal.positive:
for variable in literal.getVariables():
universalDomain.add(variable)
possibleMappings: Set[Tuple[int]] = set()
for potential in literalsPerPredicate[literal.getPredicate()]:
possibleUnification = unifyFirstWithSecond(literal, potential)
if None is possibleUnification:
continue
possibleMappings.add(tuple(assignments[var][target] for var, target in possibleUnification.items()))
if literal.positive and not possibleMappings: # there is no literal in world to which l can be mapped, therefore unsatisfiable
return []
if literal.positive:
mappingVariants = []
for mapping in possibleMappings:
auxiliarLiteralVariable = varCounter()
mappingVariants.append(auxiliarLiteralVariable)
implication = [-propositionalVariable for propositionalVariable in mapping]
implication.append(auxiliarLiteralVariable)
constraints.append(implication)
for propositionalVariable in mapping:
constraints.append([propositionalVariable, -auxiliarLiteralVariable])
addExactlyOneHoldConstraint(constraints, mappingVariants)
else: # actually restriction on solutions
for forbidden in possibleMappings:
constraints.append([-propositionalVariable for propositionalVariable in forbidden])
for variable, term in itertools.product(universalDomain, terms):
addingPropositionalVariable = assignments[variable][term]
for var, termsAssignment in assignments.items():
addExactlyOneHoldConstraint(constraints, termsAssignment.values())
encodingTime = time.time() - start
# solver
start = time.time()
solutions = []
if allSolutions:
for solution in pycosat.itersolve(constraints):
if solution not in ("UNSAT", "UNKNOWN"):
solutions.append(solution)
else:
solution = pycosat.solve(constraints)
if solution not in ("UNSAT", "UNKNOWN"):
solutions.append(solution)
satTime = time.time() - start
# print("encoding\t{}\nsat \t{}".format(encodingTime, satTime))
# transfer solution to FOL representation
propositionalToAssignment = {propositionalVariable: (variable, term) for variable, termsAssignment in assignments.items() for term, propositionalVariable in termsAssignment.items()}
substitutions = [dict(propositionalToAssignment[propositionalVariable] for propositionalVariable in model if propositionalVariable in propositionalToAssignment) for model in solutions]
return substitutions
def findSubstitutions(query: Clause, world: Clause, allSolutions=True) -> List[Dict[Variable, Term]]:
'''
By default it searches for all substitutions (all_solutions=True). If all_solutions=False, then only one is returned.
:param query: Clause
:param world: Clause
:param allSolutions: bool
:return: List[Dict[Variable,Term]]
'''
# special (ground) case
if len(query.getVariables()) < 1:
for l in query:
if (l.positive and l not in world) or ((not l.positive) and l.negation() in world):
return []
return [{}] # although it looks weird, it actually means that there is one empty substitution, i.e. a very trivial one
return findPycosatSubstitutions(allSolutions, query, world)
def subsumes(query: Clause, world: Clause) -> bool:
'''
Given a world and a query, the method decides whether the query theta-subsume the world.
:param query: Clause
:param world: Clause
:return: bool
'''
query = Clause(map(addSpecialSymbol, query))
world = Clause(map(addSpecialSymbol, world))
substitutions = findSubstitutions(query, world, allSolutions=False)
return len(substitutions) > 0
from modgrammar import *
from logic import *
'''
This file contains functionality for parsing expressions of FOL terms and universally quantified clauses.
Note that constants should start with an uppercase letter while variables should start with a lowercase letter.
Also note that symbols (names of variables, constants, functors, predicates) should not contain brackets and commas.
'''
grammar_whitespace_mode = 'optional'
delimiters = set([",", "(", ")"])
predicateCache: Dict[Tuple[str, int], Predicate] = {}
functorsCache: Dict[Tuple[str, int], Functor] = {}
varConstCache: Dict[str, Term] = {}
class Name(Grammar):
grammar = (ANY_EXCEPT(",()"))
def toTerm(self) -> Term:
name = str(self.elements[0])
if len(name) < 1:
raise ValueError("term cannot be an empty string")
if name[0].isupper():
return Variable(name)
return Constant(name)
class CompTerm(Grammar):
grammar = (Name, "(", LIST_OF(REF("Ter"), sep=","), ")")
def toTerm(self) -> Term:
name = str(self.elements[0])
termsList = self.elements[2].elements
terms = [term.toTerm() for term in termsList if str(term) not in delimiters]
arity = len(terms)
key = (name, arity)
if key not in functorsCache:
functorsCache[key] = Functor(name, arity)
functor = functorsCache[key]
return CompoundTerm(functor, terms)
# aka term
class Ter(Grammar):
grammar = (Name | CompTerm)
def toTerm(self) -> Term:
return self.elements[0].toTerm()
# aka Literal
class Lit(Grammar):
grammar = (Name, "(", OR(EMPTY, LIST_OF(Ter, sep=",")), ")")
def toLiteral(self) -> Literal:
name = str(self.elements[0])
positive = True
if name.startswith("!"):
positive = False
name = name[1:]
terms = []
if self.elements[2]:
termsList = self.elements[2].elements
terms = [term.toTerm() for term in termsList if str(term) not in delimiters]
arity = len(terms)
key = (name, arity)
if key not in predicateCache:
predicateCache[key] = Predicate(name, arity)
predicate = predicateCache[key]
return Literal(Atom(predicate, terms), positive)
class ClauseGrammar(Grammar):
grammar = (LIST_OF(Lit, sep=","))
def toClause(self) -> Clause:
literals = []
if len(self.elements) > 0:
literals = [l.toLiteral() for l in self.elements[0].elements if str(l) not in delimiters]
return Clause(literals)
class SampleGrammar(Grammar):
grammar = (OR(L("+"), L("-")), ClauseGrammar)
def toSample(self) -> Tuple[bool, Iterable[Atom]]:
return (True if "+" == str(self.elements[0]) else False, [l.atom for l in self.elements[1].toClause()])
def parseClause(string: str) -> Clause:
'''
Use to parse a clause.
:param string:
:return: Clause
'''
parsing = ClauseGrammar.parser()
return parsing.parse_text(string, eof=True).toClause()
def parseLiteral(string: str) -> Literal:
'''
Use to parse a literal.
:param string:
:return: Literal
'''
parsing = Lit.parser()
return parsing.parse_text(string, eof=True).toLiteral()
def parseTerm(string: str) -> Term:
'''
Use to parse a term.
:param string:
:return: Term
'''
parsing = Ter.parser()
return parsing.parse_text(string, eof=True).toTerm()
def parseSample(string: str) -> Tuple[bool, Iterable[Atom]]:
'''
Use to parse a sample, which consists of a label and an interpretation.
:param string:
:return: Tuple[bool, Iterable[Atom]]
'''
parsing = SampleGrammar.parser()
return parsing.parse_text(string, eof=True).toSample()
from typing import Set, Iterable, Tuple, Dict, Iterator
import functools
'''
This file contains various support for first-order predicate (FOL) logic.
Note that constants should start with an upper-case letter while variables should start with a lower-case one.
Also note that symbols (names of variables, constants, functors, predicates) should not contain brackets and commas.
'''
def unionSets(iterableOfSets: Iterable[Set['Generic']]) -> Set['Generic']:
'''
Taking iterable of set, this method makes one big set by union of all the set given.
:type iterableOfSets: iterable of set of T
:rtype: set of T
'''
iterableOfSets = tuple(iterableOfSets)
if len(iterableOfSets) == 1:
# special case, trailing comma at the end of the tuple makes the problem
return iterableOfSets[0]
try:
if len(iterableOfSets) <= 0:
return set()
return functools.reduce(lambda x, y: x.union(y), iterableOfSets)
except Exception as e:
raise ValueError('unionSets: {}\n{}'.format(iterableOfSets, e))
class Term:
'''
An interface for FOL term.
'''
def getVariables(self) -> Set['Variable']:
'''
Returns set of the term's variables.
:rtype: set of Variable
'''
raise NotImplementedError("Method not implemented.")
def getConstants(self) -> Set['Constant']:
'''
Returns set of constants of the term.
:rtype: set of Constant
'''
raise NotImplementedError("Method not implemented.")
def substitute(self, substitution: Dict['Variable', 'Term']) -> 'Term':
'''
Returns the same term but substituted by the substitution represented by dict of (Variable,Term).
:type substitution: dict of (Variable,Term)
:rtype: Term
'''
raise NotImplementedError("Method not implemented.")
def getFunctors(self) -> Set['Functor']:
'''
Returns set of functors.
:rtype: set of Functor
'''
raise NotImplementedError("Method not implemented.")
class Variable(Term):
'''
Represents FOL variable.
'''
def __init__(self, name: str):
self.name: str = name
def __hash__(self):
return hash(str(self.name))
def __str__(self):
return self.name
def __eq__(self, o: object) -> bool:
return isinstance(o, self.__class__) and str(self) == str(o)
def __ne__(self, o: object) -> bool:
return not self.__eq__(o)
def getVariables(self) -> Set['Variable']:
'''
Returns set of the term's variables.
:rtype: set of Variable
'''
r = set()
r.add(self)
return r
def substitute(self, substitution: Dict['Variable', Term]) -> Term:
'''
Returns the same term but substituted by the substitution represented by dict of (Variable,Term).
:type substitution: dict of (Variable,Term)
:rtype: Term
'''
if self in substitution:
return substitution[self]
return self
def getConstants(self) -> Set['Constant']:
'''
Returns set of constants of the term.
:rtype: set of Constant
'''
return set()
def getFunctors(self) -> Set['Functor']:
'''
Returns set of functors.
:rtype: set of Functor
'''
return set()
class Constant(Term):
'''
Represents FOL constant.
'''
def __init__(self, name: str):
self.name: str = name
def __str__(self):
return self.name
def __eq__(self, other):
return isinstance(other, self.__class__) and str(self) == str(other)
def __ne__(self, other):
return not self == other
def __hash__(self):
return hash(str(self))
def getVariables(self) -> Set[Variable]:
'''
Returns set of the term's variables.
:rtype: set of Variable
'''
return set()
def substitute(self, substitution: Dict[Variable, Term]) -> Term:
'''
Returns the same term but substituted by the substitution represented by dict of (Variable,Term).
:type substitution: dict of (Variable,Term)
:rtype: Term
'''
return self
def getConstants(self) -> Set['Constant']:
'''
Returns set of constants of the term.
:rtype: set of Constant
'''
r = set()
r.add(self)
return r
def getFunctors(self) -> Set['Functor']:
'''
Returns set of functors.
:rtype: set of Functor
'''
return set()
class Functor:
'''
Represents FOL functor.
'''
def __init__(self, name: str, arity: int):
self.name: str = name
self.arity: int = arity
def __eq__(self, other):
return isinstance(other, self.__class__) and self.name == other.name and self.arity == other.arity
def __ne__(self, other):
return not self == other
def __hash__(self):
return (self.name, self.arity).__hash__()
def __str__(self):
return "{}/{}".format(self.name, self.arity)
class CompoundTerm(Term):
'''
Use .functor to get Functor of this composed term.
Use .terms to get tuple of terms.
'''
def __init__(self, functor: Functor, terms: Iterable[Term]):
'''
Creates and returns a new compound term which is constructed by a functor applied to list of arguments.
:type functor: Functor
:type terms: iterable of Term
:rtype: CompoundTerm
'''
terms = tuple(terms)
if functor.arity != len(terms):
raise ValueError(
"functor's arity '{}' is different than arguments given '{}'".format(functor,
', '.join(map(str, terms))))
self.functor: Functor = functor
self.terms: Tuple[Term] = terms
def __eq__(self, other):
return isinstance(other, self.__class__) and str(self).__eq__(str(other))
def __ne__(self, other):
return not self == other
def __hash__(self):
return str(self).__hash__()
def __str__(self):
if len(self.terms) != self.functor.arity:
raise AssertionError()
return "{}({})".format(self.functor.name, ", ".join(map(str, self.terms)))
def __iter__(self) -> Iterator[Term]:
return iter(self.terms)
def __getitem__(self, idx) -> Term:
return self.terms[idx]
def __len__(self):
return len(self.terms)
def getVariables(self) -> Set[Variable]:
'''
Returns set of the term's variables.
:rtype: set of Variable
'''
return unionSets(term.getVariables() for term in self.terms)
def substitute(self, substitution: Dict[Variable, Term]) -> Term:
'''
Returns the same term but substituted by the substitution represented by dict of (Variable,Term).
:type substitution: dict of (Variable,Term)
:rtype: Term
'''
return CompoundTerm(self.functor, [term.substitute(substitution) for term in self.terms])
def getConstants(self) -> Set[Constant]:
'''
Returns set of constants of the term.
:rtype: set of Constant
'''
return unionSets(term.getConstants() for term in self.terms)
def getFunctors(self) -> Set[Functor]:
'''
Returns set of functors.
:rtype: set of Functor
'''
result = set()
result.add(self.functor)
result = result.union(unionSets(map(lambda term: term.getFunctors(), self.terms)))
return result
class Predicate:
def __init__(self, name: str, arity: int):
'''
Creates and returns a new predicate by given name and arity. Length of the name should be longer than zero.
:param name: str
:param arity: int,>=0
:rtype: Predicate
'''
self.name: str = name
self.arity: int = arity
def __eq__(self, other):
return isinstance(other, self.__class__) and self.name == other.name and self.arity == other.arity
def __ne__(self, other):
return not self == other
def __hash__(self):
return (self.name, self.arity).__hash__()
def __str__(self):
'''
Get Prolog-like notation.
:rtype: str
'''
return "{}/{}".format(self.name, self.arity)
class Atom:
def __init__(self, predicate: Predicate, terms: Iterable[Term]) -> 'Atom':
'''
Creates new atom given predicate and list of terms.
:type predicate: Predicate
:type terms: list of Term
:rtype: Atom
'''
terms = tuple(terms)
if isinstance(predicate, Predicate) and predicate.arity != len(terms):
raise ValueError(
"predicate's '{}' arity differs from the arguments given '{}'".format(predicate,
', '.join(map(str, terms))))
self.predicate: Predicate = predicate if isinstance(predicate, Predicate) else Predicate(predicate.name, len(terms))
self.terms: Tuple[Term] = terms
self.arity: int = predicate.arity
def __str__(self):
if 1 > self.arity:
return self.predicate.name