goel

type ABox ¶

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

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

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

type AddRNotification ¶

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

func NewAddRNotification(role uint, notification RNotification) AddRNotification

type AddSNotification ¶

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

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() *AllChangesCR6

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

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() *AllChangesRuleMap

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

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(graph ConceptGraph, search ExtendedReachabilitySearch) *AllChangesSolver

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

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

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

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

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

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(c *ELBaseComponents,
	domains *domains.CDManager, g ConceptGraph, search ExtendedReachabilitySearch) *AllChangesSolverState

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

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

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(c *ELBaseComponents, initialCapacity uint) *BCPairSet

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

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

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

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(c *ELBaseComponents, initialCapacity uint) *BCSet

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

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

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

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

func (s *BCSet) Copy() *BCSet

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

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

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

func (s *BCSet) String() string

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

type BidirectionalSearch ¶

type BidirectionalSearch int

const (
	BidirectionalFalse BidirectionalSearch = iota
	BidrectionalDirect
	BidrectionalReverse
	BidrectionalBoth
)

func (i BidirectionalSearch) String() string

type BottomConcept ¶

type BottomConcept struct{}

BottomConcept is the Bottom Concept ⊥.

var Bottom BottomConcept = NewBottomConcept()

func NewBottomConcept() BottomConcept

func (bot BottomConcept) IsInBCD() bool

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

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(graph ConceptGraph, search ExtendedReachabilitySearch) *BulkSolver

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

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

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

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

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

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(solver *BulkSolver) *BulkWorker

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

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

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

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

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(d uint) CR1

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(s uint) CR10

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(r1, r2, r3 uint) *CR11

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(c1, c2, d uint) *CR2

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(r, d uint) *CR3

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(r, dPrime, e uint) *CR4

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

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() *CR5

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

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() CR7AndCR8

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

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(concepts ...Concept) Concept

type ConceptAssertion ¶

type ConceptAssertion struct {
	C Concept
	A Nominal
}

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

func NewConceptAssertion(c Concept, a Nominal) *ConceptAssertion

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(i uint) ConcreteDomainExtension

func (cd ConcreteDomainExtension) IsInBCD() bool

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

func (cd ConcreteDomainExtension) String() string

type ConcurrentNotificationSolver ¶

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

func NewConcurrentNotificationSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *ConcurrentNotificationSolver

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

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

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

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

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(graph ConceptGraph, search ExtendedReachabilitySearch) *ConcurrentSolver

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

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

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

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

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

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

type ConcurrentWorkerPool ¶

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

func NewConcurrentWorkerPool() *ConcurrentWorkerPool

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

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

func (p *ConcurrentWorkerPool) Close()

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

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

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

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(c, d Concept) Conjunction

func (conjunction Conjunction) IsInBCD() bool

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

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(k int) *DefaultNormalFormBuilder

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(nominals, cdExtensions, names, roles uint) *ELBaseComponents

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

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

func (c *ELBaseComponents) NumBCD() uint

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(r Role, c Concept) ExistentialConcept

func (existential ExistentialConcept) IsInBCD() bool

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

func (existential ExistentialConcept) String() string

type ExtendedGraphSearcher ¶

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

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

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

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

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(c, d Concept) *GCIConstraint

func (gci *GCIConstraint) String() string

type GraphSearcher ¶

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

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

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

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(next uint) *IntDistributor

func (dist *IntDistributor) Next() uint

type NCAllChangesCR6 ¶

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

func NewNCAllChangesCR6() *NCAllChangesCR6

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

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

type NCAllChangesRuleMap ¶

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

func NewNCAllChangesRuleMap() *NCAllChangesRuleMap

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

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

type NCAllChangesSolverState ¶

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

	Graph    ConceptGraph
	Searcher *ExtendedGraphSearcher
}

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

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

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

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

type NCRBSolver ¶

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

func NewNCRBSolver(graph ConceptGraph, search ExtendedReachabilitySearch) *NCRBSolver

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

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

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

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

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

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

type NCSolverState ¶

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

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

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

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

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

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

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

func (state *NCSolverState) GetComponents() *ELBaseComponents

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

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

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

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

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

type NaiveSolver ¶

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

func NewNaiveSolver(graph ConceptGraph, search ReachabilitySearch) *NaiveSolver

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

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(i uint) NamedConcept

func (name NamedConcept) IsInBCD() bool

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

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 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(i uint) NominalConcept

func (nominal NominalConcept) IsInBCD() bool

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

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(c1, c2, d Concept) *NormalizedCI

func NewNormalizedCISingle(c1, d Concept) *NormalizedCI

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

func (ci *NormalizedCI) String() string

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(r Role, c1, d Concept) *NormalizedCILeftEx

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

func (ci *NormalizedCILeftEx) String() string

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(c1 Concept, r Role, c2 Concept) *NormalizedCIRightEx

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

func (ci *NormalizedCIRightEx) String() string

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(r1, r2, s Role) *NormalizedRI

func NewNormalizedRISingle(r1, s Role) *NormalizedRI

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

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

func (ri *NormalizedRI) String() string

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

type NormalizedRandomELBuilder ¶

type NormalizedRandomELBuilder struct {
	NumIndividuals  uint
	NumConceptNames uint
	NumRoles        uint
}

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(r io.Reader) (*NormalizedTBox, error)

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(distributor *IntDistributor) *PhaseOneResult

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

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

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(distributor *IntDistributor) *PhaseTwoResult

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

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(r, c, d uint) *RUpdate

type RandomELBuilder ¶

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

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(initialCapacity uint) *Relation

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

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

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(i uint) Role

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(r Role, a, b Nominal) *RoleAssertion

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(lhs []Role, rhs Role) *RoleInclusion

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() *RuleMap

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

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

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(c, d uint) *SUpdate

type SetGraph ¶

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

func NewSetGraph() *SetGraph

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

func (g *SetGraph) Init(numConcepts uint)

func (g *SetGraph) String() string

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

type SliceGraph ¶

type SliceGraph struct {
	Graph [][]uint
}

func NewSliceGraph() *SliceGraph

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

func (g *SliceGraph) Init(numConcepts uint)

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(c *ELBaseComponents, domains *domains.CDManager) *SolverState

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

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

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

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

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

func (state *SolverState) GetComponents() *ELBaseComponents

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

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

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

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

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

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(components *ELBaseComponents, gcis []*GCIConstraint, ris []*RoleInclusion) *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()

func NewTopConcept() TopConcept

func (top TopConcept) IsInBCD() bool

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

func (top TopConcept) String() string

type TransitiveClosureGraph ¶

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

func NewTransitiveClosureGraph() *TransitiveClosureGraph

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

func (g *TransitiveClosureGraph) Init(numConcepts uint)