History | View | Annotate | Download (38.9 KB)

Rewrap some code to fit into 90 chars width

Only deallocate solver for unsat nodes

We want to still have the solver for naive unsat propagation

Remove debug output

Only remove solver after Unsat Propagation

Deallocate satsolver once core becomes `Open`

The satsolver is reatined and only updated with new clauses for everystate that is generated out of a core. Once the core becomes Open (asopposed to expandable), the solver is no longer needed.

This patch makes the solver a `Solver option` and gets it deallocated...

Use proper number of open States when calculating frequency

Instead of some calculation based of finishing on normal Cores reallycount proper Open States

substract number of finishing/Sat nodes when calculating propagation frequency

Remove nominal propagation for now

Make number of waves between propagation depend on #openCores

Add comment

Do both sat and unsat propagation

Remove debug output from propagateSatMu

Do a final propagation round at the end

Obvious simplification

Fix typo in propagateUnsatMu function name

Expandable states are always acceptable Finishing states for Unsat propagation

Switch to only unsat propagation for testing

If root is Sat, formula is unconditionally Sat

First implementation of propagateUnsat

Add some comments to propagateSatMu

Allow finishing cycles depending on only Sat states

Don't assume Open means Sat when finished

Assumption doesn't hold true currently

Treat Sat states like finishing states

With Sat states only treated like other states in the second fixpointiteration, the outer fixpoint was not ncessarily monononously decreasingcausing wrong results when in the first round the same number of nodesgot removed as added due to sat states.

Consider expanable Cores (but not states)

Acceptance test for cores is ∃ which is safe to use when non or onlysome child states are created tus far

Turn inner fixpoint inside-out

Mark `True` only node as Sat

For now, don't consider Expandable states

Fix inclusion condition for A_x

Make Sat children actually propagate their state to the parents

Preliminarily mark States with no childs Sat in propagateSatMu

Should actually happen when the State changes from `Expandable` to`Open` and trigger the propagateSatMu but for now just do it inpropagateSatMu so we can observe the algorithm working.

Reorganize code, start from Sat nodes as well

Not only finishing cycles but also plain sat nodes may cause a node tobe satisfiable

Restrict finishing nodes used as startingpoint

Only finishing nodes with enough Open / Sat children are to beconsidered as startingpoints

Also accept already Satisfiable nodes when finding paths

Call new propagateSatMu instead of old propagateSat

preliminary propafateSat for μ-Calculus

This still produces wrong results: It assumes every node with emptyfocus to be sat.

whitespace cleanup

Some more comments

Make reasoner nodes include deferrals

This makes the identifying information be of type bset*bset instead ofbset and adds tracking of deferrals for propositional reasoning and --in case of K -- for modal reasoning

track deferrals across propositional reasoning

Add deferral flags to core/state data structure

Whitespace cleanup

Unfold fixpoints when generating new states

unfold fixpoints when creating new Cores

Add a lot of comments about cores

Implement state listing for debugger

Implement lscores for debugger

One debugger step takes one element from the queue

Now one step in the debugger removes exactly one element from the queue(if it's not empty). If this action empties the queue, nominals arepropagated.

Add basic debugging repl

Change ConstF to TrueFalseF

Reset CoAlgReasoner to the version ee45f2f

This fixes an assertion that failed for the PML+K formula

sat "({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"

which is satisfiable.

Add more comments to the reasoner core

Make Or-step in And-Or-rules lazy

Generalize ruleEnumeration by introducing lazylist

Introduce a new generic data type lazylist, e.g. used for lazy ruleenumerations.

Remove Disjunctive ruleEnumerations

Propagation of satisfiability and unsatisfiability does not coverdisjunctions and I don't get how propagation works, so I won't touch ityet. So this reverts the only partially implemented DisjunctiveruleEnumerations,

Add more comments to CoAlgReasoner.ml

Add many comments in CoAlgReasoner.ml

Make insertRule more disjunctive-aware

Introduce junctions (Disjunction, Conjunction)

Connect OWL ontologies with CoAlgReasoner

Separate cool into library and coalg frontend