Stefan Ellmauthaler
b73231f501
Utilised quickcheck, assert_cmd, predicates, and assert_fs for better tests of low-level functionality as well as cli-testing. Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams
Abstract Dialectical Frameworks
An abstract dialectical framework (ADF) consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration.
Ordered Binary Decision Diagram
An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap.
Input-file format:
Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement. The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows:
- and(x,y): conjunction
- or(x,y): disjunctin
- iff(x,Y): if and only if
- xor(x,y): exclusive or
- neg(x): classical negation
- c(v): constant symbol "verum" - tautology/top
- c(f): constant symbol "falsum" - inconsistency/bot
Development notes
To run all the tests placed in the submodule you need to run
$> git submodule init
at the first time. Afterwards you need to update the content of the submodule to be on the currently used revision by
$> git submodule update
The tests can be started by using the test-framework of cargo, i.e.
$> cargo test
Note that some of the instances are quite big and it might take some time to finish all the tests. If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests.