goel

package module
v0.0.0-...-97a57b4 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Mar 17, 2018 License: MIT Imports: 12 Imported by: 5

README

goel

goel is a reasoner for the Description Logic (DL) EL++ (see Pushing the EL Envelope Further by Franz Baader, Sebastian Brandt and Carsten Lutz).

More information about the state and usage comming soon, but here are some important installation instructions.

Installation

The EL++ solver requires that a LP solver is installed. We use lp_solve for this, together with the Go wrapper golp. However security issues in some newer Go versions broke many of the working cgo projects. At the best of my information right now the last version to really work is go1.9.3. The issue should be fixed in go1.10.1 but that is not released yet. So you need go1.9.3 at the moment.

To install lp_solve and golp correctly first follow the installation instructions for golp. Note that lp_solve is LGPL licensed and thus not shipped with goel. This means goel uses at run time a copy of the Library already present on the user's computer system.

Documentation

The code documentation is available via godoc.org:

  • goel Documentation for the reasoner
  • goel/domains Documentation for concrete domain support.

The MIT License (MIT)

Copyright (c) 2016, 2017, 2018 Fabian Wenzelmann

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

Third-Party Licenses

Despite from Go the following libraries are used.

lp_solve wance to be cited the following way as well: lpsolve citation data

Description : Open source (Mixed-Integer) Linear Programming system Language : Multi-platform, pure ANSI C / POSIX source code, Lex/Yacc based parsing Official name : lp_solve (alternatively lpsolve) Release data : Version 5.1.0.0 dated 1 May 2004 Co-developers : Michel Berkelaar, Kjell Eikland, Peter Notebaert Licence terms : GNU LGPL (Lesser General Public Licence) Citation policy : General references as per LGPL Module specific references as specified therein

Documentation

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func BCDOrFalse 

func BCDOrFalse(c Concept) bool

BCDOrFalse checks if the concept is either the bottom concept ⊥ or otherwise if it is in the BCD.

func BFS 

func BFS(g ConceptGraph, goal uint, start ...uint) bool

TODO there seems to be an infinite loop somewhere... TODO could easily be turned into a more concurrent version TODO think about the extended approach again... TODO maybe stop a node from being expanded if it has been expanded before? that is also true in the extended search.

func BFSToSet 

func BFSToSet(g ConceptGraph, goals map[uint]struct{}, start ...uint) map[uint]struct{}

TODO think about this again, seems rather slow... but why? hmmm...

func CheckCR1 

func CheckCR1(gci *NormalizedCI, sc *BCSet) bool

func CheckCR10 

func CheckCR10(sr BCPairSet, c, d Concept) bool

func CheckCR11 

func CheckCR11(sr1, sr2 *BCPairSet, c, d, e Concept) bool

func CheckCR2 

func CheckCR2(gci *NormalizedCI, sc *BCSet) bool

func CheckCR3 

func CheckCR3(gci *NormalizedCIRightEx, sc *BCSet) bool

func CheckCR4 

func CheckCR4(gci *NormalizedCILeftEx, c, d Concept, sd *BCSet, sr *BCPairSet) bool

func CheckCR5 

func CheckCR5(c, d Concept, sd *BCSet, sr *BCPairSet) bool

func ClosureToSet 

func ClosureToSet(g ConceptGraph, goals map[uint]struct{}, start ...uint) map[uint]struct{}

func CompareRMapping 

func CompareRMapping(first, second []*Relation) bool

func CompareSMapping 

func CompareSMapping(first, second []*BCSet) bool

CompareSMapping compares to mappings S1 and S2 (the mappings S from the algorithm).

func ContainsSorted 

func ContainsSorted(a []uint, x uint) bool

func InsertedSorted 

func InsertedSorted(values []uint, newValues map[uint]struct{}) []uint

func IntMax 

func IntMax(a, b int) int

IntMax returns the maximum of a and b.

func IntMin 

func IntMin(a, b int) int

IntMin returns the minimum of a and b.

func NormalizeStepPhaseOne 

func NormalizeStepPhaseOne(gci *GCIConstraint, intermediate *PhaseOneResult)

NormalizeStepPhaseOne performs one step of the normalization in phase 1. It tests what form the gci has and adds new formulae to the right slice of the intermediate result. That is it appends formulae to waiting or one of the intermediate results.

Phase one means to apply the rules NF2 - NF4 (NF1 is applied somewhere else).

func NormalizeStepPhaseTwo 

func NormalizeStepPhaseTwo(gci *GCIConstraint, intermediate *PhaseTwoResult)

NormalizeStepPhaseTwo performs one step of the normalization in phase 2. It tests what form the gci has and adds new formulae to the right slice of the intermediate result. That is it appends formulae to waiting or one of the intermediate results.

Phase one means to apply the rules NF5 - NF7.

func StringUintSet 

func StringUintSet(vals map[uint]struct{}) string

StringUintSet returns a set representation of a set of uints, escpecially useful during debugging.

func UIntMax 

func UIntMax(a, b uint) uint

UIntMax returns the maximum of a and b.

func UIntMin 

func UIntMin(a, b uint) uint

UIntMin returns the minimum of a and b.

Types

type ABox 

type ABox struct {
	ConceptAssertions []*ConceptAssertion
	RoleAssertions    []*RoleAssertion
}

ABox describes an ABox as a set of concept assertions and role assertions.

func NewABox 

func NewABox(conceptAssertions []*ConceptAssertion, roleAssertions []*RoleAssertion) *ABox

NewABox returns a new ABox.

type AddRNotification 

type AddRNotification struct {
	// contains filtered or unexported fields
}

func NewAddRNotification 

func NewAddRNotification(role uint, notification RNotification) AddRNotification

type AddSNotification 

type AddSNotification struct {
	// contains filtered or unexported fields
}

func NewAddSNotification 

func NewAddSNotification(value uint, notification SNotification) AddSNotification

type AllChangesCR6 

type AllChangesCR6 struct {
	// contains filtered or unexported fields
}

We add a map here that maps for each {a} to a list of all C with {a} ∈ S(C). This requires a bit more memory but I think(!) that it's worth it. Otherwise we always have to iterate over all S(D) and test where {a} is contained. This way finding all C, D with {a} ∈ S(C) ⊓ S(D) is easy.

func NewAllChangesCR6 

func NewAllChangesCR6() *AllChangesCR6

func (*AllChangesCR6) GetGraphNotification 

func (n *AllChangesCR6) GetGraphNotification(state AllChangesState) bool

func (*AllChangesCR6) GetSNotification 

func (n *AllChangesCR6) GetSNotification(state AllChangesState, c, cPrime uint) bool

type AllChangesRuleMap 

type AllChangesRuleMap struct {
	*RuleMap
	// contains filtered or unexported fields
}

AllChangesRuleMap is an extension of RuleMap. It has some extended functionality: It stores the subset mapping as required by rule CR6 and methods to add new elements to it / perform the update on a given state. These functions are safe for concurrent use (protected by a mutex, so better understand what happens to avoid deadlocks; sorry). And also holds an instance of AllChangesCR6 to perform this update when required.

func NewAllChangesRuleMap 

func NewAllChangesRuleMap() *AllChangesRuleMap

func (*AllChangesRuleMap) ApplySubsetNotification 

func (rm *AllChangesRuleMap) ApplySubsetNotification(state AllChangesState, d, cPrime uint) bool

func (*AllChangesRuleMap) Init 

func (rm *AllChangesRuleMap) Init(tbox *NormalizedTBox)

type AllChangesSNotification 

type AllChangesSNotification interface {
	// Information, that C' was added to S(C)
	GetSNotification(state AllChangesState, c, cPrime uint) bool
}

AllChangesSNotification is a special handler type for rule CR6. We're interested in updates on all {a} for all S(C) and S(D). Thus storing this in the proposed pattern for SNotifications would require much memory. So we do the following: Wait until some set S(C) gets updated with C'. If C' is not of the form {a} do nothing. If it is of the form perform the test and apply the rule if required. Note that here we use the extendted AllChangesState interface, not just SolverState. So this interface is used to show the difference between SNotification and to use the extended state interface.

type AllChangesSolver 

type AllChangesSolver struct {
	*AllChangesSolverState
	*AllChangesRuleMap
	// contains filtered or unexported fields
}

func NewAllChangesSolver 

func NewAllChangesSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *AllChangesSolver

func (*AllChangesSolver) AddConcept 

func (solver *AllChangesSolver) AddConcept(c, d uint) bool

func (*AllChangesSolver) AddRole 

func (solver *AllChangesSolver) AddRole(r, c, d uint) bool

func (*AllChangesSolver) AddSubsetRule 

func (solver *AllChangesSolver) AddSubsetRule(c, d uint) bool

func (*AllChangesSolver) Init 

func (solver *AllChangesSolver) Init(tbox *NormalizedTBox, domains *domains.CDManager)

func (*AllChangesSolver) Solve 

func (solver *AllChangesSolver) Solve(tbox *NormalizedTBox)

func (*AllChangesSolver) UnionConcepts 

func (solver *AllChangesSolver) UnionConcepts(c, d uint) bool

type AllChangesSolverState 

type AllChangesSolverState struct {
	*SolverState

	Graph    ConceptGraph
	Searcher *ExtendedGraphSearcher
	// contains filtered or unexported fields
}

TODO there is graph and Graph somewhere... we really should fix this

func NewAllChangesSolverState 

func NewAllChangesSolverState(c *ELBaseComponents,
	domains *domains.CDManager, g ConceptGraph, search ExtendedReachabilitySearch) *AllChangesSolverState

func (*AllChangesSolverState) BidrectionalSearch 

func (state *AllChangesSolverState) BidrectionalSearch(oldElements map[uint]struct{},
	newElement uint) map[uint]BidirectionalSearch

func (*AllChangesSolverState) ExtendedSearch 

func (state *AllChangesSolverState) ExtendedSearch(goals map[uint]struct{},
	additionalStart uint) map[uint]struct{}

func (*AllChangesSolverState) FindConnectedPairs 

func (state *AllChangesSolverState) FindConnectedPairs(s map[uint]struct{}) *BCPairSet

type AllChangesState 

type AllChangesState interface {
	StateHandler

	SubsetConcepts(c, d uint) bool

	ExtendedSearch(goals map[uint]struct{}, additionalStart uint) map[uint]struct{}

	BidrectionalSearch(oldElements map[uint]struct{}, newElement uint) map[uint]BidirectionalSearch

	FindConnectedPairs(s map[uint]struct{}) *BCPairSet

	// AddSubsetRule is used to create a new subset rule that says that S(D)
	// must always be a subset of S(C). That is whenever an add to S(D) happens
	// that element must be added to S(C) as well.
	//
	// However this is a complicated matter when things run concurrently.
	// The rule creating a these subset rules (CR6 in general) perform once a
	// union and thus ensure that S(D) ⊆ S(C).
	//
	// So AddSubsetRule must take care of the following: If things run
	// concurrently it must be ensured that once this function terminates all
	// s updates will comply by this rule.
	//
	// This means basically the following: Once AddSubsetRule has terminated
	// any pending s update that is (concurrently started) and its notifications
	// are (possibly also concurrently applied) will apply this rule as well.
	//
	// This way we ensure that nothing is missing in S(C).
	// Let's briefly discuss the problem concerning CR6.
	//
	// CR6 will call first AddSubsetRule and then apply S(C) = S(C) ∪ S(D).
	// Now if concurrenlty something somehow becomes added to S(D), and is not
	// yet present in S(C), the union will not add this element to S(C) as well,
	// the element has to be added due to the subset rule.
	//
	// The problem now is this: We call AddSubsetRule and an element x gets
	// added to S(D) concurrently. Now if we imagine that this add will not be
	// executed before the union (so the union will not add this element to S(C))
	// x must be added to S(C) later due to this new subset rule.
	//
	// The solver as they're implemented here don't have to worry about this for
	// the reason that first the update to S(D) will happen in go and only once
	// the value has been added to the field in go the notifications for this
	// update can run.
	//
	// A little "proof" that our solver should ensure why we don't miss any add:
	// If x gets added to S(D) two things will happen:
	//
	// (1) The element gets added to S[D] (meaning the mapping in go)
	// (2) An update gets created that x was added to S(D) and all notifications
	// concerning this update may run.
	//
	// Now to proof that updates will be applied it's important to know when
	// the update on S[D] is applied (remember that this happens concurrently).
	//
	// If the S[D] is updated before AddSubsetRule we don't have to worry,
	// the union will add x to S(C).
	// If S[D] is updated during AddSubsetRule: It's important to know that
	// the subset notifications for S[D] can't be applied during AddSubsetRule
	// because it requires a write lock on the data structure containing the
	// subset rules. AddSubsetRule requires a write lock and thus no notifications
	// can be made. So what happens if x gets added concurrently while
	// AddSubsetRule is running?
	// Case (a): Before the write lock: x will be added during the union, that's
	// ok.
	// Case (b): During the write lock. The notifications can't be applied because
	// that would require a read lock on the subset data structure. But we have
	// write locked it. The notifications can run only after the subset rule
	// has been added to that data structure and then x will get added.
	// Case (c): After AddSubsetRule: All notifications that start now already
	// apply that rule.
	AddSubsetRule(c, d uint) bool
}

AllChangesState extends the StateHandler interface as mentioned in the comment there. This is the version in which the graph only checks if an edge was added. It has additional methods for updating the graph (add an edge between C and D), check reachability of two concepts and test if S(C) ⊆ S(D).

A default implementation is given in AllChangesSolverState. TODO add name of CR6 here.

TODO There are some improvements possible, for example from "Practical Reasoning with Nominals in the EL Family of Description Logics" (Kazakov et al.) and "The incredible ELK" (also Kazakov et al.)

Also, if not dealing with nominals, it is possible to just turn the graph completely off and thus avoid adding edges to it

type AllGraphChangeNotification 

type AllGraphChangeNotification interface {
	GetGraphNotification(state AllChangesState) bool
}

type BCPair 

type BCPair struct {
	First, Second uint
}

type BCPairSet 

type BCPairSet struct {
	M map[BCPair]struct{}
	// contains filtered or unexported fields
}

func NewBCPairSet 

func NewBCPairSet(c *ELBaseComponents, initialCapacity uint) *BCPairSet

func (*BCPairSet) Add 

func (s *BCPairSet) Add(c, d Concept) bool

func (*BCPairSet) AddID 

func (s *BCPairSet) AddID(c, d uint) bool

func (*BCPairSet) Contains 

func (s *BCPairSet) Contains(c, d Concept) bool

func (*BCPairSet) ContainsID 

func (s *BCPairSet) ContainsID(c, d uint) bool

type BCSet 

type BCSet struct {
	M map[uint]struct{}
	// contains filtered or unexported fields
}

BCSet is a set of uints (concepts). Thus it is used for the entries S(C).

func NewBCSet 

func NewBCSet(c *ELBaseComponents, initialCapacity uint) *BCSet

func (*BCSet) Add 

func (s *BCSet) Add(c Concept) bool

func (*BCSet) AddID 

func (s *BCSet) AddID(c uint) bool

func (*BCSet) Contains 

func (s *BCSet) Contains(c Concept) bool

func (*BCSet) ContainsID 

func (s *BCSet) ContainsID(c uint) bool

func (*BCSet) Copy 

func (s *BCSet) Copy() *BCSet

func (*BCSet) Equals 

func (s *BCSet) Equals(other *BCSet) bool

Equals checks if s = other.

func (*BCSet) GetCDConjunction 

func (s *BCSet) GetCDConjunction(manager *domains.CDManager) [][]*domains.PredicateFormula

GetCDConjunction iterates over tha whole set S(C) and returns for each concrete domain all formulae contained in that concrete domain. We could store the conjunctions instead of creating them again all the time, but this should be ok.

func (*BCSet) IsSubset 

func (s *BCSet) IsSubset(other *BCSet) bool

IsSubset tests if s ⊆ other.

func (*BCSet) String 

func (s *BCSet) String() string

func (*BCSet) Union 

func (s *BCSet) Union(other *BCSet) bool

type BidirectionalSearch 

type BidirectionalSearch int
const (
	BidirectionalFalse BidirectionalSearch = iota
	BidrectionalDirect
	BidrectionalReverse
	BidrectionalBoth
)

func (BidirectionalSearch) String 

func (i BidirectionalSearch) String() string

type BottomConcept 

type BottomConcept struct{}

BottomConcept is the Bottom Concept ⊥. 

var Bottom BottomConcept = NewBottomConcept()

Bottom is a constant concept that represents the bottom concept ⊥.

func NewBottomConcept 

func NewBottomConcept() BottomConcept

NewBottomConcept returns a new BottomConcept. Instead of creating it again and again all the time you should use the const value Bottom.

func (BottomConcept) IsInBCD 

func (bot BottomConcept) IsInBCD() bool

func (BottomConcept) NormalizedID 

func (bot BottomConcept) NormalizedID(c *ELBaseComponents) uint

func (BottomConcept) String 

func (bot BottomConcept) String() string

type BulkSolver 

type BulkSolver struct {
	*AllChangesSolverState
	*AllChangesRuleMap

	// K is the number of updates that will be run by a concurrent worker
	// (maximal K things, maybe less). This is a way to let the solver know
	// how many updates will be processed without concurrency.
	// If set to a number ≤ 0 everything that is currently at the queue gets
	// processed in parallel.
	// TODO add a nice way to find a good k automatically?
	K int

	// stuff for the workers
	Workers    int
	WorkerPool chan bool
	// contains filtered or unexported fields
}

BulkSolver is a solver that runs concurrently but tries to avoid that consequences of a single update are performed concurrently, instead updates are accumulated and then performed in bulks.

After creating a BulkSolver via NewBulkSolver the following settings can be changed before solving: Workers: The number of workers that are allowed to run concurrently. A worker will process a set of updates concurrently, i.e. use BulkWorker to compute all consequences.

K is an option that stores how many updates at most are processed by a single worker. Setting K to a lower value usually means that more updates will be processed concurrently (instead of running them all at once).

Internally it works by a method that waits for updates, computes the bulks and runs them concurrently. This method may get deactivated and then activated again.

func NewBulkSolver 

func NewBulkSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *BulkSolver

func (*BulkSolver) AddConcept 

func (solver *BulkSolver) AddConcept(c, d uint) bool

func (*BulkSolver) AddRole 

func (solver *BulkSolver) AddRole(r, c, d uint) bool

func (*BulkSolver) AddSubsetRule 

func (solver *BulkSolver) AddSubsetRule(c, d uint) bool

func (*BulkSolver) Init 

func (solver *BulkSolver) Init(tbox *NormalizedTBox, domains *domains.CDManager)

func (*BulkSolver) Solve 

func (solver *BulkSolver) Solve(tbox *NormalizedTBox)

func (*BulkSolver) UnionConcepts 

func (solver *BulkSolver) UnionConcepts(c, d uint) bool

type BulkWorker 

type BulkWorker struct {
	*AllChangesSolverState
	*AllChangesRuleMap

	ComputedR []*RUpdate
	ComputedS []*SUpdate
	// contains filtered or unexported fields
}

BulkWorker is a helper class for the BulkSolver. It can be used as a solver state that adds consequences to an internal queue and changes the global mappings S and R (given from the BulkSolver). S and R are updated / queried through the AllChangesSolverState of the linked BulkSolver directly, i.e. it does not call for example AddConcept on the bulk solver but on the solver state of that solver. That way the bulk solver can process all consequences from the queues.

func NewBulkWokrer 

func NewBulkWokrer(solver *BulkSolver) *BulkWorker

func (*BulkWorker) AddConcept 

func (worker *BulkWorker) AddConcept(c, d uint) bool

func (*BulkWorker) AddRole 

func (worker *BulkWorker) AddRole(r, c, d uint) bool

func (*BulkWorker) AddSubsetRule 

func (worker *BulkWorker) AddSubsetRule(c, d uint) bool

TODO right?

func (*BulkWorker) Run 

func (worker *BulkWorker) Run(sUpdates []*SUpdate, rUpdates []*RUpdate)

Run runs all updates and adds the derived consequences to the internal queues.

func (*BulkWorker) UnionConcepts 

func (worker *BulkWorker) UnionConcepts(c, d uint) bool

type CR1 

type CR1 uint

CR1 implements the rule CR1: for C' ⊑ D: If C' ∈ S(C) then add D to S(C).

This rule implements an SNotification and as a result must simply add D to S(C). We only need to remember D (assuming the rule was correctly added). That is the value of the uint.

The intended use is that such a notification is created for each C' ⊑ D and then listens to all S(C) until C' gets added.

func NewCR1 

func NewCR1(d uint) CR1

func (CR1) GetSNotification 

func (n CR1) GetSNotification(state StateHandler, c, cPrime uint) bool

type CR10 

type CR10 uint

CR10 implements the rule CR10: for r ⊑ s: If (C, D) ∈ R(r) then add (C, D) to R(s).

This rule implements RNotification and as a result simply adds (C, D) to R(S). We only need to remember s (assuming the rule was correctly added). That is the value of the uint.

The intended use is that such a notification is created for each r ⊑ s and then listens to changes on R(r) (for that specific r).

func NewCR10 

func NewCR10(s uint) CR10

func (CR10) GetRNotification 

func (n CR10) GetRNotification(state StateHandler, r, c, d uint) bool

type CR11 

type CR11 struct {
	R1, R2, R3 uint
}

CR11 implements the rule CR11: for r1 o r2 ⊑ r3: If (C, D) ∈ R(r1) and (D, E) ∈ R(r2) then add (C, E) to R(r3).

This rule implements RNotification and waits on changes for both r1 and r2. Updates require iterating over R(r1) / R(r2).

The intended use is that such a notification is created for each r1 o r2 ⊑ r3 and then listens to changes on R(r1) and R(r2).

func NewCR11 

func NewCR11(r1, r2, r3 uint) *CR11

func (*CR11) GetRNotification 

func (n *CR11) GetRNotification(state StateHandler, r, c, d uint) bool

type CR2 

type CR2 struct {
	C1, C2, D uint
}

CR2 implements the rule CR2: for C1 ⊓ C2 ⊑ D: If C1, C2 ∈ S(C) add D to S(C).

This rule implements an SNotification that waits for updates on any C with either C1 or C2. If triggered it checks if both values are present in S(C) and as a result adds D to S(C).

The intended use is that such a notification is created for each C1 ⊓ C2 ⊑ D and then this instance listens on both C1 and C2 for all S(C).

func NewCR2 

func NewCR2(c1, c2, d uint) *CR2

func (*CR2) GetSNotification 

func (n *CR2) GetSNotification(state StateHandler, c, cPrime uint) bool

type CR3 

type CR3 struct {
	R, D uint
}

CR3 implements the rule CR3: for C' ⊑ ∃r.D: If C' ∈ S(C) add (C, D) to R(r).

This rule implements an SNotificationthat waits for updates on any C with C'. When triggered it directly performs the update.

The intended use is that such a notification is created for each C' ⊑ ∃r.D and then waits for updates on all S(C) with C'.

func NewCR3 

func NewCR3(r, d uint) *CR3

func (*CR3) GetSNotification 

func (n *CR3) GetSNotification(state StateHandler, c, cPrime uint) bool

type CR4 

type CR4 struct {
	R, DPrime, E uint
}

CR4 implements the rule CR4: for ∃r.D' ⊑ E: If (C, D) ∈ R(r) and D' ∈ S(D) then add E to S(C). It implements both SNotification and RNotification.

On an update on R(r) with (C, D) it checks if D' ∈ S(D). If yes the update is applied.

On an update on S(D) with D' it checks all pairs (C, D) ∈ R(r) and applies the update for these pairs.

The intended use is that such a notification is created for each ∃r.D' ⊑ E and then waits for updates on all S(D) with D' and for any update on R(r) (for that particular r).

func NewCR4 

func NewCR4(r, dPrime, e uint) *CR4

func (*CR4) GetRNotification 

func (n *CR4) GetRNotification(state StateHandler, r, c, d uint) bool

func (*CR4) GetSNotification 

func (n *CR4) GetSNotification(state StateHandler, d, dPrime uint) bool

type CR5 

type CR5 struct{}

CR5 implements the rule CR5: If (C, D) ∈ R(r) and ⊥ ∈ S(D) then add ∈ to S(C).

It implements both SNotification and RNotification.

On an update on R(r) with (C, D) it checks if ⊥ ∈ S(D) and if yes applies the rule.

On an update on S(D) with ⊥ it iterates over all pairs (C, D) in R(r) for all r and applies the rule. That is a rather cumbersome process but it can't be helped.

This notification should be created once and then listen on all r and all D (for ⊥).

func NewCR5 

func NewCR5() *CR5

func (*CR5) GetRNotification 

func (n *CR5) GetRNotification(state StateHandler, r, c, d uint) bool

func (*CR5) GetSNotification 

func (n *CR5) GetSNotification(state StateHandler, d, bot uint) bool

type CR7AndCR8 

type CR7AndCR8 struct{}

CR7AndCR8 implements both rules CR7 and CR8 (because they're easily connected).

The rule implements SNotification.

The SNotification must be received whenever an element gets added to some S(C). The rule itself will then determine if it must do something or not.

Some implementation details because it's important to understand what happens here.

This rule will first check if the element that was added is a CDExtensions. If so it will compute conj(C) and then test the rule premiss.

First it will test if conj(C) is not satisfiable, in this case ⊥ gets added to S(C) and all formulae of the domain (because ⊥ implies everything). The ⊥ satisfies rule CR7, the rest is just a speedup of rule CR8 (no need) to test the implication.

If it is satisfiable then it will test the implication condition of rule CR8. But it will not test all formulae that are implied but the conjunction. Instead it will find the first formula that is not contained in S(C) yet that is implied by conj(C). If it finds such a formula the formula gets added. In this case we don't have to check the implication for the other formulae as well. Because we added a new formula to S(C) the implication test will be performed again in any case.

This way we don't test the implication again and again (especially if things run concurrently). We can do that because if a conjunction implies a certain formula it will apply the formula even if we added a new formula to the conjunction. TODO Think again, but I'm sure it's correct this way.

func NewCR7AndCR8 

func NewCR7AndCR8() CR7AndCR8

func (CR7AndCR8) GetSNotification 

func (n CR7AndCR8) GetSNotification(state StateHandler, c, cPrime uint) bool

TODO A speedup example: Instead when things like formulae get added it's better to first apply subset rules etc. because this way we don't have to reason that much I think that would be an actually really good improvement. So in short: If we know that p(f1, ..., fk) gets added to some S(D): first add it to everything that always contains all elements from S(D) before reasoning with it (otherwise we start a reasoner for nothing... gets added anyway)

type Concept 

type Concept interface {
	// IsInBCD must return true for all concepts that are in the basic concept
	// description, these are: ⊤, all concept names, all concepts of the form {a}
	// and p(f1, ..., fk).
	IsInBCD() bool

	// NormalizedID is used to give each element of the basic concept description
	// and the bottom concept a unique id.
	// This might be useful if we want to store for example a set of elements from
	// the BCD.
	// The ids are defined in the following way:
	// The bottom concept has an id of 0
	// The top concept has an id of 1
	// All nominals have an id in 2...NumNoinals + 1
	// All CDExtensions have an id in NumNoinals + 2...NumNomials + NumCDExtensions + 1
	// All names haven an id in NumNomials + NumCDExtensions + 2....NumNomials + NumCDExtensions + NumNames + 1
	// This way we can easily add new names all the time, because the ids are at
	// the end of the representation and when we add a new name we don't have to
	// adjust all other ids in use (if this is ever required).
	//
	// So we can think of the representation in the wollowing way:
	// [⊥ ⊤ Individiaul1...IndividualN CDExtension1...CDExtensioN Name1...NameN]
	NormalizedID(c *ELBaseComponents) uint
}

Concept is the interface for all Concept defintions. Concepts in EL++ are defined recursively, this is the general interface.

func NewMultiConjunction 

func NewMultiConjunction(concepts ...Concept) Concept

type ConceptAssertion 

type ConceptAssertion struct {
	C Concept
	A Nominal
}

ConceptAssertion is an concept assertion of the form C(a).

func NewConceptAssertion 

func NewConceptAssertion(c Concept, a Nominal) *ConceptAssertion

NewConceptAssertion returns a new concept assertion C(a).

func (*ConceptAssertion) String 

func (ca *ConceptAssertion) String() string

type ConceptGraph 

type ConceptGraph interface {
	Init(numConcepts uint)
	AddEdge(source, target uint) bool
	Succ(vertex uint, ch chan<- uint)
}

type ConcreteDomainExtension 

type ConcreteDomainExtension uint

ConcreteDomainExtension is a concrete domain extension of the form p(f1, ..., fk). All this information (predicate and function) has to be stored somewhere else, we only store the an id that identifies the concrete domain.

func NewConcreteDomainExtension 

func NewConcreteDomainExtension(i uint) ConcreteDomainExtension

NewConcreteDomainExtension returns a new ConcreteDomainExtension with the given id.

func (ConcreteDomainExtension) IsInBCD 

func (cd ConcreteDomainExtension) IsInBCD() bool

func (ConcreteDomainExtension) NormalizedID 

func (cd ConcreteDomainExtension) NormalizedID(c *ELBaseComponents) uint

func (ConcreteDomainExtension) String 

func (cd ConcreteDomainExtension) String() string

type ConcurrentNotificationSolver 

type ConcurrentNotificationSolver struct {
	*AllChangesSolver
	// contains filtered or unexported fields
}

func NewConcurrentNotificationSolver 

func NewConcurrentNotificationSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *ConcurrentNotificationSolver

func (*ConcurrentNotificationSolver) AddConcept 

func (solver *ConcurrentNotificationSolver) AddConcept(c, d uint) bool

func (*ConcurrentNotificationSolver) AddRole 

func (solver *ConcurrentNotificationSolver) AddRole(r, c, d uint) bool

func (*ConcurrentNotificationSolver) AddSubsetRule 

func (solver *ConcurrentNotificationSolver) AddSubsetRule(c, d uint) bool

func (*ConcurrentNotificationSolver) Solve 

func (solver *ConcurrentNotificationSolver) Solve(tbox *NormalizedTBox)

func (*ConcurrentNotificationSolver) UnionConcepts 

func (solver *ConcurrentNotificationSolver) UnionConcepts(c, d uint) bool

type ConcurrentSolver 

type ConcurrentSolver struct {
	*AllChangesSolverState
	*AllChangesRuleMap

	SChanSize, RChanSize, Workers int
	// contains filtered or unexported fields
}

func NewConcurrentSolver 

func NewConcurrentSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *ConcurrentSolver

func (*ConcurrentSolver) AddConcept 

func (solver *ConcurrentSolver) AddConcept(c, d uint) bool

func (*ConcurrentSolver) AddRole 

func (solver *ConcurrentSolver) AddRole(r, c, d uint) bool

func (*ConcurrentSolver) AddSubsetRule 

func (solver *ConcurrentSolver) AddSubsetRule(c, d uint) bool

TODO right?

func (*ConcurrentSolver) Init 

func (solver *ConcurrentSolver) Init(tbox *NormalizedTBox, domains *domains.CDManager)

func (*ConcurrentSolver) Solve 

func (solver *ConcurrentSolver) Solve(tbox *NormalizedTBox)

func (*ConcurrentSolver) UnionConcepts 

func (solver *ConcurrentSolver) UnionConcepts(c, d uint) bool

TODO experiment

type ConcurrentWorkerPool 

type ConcurrentWorkerPool struct {
	// contains filtered or unexported fields
}

func NewConcurrentWorkerPool 

func NewConcurrentWorkerPool() *ConcurrentWorkerPool

TODO document that init must be called

func (*ConcurrentWorkerPool) AddR 

func (p *ConcurrentWorkerPool) AddR(update *RUpdate)

func (*ConcurrentWorkerPool) AddS 

func (p *ConcurrentWorkerPool) AddS(update ...*SUpdate)

func (*ConcurrentWorkerPool) Close 

func (p *ConcurrentWorkerPool) Close()

func (*ConcurrentWorkerPool) Init 

func (p *ConcurrentWorkerPool) Init(sSize, rSize, workers int)

func (*ConcurrentWorkerPool) RWorker 

func (p *ConcurrentWorkerPool) RWorker(solver *ConcurrentSolver)

func (*ConcurrentWorkerPool) SWorker 

func (p *ConcurrentWorkerPool) SWorker(solver *ConcurrentSolver)

TODO add discussion here involving everything concurrent vs. part of it concurrent It seems that not running all notifications concurrently really improves the outcome

func (*ConcurrentWorkerPool) Wait 

func (p *ConcurrentWorkerPool) Wait()

type Conjunction 

type Conjunction struct {
	// C, D are the parts of the conjuntion.
	C, D Concept
}

Conjunction is a concept of the form C ⊓ D.

func NewConjunction 

func NewConjunction(c, d Concept) Conjunction

NewConjunction returns a new conjunction given C and D.

func (Conjunction) IsInBCD 

func (conjunction Conjunction) IsInBCD() bool

func (Conjunction) NormalizedID 

func (conjunction Conjunction) NormalizedID(c *ELBaseComponents) uint

func (Conjunction) String 

func (conjunction Conjunction) String() string

type DefaultNormalFormBuilder 

type DefaultNormalFormBuilder struct {
	// contains filtered or unexported fields
}

DefaultNormalFormBuilder is an implementation of TBoxNormalformBuilder that normalizes up to k formulae concurrently.

func NewDefaultNormalFormBUilder 

func NewDefaultNormalFormBUilder(k int) *DefaultNormalFormBuilder

NewDefaultNormalFormBUilder returns a new DefaultNormalFormBuilder. k must be a value > 0 and is the number of formulae that will be normalized concurrently. That is at most k normalizations will be performed at the same time. So k = 1 means that no concurrency happens, instead each formulae is normalized on it's own.

func (*DefaultNormalFormBuilder) Normalize 

func (builder *DefaultNormalFormBuilder) Normalize(tbox *TBox) *NormalizedTBox

type ELBaseComponents 

type ELBaseComponents struct {
	Nominals     uint
	CDExtensions uint
	Names        uint
	Roles        uint
}

ELBaseComponents used to save basic information about an EL++ instance. It stores only the number of each base concept, nothing else.

func NewELBaseComponents 

func NewELBaseComponents(nominals, cdExtensions, names, roles uint) *ELBaseComponents

NewELBaseComponents returns a new ELBaseComponents instance.

func ParseELBaseComponents 

func ParseELBaseComponents(line string) (*ELBaseComponents, error)

func (*ELBaseComponents) GetConcept 

func (c *ELBaseComponents) GetConcept(normalizedID uint) Concept

TODO think this through, escpecially if one is 0!

func (*ELBaseComponents) NumBCD 

func (c *ELBaseComponents) NumBCD() uint

NumBCD returns the number of elements in the basic concept description. That is the number of nominals, names, cd extensions + 1 (⊤).

func (*ELBaseComponents) Write 

func (c *ELBaseComponents) Write(w io.Writer) error

type ExistentialConcept 

type ExistentialConcept struct {
	R Role
	C Concept
}

ExistentialConcept is a concept of the form ∃r.C.

func NewExistentialConcept 

func NewExistentialConcept(r Role, c Concept) ExistentialConcept

NewExistentialConcept returns a new existential concept of the form ∃r.C.

func (ExistentialConcept) IsInBCD 

func (existential ExistentialConcept) IsInBCD() bool

func (ExistentialConcept) NormalizedID 

func (existential ExistentialConcept) NormalizedID(c *ELBaseComponents) uint

func (ExistentialConcept) String 

func (existential ExistentialConcept) String() string

type ExtendedGraphSearcher 

type ExtendedGraphSearcher struct {
	// contains filtered or unexported fields
}

func NewExtendedGraphSearcher 

func NewExtendedGraphSearcher(extendedSearch ExtendedReachabilitySearch,
	bc *ELBaseComponents) *ExtendedGraphSearcher

func (*ExtendedGraphSearcher) BidrectionalSearch 

func (searcher *ExtendedGraphSearcher) BidrectionalSearch(g ConceptGraph, oldElements map[uint]struct{}, newElement uint) map[uint]BidirectionalSearch

func (*ExtendedGraphSearcher) FindConnectedPairs 

func (searcher *ExtendedGraphSearcher) FindConnectedPairs(g ConceptGraph, s map[uint]struct{}) *BCPairSet

func (*ExtendedGraphSearcher) Search 

func (searcher *ExtendedGraphSearcher) Search(g ConceptGraph, goals map[uint]struct{}, additionalStart uint) map[uint]struct{}

type ExtendedReachabilitySearch 

type ExtendedReachabilitySearch func(g ConceptGraph, goals map[uint]struct{}, start ...uint) map[uint]struct{}

Extended Search

type GCIConstraint 

type GCIConstraint struct {
	C, D Concept
}

GCIConstraint is a general concept inclusion of the form C ⊑ D.

func NewGCIConstraint 

func NewGCIConstraint(c, d Concept) *GCIConstraint

NewGCIConstraint returns a new general concept inclusion C ⊑ D.

func (*GCIConstraint) String 

func (gci *GCIConstraint) String() string

type GraphSearcher 

type GraphSearcher struct {
	// contains filtered or unexported fields
}

func NewGraphSearcher 

func NewGraphSearcher(search ReachabilitySearch, bc *ELBaseComponents) *GraphSearcher

func (*GraphSearcher) BidrectionalSearch 

func (searcher *GraphSearcher) BidrectionalSearch(g ConceptGraph, c, d uint) BidirectionalSearch

TODO is this even required? See comment in NaiveSolver rule 6

func (*GraphSearcher) Search 

func (searcher *GraphSearcher) Search(g ConceptGraph, additionalStart, goal uint) bool

type IntDistributor 

type IntDistributor struct {
	// contains filtered or unexported fields
}

IntDistributor is a type used to generate new uint values. The solving algorithm requires that new names are introduced, we use this distributor to generate new integer values concurrently. This means that the Next method can be used concurrently from different goroutines.

func NewIntDistributor 

func NewIntDistributor(next uint) *IntDistributor

NewIntDistributor returns a new distributor s.t. the Next method first produces the value next.

func (*IntDistributor) Next 

func (dist *IntDistributor) Next() uint

Next returns the next integer value. That is the first element produced is the provided next value, then next + 1 etc.

It is safe to use concurrently from different goroutines.

type NCAllChangesCR6 

type NCAllChangesCR6 struct {
	// contains filtered or unexported fields
}

func NewNCAllChangesCR6 

func NewNCAllChangesCR6() *NCAllChangesCR6

func (*NCAllChangesCR6) GetGraphNotification 

func (n *NCAllChangesCR6) GetGraphNotification(state AllChangesState) bool

func (*NCAllChangesCR6) GetSNotification 

func (n *NCAllChangesCR6) GetSNotification(state AllChangesState, c, cPrime uint) bool

type NCAllChangesRuleMap 

type NCAllChangesRuleMap struct {
	*RuleMap
	// contains filtered or unexported fields
}

func NewNCAllChangesRuleMap 

func NewNCAllChangesRuleMap() *NCAllChangesRuleMap

func (*NCAllChangesRuleMap) ApplySubsetNotification 

func (rm *NCAllChangesRuleMap) ApplySubsetNotification(state AllChangesState, d, cPrime uint) bool

func (*NCAllChangesRuleMap) Init 

func (rm *NCAllChangesRuleMap) Init(tbox *NormalizedTBox)

type NCAllChangesSolverState 

type NCAllChangesSolverState struct {
	// TODO graph still protected by mutex
	*NCSolverState

	Graph    ConceptGraph
	Searcher *ExtendedGraphSearcher
}

func NewNCAllChangesSolverState 

func NewNCAllChangesSolverState(c *ELBaseComponents,
	domains *domains.CDManager, g ConceptGraph, search ExtendedReachabilitySearch) *NCAllChangesSolverState

func (*NCAllChangesSolverState) BidrectionalSearch 

func (state *NCAllChangesSolverState) BidrectionalSearch(oldElements map[uint]struct{},
	newElement uint) map[uint]BidirectionalSearch

func (*NCAllChangesSolverState) ExtendedSearch 

func (state *NCAllChangesSolverState) ExtendedSearch(goals map[uint]struct{},
	additionalStart uint) map[uint]struct{}

func (*NCAllChangesSolverState) FindConnectedPairs 

func (state *NCAllChangesSolverState) FindConnectedPairs(s map[uint]struct{}) *BCPairSet

type NCRBSolver 

type NCRBSolver struct {
	*NCAllChangesSolverState
	*NCAllChangesRuleMap
	// contains filtered or unexported fields
}

func NewNCRBSolver 

func NewNCRBSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *NCRBSolver

func (*NCRBSolver) AddConcept 

func (solver *NCRBSolver) AddConcept(c, d uint) bool

func (*NCRBSolver) AddRole 

func (solver *NCRBSolver) AddRole(r, c, d uint) bool

func (*NCRBSolver) AddSubsetRule 

func (solver *NCRBSolver) AddSubsetRule(c, d uint) bool

func (*NCRBSolver) Init 

func (solver *NCRBSolver) Init(tbox *NormalizedTBox, domains *domains.CDManager)

func (*NCRBSolver) Solve 

func (solver *NCRBSolver) Solve(tbox *NormalizedTBox)

func (*NCRBSolver) UnionConcepts 

func (solver *NCRBSolver) UnionConcepts(c, d uint) bool

type NCSolverState 

type NCSolverState struct {
	S []*BCSet
	R []*Relation
	// contains filtered or unexported fields
}

func NewNCSolverState 

func NewNCSolverState(c *ELBaseComponents, domains *domains.CDManager) *NCSolverState

func (*NCSolverState) AddConcept 

func (state *NCSolverState) AddConcept(c, d uint) bool

func (*NCSolverState) AddRole 

func (state *NCSolverState) AddRole(r, c, d uint) bool

func (*NCSolverState) ContainsConcept 

func (state *NCSolverState) ContainsConcept(c, d uint) bool

func (*NCSolverState) ContainsRole 

func (state *NCSolverState) ContainsRole(r, c, d uint) bool

func (*NCSolverState) GetCDs 

func (state *NCSolverState) GetCDs() *domains.CDManager

func (*NCSolverState) GetComponents 

func (state *NCSolverState) GetComponents() *ELBaseComponents

func (*NCSolverState) GetConjunction 

func (state *NCSolverState) GetConjunction(c uint) [][]*domains.PredicateFormula

func (*NCSolverState) ReverseRoleMapping 

func (state *NCSolverState) ReverseRoleMapping(r, d uint) []uint

func (*NCSolverState) RoleMapping 

func (state *NCSolverState) RoleMapping(r, c uint) []uint

func (*NCSolverState) SubsetConcepts 

func (state *NCSolverState) SubsetConcepts(c, d uint) bool

func (*NCSolverState) UnionConcepts 

func (state *NCSolverState) UnionConcepts(c, d uint) bool

type NaiveSolver 

type NaiveSolver struct {
	S []*BCSet
	R []*BCPairSet
	// contains filtered or unexported fields
}

func NewNaiveSolver 

func NewNaiveSolver(graph ConceptGraph, search ReachabilitySearch) *NaiveSolver

func (*NaiveSolver) Solve 

func (solver *NaiveSolver) Solve(tbox *NormalizedTBox, manager *domains.CDManager)

check again!

type NamedConcept 

type NamedConcept uint

NamedConcept is a concept from the set of concept names, identified by an id. Each concept name A ∈ N_C is encoded as a unique integer with this type.

func NewNamedConcept 

func NewNamedConcept(i uint) NamedConcept

NewNamedConcept returns a new NamedConcept with the given id.

func (NamedConcept) IsInBCD 

func (name NamedConcept) IsInBCD() bool

func (NamedConcept) NormalizedID 

func (name NamedConcept) NormalizedID(c *ELBaseComponents) uint

func (NamedConcept) String 

func (name NamedConcept) String() string

type Nominal 

type Nominal uint

Nominal is a nominal a ∈ N_I, identified by id. Each nominal a ∈ N_I is encoded as a unique integer with this type.

func (Nominal) String 

func (nominal Nominal) String() string

type NominalConcept 

type NominalConcept Nominal

NominalConcept is a nominal concept of the form {a}, identified by id. A Nominal is encoded by the type Nominal, a NominalConcept is just the usage of a Nominal as a Concept.

func NewNominalConcept 

func NewNominalConcept(i uint) NominalConcept

NewNominalConcept returns a new NominalConcept with the given id.

func (NominalConcept) IsInBCD 

func (nominal NominalConcept) IsInBCD() bool

func (NominalConcept) NormalizedID 

func (nominal NominalConcept) NormalizedID(c *ELBaseComponents) uint

func (NominalConcept) String 

func (nominal NominalConcept) String() string

type NormalizedCI 

type NormalizedCI struct {
	// C1 and C2 form the LHS of the CI.
	C1, C2 Concept
	// D is the RHS of the CI
	D Concept
}

NormalizedCI is a normalized CI of the form C1 ⊓ C2 ⊑ D or C1 ⊑ D. For C1 ⊑ D C2 is set to nil. C1 and C2 must be in BC(T) and D must be in BC(T) or ⊥.

func NewNormalizedCI 

func NewNormalizedCI(c1, c2, d Concept) *NormalizedCI

NewNormalizedCI returns a new normalized CI of the form C1 ⊓ C2 ⊑ D. C1 and C2 must be in BC(T) and D must be in BC(T) or ⊥.

func NewNormalizedCISingle 

func NewNormalizedCISingle(c1, d Concept) *NormalizedCI

NewNormalizedCISingle returns a new normalized CI of the form C1 ⊑ D.

func ParseNormalizedCI 

func ParseNormalizedCI(line string, c *ELBaseComponents) (*NormalizedCI, error)

func (*NormalizedCI) String 

func (ci *NormalizedCI) String() string

func (*NormalizedCI) Write 

func (ci *NormalizedCI) Write(w io.Writer, c *ELBaseComponents) error

type NormalizedCILeftEx 

type NormalizedCILeftEx struct {
	C1, D Concept
	R     Role
}

NormalizedCILeftEx is a normalized CI where the existential quantifier is on the left-hand side, i.e. of the form ∃r.C1 ⊑ D. C1 must be in BC(T) and D must be in BC(T) or ⊥.

func NewNormalizedCILeftEx 

func NewNormalizedCILeftEx(r Role, c1, d Concept) *NormalizedCILeftEx

NewNormalizedCILeftEx returns a new CI of the form ∃r.C1 ⊑ D.

func ParseNormalizedCILeftEx 

func ParseNormalizedCILeftEx(line string, c *ELBaseComponents) (*NormalizedCILeftEx, error)

func (*NormalizedCILeftEx) String 

func (ci *NormalizedCILeftEx) String() string

func (*NormalizedCILeftEx) Write 

func (ci *NormalizedCILeftEx) Write(w io.Writer, c *ELBaseComponents) error

type NormalizedCIRightEx 

type NormalizedCIRightEx struct {
	C1, C2 Concept
	R      Role
}

NormalizedCIRightEx is a normalized CI where the existential quantifier is on the right-hand side, i.e. of the form C1 ⊑ ∃r.C2. C1 and C2 must be in BC(T) and D must be in BC(T) or ⊥.

func NewNormalizedCIRightEx 

func NewNormalizedCIRightEx(c1 Concept, r Role, c2 Concept) *NormalizedCIRightEx

NewNormalizedCIRightEx returns a new CI of the form C1 ⊑ ∃r.C2.

func ParseNormalizedCIRightEx 

func ParseNormalizedCIRightEx(line string, c *ELBaseComponents) (*NormalizedCIRightEx, error)

func (*NormalizedCIRightEx) String 

func (ci *NormalizedCIRightEx) String() string

func (*NormalizedCIRightEx) Write 

func (ci *NormalizedCIRightEx) Write(w io.Writer, c *ELBaseComponents) error

type NormalizedRI 

type NormalizedRI struct {
	R1, R2, S Role
}

NormalizedRI is a normalized RI of the form r1 o r2 ⊑ s or r1 ⊑ s. For the second form R2 is set to NoRole.

func NewNormalizedRI 

func NewNormalizedRI(r1, r2, s Role) *NormalizedRI

NewNormalizedRI returns a new normalized RI of the form r1 o r2 ⊑ s.

func NewNormalizedRISingle 

func NewNormalizedRISingle(r1, s Role) *NormalizedRI

NewNormalizedRISingle returns a new normalized RI of the form r1 ⊑ s.

func NormalizeSingleRI 

func NormalizeSingleRI(ri *RoleInclusion, firstNewIndex uint) []*NormalizedRI

NormalizeSingleRI normalizes a rule inclusion, that is it exhaustively applies rule NF1. firstNewIndex must be the next index we can use to create new roles. If k is the length of the left hand side it requires k - 2 new role names if k > 2 and 0 new names otherwise.

func ParseNormalizedRI 

func ParseNormalizedRI(line string) (*NormalizedRI, error)

func (*NormalizedRI) String 

func (ri *NormalizedRI) String() string

func (*NormalizedRI) Write 

func (ci *NormalizedRI) Write(w io.Writer) error

TODO should be called ri... copied something wrong it seems...

type NormalizedRandomELBuilder 

type NormalizedRandomELBuilder struct {
	NumIndividuals  uint
	NumConceptNames uint
	NumRoles        uint
}

func (*NormalizedRandomELBuilder) GenerateRandomTBox 

func (builder *NormalizedRandomELBuilder) GenerateRandomTBox(numNormalizedCI,
	numExistentialRestrictions, numRI int) *NormalizedTBox

type NormalizedTBox 

type NormalizedTBox struct {
	Components *ELBaseComponents
	CIs        []*NormalizedCI
	CILeft     []*NormalizedCILeftEx
	CIRight    []*NormalizedCIRightEx
	RIs        []*NormalizedRI
}

NormalizedTBox is a TBox containing only normalized CIs.

func ParseNormalizedTBox 

func ParseNormalizedTBox(r io.Reader) (*NormalizedTBox, error)

func (*NormalizedTBox) Write 

func (tbox *NormalizedTBox) Write(w io.Writer) error

type PhaseOneResult 

type PhaseOneResult struct {
	Distributor     *IntDistributor
	Waiting         []*GCIConstraint
	IntermediateRes []*GCIConstraint
	// for CIs already in normal form we can just add them already for phase 2
	IntermediateCIs     []*NormalizedCI
	IntermediateCILeft  []*NormalizedCILeftEx
	IntermediateCIRight []*NormalizedCIRightEx
}

PhaseOneResult is a helper type that stores certain information about normalization in phase 1.

The idea is that each formula that gets normalized uses its own result and stores all information inside.

It is not save for concurrent use.

The following information is stored:

Distributor is used to create new names, so it should be the same in all objects of this type when normalizing a set of formulae. Waiting is a "queue" that stores all elements that need further processing, that means it may be that additional rules can be applied in phase 1. So when replacing a formula with other formulae just add the new formulae to Waiting. IntermediateRes is the set of all formulae that must not be processed in phase 1 but must be used in phase 2. The other intermediate results are used for formulae already in normal form: We don't have to check them again in phase 2 so we can already add them here.

func NewPhaseOneResult 

func NewPhaseOneResult(distributor *IntDistributor) *PhaseOneResult

func PhaseOneSingle 

func PhaseOneSingle(gci *GCIConstraint, distributor *IntDistributor) *PhaseOneResult

PhaseOneSingle runs phase 1 of the normalization for a given gci. That is it exhaustively applies the rules NF2 - NF4 and returns the result.

func (*PhaseOneResult) Union 

func (res *PhaseOneResult) Union(other *PhaseOneResult)

Union merges two results. That is it builds the union of all intermediate results. This is useful when combining results from different normalizations. The combined results are stored in res.

type PhaseTwoResult 

type PhaseTwoResult struct {
	Distributor         *IntDistributor
	Waiting             []*GCIConstraint
	IntermediateCIs     []*NormalizedCI
	IntermediateCILeft  []*NormalizedCILeftEx
	IntermediateCIRight []*NormalizedCIRightEx
}

PhaseTwoResult stores information about normalization in phase 2. The idea is the same as for PhaseOneResult, so see documentation there.

func NewPhaseTwoResult 

func NewPhaseTwoResult(distributor *IntDistributor) *PhaseTwoResult

func PhaseTwoSingle 

func PhaseTwoSingle(gci *GCIConstraint, distributor *IntDistributor) *PhaseTwoResult

PhaseTwoSingle runs phase 2 of the normalization for a given gci. That is it exhaustively applies the rules NF5 - NF7 and returns the result.

func (*PhaseTwoResult) Union 

func (res *PhaseTwoResult) Union(other *PhaseTwoResult)

type RNotification 

type RNotification interface {
	// Information, that (C, D) was added to R(r)
	GetRNotification(state StateHandler, r, c, d uint) bool
}

type RUpdate 

type RUpdate struct {
	R, C, D uint
}

RUpdate is a type that stores the information that (C, D) has been added to r. Similar to SUpdate it is usually used in a queue that stores updates that still must be executed (notifcations for that update must be issued).

func NewRUpdate 

func NewRUpdate(r, c, d uint) *RUpdate

NewRUpdate returns a new RUpdate.

type RandomELBuilder 

type RandomELBuilder struct {
	NumIndividuals     uint
	NumConceptNames    uint
	NumRoles           uint
	NumConcreteDomains uint
	MaxCDSize          uint
	MaxNumPredicates   uint
	MaxNumFeatures     uint
}

func (*RandomELBuilder) GenerateRandomTBox 

func (builder *RandomELBuilder) GenerateRandomTBox(numCDExtensions, numConjunctions,
	numExistentialRestrictions, maxtRILHS, numGCI, numRI uint) ([]Concept, *TBox)

type ReachabilitySearch 

type ReachabilitySearch func(g ConceptGraph, goal uint, start ...uint) bool

TODO: It's important that the search can easily assume that start is unique, i.e. no duplicates. That is required for the reachability search that requires path lengths >= 1.

type Relation 

type Relation struct {
	Mapping        map[uint]map[uint]struct{}
	ReverseMapping map[uint]map[uint]struct{}
}

func NewRelation 

func NewRelation(initialCapacity uint) *Relation

func (*Relation) Add 

func (r *Relation) Add(c, d uint) bool

func (*Relation) Contains 

func (r *Relation) Contains(c, d uint) bool

func (*Relation) Equals 

func (r *Relation) Equals(other *Relation) bool

type Role 

type Role uint

Role is an EL++ role r ∈ N_R, identifiey by id. Each r ∈ N_R is encoded as a unique integer with this type. 

const (
	// NoRule is used to identify a role as not valid.
	NoRole Role = Role(^uint(0))
)

func NewRole 

func NewRole(i uint) Role

NewRole returns a new Rolen with the given id.

func (Role) String 

func (role Role) String() string

type RoleAssertion 

type RoleAssertion struct {
	R    Role
	A, B Nominal
}

RoleAssertion is a role assertion of the form r(a, b).

func NewRoleAssertion 

func NewRoleAssertion(r Role, a, b Nominal) *RoleAssertion

NewRoleAssertion returns a new role assertion r(a, b).

func (*RoleAssertion) String 

func (ra *RoleAssertion) String() string

type RoleInclusion 

type RoleInclusion struct {
	// LHS contains the left-hand side r1 o ... o rk.
	LHS []Role
	// RHS is the right-hand side r.
	RHS Role
}

RoleInclusion is a role inclusion of the form r1 o ... o rk ⊑ r.

func NewRoleInclusion 

func NewRoleInclusion(lhs []Role, rhs Role) *RoleInclusion

NewRoleInclusion returns a new role inclusion r1 o ... o rk ⊑ r.

func (*RoleInclusion) String 

func (ri *RoleInclusion) String() string

type RuleMap 

type RuleMap struct {
	SRules map[uint][]SNotification
	RRules map[uint][]RNotification
	// contains filtered or unexported fields
}

RuleMap is used to store all rules in a way in which we can easily determin which rules are to be notified about a certain change.

There are two types of notifications: SNotification which handles updates of the form "C' was added to S(C)" and RNotification which handles updates of the form "(C, D) was added to R(r)".

SNotifications (or better to say rules they represent) are always of the form that they listen for the change made to any C and wait until a certain value is added to that C.

For example consider rule CR1: If C' ∈ S(C), C' ⊑ D then S(C) = S(C) ∪ {D} That means: We only wait for an update with the value C' (that's the only thing that can trigger this rule). Thus when we add C' to some S(C) we lookup which notifications are interested in this update (CR1 being one of them) and inform them about this update. We implement this by a map that maps C' → list of notifications. This means: When C' is added to some C inform all notifications in map[C'].

Rules waiting for some R(r) are organized a bit diffent: They don't want to be informed about a certain (C, D) being added, but want to be informed about all (C, D) that are added.

Most of the rules want to listen only on a certain r, for example rule CR4 says that if we have ∃r.D' ⊑ E we have to listen to all elements added to R(r) for that specific r. Rule CR5 on the other hand waits on updates on all roles. Thus we have a map that maps r → list of notifications. This list holds all notifications that are interested in r. It also contains an entry for NoRole (which is used to describe an id that is not really a role) and stores all notifcations interested in updates on all R(r) (should only be CR5).

Thus when we receive information that (C, D) was added to R(r) we inform all notifications in map[r] and map[NoRole].

A RuleMap is initialized with a given normalized TBox and creates all notifications and adds them. Thus before usage the Init method must be called with that TBox. If other rules are required and should be added it should be noted that it is not safe for concurrent writing acces.

If it is really required see the worker methods (should not be needed if you just want to initialize it with a given TBox).

func NewRuleMap 

func NewRuleMap() *RuleMap

func (*RuleMap) AddRWorker 

func (rm *RuleMap) AddRWorker(ch <-chan AddRNotification, done chan<- bool)

AddRWorker works similar as AddSWorker, only for RNotifications.

func (*RuleMap) AddSWorker 

func (rm *RuleMap) AddSWorker(ch <-chan AddSNotification, done chan<- bool)

AddSWorker is a little helper method that is used to concurrently add new entries to SRules. Start a gourotine for that message, write all notifications to the channel ch, close the channel once you're done and wait on the done channel until all updates certainly happened.

func (*RuleMap) Init 

func (rm *RuleMap) Init(tbox *NormalizedTBox)

type SNotification 

type SNotification interface {
	// Information, that C' was added to S(C)
	GetSNotification(state StateHandler, c, cPrime uint) bool
}

type SUpdate 

type SUpdate struct {
	C, D uint
}

SUpdate is a type that stores the information that D has been added to S(C). It is usually used in a queue that stores all updates that still must be executed (notifications for that update must be issued). TODO Is there a mix-up with C / D?

func NewSUpdate 

func NewSUpdate(c, d uint) *SUpdate

NewSUpdate creates a new SUpdate.

type SetGraph 

type SetGraph struct {
	// contains filtered or unexported fields
}

func NewSetGraph 

func NewSetGraph() *SetGraph

func (*SetGraph) AddEdge 

func (g *SetGraph) AddEdge(source, target uint) bool

func (*SetGraph) Init 

func (g *SetGraph) Init(numConcepts uint)

func (*SetGraph) String 

func (g *SetGraph) String() string

func (*SetGraph) Succ 

func (g *SetGraph) Succ(vertex uint, ch chan<- uint)

type SliceGraph 

type SliceGraph struct {
	Graph [][]uint
}

func NewSliceGraph 

func NewSliceGraph() *SliceGraph

func (*SliceGraph) AddEdge 

func (g *SliceGraph) AddEdge(source, target uint) bool

func (*SliceGraph) Init 

func (g *SliceGraph) Init(numConcepts uint)

func (*SliceGraph) Succ 

func (g *SliceGraph) Succ(vertex uint, ch chan<- uint)

type SolverState 

type SolverState struct {
	S []*BCSet
	R []*Relation
	// contains filtered or unexported fields
}

SolverState is an implementation of StateHandler, for more details see there. It protects each S(C) and R(r) with a RWMutex.

func NewSolverState 

func NewSolverState(c *ELBaseComponents, domains *domains.CDManager) *SolverState

NewSolverState returns a new solver state given the base components, thus it initializes S and R and the mutexes used to control r/w access.

func (*SolverState) AddConcept 

func (state *SolverState) AddConcept(c, d uint) bool

add D to S(C)

func (*SolverState) AddRole 

func (state *SolverState) AddRole(r, c, d uint) bool

func (*SolverState) ContainsConcept 

func (state *SolverState) ContainsConcept(c, d uint) bool

Does S(C) contain D?

func (*SolverState) ContainsRole 

func (state *SolverState) ContainsRole(r, c, d uint) bool

func (*SolverState) GetCDs 

func (state *SolverState) GetCDs() *domains.CDManager

func (*SolverState) GetComponents 

func (state *SolverState) GetComponents() *ELBaseComponents

func (*SolverState) GetConjunction 

func (state *SolverState) GetConjunction(c uint) [][]*domains.PredicateFormula

func (*SolverState) ReverseRoleMapping 

func (state *SolverState) ReverseRoleMapping(r, d uint) []uint

func (*SolverState) RoleMapping 

func (state *SolverState) RoleMapping(r, c uint) []uint

func (*SolverState) SubsetConcepts 

func (state *SolverState) SubsetConcepts(c, d uint) bool

func (*SolverState) UnionConcepts 

func (state *SolverState) UnionConcepts(c, d uint) bool

S(C) = S(C) + S(D)

type StateHandler 

type StateHandler interface {
	// ContainsConcept checks whether D ∈ S(C).
	ContainsConcept(c, d uint) bool

	// AddConcept adds D to S(C) and returns true if the update changed S(C).
	AddConcept(c, d uint) bool

	// UnionConcepts adds all elements from S(D) to S(C), thus performs the update
	// S(C) = S(C) ∪ S(D). Returns true if some elements were added to S(C).
	UnionConcepts(c, d uint) bool

	// ContainsRole checks whether (C, D) ∈ R(r).
	ContainsRole(r, c, d uint) bool

	// AddRole adds (C, D) to R(r). It must also update the graph.
	// The first boolean signals if an update in R(r) occurred, the second
	// if an update in the graph occurred.
	// TODO This is not really nice, we probably need something else later...
	// and is ignored in the rules now.
	AddRole(r, c, d uint) bool

	// RoleMapping returns all pairs (C, D) in R(r) for a given C.
	// TODO document: must return a new slice
	RoleMapping(r, c uint) []uint

	// ReverseRoleMapping returns all pairs (C, D) in R(r) for a given D.
	ReverseRoleMapping(r, d uint) []uint

	// GetComponents returns the number of all objects, s.t. we can use it when
	// needed.
	GetComponents() *ELBaseComponents

	// GetCDs returns the concrete domain manager.
	GetCDs() *domains.CDManager

	// GetConjunction returns conj(C)
	GetConjunction(c uint) [][]*domains.PredicateFormula
}

StateHandler is used by the concurrent (and maybe other solvers) to update state information. That is update the mappings S(C) and R(r) and check if certain elements are present in it. For R(r) it is sometimes required to iterate over each element in R(r), therefor exists methods that take a channel as an input, write each element to that channel and then close the channel. Thus methods that require to iterate over each R(r) start a go routine with a channel and iterate the channel until it is closed. A basic implementation is given in SolverState, other state handlers or even solvers can simply delegate certain methods to this basic implementation. That is they can add additional logic (such as triggering certain rules) and let the SolverState handle everything else. Of course it is also possible to write a completely new handler.

State handlers must be safe to use concurrently from multiple go routines. That is also true for methods that iterate over objects: No write operations may happen during that time.

Note that the rule CR6 is rather nasty. If the graph changes we must get a notification for all C, D that are now connected (meaning that C ↝ D) but where not connected before. However it is rather difficult to decide for which C, D that now is true. (Partially) dynamic graph algorithmus would be required for this, see for example "A fully dynamic reachability algorithm for directed graphs with an almost linear update time" (Roditty, Zwick, 2004) or "Improved dynamic reachability algorithms for directed graphs" (Roditty, Zwick, 2002).

However I think this is out of the scope of this project (at least for now). Therefor we have different ways to implement this. Therefor we have extensions of this interface to provide the required operations. This is not an ideal solution, but until there is an efficient (and final) implementation I think it's best to keep it that way.

Also another interesting approach is given in "Practical Reasoning with Nominals in the EL Family of Description Logics" (Kazakov, Krötzsch, Simancík)

Here is a quick summary of the ideas I came up with: (1) Check only if an edge was inserted in the graph, in this case check 

all {a}, C, D for the conditions of rule CR6.

(2) Really compute all C, D for which the condition changed and then update 

only those. This requires either a complicated graph algorithm or

the storage of the transitive closure, which may require a log of memory.

Also this rule is different in the case of the "update guard". The other rules always add a certain element we're waiting for. That is for example CR1 waits for C' ∈ S(C) and then adds it to S(D), C' was already in S(D) or it will be added now. In CR6 however we have the condition S(D) ⊊ S(C). That means: If either {a} added somewhere or the graph has changed we get a notification for that, but whenever an element gets added to S(C) afterwards we must add it to S(D) as well.

There are different ways to handle this, so the solvers for more details on that.

TODO document what we do about this problem. TODO report current state.

type TBox 

type TBox struct {
	Components *ELBaseComponents
	GCIs       []*GCIConstraint
	RIs        []*RoleInclusion
}

TBox describes a TBox as a set of GCIs and RIs.

func NewTBox 

func NewTBox(components *ELBaseComponents, gcis []*GCIConstraint, ris []*RoleInclusion) *TBox

NewTBox returns a new TBox.

type TBoxNormalformBuilder 

type TBoxNormalformBuilder interface {
	Normalize(tbox *TBox) *NormalizedTBox
}

TBoxNormalformBuilder is anything that transforms a tbox to a normalized tbox. Multiple calls to Normalize should be possible (i.e. data must be reset when running this method).

type TopConcept 

type TopConcept struct{}

TopConcept is the Top concept ⊤. 

var Top TopConcept = NewTopConcept()

Top is a constant concept that represents to top concept ⊤.

func NewTopConcept 

func NewTopConcept() TopConcept

NewTopConcept returns a new TopConcept. Instead of creating it again and again all the time you should use the const value Top.

func (TopConcept) IsInBCD 

func (top TopConcept) IsInBCD() bool

func (TopConcept) NormalizedID 

func (top TopConcept) NormalizedID(c *ELBaseComponents) uint

func (TopConcept) String 

func (top TopConcept) String() string

type TransitiveClosureGraph 

type TransitiveClosureGraph struct {
	*SetGraph
	// contains filtered or unexported fields
}

func NewTransitiveClosureGraph 

func NewTransitiveClosureGraph() *TransitiveClosureGraph

func (*TransitiveClosureGraph) AddEdge 

func (g *TransitiveClosureGraph) AddEdge(source, target uint) bool

func (*TransitiveClosureGraph) Init 

func (g *TransitiveClosureGraph) Init(numConcepts uint)

Source Files

View all Source files

Directories

Path Synopsis
cmd
cddebug
domainsdebug
goel
goelbench
goeldebug
medexample
legacy
elowl
Package elowl builds a bridge between OWL ontology file and the internal representation of EL++.
 Package elowl builds a bridge between OWL ontology file and the internal representation of EL++.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.