From e0abe7eeefa7c6087431b65eab8cfe6171feb0e7 Mon Sep 17 00:00:00 2001 From: Drodt Date: Tue, 21 Nov 2023 16:04:19 +0100 Subject: [PATCH] Update detekt and hashing --- backend/build.gradle.kts | 13 +- backend/config/detekt/detekt.yml | 97 +++++------ backend/src/main/kotlin/{main.kt => Main.kt} | 24 ++- .../{constants.kt => Constants.kt} | 0 .../{exceptions.kt => Exceptions.kt} | 0 .../main/kotlin/kalkulierbar/JSONCalculus.kt | 9 +- .../kotlin/kalkulierbar/ScoredCalculus.kt | 3 +- .../main/kotlin/kalkulierbar/clause/Atom.kt | 12 +- .../kotlin/kalkulierbar/clause/ClauseSet.kt | 3 +- .../kotlin/kalkulierbar/dpll/BasicMoves.kt | 66 ++++---- .../src/main/kotlin/kalkulierbar/dpll/DPLL.kt | 4 +- .../{abstractLogic.kt => AbstractLogic.kt} | 15 +- .../kalkulierbar/logic/FirstOrderTerm.kt | 18 ++- .../kotlin/kalkulierbar/logic/LogicNodes.kt | 63 +++++--- .../logic/transform/Collectors.kt | 13 +- .../logic/transform/DoNothingCollector.kt | 10 +- .../logic/transform/FirstOrderCNF.kt | 11 +- .../kalkulierbar/logic/transform/NaiveCNF.kt | 12 +- .../logic/transform/PrenexNormalForm.kt | 11 +- .../kalkulierbar/logic/transform/Signature.kt | 9 +- .../logic/transform/Skolemization.kt | 14 +- .../transform/TermVariableManipulation.kt | 19 ++- .../logic/transform/TseytinCNF.kt | 8 +- .../logic/transform/UniqueVariables.kt | 14 +- .../kalkulierbar/logic/util/Unification.kt | 21 ++- .../logic/util/UnifierEquivalence.kt | 5 +- .../nonclausaltableaux/BasicMoves.kt | 64 +++++--- .../nonclausaltableaux/DeltaSkolemization.kt | 11 +- .../nonclausaltableaux/NcTableauxMove.kt | 3 +- .../nonclausaltableaux/NonClausalTableaux.kt | 13 +- .../NonClausalTableauxMisc.kt | 4 +- .../kalkulierbar/parsers/ClauseSetParser.kt | 9 +- .../kalkulierbar/parsers/FirstOrderParser.kt | 83 ++++++---- .../parsers/FirstOrderSequentParser.kt | 11 +- .../parsers/FlexibleClauseSetParser.kt | 14 +- .../parsers/PropositionalParser.kt | 25 ++- .../parsers/PropositionalSequentParser.kt | 5 +- .../kotlin/kalkulierbar/parsers/Tokenizer.kt | 7 +- .../resolution/FirstOrderBasicMoves.kt | 35 ++-- .../resolution/GenericResolution.kt | 14 +- .../resolution/HelperFunctions.kt | 22 ++- .../resolution/PropositionalResolution.kt | 30 ++-- .../resolution/RestrictionChecking.kt | 25 +-- .../GenericSequentCalculusBasicMoves.kt | 56 +++---- .../kalkulierbar/sequent/fo/BasicMoves.kt | 45 ++++-- .../sequent/fo/FirstOrderSequent.kt | 43 ++++- .../sequent/prop/PropositionalSequent.kt | 47 +++++- .../kalkulierbar/signedtableaux/BasicMoves.kt | 93 +++++++---- .../signedtableaux/SignedModalTableaux.kt | 13 +- .../signedtableaux/SignedModalTableauxMisc.kt | 10 +- .../tableaux/FirstOrderBasicMoves.kt | 16 +- .../tableaux/FirstOrderTableaux.kt | 12 +- .../tableaux/FirstOrderTableauxMisc.kt | 3 +- .../kalkulierbar/tableaux/GenericTableaux.kt | 47 +++--- .../tableaux/PropositionalBasicMoves.kt | 8 +- .../tableaux/PropositionalTableauxMisc.kt | 6 +- .../tableaux/RestrictionChecking.kt | 78 +++++---- .../tamperprotect/TamperProtect.kt | 1 + .../kotlin/kalkulierbar/tree/TreeGardener.kt | 28 ++-- .../{constants.kt => Constants.kt} | 0 .../src/main/kotlin/statekeeper/Scoreboard.kt | 36 +++-- .../{statekeeper.kt => Statekeeper.kt} | 38 +++-- backend/src/main/kotlin/statekeeper/Stats.kt | 8 +- .../kotlin/kalkulierbar/TestTamperProtect.kt | 16 +- .../kotlin/kalkulierbar/dpll/TestDpllJson.kt | 94 ++++++++++- .../firstordersequent/TestAndRight.kt | 6 +- .../firstordersequent/TestUndo.kt | 6 +- .../logic/TestPropositionalLogic.kt | 33 +++- .../logic/transform/TestSignature.kt | 16 +- .../nonclausaltableaux/TestBeta.kt | 4 +- .../parsers/TestFirstOrderSequentParser.kt | 5 +- .../kalkulierbar/propsequent/TestAndRight.kt | 6 +- .../kalkulierbar/propsequent/TestUndo.kt | 6 +- .../kalkulierbar/regression/TestIssue50.kt | 9 +- .../resolution/TestFOResolveUnify.kt | 40 ++++- .../resolution/TestHyperResolution.kt | 32 +++- .../resolution/TestResolutionJson.kt | 150 ++++++++++++++++-- .../kalkulierbar/signedtableaux/TestPrune.kt | 2 +- .../kalkulierbar/statekeeper/TestAdmin.kt | 33 +++- .../tableaux/TestFirstOrderJson.kt | 42 ++++- .../tableaux/TestPropositionalJson.kt | 51 +++++- .../kalkulierbar/tableaux/TestUndoFO.kt | 7 +- 82 files changed, 1389 insertions(+), 606 deletions(-) rename backend/src/main/kotlin/{main.kt => Main.kt} (94%) rename backend/src/main/kotlin/kalkulierbar/{constants.kt => Constants.kt} (100%) rename backend/src/main/kotlin/kalkulierbar/{exceptions.kt => Exceptions.kt} (100%) rename backend/src/main/kotlin/kalkulierbar/logic/{abstractLogic.kt => AbstractLogic.kt} (92%) rename backend/src/main/kotlin/statekeeper/{constants.kt => Constants.kt} (100%) rename backend/src/main/kotlin/statekeeper/{statekeeper.kt => Statekeeper.kt} (91%) diff --git a/backend/build.gradle.kts b/backend/build.gradle.kts index a2ab2110f..fc8998edb 100644 --- a/backend/build.gradle.kts +++ b/backend/build.gradle.kts @@ -1,9 +1,9 @@ plugins { kotlin("jvm") version "1.7.20" - kotlin("plugin.serialization") version "1.7.20" + kotlin("plugin.serialization") version "1.9.20" application id("org.jmailen.kotlinter") version "3.10.0" - id("io.gitlab.arturbosch.detekt") version "1.21.0" + id("io.gitlab.arturbosch.detekt") version "1.23.3" id("com.github.johnrengelman.shadow") version "7.1.2" id("java") id("jacoco") @@ -27,11 +27,13 @@ dependencies { implementation("org.slf4j:slf4j-simple:2.0.9") // Hashing - implementation("com.github.komputing:khash:1.1.3") + implementation("com.github.komputing.khash:keccak:1.1.3") // Testing testImplementation(kotlin("test-junit5")) testRuntimeOnly("org.junit.jupiter", "junit-jupiter-engine", "5.10.1") + + detektPlugins("io.gitlab.arturbosch.detekt:detekt-formatting:1.23.3") } application { @@ -57,13 +59,12 @@ java { detekt { toolVersion = "1.23.3" - source = files("src/main/kotlin") - config = files("$projectDir/config/detekt/detekt.yml") + source.setFrom("src/main/kotlin") + config.setFrom("$projectDir/config/detekt/detekt.yml") } kotlinter { ignoreFailures = false reporters = arrayOf("checkstyle", "plain") experimentalRules = false - disabledRules = arrayOf("no-wildcard-imports", "filename") } diff --git a/backend/config/detekt/detekt.yml b/backend/config/detekt/detekt.yml index f85ec2f37..99688222f 100644 --- a/backend/config/detekt/detekt.yml +++ b/backend/config/detekt/detekt.yml @@ -8,7 +8,7 @@ build: processors: active: true - exclude: + exclude: [] # - 'DetektProgressListener' # - 'FunctionCountProcessor' # - 'PropertyCountProcessor' @@ -64,14 +64,14 @@ complexity: active: false threshold: 10 includeStaticDeclarations: false - ComplexMethod: + CyclomaticComplexMethod: active: true threshold: 13 ignoreSingleWhenExpression: false ignoreSimpleWhenEntries: false LabeledExpression: active: false - ignoredLabels: "" + ignoredLabels: [] LargeClass: active: true threshold: 600 @@ -91,15 +91,15 @@ complexity: threshold: 4 StringLiteralDuplication: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] threshold: 3 ignoreAnnotation: true excludeStringsWithLessThan5Characters: true ignoreStringsRegex: '$^' TooManyFunctions: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" - thresholdInFiles: 11 + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] + thresholdInFiles: 13 thresholdInClasses: 11 thresholdInInterfaces: 11 thresholdInObjects: 11 @@ -145,10 +145,10 @@ exceptions: active: true ExceptionRaisedInUnexpectedLocation: active: false - methodNames: 'toString,hashCode,equals,finalize' + methodNames: ['toString', 'hashCode', 'equals', 'finalize'] InstanceOfCheckForException: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] NotImplementedDeclaration: active: false PrintStackTrace: @@ -160,7 +160,12 @@ exceptions: ignoreLabeled: false SwallowedException: active: false - ignoredExceptionTypes: 'InterruptedException,NumberFormatException,ParseException,MalformedURLException' + ignoredExceptionTypes: [ + 'InterruptedException', + 'NumberFormatException', + 'ParseException', + 'MalformedURLException' + ] allowedExceptionNameRegex: "^(_|(ignore|expected).*)" ThrowingExceptionFromFinally: active: false @@ -168,12 +173,12 @@ exceptions: active: false ThrowingExceptionsWithoutMessageOrCause: active: false - exceptions: 'IllegalArgumentException,IllegalStateException,IOException' + exceptions: ['IllegalArgumentException', 'IllegalStateException', 'IOException'] ThrowingNewInstanceOfSameException: active: false TooGenericExceptionCaught: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] exceptionNames: - ArrayIndexOutOfBoundsException - Error @@ -217,7 +222,6 @@ formatting: active: false autoCorrect: true indentSize: 4 - continuationIndentSize: 4 MaximumLineLength: active: true maxLineLength: 120 @@ -298,42 +302,40 @@ naming: active: true ClassNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] classPattern: '[A-Z$][a-zA-Z0-9$]*' ConstructorParameterNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] parameterPattern: '[a-z][A-Za-z0-9]*' privateParameterPattern: '[a-z][A-Za-z0-9]*' excludeClassPattern: '$^' EnumNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] enumEntryPattern: '^[A-Z][_a-zA-Z0-9]*' ForbiddenClassName: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" - forbiddenName: '' + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] + forbiddenName: [] FunctionMaxLength: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] maximumFunctionNameLength: 30 FunctionMinLength: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] minimumFunctionNameLength: 3 FunctionNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] functionPattern: '^([a-z$][a-zA-Z$0-9]*)|(`.*`)$' excludeClassPattern: '$^' - ignoreOverridden: true FunctionParameterNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] parameterPattern: '[a-z][A-Za-z0-9]*' excludeClassPattern: '$^' - ignoreOverridden: true InvalidPackageDeclaration: active: false rootPackage: '' @@ -344,35 +346,34 @@ naming: ignoreOverridden: true ObjectPropertyNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] constantPattern: '[A-Za-z][_A-Za-z0-9]*' propertyPattern: '[A-Za-z][_A-Za-z0-9]*' privatePropertyPattern: '(_)?[A-Za-z][_A-Za-z0-9]*' PackageNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] packagePattern: '^[a-z]+(\.[a-z][A-Za-z0-9]*)*$' TopLevelPropertyNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] constantPattern: '[A-Z][_A-Z0-9]*' propertyPattern: '[A-Za-z][_A-Za-z0-9]*' privatePropertyPattern: '_?[A-Za-z][_A-Za-z0-9]*' VariableMaxLength: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] maximumVariableNameLength: 64 VariableMinLength: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] minimumVariableNameLength: 1 VariableNaming: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] variablePattern: '[a-z][A-Za-z0-9]*' privateVariablePattern: '(_)?[a-z][A-Za-z0-9]*' excludeClassPattern: '$^' - ignoreOverridden: true performance: active: true @@ -380,10 +381,10 @@ performance: active: false ForEachOnRange: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] SpreadOperator: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] UnnecessaryTemporaryInstantiation: active: true @@ -391,8 +392,6 @@ potential-bugs: active: true Deprecation: active: false - DuplicateCaseInWhenExpression: - active: true EqualsAlwaysReturnsTrueOrFalse: active: false EqualsWithHashCodeExist: @@ -409,13 +408,9 @@ potential-bugs: active: false LateinitUsage: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] ignoreAnnotated: [] ignoreOnClassesPattern: "" - MissingWhenCase: - active: false - RedundantElseInWhen: - active: false UnconditionalJumpStatementInLoop: active: false UnreachableCode: @@ -435,7 +430,7 @@ style: active: false DataClassContainsFunctions: active: false - conversionFunctionPrefix: 'to' + conversionFunctionPrefix: ['to'] DataClassShouldBeImmutable: active: false EqualsNullCall: @@ -449,11 +444,11 @@ style: includeLineWrapping: false ForbiddenComment: active: true - values: 'TODO:,FIXME:,STOPSHIP:' + comments: ['TODO:', 'FIXME:', 'STOPSHIP:'] allowedPatterns: "" ForbiddenImport: active: false - imports: '' + imports: [] forbiddenPatterns: "" ForbiddenVoid: active: false @@ -462,17 +457,15 @@ style: FunctionOnlyReturningConstant: active: false ignoreOverridableFunction: true - excludedFunctions: 'describeContents' + excludedFunctions: ['describeContents'] ignoreAnnotated: ["dagger.Provides"] - LibraryCodeMustSpecifyReturnType: - active: false LoopWithTooManyJumpStatements: active: false maxJumpCount: 1 MagicNumber: active: true - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" - ignoreNumbers: '-1,0,1,2' + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] + ignoreNumbers: ['-1', '0', '1', '2'] ignoreHashCodeFunction: true ignorePropertyDeclaration: false ignoreConstantDeclaration: true @@ -481,8 +474,6 @@ style: ignoreNamedArgument: true ignoreEnums: false ignoreRanges: false - MandatoryBracesIfStatements: - active: false MaxLineLength: active: true maxLineLength: 135 @@ -503,8 +494,6 @@ style: active: true OptionalUnit: active: false - OptionalWhenBraces: - active: false PreferToOverPairSyntax: active: false ProtectedMemberInFinalClass: @@ -516,7 +505,7 @@ style: ReturnCount: active: true max: 2 - excludedFunctions: "equals" + excludedFunctions: ["equals"] excludeLabeled: false excludeReturnFromLambda: true excludeGuardClauses: false @@ -574,5 +563,5 @@ style: active: false WildcardImport: active: false - excludes: "**/test/**,**/androidTest/**,**/*.Test.kt,**/*.Spec.kt,**/*.Spek.kt" - excludeImports: 'java.util.*,kotlinx.android.synthetic.*' + excludes: ["**/test/**", "**/androidTest/**", "**/*.Test.kt", "**/*.Spec.kt", "**/*.Spek.kt"] + excludeImports: ['java.util.*', 'kotlinx.android.synthetic.*'] diff --git a/backend/src/main/kotlin/main.kt b/backend/src/main/kotlin/Main.kt similarity index 94% rename from backend/src/main/kotlin/main.kt rename to backend/src/main/kotlin/Main.kt index 17b3ed78e..160a30983 100644 --- a/backend/src/main/kotlin/main.kt +++ b/backend/src/main/kotlin/Main.kt @@ -1,7 +1,12 @@ package main.kotlin import io.javalin.Javalin -import kalkulierbar.* +import kalkulierbar.ApiMisuseException +import kalkulierbar.Calculus +import kalkulierbar.KBAR_DEFAULT_PORT +import kalkulierbar.KalkulierbarException +import kalkulierbar.ScoredCalculus +import kalkulierbar.Scores import kalkulierbar.dpll.DPLL import kalkulierbar.nonclausaltableaux.NonClausalTableaux import kalkulierbar.resolution.FirstOrderResolution @@ -32,13 +37,15 @@ val endpoints: Set = setOf( fun main(args: Array) { // Verify that all calculus implementations have unique names - if (endpoints.size != endpoints.map { it.identifier }.distinct().size) + if (endpoints.size != endpoints.map { it.identifier }.distinct().size) { throw KalkulierbarException("Set of active calculus implementations contains duplicate identifiers") - + } // Verify that no calculus is overriding /admin and /config endpoints - if (endpoints.any { it.identifier == "admin" || it.identifier == "config" || it.identifier == "stats" }) - throw KalkulierbarException("Set of active calculi contains forbidden identifiers \"admin\", \"config\" or \"stats\"") - + if (endpoints.any { it.identifier == "admin" || it.identifier == "config" || it.identifier == "stats" }) { + throw KalkulierbarException( + "Set of active calculi contains forbidden identifiers \"admin\", \"config\" or \"stats\"" + ) + } // Pass list of available calculi to StateKeeper StateKeeper.importAvailable(endpoints.map { it.identifier }) @@ -227,10 +234,11 @@ fun createCalculusEndpoints(app: Javalin, calculus: Calculus) { fun getParam(map: Map>, key: String, optional: Boolean = false): String? { val lst = map[key] - if (lst == null && !optional) + if (lst == null && !optional) { throw ApiMisuseException("POST parameter '$key' needs to be present") - else if (lst == null) + } else if (lst == null) { return null + } return lst[0] } diff --git a/backend/src/main/kotlin/kalkulierbar/constants.kt b/backend/src/main/kotlin/kalkulierbar/Constants.kt similarity index 100% rename from backend/src/main/kotlin/kalkulierbar/constants.kt rename to backend/src/main/kotlin/kalkulierbar/Constants.kt diff --git a/backend/src/main/kotlin/kalkulierbar/exceptions.kt b/backend/src/main/kotlin/kalkulierbar/Exceptions.kt similarity index 100% rename from backend/src/main/kotlin/kalkulierbar/exceptions.kt rename to backend/src/main/kotlin/kalkulierbar/Exceptions.kt diff --git a/backend/src/main/kotlin/kalkulierbar/JSONCalculus.kt b/backend/src/main/kotlin/kalkulierbar/JSONCalculus.kt index 1df68d0dc..58811967a 100644 --- a/backend/src/main/kotlin/kalkulierbar/JSONCalculus.kt +++ b/backend/src/main/kotlin/kalkulierbar/JSONCalculus.kt @@ -43,7 +43,7 @@ abstract class JSONCalculus : Calculus { /** * Takes a state and evaluates whether it is valid * @param state The current state - * @return Whether or not it is valid + * @return Whether it is valid */ open fun validateOnState(state: State): Boolean { return true @@ -96,9 +96,9 @@ abstract class JSONCalculus : Calculus { val parsed: State = serializer.decodeFromString(stateSerializer, json) // Ensure valid, unmodified state object - if (parsed is ProtectedState && !parsed.verifySeal()) + if (parsed is ProtectedState && !parsed.verifySeal()) { throw JsonParseException("Invalid tamper protection seal, state object appears to have been modified") - + } return parsed } catch (e: Exception) { val msg = "Could not parse JSON state: " @@ -112,8 +112,9 @@ abstract class JSONCalculus : Calculus { * @return JSON state representation */ open fun stateToJson(state: State): String { - if (state is ProtectedState) + if (state is ProtectedState) { state.computeSeal() + } return serializer.encodeToString(stateSerializer, state) } diff --git a/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt b/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt index 61cced3f3..a1d188478 100644 --- a/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt +++ b/backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt @@ -26,8 +26,9 @@ abstract class ScoredCalculus : JSONCalculus { val state = jsonToState(json) - if (!checkCloseOnState(state).closed) + if (!checkCloseOnState(state).closed) { throw IllegalMove("Cannot get score for unclosed proof") + } return scoreFromState(state, name) } diff --git a/backend/src/main/kotlin/kalkulierbar/clause/Atom.kt b/backend/src/main/kotlin/kalkulierbar/clause/Atom.kt index 941761343..383788661 100644 --- a/backend/src/main/kotlin/kalkulierbar/clause/Atom.kt +++ b/backend/src/main/kotlin/kalkulierbar/clause/Atom.kt @@ -16,21 +16,23 @@ data class Atom(val lit: AtomType, val negated: Boolean = false) : Syn if (other is Atom<*> && other.negated == negated) { // Use syntactic equality for literal comparison if defined - eq = if (lit is SyntacticEquality) + eq = if (lit is SyntacticEquality) { lit.synEq(other.lit) - else - (lit == other.lit) + } else { + lit == other.lit + } } return eq } override fun clone(): Atom { - return if (lit is SyntacticEquality) + return if (lit is SyntacticEquality) { @Suppress("UNCHECKED_CAST") Atom(lit.clone() as AtomType, negated) - else + } else { Atom(lit, negated) + } } /** diff --git a/backend/src/main/kotlin/kalkulierbar/clause/ClauseSet.kt b/backend/src/main/kotlin/kalkulierbar/clause/ClauseSet.kt index a02889822..8deaa706f 100644 --- a/backend/src/main/kotlin/kalkulierbar/clause/ClauseSet.kt +++ b/backend/src/main/kotlin/kalkulierbar/clause/ClauseSet.kt @@ -10,8 +10,9 @@ class ClauseSet(var clauses: MutableList> = mutableLi fun addAll(c: Collection>) { c.forEach { - if (!clauses.contains(it)) + if (!clauses.contains(it)) { add(it) + } } } diff --git a/backend/src/main/kotlin/kalkulierbar/dpll/BasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/dpll/BasicMoves.kt index 30608eb14..2fc98f331 100644 --- a/backend/src/main/kotlin/kalkulierbar/dpll/BasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/dpll/BasicMoves.kt @@ -60,30 +60,37 @@ fun propagate(state: DPLLState, branchID: Int, baseID: Int, propID: Int, atomID: @Suppress("ThrowsCount", "ComplexMethod") private fun checkPropagateRestrictions(state: DPLLState, branchID: Int, baseID: Int, propID: Int, atomID: Int) { // Check branch validity - if (branchID < 0 || branchID >= state.tree.size) + if (branchID < 0 || branchID >= state.tree.size) { throw IllegalMove("Branch with ID $branchID does not exist") + } val branch = state.tree[branchID] - if (!branch.isLeaf) + if (!branch.isLeaf) { throw IllegalMove("ID $branchID does not reference a leaf") - if (branch.isAnnotation) + } + if (branch.isAnnotation) { throw IllegalMove("Cannot propagate on annotation '$branch'") + } val clauseSet = state.getClauseSet(branchID) val clauses = clauseSet.clauses // Check baseID, propID, atomID validity - if (baseID < 0 || baseID >= clauses.size) + if (baseID < 0 || baseID >= clauses.size) { throw IllegalMove("Clause set $clauses has no clause with ID $baseID") - if (propID < 0 || propID >= clauses.size) + } + if (propID < 0 || propID >= clauses.size) { throw IllegalMove("Clause set $clauses has no clause with ID $propID") - if (atomID < 0 || atomID >= clauses[propID].size) + } + if (atomID < 0 || atomID >= clauses[propID].size) { throw IllegalMove("Clause ${clauses[propID]} has no atom with ID $atomID") - if (baseID == propID) + } + if (baseID == propID) { throw IllegalMove("Base and propagation clauses have to be different") - + } val base = clauses[baseID] - if (base.size != 1) + if (base.size != 1) { throw IllegalMove("Base clause $base may only have exactly one atom") + } } /** @@ -115,24 +122,26 @@ fun split(state: DPLLState, branchID: Int, literal: String) { @Suppress("ThrowsCount") private fun checkSplitRestrictions(state: DPLLState, branchID: Int, literal: String) { - if (branchID < 0 || branchID >= state.tree.size) + if (branchID < 0 || branchID >= state.tree.size) { throw IllegalMove("Branch with ID $branchID does not exist") - + } val branch = state.tree[branchID] - if (!branch.isLeaf) + if (!branch.isLeaf) { throw IllegalMove("ID $branchID does not reference a leaf") - if (branch.isAnnotation) + } + if (branch.isAnnotation) { throw IllegalMove("Cannot split on annotation '$branch'") - + } val tokenized = Tokenizer.tokenize(literal) - if (tokenized.size != 1) + if (tokenized.size != 1) { throw IllegalMove("Invalid variable name '$literal'") - + } val varToken = tokenized[0] - if (varToken.type != TokenType.CAPID && varToken.type != TokenType.LOWERID) + if (varToken.type != TokenType.CAPID && varToken.type != TokenType.LOWERID) { throw IllegalMove("Invalid variable name '$literal'") + } } /** @@ -143,15 +152,15 @@ private fun checkSplitRestrictions(state: DPLLState, branchID: Int, literal: Str * @branchID ID of the node whose children will be pruned */ fun prune(state: DPLLState, branchID: Int) { - if (branchID < 0 || branchID >= state.tree.size) + if (branchID < 0 || branchID >= state.tree.size) { throw IllegalMove("Branch with ID $branchID does not exist") - + } val node = state.tree[branchID] // Weird things would happen if we would allow removing annotations - if (node.children.size == 1 && state.tree[node.children[0]].isAnnotation) + if (node.children.size == 1 && state.tree[node.children[0]].isAnnotation) { throw IllegalMove("Cannot prune annotation '${state.tree[node.children[0]]}'") - + } state.pruneBranch(branchID) } @@ -163,25 +172,26 @@ fun prune(state: DPLLState, branchID: Int) { */ @Suppress("ThrowsCount") fun checkModel(state: DPLLState, branchID: Int, interpretation: Map) { - if (branchID < 0 || branchID >= state.tree.size) + if (branchID < 0 || branchID >= state.tree.size) { throw IllegalMove("Branch with ID $branchID does not exist") - + } val branch = state.tree[branchID] - if (branch.type != NodeType.MODEL) + if (branch.type != NodeType.MODEL) { throw IllegalMove("Node '$branch' is not a model node") - - if (branch.modelVerified == true) + } + if (branch.modelVerified == true) { throw IllegalMove("This node has already been checked") - + } val clauseSet = state.getClauseSet(branchID) // Check that the mapping satisfies every clause clauseSet.clauses.forEach { clause -> // Check if any atom in the clause is satisfied by the interpretation // (-> the atom's negated value is the opposite of the interp. truth value) - if (!clause.atoms.any { !it.negated == interpretation[it.lit] }) + if (!clause.atoms.any { !it.negated == interpretation[it.lit] }) { throw IllegalMove("The given interpretation does not satisfy any atom of clause $clause") + } } branch.modelVerified = true diff --git a/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt b/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt index 6b5b383ab..58e653cf1 100644 --- a/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt +++ b/backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt @@ -41,9 +41,9 @@ class DPLL : JSONCalculus() { // (-> every proper leaf is either closed or has a model) val done = state.tree.all { !it.isLeaf || it.isAnnotation } - val msg = if (closed) + val msg = if (closed) { "The proof is closed and proves the unsatisfiability of the clause set" - else { + } else { val donemsg = if (done) "- however, all branches are completed. The clause set is satisfiable." else "yet." "The proof is not closed $donemsg" } diff --git a/backend/src/main/kotlin/kalkulierbar/logic/abstractLogic.kt b/backend/src/main/kotlin/kalkulierbar/logic/AbstractLogic.kt similarity index 92% rename from backend/src/main/kotlin/kalkulierbar/logic/abstractLogic.kt rename to backend/src/main/kotlin/kalkulierbar/logic/AbstractLogic.kt index 767b8013b..26dc63231 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/abstractLogic.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/AbstractLogic.kt @@ -56,8 +56,9 @@ abstract class UnaryOp : LogicNode() { } override fun synEq(other: Any?): Boolean { - if (other == null || other !is UnaryOp) + if (other == null || other !is UnaryOp) { return false + } return this.child.synEq(other.child) } @@ -69,18 +70,22 @@ abstract class Quantifier : UnaryOp() { @Suppress("ReturnCount") override fun synEq(other: Any?): Boolean { - if (other == null || other !is Quantifier) + if (other == null || other !is Quantifier) { return false + } - if (this.varName != other.varName) + if (this.varName != other.varName) { return false + } - if (this.boundVariables.size != other.boundVariables.size) + if (this.boundVariables.size != other.boundVariables.size) { return false + } for (i in this.boundVariables.indices) { - if (!this.boundVariables[i].synEq(other.boundVariables[i])) + if (!this.boundVariables[i].synEq(other.boundVariables[i])) { return false + } } return true } diff --git a/backend/src/main/kotlin/kalkulierbar/logic/FirstOrderTerm.kt b/backend/src/main/kotlin/kalkulierbar/logic/FirstOrderTerm.kt index b91dd8c46..49e746ff0 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/FirstOrderTerm.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/FirstOrderTerm.kt @@ -41,15 +41,17 @@ class QuantifiedVariable(var spelling: String) : FirstOrderTerm() { val newVar = QuantifiedVariable(spelling) // Register the new variable with a binding quantifier, should one exist - if (qm[spelling] != null) + if (qm[spelling] != null) { qm[spelling]!!.boundVariables.add(newVar) + } return newVar } override fun synEq(other: Any?): Boolean { - if (other == null || other !is QuantifiedVariable) + if (other == null || other !is QuantifiedVariable) { return false + } return spelling == other.spelling } @@ -63,8 +65,9 @@ class Constant(val spelling: String) : FirstOrderTerm() { override fun clone(qm: Map) = Constant(spelling) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Constant) + if (other == null || other !is Constant) { return false + } return spelling == other.spelling } @@ -79,15 +82,18 @@ class Function(val spelling: String, var arguments: List) : Firs @Suppress("ReturnCount") override fun synEq(other: Any?): Boolean { - if (other == null || other !is Function) + if (other == null || other !is Function) { return false + } - if (spelling != other.spelling || arguments.size != other.arguments.size) + if (spelling != other.spelling || arguments.size != other.arguments.size) { return false + } for (i in arguments.indices) { - if (!arguments[i].synEq(other.arguments[i])) + if (!arguments[i].synEq(other.arguments[i])) { return false + } } return true diff --git a/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt b/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt index cb7b055d8..a402cd24c 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt @@ -15,8 +15,9 @@ class Var(var spelling: String) : LogicNode() { override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Var) + if (other == null || other !is Var) { return false + } return this.spelling == other.spelling } @@ -33,8 +34,9 @@ class Not(override var child: LogicNode) : UnaryOp() { override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Not) + if (other == null || other !is Not) { return false + } return this.child.synEq(other.child) } @@ -51,8 +53,9 @@ class And(override var leftChild: LogicNode, override var rightChild: LogicNode) override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is And) + if (other == null || other !is And) { return false + } return this.leftChild.synEq(other.leftChild) && this.rightChild.synEq(other.rightChild) } @@ -69,8 +72,9 @@ class Or(override var leftChild: LogicNode, override var rightChild: LogicNode) override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Or) + if (other == null || other !is Or) { return false + } return this.leftChild.synEq(other.leftChild) && this.rightChild.synEq(other.rightChild) } @@ -87,8 +91,9 @@ class Impl(override var leftChild: LogicNode, override var rightChild: LogicNode override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Impl) + if (other == null || other !is Impl) { return false + } return this.leftChild.synEq(other.leftChild) && this.rightChild.synEq(other.rightChild) } @@ -105,8 +110,9 @@ class Equiv(override var leftChild: LogicNode, override var rightChild: LogicNod override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Equiv) + if (other == null || other !is Equiv) { return false + } return this.leftChild.synEq(other.leftChild) && this.rightChild.synEq(other.rightChild) } @@ -135,15 +141,18 @@ class Relation(val spelling: String, var arguments: List) : Synt */ @Suppress("ReturnCount") override fun synEq(other: Any?): Boolean { - if (other == null || other !is Relation) + if (other == null || other !is Relation) { return false + } - if (spelling != other.spelling || arguments.size != other.arguments.size) + if (spelling != other.spelling || arguments.size != other.arguments.size) { return false + } for (i in arguments.indices) { - if (!arguments[i].synEq(other.arguments[i])) + if (!arguments[i].synEq(other.arguments[i])) { return false + } } return true @@ -176,21 +185,26 @@ class UniversalQuantifier( @Suppress("ReturnCount") override fun synEq(other: Any?): Boolean { - if (other == null || other !is UniversalQuantifier) + if (other == null || other !is UniversalQuantifier) { return false + } - if (this.varName != other.varName) + if (this.varName != other.varName) { return false + } - if (!this.child.synEq(other.child)) + if (!this.child.synEq(other.child)) { return false + } - if (this.boundVariables.size != other.boundVariables.size) + if (this.boundVariables.size != other.boundVariables.size) { return false + } for (i in this.boundVariables.indices) { - if (!this.boundVariables[i].synEq(other.boundVariables[i])) + if (!this.boundVariables[i].synEq(other.boundVariables[i])) { return false + } } return true } @@ -222,21 +236,26 @@ class ExistentialQuantifier( @Suppress("ReturnCount") override fun synEq(other: Any?): Boolean { - if (other == null || other !is ExistentialQuantifier) + if (other == null || other !is ExistentialQuantifier) { return false + } - if (this.varName != other.varName) + if (this.varName != other.varName) { return false + } - if (!this.child.synEq(other.child)) + if (!this.child.synEq(other.child)) { return false + } - if (this.boundVariables.size != other.boundVariables.size) + if (this.boundVariables.size != other.boundVariables.size) { return false + } for (i in this.boundVariables.indices) { - if (!this.boundVariables[i].synEq(other.boundVariables[i])) + if (!this.boundVariables[i].synEq(other.boundVariables[i])) { return false + } } return true } @@ -253,8 +272,9 @@ class Box(override var child: LogicNode) : UnaryOp() { override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Box) + if (other == null || other !is Box) { return false + } return this.child.synEq(other.child) } @@ -271,8 +291,9 @@ class Diamond(override var child: LogicNode) : UnaryOp() { override fun accept(visitor: LogicNodeVisitor) = visitor.visit(this) override fun synEq(other: Any?): Boolean { - if (other == null || other !is Diamond) + if (other == null || other !is Diamond) { return false + } return this.child.synEq(other.child) } diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt index d639c1fe2..411c29024 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt @@ -1,7 +1,12 @@ package kalkulierbar.logic.transform -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier import kalkulierbar.logic.Function +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier /** * Collects free variables in a logic-node formula structure @@ -58,9 +63,11 @@ class FreeVariableTermCollector( override fun visit(node: QuantifiedVariable): Set { // return node if free - return if (boundVariables.contains(node)) + return if (boundVariables.contains(node)) { mutableSetOf() - else mutableSetOf(node) + } else { + mutableSetOf(node) + } } override fun visit(node: Function): Set { diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/DoNothingCollector.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/DoNothingCollector.kt index 326e4a678..6dafe5069 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/DoNothingCollector.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/DoNothingCollector.kt @@ -1,6 +1,14 @@ package kalkulierbar.logic.transform -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.Equiv +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.Impl +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier +import kalkulierbar.logic.Var /** * Implements a default visitor recursively visiting an entire formula. diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/FirstOrderCNF.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/FirstOrderCNF.kt index 12d6ab810..eff0e266f 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/FirstOrderCNF.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/FirstOrderCNF.kt @@ -5,7 +5,12 @@ import kalkulierbar.FormulaConversionException import kalkulierbar.clause.Atom import kalkulierbar.clause.Clause import kalkulierbar.clause.ClauseSet -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier /** * Visitor-based implementation of a first order CNF transformation @@ -91,9 +96,9 @@ class FirstOrderCNF : LogicNodeVisitor>() { // Not limiting resulting clause amount causes server to run out of memory attempting conversion // Don't mess with exponential growth - if (leftClauses.size * rightClauses.size > CNF_BLOWUP_LIMIT) + if (leftClauses.size * rightClauses.size > CNF_BLOWUP_LIMIT) { throw FormulaConversionException("First order CNF transformation resulted in too heavy blow-up") - + } for (lc in leftClauses) { for (rc in rightClauses) { val atoms = mutableListOf>() diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/NaiveCNF.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/NaiveCNF.kt index 83cc3acc8..bc479136e 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/NaiveCNF.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/NaiveCNF.kt @@ -5,7 +5,13 @@ import kalkulierbar.FormulaConversionException import kalkulierbar.clause.Atom import kalkulierbar.clause.Clause import kalkulierbar.clause.ClauseSet -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.Equiv +import kalkulierbar.logic.Impl +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or +import kalkulierbar.logic.Var /** * Visitor-based implementation of the naive CNF transformation @@ -109,9 +115,9 @@ class NaiveCNF : LogicNodeVisitor>() { // Not limiting resulting clause amount causes server to run out of memory attempting conversion // Don't mess with exponential growth - if (leftClauses.size * rightClauses.size > CNF_BLOWUP_LIMIT) + if (leftClauses.size * rightClauses.size > CNF_BLOWUP_LIMIT) { throw FormulaConversionException("Naive CNF transformation resulted in too heavy blow-up") - + } for (lc in leftClauses) { for (rc in rightClauses) { val atoms = mutableListOf>() diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt index 403bc2efe..2c46417ad 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt @@ -32,10 +32,11 @@ class PrenexNormalForm : DoNothingVisitor() { // re-create quantifier prefix from saved data instance.quantifiers.asReversed().forEach { val (varName, isUniversal, boundVars) = it - res = if (isUniversal) + res = if (isUniversal) { UniversalQuantifier(varName, res, boundVars) - else + } else { ExistentialQuantifier(varName, res, boundVars) + } } return res @@ -53,11 +54,12 @@ class PrenexNormalForm : DoNothingVisitor() { */ override fun visit(node: UniversalQuantifier): LogicNode { - if (encounteredVars.contains(node.varName)) + if (encounteredVars.contains(node.varName)) { throw FormulaConversionException( "Prenex Normal Form conversion encountered " + "double-binding of variable '${node.varName}'" ) + } quantifiers.add(Triple(node.varName, true, node.boundVariables)) encounteredVars.add(node.varName) @@ -73,11 +75,12 @@ class PrenexNormalForm : DoNothingVisitor() { */ override fun visit(node: ExistentialQuantifier): LogicNode { - if (encounteredVars.contains(node.varName)) + if (encounteredVars.contains(node.varName)) { throw FormulaConversionException( "Prenex Normal Form conversion encountered " + " double-binding of variable '${node.varName}'" ) + } quantifiers.add(Triple(node.varName, false, node.boundVariables)) encounteredVars.add(node.varName) diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt index 83cc87c23..1e92f1b25 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt @@ -3,8 +3,14 @@ package kalkulierbar.logic.transform import kalkulierbar.IncorrectArityException import kalkulierbar.UnknownFunctionException import kalkulierbar.clause.ClauseSet -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.FirstOrderTerm import kalkulierbar.logic.Function +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier data class CompoundSignature(val name: String, val arity: Int) { override fun toString(): String { @@ -207,6 +213,7 @@ class SignatureAdherenceChecker( } } + @Suppress("EmptyFunctionBlock") override fun visit(node: QuantifiedVariable) {} override fun visit(node: Function) { diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt index c54d576cd..a719f1bc0 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt @@ -1,8 +1,14 @@ package kalkulierbar.logic.transform import kalkulierbar.FormulaConversionException -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.FirstOrderTerm import kalkulierbar.logic.Function +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier /** * Visitor-based Skolemization transformation @@ -58,11 +64,12 @@ class Skolemization(private val signature: Signature) : DoNothingVisitor() { */ override fun visit(node: ExistentialQuantifier): LogicNode { - if (quantifierScope.size > quantifierScope.distinctBy { it.varName }.size) + if (quantifierScope.size > quantifierScope.distinctBy { it.varName }.size) { throw FormulaConversionException( "Double-bound universally quantified variable encountered " + "during Skolemization" ) + } val term = getSkolemTerm() @@ -99,8 +106,9 @@ class Skolemization(private val signature: Signature) : DoNothingVisitor() { skolemName = "sk$skolemCounter" } - if (quantifierScope.size == 0) + if (quantifierScope.size == 0) { return Constant(skolemName) + } val argList = mutableListOf() diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt index 7357bd6a3..ff4839fc2 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt @@ -1,10 +1,15 @@ package kalkulierbar.logic.transform import kalkulierbar.FormulaConversionException -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.FirstOrderTerm import kalkulierbar.logic.Function +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Quantifier -class VariableInstantiator(private val replacementMap: Map) : FirstOrderTermVisitor() { +class VariableInstantiator( + private val replacementMap: Map +) : FirstOrderTermVisitor() { companion object { /** @@ -165,7 +170,10 @@ class TermContainsVariable(val variable: String) : FirstOrderTermVisitor, private val enforceUnique: Boolean) : FirstOrderTermVisitor() { +class QuantifierLinker( + private val quantifiers: List, + private val enforceUnique: Boolean +) : FirstOrderTermVisitor() { /** * Match a QuantifiedVariable to its binding quantifier @@ -174,16 +182,17 @@ class QuantifierLinker(private val quantifiers: List, private val en override fun visit(node: QuantifiedVariable) { val matchingQuantifiers = quantifiers.filter { it.varName == node.spelling } - if (matchingQuantifiers.isEmpty()) + if (matchingQuantifiers.isEmpty()) { throw FormulaConversionException( "Error linking variables to quantifiers: " + "Variable '${node.spelling}' is not bound by any quantifier" ) - else if (matchingQuantifiers.size > 1 && enforceUnique) + } else if (matchingQuantifiers.size > 1 && enforceUnique) { throw FormulaConversionException( "Error linking variables to quantifiers: " + "Variable '${node.spelling}' is bound by more than one quantifier" ) + } // The last-defined quantifier is the binding one for the variable occurrence matchingQuantifiers[matchingQuantifiers.size - 1].boundVariables.add(node) diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/TseytinCNF.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/TseytinCNF.kt index 4e1ae4fd9..7aacc486e 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/TseytinCNF.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/TseytinCNF.kt @@ -4,7 +4,13 @@ import kalkulierbar.FormulaConversionException import kalkulierbar.clause.Atom import kalkulierbar.clause.Clause import kalkulierbar.clause.ClauseSet -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.Equiv +import kalkulierbar.logic.Impl +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or +import kalkulierbar.logic.Var /** * Recursively applies Tseytin transformation on a logic node diff --git a/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt b/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt index 39c70a15e..00fa19f6d 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt @@ -1,8 +1,13 @@ package kalkulierbar.logic.transform import kalkulierbar.FormulaConversionException -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier import kalkulierbar.logic.Function +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier /** * Visitor-based variable renaming transformation @@ -105,7 +110,7 @@ class UniqueVariables : DoNothingVisitor() { /** * FirstOrderTerm visitor to re-name variables * @param replacementMap Map of all variables to replace and their new variable name - * @param strict Set to false to allow variables with no associated replacement + * @param strict Set to false in order to allow variables with no associated replacement */ class VariableRenamer( private val replacementMap: Map, @@ -117,10 +122,11 @@ class VariableRenamer( * @param node: QuantifiedVariable encountered */ override fun visit(node: QuantifiedVariable) { - if (replacementMap[node] != null) + if (replacementMap[node] != null) { node.spelling = replacementMap[node]!! - else if (strict) + } else if (strict) { throw FormulaConversionException("Encountered QuantifiedVariable with no disambiguation replacement: $node") + } } @Suppress("EmptyFunctionBlock") diff --git a/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt b/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt index 378c45cdf..ab6685231 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt @@ -38,17 +38,22 @@ class Unification { return unifyTerms(terms) } - private fun findTermsToUnify(terms: MutableList>, r1: Relation, r2: Relation) { + private fun findTermsToUnify( + terms: MutableList>, + r1: Relation, + r2: Relation + ) { val arg1 = r1.arguments val arg2 = r2.arguments // Spelling has to be the same - if (r1.spelling != r2.spelling) + if (r1.spelling != r2.spelling) { throw UnificationImpossible("Relations '$r1' and '$r2' have different names") + } // Arg size has to be the same length - if (arg1.size != arg2.size) + if (arg1.size != arg2.size) { throw UnificationImpossible("Relations '$r1' and '$r2' have different numbers of arguments") - + } for (i in arg1.indices) terms.add(Pair(arg1[i], arg2[i])) } @@ -76,9 +81,9 @@ class Unification { continue } else if (term1 is QuantifiedVariable) { // Unification not possible if one is variable and appears in others arguments - if (term2 is Function && TermContainsVariable.check(term2, term1.spelling)) + if (term2 is Function && TermContainsVariable.check(term2, term1.spelling)) { throw UnificationImpossible("Variable '$term1' appears in '$term2'") - + } // Update the right side of all substitutions map.mapValuesTo(map) { VariableInstantiator.transform(it.value, mapOf(term1.spelling to term2)) @@ -109,9 +114,9 @@ class Unification { * @return true iff the two terms represent the same functions */ private fun isCompatibleFunction(t1: FirstOrderTerm, t2: FirstOrderTerm): Boolean { - if (t1 is Function && t2 is Function) + if (t1 is Function && t2 is Function) { return t1.spelling == t2.spelling && t1.arguments.size == t2.arguments.size - + } return false } } diff --git a/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt b/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt index 32a9ef75f..a18e5745e 100644 --- a/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt +++ b/backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt @@ -1,8 +1,11 @@ package kalkulierbar.logic.util import kalkulierbar.UnificationImpossible -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.FirstOrderTerm import kalkulierbar.logic.Function +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation import kalkulierbar.logic.transform.FirstOrderTermVisitor class UnifierEquivalence { diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt index 854b08cd5..230874ced 100644 --- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt @@ -2,7 +2,14 @@ package kalkulierbar.nonclausaltableaux import kalkulierbar.IllegalMove import kalkulierbar.UnificationImpossible -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.FirstOrderTerm +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier import kalkulierbar.logic.transform.LogicNodeVariableInstantiator import kalkulierbar.logic.transform.SelectiveSuffixAppender import kalkulierbar.logic.transform.Signature @@ -12,7 +19,7 @@ import kalkulierbar.logic.util.UnifierEquivalence /** * While the outermost LogicNode is an AND: * Split into subformulae, chain onto a single branch - * @param state: Non clausal tableaux state to apply move on + * @param state: Non-clausal tableaux state to apply move on * @param nodeID: node ID to apply move on * @return new state after applying move */ @@ -24,9 +31,9 @@ fun applyAlpha(state: NcTableauxState, nodeID: Int): NcTableauxState { val savedChildren = node.children.toMutableList() // Save a copy of the node's children node.children.clear() // We will insert new nodes between the node and its children - if (node.formula !is And) + if (node.formula !is And) { throw IllegalMove("Outermost logic operator is not AND") - + } val workList = mutableListOf(node.formula) var parentID = nodeID @@ -46,8 +53,9 @@ fun applyAlpha(state: NcTableauxState, nodeID: Int): NcTableauxState { nodes[parentID].children.addAll(savedChildren) state.setParent(savedChildren, nodes.size - 1) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(AlphaMove(nodeID)) + } return state } @@ -62,9 +70,9 @@ fun applyBeta(state: NcTableauxState, nodeID: Int): NcTableauxState { checkNodeRestrictions(state, nodeID) val node = state.tree[nodeID] - if (node.formula !is Or) + if (node.formula !is Or) { throw IllegalMove("Outermost logic operator is not OR") - + } // Collect all leaves in the current branch where the split nodes // will have to be appended // If the node is a leaf, this will only be the nodeID @@ -87,8 +95,9 @@ fun applyBeta(state: NcTableauxState, nodeID: Int): NcTableauxState { } // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(BetaMove(nodeID)) + } return state } @@ -108,9 +117,9 @@ fun applyGamma(state: NcTableauxState, nodeID: Int): NcTableauxState { // Which cannot be recovered from deserialization val formula = node.formula.clone() - if (formula !is UniversalQuantifier) + if (formula !is UniversalQuantifier) { throw IllegalMove("Outermost logic operator is not a universal quantifier") - + } // Prepare the selected node for insertion of new nodes val savedChildren = node.children.toMutableList() node.children.clear() @@ -135,8 +144,9 @@ fun applyGamma(state: NcTableauxState, nodeID: Int): NcTableauxState { state.setParent(savedChildren, nodes.size - 1) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(GammaMove(nodeID)) + } return state } @@ -159,9 +169,9 @@ fun applyDelta(state: NcTableauxState, nodeID: Int): NcTableauxState { val formula = node.formula.clone() // Check node == UniversalQuantifier - if (formula !is ExistentialQuantifier) + if (formula !is ExistentialQuantifier) { throw IllegalMove("The outermost logic operator is not an existential quantifier") - + } // Prepare the selected node for insertion of new nodes val savedChildren = node.children.toMutableList() node.children.clear() @@ -178,8 +188,9 @@ fun applyDelta(state: NcTableauxState, nodeID: Int): NcTableauxState { state.setParent(savedChildren, nodes.size - 1) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(DeltaMove(nodeID)) + } return state } @@ -219,9 +230,9 @@ fun applyClose( throw IllegalMove("Cannot unify '$nodeRelation' and '$closeRelation': ${e.message}") } - if (!UnifierEquivalence.isMGUorNotUnifiable(unifier, nodeRelation, closeRelation)) + if (!UnifierEquivalence.isMGUorNotUnifiable(unifier, nodeRelation, closeRelation)) { state.statusMessage = "The unifier you specified is not an MGU" - + } // Apply all specified variable instantiations globally val instantiator = LogicNodeVariableInstantiator(unifier) state.tree.forEach { @@ -229,11 +240,12 @@ fun applyClose( } // Check relations after instantiation - if (!nodeRelation.synEq(closeRelation)) + if (!nodeRelation.synEq(closeRelation)) { throw IllegalMove( "Relations '$nodeRelation' and '$closeRelation' are" + " not equal after variable instantiation" ) + } // Close branch node.closeRef = closeID @@ -259,8 +271,9 @@ private fun checkCloseIDRestrictions(state: NcTableauxState, nodeID: Int, closeI val node = state.tree[nodeID] val closeNode = state.tree[closeID] // Verify that closeNode is transitive parent of node - if (!state.nodeIsParentOf(closeID, nodeID)) + if (!state.nodeIsParentOf(closeID, nodeID)) { throw IllegalMove("Node '$closeNode' is not an ancestor of node '$node'") + } } /** @@ -271,18 +284,22 @@ private fun checkCloseIDRestrictions(state: NcTableauxState, nodeID: Int, closeI private fun checkCloseRelation(nodeFormula: LogicNode, closeNodeFormula: LogicNode): Pair { when { nodeFormula is Not -> { - if (nodeFormula.child !is Relation) + if (nodeFormula.child !is Relation) { throw IllegalMove("Node formula '$nodeFormula' is not a negated relation") - if (closeNodeFormula !is Relation) + } + if (closeNodeFormula !is Relation) { throw IllegalMove("Close node formula '$closeNodeFormula' has to be a positive relation") + } val nodeRelation = nodeFormula.child as Relation return Pair(nodeRelation, closeNodeFormula) } closeNodeFormula is Not -> { - if (closeNodeFormula.child !is Relation) + if (closeNodeFormula.child !is Relation) { throw IllegalMove("Close node formula '$closeNodeFormula' is not a negated relation") - if (nodeFormula !is Relation) + } + if (nodeFormula !is Relation) { throw IllegalMove("Node formula '$nodeFormula' has to be a positive relation") + } val closeRelation = closeNodeFormula.child as Relation return Pair(nodeFormula, closeRelation) } @@ -299,6 +316,7 @@ fun checkNodeRestrictions(state: NcTableauxState, nodeID: Int) { state.checkNodeID(nodeID) // Verify that node is not already closed val node = state.tree[nodeID] - if (node.isClosed) + if (node.isClosed) { throw IllegalMove("Node '$node' is already closed") + } } diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt index 7b2efd5e6..e6d37d83e 100644 --- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt +++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt @@ -1,7 +1,12 @@ package kalkulierbar.nonclausaltableaux -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.FirstOrderTerm import kalkulierbar.logic.Function +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation import kalkulierbar.logic.transform.DoNothingVisitor import kalkulierbar.logic.transform.FirstOrderTermVisitor import kalkulierbar.logic.transform.FreeVariableCollector @@ -60,9 +65,9 @@ class DeltaSkolemization( nameBlacklist.add(skolemName) // Constant iff no free vars - if (freeVariables.isEmpty()) + if (freeVariables.isEmpty()) { return Constant(skolemName) - + } // Create skolem term with free variables val argList = mutableListOf() freeVariables.forEach { diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt index 310d2ee10..5a0492b6c 100644 --- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt +++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt @@ -62,8 +62,9 @@ class CloseMove( * parsed map-values iff varAssign != null */ fun getVarAssignTerms(): Map? { - if (varAssign == null) + if (varAssign == null) { return null + } return varAssign.mapValues { try { FirstOrderParser.parseTerm(it.value) diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableaux.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableaux.kt index 87f84b57a..8f843b9fe 100644 --- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableaux.kt +++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableaux.kt @@ -12,7 +12,10 @@ import kotlinx.serialization.modules.plus class NonClausalTableaux : JSONCalculus() { - override val serializer = Json { serializersModule = FoTermModule + LogicModule + NcMoveModule; encodeDefaults = true } + override val serializer = Json { + serializersModule = FoTermModule + LogicModule + NcMoveModule + encodeDefaults = true + } override val stateSerializer = NcTableauxState.serializer() override val moveSerializer = NcTableauxMove.serializer() @@ -45,13 +48,13 @@ class NonClausalTableaux : JSONCalculus() * @return Equivalent state with the most recent rule application removed */ private fun applyUndo(state: NcTableauxState): NcTableauxState { - if (!state.backtracking) + if (!state.backtracking) { throw IllegalMove("Backtracking is not enabled for this proof") - + } // Can't undo any more moves in initial state - if (state.moveHistory.isEmpty()) + if (state.moveHistory.isEmpty()) { return state - + } // Create a fresh clone-state with the same parameters and input formula var freshState = NcTableauxState(state.formula) freshState.usedBacktracking = true diff --git a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt index 9a9c377b3..39928caa0 100644 --- a/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt +++ b/backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt @@ -33,8 +33,10 @@ class NcTableauxState( // Set isClosed to true for all nodes dominated by node in reverse tree while (node == tree[nodeID] || node.children.fold(true) { acc, e -> acc && tree[e].isClosed }) { node.isClosed = true - if (node.parent == null) + if (node.parent == null) { break + } + node = tree[node.parent!!] } diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt index d9e60976f..e9d56ebd2 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt @@ -46,11 +46,12 @@ object ClauseSetParser { val atomRegex = "($nSig)?[a-zA-Z0-9]+" val formulaFormat = "$atomRegex($aSep$atomRegex)*($cSep$atomRegex($aSep$atomRegex)*)*" - if (!(Regex(formulaFormat) matches pf)) + if (!(Regex(formulaFormat) matches pf)) { throw InvalidFormulaFormat( "Please use alphanumeric variables only, " + "separate atoms with '$atomSeparator' and clauses with '$clauseSeparator'." ) + } val parsed = ClauseSet() val clauses = pf.split(clauseSeparator) @@ -62,11 +63,11 @@ object ClauseSetParser { for (member in members) { // Check if the member variable is negated and set a boolean flag accordingly // true -> positive variable / false -> negated variable - val atom = if (member[0] == negSign) + val atom = if (member[0] == negSign) { Atom(member.substring(1), true) - else + } else { Atom(member) - + } parsedClause.add(atom) } diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt index 93cb437f9..a8e201139 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt @@ -2,14 +2,21 @@ package kalkulierbar.parsers import kalkulierbar.IncorrectArityException import kalkulierbar.InvalidFormulaFormat -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.FirstOrderTerm import kalkulierbar.logic.Function +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.Not +import kalkulierbar.logic.QuantifiedVariable +import kalkulierbar.logic.Relation +import kalkulierbar.logic.UniversalQuantifier /** * Recursive descent parser for first-order logic * For format specification, see docs/FirstOrderFormula.md */ -@Suppress("TooManyFunctions") +@Suppress("TooManyFunctions", "ThrowsCount") class FirstOrderParser : PropositionalParser() { companion object { @@ -64,9 +71,9 @@ class FirstOrderParser : PropositionalParser() { boundVars.clear() relationNames.clear() val res = parseTerm() - if (tokens.isNotEmpty()) + if (tokens.isNotEmpty()) { throw InvalidFormulaFormat("Expected end of term but got ${gotMsg()}") - + } return res } @@ -79,9 +86,9 @@ class FirstOrderParser : PropositionalParser() { tokens = Tokenizer.tokenize(relation) bindQuantifiedVariables = false val res = parseAtomic() - if (tokens.isNotEmpty()) + if (tokens.isNotEmpty()) { throw InvalidFormulaFormat("Expected end of term but got ${gotMsg()}") - + } return res } @@ -93,16 +100,18 @@ class FirstOrderParser : PropositionalParser() { fun parseConstant(constant: String): FirstOrderTerm { tokens = Tokenizer.tokenize(constant, extended = true) // Allow extended identifier chars bindQuantifiedVariables = false - if (!nextTokenIsIdentifier()) + if (!nextTokenIsIdentifier()) { throw InvalidFormulaFormat("Expected identifier but got ${gotMsg()}") - if (!nextTokenIs(TokenType.LOWERID)) + } + if (!nextTokenIs(TokenType.LOWERID)) { throw InvalidFormulaFormat("Expected '${TokenType.LOWERID}' but got ${gotMsg()}") + } // Next token is constant or function val identifier = tokens.first().spelling consume() - if (tokens.isNotEmpty()) + if (tokens.isNotEmpty()) { throw InvalidFormulaFormat("Expected end of constant but got ${gotMsg()}") - + } return Constant(identifier) } @@ -125,15 +134,15 @@ class FirstOrderParser : PropositionalParser() { */ private fun parseQuantifier(): LogicNode { - if (!nextTokenIs(TokenType.UNIVERSALQUANT) && !nextTokenIs(TokenType.EXISTENTIALQUANT)) + if (!nextTokenIs(TokenType.UNIVERSALQUANT) && !nextTokenIs(TokenType.EXISTENTIALQUANT)) { return parseParen() - + } val quantType = tokens.first().type consume() - if (!nextTokenIs(TokenType.CAPID)) + if (!nextTokenIs(TokenType.CAPID)) { throw InvalidFormulaFormat("Expected quantified variable but got ${gotMsg()}") - + } val varName = tokens.first().spelling consume() consume(TokenType.COLON) @@ -152,19 +161,21 @@ class FirstOrderParser : PropositionalParser() { // If not yet bound variables remain in our scope, add them to the next higher scope // If no scope exists, the variables are unbound and the formula is incorrect - if (quantifierScope.size == 0 && boundBefore.isNotEmpty()) + if (quantifierScope.size == 0 && boundBefore.isNotEmpty()) { throw InvalidFormulaFormat("Unbound Variables found: ${boundBefore.joinToString(", ")}") - else if (boundBefore.isNotEmpty()) + } else if (boundBefore.isNotEmpty()) { quantifierScope.last().addAll(boundBefore) - - if (relationNames.contains(varName)) + } + if (relationNames.contains(varName)) { throw InvalidFormulaFormat("Identifier '$varName' is used both as a relation and bound variable") + } boundVars.add(varName) - return if (quantType == TokenType.UNIVERSALQUANT) + return if (quantType == TokenType.UNIVERSALQUANT) { UniversalQuantifier(varName, subexpression, boundVariables) - else + } else { ExistentialQuantifier(varName, subexpression, boundVariables) + } } /** @@ -187,9 +198,9 @@ class FirstOrderParser : PropositionalParser() { * @return LogicNode representing the parsed Relation */ private fun parseAtomic(): Relation { - if (!nextTokenIs(TokenType.CAPID)) + if (!nextTokenIs(TokenType.CAPID)) { throw InvalidFormulaFormat("Expected relation identifier but got ${gotMsg()}") - + } val relationIdentifier = tokens.first().spelling consume() consume(TokenType.LPAREN) @@ -216,8 +227,9 @@ class FirstOrderParser : PropositionalParser() { arities[relationIdentifier] = arguments.size } - if (boundVars.contains(relationIdentifier)) + if (boundVars.contains(relationIdentifier)) { throw InvalidFormulaFormat("Identifier '$relationIdentifier' is used both as a relation and bound variable") + } relationNames.add(relationIdentifier) return Relation(relationIdentifier, arguments) @@ -229,9 +241,9 @@ class FirstOrderParser : PropositionalParser() { * @return FirstOrderTerm representing the parsed term */ private fun parseTerm(): FirstOrderTerm { - if (!nextTokenIsIdentifier()) + if (!nextTokenIsIdentifier()) { throw InvalidFormulaFormat("Expected identifier but got ${gotMsg()}") - + } return if (nextTokenIs(TokenType.CAPID)) { // Next token is quantified variable parseQuantifiedVariable() @@ -239,11 +251,12 @@ class FirstOrderParser : PropositionalParser() { // Next token is constant or function val identifier = tokens.first().spelling consume() - if (nextTokenIs(TokenType.LPAREN)) + if (nextTokenIs(TokenType.LPAREN)) { parseFunction(identifier) - else { - if (functionNames.contains(identifier)) + } else { + if (functionNames.contains(identifier)) { throw InvalidFormulaFormat("Identifier '$identifier' is used both as a function and constant") + } constants.add(identifier) Constant(identifier) } @@ -282,8 +295,9 @@ class FirstOrderParser : PropositionalParser() { arities[identifier] = arguments.size } - if (constants.contains(identifier)) + if (constants.contains(identifier)) { throw InvalidFormulaFormat("Identifier '$identifier' is used both as a function and constant") + } functionNames.add(identifier) return Function(identifier, arguments) @@ -297,14 +311,15 @@ class FirstOrderParser : PropositionalParser() { val res = QuantifiedVariable(tokens.first().spelling) // Add variable to list of bound variables so the binding quantifier is informed of its existence - if (quantifierScope.size == 0 && bindQuantifiedVariables) + if (quantifierScope.size == 0 && bindQuantifiedVariables) { throw InvalidFormulaFormat("Unbound variable ${gotMsg()}") - - if (bindQuantifiedVariables) + } + if (bindQuantifiedVariables) { quantifierScope.last().add(res) - - if (relationNames.contains(res.spelling)) + } + if (relationNames.contains(res.spelling)) { throw InvalidFormulaFormat("Identifier '${res.spelling}' is used both as a relation and bound variable") + } boundVars.add(res.spelling) consume(TokenType.CAPID) diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderSequentParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderSequentParser.kt index 0e077f2db..4f3b607cd 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderSequentParser.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderSequentParser.kt @@ -40,10 +40,11 @@ object FirstOrderSequentParser { try { ChangeEquivalences.transform(FirstOrderParser().parse(formula, inputPosition)) } catch (e: EmptyFormulaException) { - if (i != 0 || rawFormulas.size != 1) + if (i != 0 || rawFormulas.size != 1) { throw InvalidFormulaFormat("Empty formula at char $inputPosition") - else + } else { null + } } } } @@ -59,11 +60,11 @@ object FirstOrderSequentParser { var startOfFormula = 0 for ((index, value) in it.withIndex()) { - if (value == '(') + if (value == '(') { openParentheses += 1 - else if (value == ')') + } else if (value == ')') { openParentheses -= 1 - else if (value == ',' && openParentheses == 0) { + } else if (value == ',' && openParentheses == 0) { foundFormulas.add(str.subSequence(startOfFormula, index).toString()) startOfFormula = index + 1 } diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt index 50206f33f..36b229f9d 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/FlexibleClauseSetParser.kt @@ -25,7 +25,7 @@ object FlexibleClauseSetParser { // Try parsing as Dimacs-Like try { return DimacsLikeParser.parse(formula) - } catch (e: InvalidFormulaFormat) {} // We don't support this officially, so no custom error for invalid dimacs + } catch (_: InvalidFormulaFormat) {} // We don't support this officially, so no custom error for invalid dimacs // Try parsing as ClauseSet try { @@ -40,12 +40,13 @@ object FlexibleClauseSetParser { } catch (e: InvalidFormulaFormat) { // If the input formula is likely intended to be certain input type, only report that error - if (likelyFormula && !likelyClauseSet) + if (likelyFormula && !likelyClauseSet) { errorMsg = "" + } - if (likelyFormula || !likelyClauseSet) + if (likelyFormula || !likelyClauseSet) { errorMsg += "\nParsing as propositional formula failed: ${e.message ?: "unknown error"}" - + } throw InvalidFormulaFormat(errorMsg) } } @@ -75,10 +76,11 @@ object FlexibleClauseSetParser { // Fall back to tseytin if so res = try { val naive = NaiveCNF.transform(formula) - if (naive.clauses.size > tseytin.clauses.size) + if (naive.clauses.size > tseytin.clauses.size) { tseytin - else + } else { naive + } } catch (e: FormulaConversionException) { tseytin } diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalParser.kt index 9c99611e4..a7df7a9fb 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalParser.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalParser.kt @@ -2,7 +2,13 @@ package kalkulierbar.parsers import kalkulierbar.EmptyFormulaException import kalkulierbar.InvalidFormulaFormat -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.Equiv +import kalkulierbar.logic.Impl +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or +import kalkulierbar.logic.Var /** * Recursive descent parser for propositional logic @@ -26,9 +32,9 @@ open class PropositionalParser { throw EmptyFormulaException("Expected a formula but got an empty String") } val res = parseEquiv() - if (tokens.isNotEmpty()) + if (tokens.isNotEmpty()) { throw InvalidFormulaFormat("Expected end of formula but got ${gotMsg()}") - + } return res } @@ -129,9 +135,9 @@ open class PropositionalParser { * @return LogicNode representing the variable */ private fun parseVar(): LogicNode { - if (!nextTokenIsIdentifier()) + if (!nextTokenIsIdentifier()) { throw InvalidFormulaFormat("Expected identifier but got ${gotMsg()}") - + } val exp = Var(tokens.first().spelling) consume() return exp @@ -158,8 +164,9 @@ open class PropositionalParser { * Consume the next token from the token list */ protected fun consume() { - if (tokens.size == 0) + if (tokens.size == 0) { throw InvalidFormulaFormat("Expected token but got end of input") + } tokens.removeAt(0) } @@ -169,14 +176,16 @@ open class PropositionalParser { * @param expectedType expected token type */ protected fun consume(expectedType: TokenType) { - if (!nextTokenIs(expectedType)) + if (!nextTokenIs(expectedType)) { throw InvalidFormulaFormat("Expected '$expectedType' but got ${gotMsg()}") + } consume() } protected fun gotMsg(): String { - if (tokens.size > 0) + if (tokens.size > 0) { return "'${tokens.first()}' at position ${tokens.first().srcPosition}" + } return "end of input" } } diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalSequentParser.kt b/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalSequentParser.kt index 9c0e97284..1a5f6294f 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalSequentParser.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/PropositionalSequentParser.kt @@ -40,10 +40,11 @@ object PropositionalSequentParser { try { ChangeEquivalences.transform(PropositionalParser().parse(formula, inputPosition)) } catch (e: EmptyFormulaException) { - if (i != 0 || rawFormulas.size != 1) + if (i != 0 || rawFormulas.size != 1) { throw InvalidFormulaFormat("Empty formula at char $inputPosition") - else + } else { null + } } } } diff --git a/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt b/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt index 96a8f4c33..761cf9257 100644 --- a/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt +++ b/backend/src/main/kotlin/kalkulierbar/parsers/Tokenizer.kt @@ -48,7 +48,12 @@ class Tokenizer { * @return start offset of the next token */ @Suppress("ComplexMethod", "MagicNumber") - private fun extractToken(formula: String, index: Int, tokens: MutableList, positionInBaseString: Int): Int { + private fun extractToken( + formula: String, + index: Int, + tokens: MutableList, + positionInBaseString: Int + ): Int { var i = index val len = formula.length diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt index 12694e0e1..2fd5e2ac6 100644 --- a/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/resolution/FirstOrderBasicMoves.kt @@ -82,9 +82,9 @@ private fun instantiate( clauseID: Int, varAssign: Map ) { - if (clauseID < 0 || clauseID >= state.clauseSet.clauses.size) + if (clauseID < 0 || clauseID >= state.clauseSet.clauses.size) { throw IllegalMove("There is no clause with id $clauseID") - + } val baseClause = state.clauseSet.clauses[clauseID] val newClause = instantiateReturn(baseClause, varAssign) @@ -140,10 +140,12 @@ fun factorize(state: FoResolutionState, clauseID: Int, atomIDs: List) { val clauses = state.clauseSet.clauses // Verify that clause id is valid - if (clauseID < 0 || clauseID >= clauses.size) + if (clauseID < 0 || clauseID >= clauses.size) { throw IllegalMove("There is no clause with id $clauseID") - if (atomIDs.size < 2) + } + if (atomIDs.size < 2) { throw IllegalMove("Please select more than 1 atom to factorize") + } // Verification of correct ID in atoms -> unifySingleClause var newClause = clauses[clauseID].clone() @@ -157,11 +159,12 @@ fun factorize(state: FoResolutionState, clauseID: Int, atomIDs: List) { newClause = instantiateReturn(newClause, mgu) // Check equality of both atoms - if (newClause.atoms[firstID] != newClause.atoms[secondID]) + if (newClause.atoms[firstID] != newClause.atoms[secondID]) { throw IllegalMove( "Atoms '${newClause.atoms[firstID]}' and '${newClause.atoms[secondID]}'" + " are not equal after instantiation" ) + } // Change every unified atom to placeholder (except last) -> later remove all placeholder // -> One Atom remains @@ -194,9 +197,9 @@ fun hyper( // Checks for correct clauseID and IDs in Map checkHyperID(state, mainID, atomMap) - if (atomMap.isEmpty()) + if (atomMap.isEmpty()) { throw IllegalMove("Please select side premisses for hyper resolution") - + } val clauses = state.clauseSet.clauses val mainPremiss = clauses[mainID].clone() @@ -209,9 +212,9 @@ fun hyper( sidePremisses.add(sidePremiss) // Check side premiss for positiveness - if (!sidePremiss.isPositive()) + if (!sidePremiss.isPositive()) { throw IllegalMove("Side premiss $sidePremiss is not positive") - + } relations.add(Pair(mainPremiss.atoms[mAtomID].lit, sidePremiss.atoms[sAtomID].lit)) } @@ -243,9 +246,9 @@ fun hyper( } // Check there are no negative atoms anymore - if (!newMainPremiss.isPositive()) + if (!newMainPremiss.isPositive()) { throw IllegalMove("Resulting clause $mainPremiss is not positive") - + } // Add resolved clause to clause set clauses.add(newMainPremiss) state.newestNode = clauses.size - 1 @@ -262,13 +265,15 @@ fun hyper( private fun unifySingleClause(clause: Clause, a1: Int, a2: Int): Map { val atoms = clause.atoms // Verify that atom ids are valid - if (a1 == a2) + if (a1 == a2) { throw IllegalMove("Cannot unify an atom with itself") - if (a1 < 0 || a1 >= atoms.size) + } + if (a1 < 0 || a1 >= atoms.size) { throw IllegalMove("There is no atom with id $a1") - if (a2 < 0 || a2 >= atoms.size) + } + if (a2 < 0 || a2 >= atoms.size) { throw IllegalMove("There is no atom with id $a2") - + } val literal1 = atoms[a1].lit val literal2 = atoms[a2].lit val mgu: Map diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt b/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt index 1b0b61f7c..0860091c1 100644 --- a/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt +++ b/backend/src/main/kotlin/kalkulierbar/resolution/GenericResolution.kt @@ -39,13 +39,15 @@ interface GenericResolutionState { val clauses = clauseSet.clauses // Verify that the clause ids are valid - if (clause1 == clause2) + if (clause1 == clause2) { throw IllegalMove("Both ids refer to the same clause") - if (clause1 < 0 || clause1 >= clauses.size) + } + if (clause1 < 0 || clause1 >= clauses.size) { throw IllegalMove("There is no clause with id $clause1") - if (clause2 < 0 || clause2 >= clauses.size) + } + if (clause2 < 0 || clause2 >= clauses.size) { throw IllegalMove("There is no clause with id $clause2") - + } val c1 = clauses[clause1] val c2 = clauses[clause2] @@ -71,9 +73,9 @@ interface GenericResolutionState { * @param clauseID ID of the clause to be hidden */ fun hide(clauseID: Int) { - if (clauseID < 0 || clauseID >= clauseSet.clauses.size) + if (clauseID < 0 || clauseID >= clauseSet.clauses.size) { throw IllegalMove("There is no clause with id $clauseID") - + } // Move clause from main clause set to hidden clause set val clauseToHide = clauseSet.clauses.removeAt(clauseID) hiddenClauses.add(clauseToHide) diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt b/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt index ac126f3f0..b6cfd7ec3 100644 --- a/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt +++ b/backend/src/main/kotlin/kalkulierbar/resolution/HelperFunctions.kt @@ -21,11 +21,12 @@ fun filterClause( // Filter clauses for atoms with correct literal val atomsInC1 = c1.atoms.filter { literalsAreEqual(it.lit, literal) } val atomsInC2 = c2.atoms.filter { literalsAreEqual(it.lit, literal) } - if (atomsInC1.isEmpty()) + if (atomsInC1.isEmpty()) { throw IllegalMove("Clause '$c1' does not contain atom '$literal'") - if (atomsInC2.isEmpty()) + } + if (atomsInC2.isEmpty()) { throw IllegalMove("Clause '$c2' does not contain atom '$literal'") - + } val msg = "Clauses '$c1' and '$c2' do not contain atom '$literal' in both positive and negated form" return findResCandidates(atomsInC1, atomsInC2) ?: throw IllegalMove(msg) @@ -47,19 +48,21 @@ fun getAutoResolutionCandidates( c2.atoms.any { literalsAreEqual(c1atom.lit, it.lit) } } - if (sharedAtoms.isEmpty()) + if (sharedAtoms.isEmpty()) { throw IllegalMove("Clauses '$c1' and '$c2' contain no common literals") + } // Sort out atoms not present in opposite polarity in c2 (shared atoms came from c1 originally) sharedAtoms = sharedAtoms.filter { c2.atoms.contains(it.not()) } - if (sharedAtoms.isEmpty()) + if (sharedAtoms.isEmpty()) { throw IllegalMove( "Clauses '$c1' and '$c2' contain no common literals that appear" + "in positive and negated form" ) + } // Choose the first shared literal val a1 = sharedAtoms[0] @@ -102,8 +105,10 @@ fun findResCandidates( for (a1 in atoms1) { val other = if (a1.negated) pos else neg - if (other.isEmpty()) + if (other.isEmpty()) { continue + } + val a2 = other[0] return Pair(a1, a2) } @@ -119,8 +124,9 @@ fun findResCandidates( */ fun literalsAreEqual(a: AtomType, b: AtomType): Boolean { // Use syntactic equality for literal comparison if defined - return if (a is SyntacticEquality && b is SyntacticEquality) + return if (a is SyntacticEquality && b is SyntacticEquality) { a.synEq(b) - else + } else { (a == b) + } } diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt b/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt index e3de4e854..2c59bedeb 100644 --- a/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt +++ b/backend/src/main/kotlin/kalkulierbar/resolution/PropositionalResolution.kt @@ -20,11 +20,11 @@ class PropositionalResolution : GenericResolution, override val moveSerializer = ResolutionMove.serializer() override fun parseFormulaToState(formula: String, params: ResolutionParam?): ResolutionState { - val parsed = if (params == null) + val parsed = if (params == null) { FlexibleClauseSetParser.parse(formula) - else + } else { FlexibleClauseSetParser.parse(formula, params.cnfStrategy) - + } return ResolutionState(parsed, params?.visualHelp ?: VisualHelp.NONE) } @@ -50,18 +50,18 @@ class PropositionalResolution : GenericResolution, val clauses = state.clauseSet.clauses // Verify that clause id is valid - if (clauseID < 0 || clauseID >= clauses.size) + if (clauseID < 0 || clauseID >= clauses.size) { throw IllegalMove("There is no clause with id $clauseID") - + } val oldClause = clauses[clauseID] // Copy old clause and factorize val newClause = oldClause.clone() newClause.atoms = newClause.atoms.distinct().toMutableList() // Throw message for no possible factorisation - if (oldClause.atoms.size == newClause.atoms.size) + if (oldClause.atoms.size == newClause.atoms.size) { throw IllegalMove("Nothing to factorize") - + } // Hide old and add new clause clauses.removeAt(clauseID) clauses.add(clauseID, newClause) @@ -85,9 +85,9 @@ class PropositionalResolution : GenericResolution, // Checks for correct clauseID and IDs in Map checkHyperID(state, mainID, atomMap) - if (atomMap.isEmpty()) + if (atomMap.isEmpty()) { throw IllegalMove("Please select side premisses for hyper resolution") - + } val clauses = state.clauseSet.clauses var mainPremiss = clauses[mainID].clone() @@ -97,23 +97,23 @@ class PropositionalResolution : GenericResolution, val sidePremiss = clauses[sClauseID] // Check side premiss for positiveness - if (!sidePremiss.isPositive()) + if (!sidePremiss.isPositive()) { throw IllegalMove("Side premiss $sidePremiss is not positive") - + } val mainAtom = clauses[mainID].atoms[mAtomID] val sideAtom = sidePremiss.atoms[sAtomID] // Check that atom in main premiss is negative - if (!mainAtom.negated) + if (!mainAtom.negated) { throw IllegalMove("Literal '$mainAtom' in main premiss has to be negative, ") - + } // Resolve mainPremiss and sidePremiss mainPremiss = buildClause(mainPremiss, mainAtom, sidePremiss, sideAtom) } // Check there are no negative atoms anymore - if (!mainPremiss.isPositive()) + if (!mainPremiss.isPositive()) { throw IllegalMove("Resulting clause $mainPremiss is not positive") - + } // Add resolved clause to clause set clauses.add(mainPremiss) state.newestNode = clauses.size - 1 diff --git a/backend/src/main/kotlin/kalkulierbar/resolution/RestrictionChecking.kt b/backend/src/main/kotlin/kalkulierbar/resolution/RestrictionChecking.kt index f50f63dc6..3539a01a8 100644 --- a/backend/src/main/kotlin/kalkulierbar/resolution/RestrictionChecking.kt +++ b/backend/src/main/kotlin/kalkulierbar/resolution/RestrictionChecking.kt @@ -13,36 +13,43 @@ fun checkHyperID(state: GenericResolutionState, clauseID: I val clauses = state.clauseSet.clauses // Check for valid clause id - if (clauseID < 0 || clauseID >= clauses.size) + if (clauseID < 0 || clauseID >= clauses.size) { throw IllegalMove("There is no (main premiss) clause with id $clauseID") - + } val mainPremiss = clauses[clauseID].atoms // Check that (mainAtomID -> (sideClauseID, atomID)) map elements are correct for ((mAtomID, pair) in atomMap) { val (sClauseID, sAtomID) = pair - if (mAtomID < 0 || mAtomID >= mainPremiss.size) + if (mAtomID < 0 || mAtomID >= mainPremiss.size) { throw IllegalMove("There is no atom with id $mAtomID in (main premiss) clause ${clauses[clauseID]}") - if (sClauseID < 0 || sClauseID >= clauses.size) + } + if (sClauseID < 0 || sClauseID >= clauses.size) { throw IllegalMove("There is no (side premiss) clause with id $sClauseID") + } val clause = clauses[sClauseID].atoms - if (sAtomID < 0 || sAtomID >= clause.size) + if (sAtomID < 0 || sAtomID >= clause.size) { throw IllegalMove("There is no atom with id $sAtomID in (side premiss) clause $clause") + } } } @Suppress("ThrowsCount") fun resolveCheckID(state: FoResolutionState, c1: Int, c2: Int, c1lit: Int, c2lit: Int) { - if (c1 < 0 || c1 >= state.clauseSet.clauses.size) + if (c1 < 0 || c1 >= state.clauseSet.clauses.size) { throw IllegalMove("There is no clause with id $c1") - if (c2 < 0 || c2 >= state.clauseSet.clauses.size) + } + if (c2 < 0 || c2 >= state.clauseSet.clauses.size) { throw IllegalMove("There is no clause with id $c1") + } val clause1 = state.clauseSet.clauses[c1] val clause2 = state.clauseSet.clauses[c2] - if (c1lit < 0 || c1lit >= clause1.atoms.size) + if (c1lit < 0 || c1lit >= clause1.atoms.size) { throw IllegalMove("Clause $clause1 has no atom with index $c1lit") - if (c2lit < 0 || c2lit >= clause2.atoms.size) + } + if (c2lit < 0 || c2lit >= clause2.atoms.size) { throw IllegalMove("Clause $clause2 has no atom with index $c2lit") + } } diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt index 9c91731b3..7165ff96d 100644 --- a/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/sequent/GenericSequentCalculusBasicMoves.kt @@ -18,9 +18,9 @@ fun applyAx(state: GenericSequentCalculusState, nodeID: Int): GenericSequentCalc state.checkNodeID(nodeID) val leaf = state.tree[nodeID] - if (!leaf.isLeaf) + if (!leaf.isLeaf) { throw IllegalMove("Rules must be applied on leaf level") - + } for (leftFormula in leaf.leftFormulas) { if (leaf.rightFormulas.any { it.synEq(leftFormula) }) { val newLeaf = TreeNode( @@ -48,15 +48,14 @@ fun applyAx(state: GenericSequentCalculusState, nodeID: Int): GenericSequentCalc * @return new state after applying move */ fun applyNotRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState { - checkRight(state, nodeID, listIndex) val leaf = state.tree[nodeID] val formula = leaf.rightFormulas[listIndex] - if (formula !is Not) + if (formula !is Not) { throw IllegalMove("Rule notRight can only be applied on a negation") - + } val newLeftFormula = leaf.leftFormulas.toMutableList() newLeftFormula.add(formula.child) val newRightFormula = leaf.rightFormulas.toMutableList() @@ -87,9 +86,9 @@ fun applyNotLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int val leaf = state.tree[nodeID] val formula = leaf.leftFormulas[listIndex] - if (formula !is Not) + if (formula !is Not) { throw IllegalMove("Rule notLeft can only be applied on a negation") - + } val newLeftFormula = leaf.leftFormulas.toMutableList() newLeftFormula.removeAt(listIndex) val newRightFormula = leaf.rightFormulas.toMutableList() @@ -120,9 +119,9 @@ fun applyOrRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int val leaf = state.tree[nodeID] val formula = leaf.rightFormulas[listIndex] - if (formula !is Or) + if (formula !is Or) { throw IllegalMove("Rule orRight can only be applied on a disjunction") - + } val newLeftFormula = leaf.leftFormulas.toMutableList() val newRightFormula = leaf.rightFormulas.toMutableList() newRightFormula.removeAt(listIndex) @@ -157,9 +156,9 @@ fun applyOrLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int) val leaf = state.tree[nodeID] val formula = leaf.leftFormulas[listIndex] - if (formula !is Or) + if (formula !is Or) { throw IllegalMove("Rule orLeft can only be applied on a disjunction") - + } val newLeftFormulaOnLeftChild = leaf.leftFormulas.toMutableList() newLeftFormulaOnLeftChild.removeAt(listIndex) newLeftFormulaOnLeftChild.add(listIndex, formula.leftChild) @@ -206,9 +205,9 @@ fun applyAndRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: In val leaf = state.tree[nodeID] val formula = leaf.rightFormulas[listIndex] - if (formula !is And) + if (formula !is And) { throw IllegalMove("Rule andRight can only be applied on a conjunction") - + } val newLeftFormulaOnLeftChild = leaf.leftFormulas.toMutableList() val newRightFormulaOnLeftChild = leaf.rightFormulas.toMutableList() newRightFormulaOnLeftChild.removeAt(listIndex) @@ -251,9 +250,9 @@ fun applyAndLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int val leaf = state.tree[nodeID] val formula = leaf.leftFormulas[listIndex] - if (formula !is And) + if (formula !is And) { throw IllegalMove("Rule andLeft can only be applied on a conjunction") - + } val newLeftFormula = leaf.leftFormulas.toMutableList() newLeftFormula.removeAt(listIndex) newLeftFormula.add(listIndex, formula.leftChild) @@ -288,8 +287,9 @@ fun applyImpLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int val leaf = state.tree[nodeID] val formula = leaf.leftFormulas[listIndex] - if (formula !is Impl) + if (formula !is Impl) { throw IllegalMove("Rule impLeft can only be applied on an implication") + } val newLeftFormulaOnLeftChild = leaf.leftFormulas.toMutableList() newLeftFormulaOnLeftChild.removeAt(listIndex) val newRightFormulaOnLeftChild = leaf.rightFormulas.toMutableList() @@ -318,7 +318,7 @@ fun applyImpLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int /** * Rule ImpRight is applied, if the LogicNode is RightFormula of node and is of type IMPL (Implication). - * The leftChild of the logicNode will moved to the leftChild of the Node, + * The leftChild of the logicNode will be moved to the leftChild of the Node, * The rightChild of the logicNode will be moved to the rightChild of the Node. * @param state: GenericSequentCalculusState state to apply move on * @param nodeID: ID of node to apply move on @@ -326,14 +326,14 @@ fun applyImpLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int * @return new state after applying move */ fun applyImpRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int): GenericSequentCalculusState { - checkRight(state, nodeID, listIndex) val leaf = state.tree[nodeID] val formula = leaf.rightFormulas[listIndex] - if (formula !is Impl) + if (formula !is Impl) { throw IllegalMove("Rule impRight can only be applied on an implication") + } val newLeftFormula = leaf.leftFormulas.toMutableList() newLeftFormula.add(formula.leftChild) val newRightFormula = leaf.rightFormulas.toMutableList() @@ -363,10 +363,11 @@ fun checkRight(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int) state.checkNodeID(nodeID) val leaf = state.tree[nodeID] - if (!leaf.isLeaf) + if (!leaf.isLeaf) { throw IllegalMove("Rules can only be applied on leaf level") - else if (listIndex < 0 || leaf.rightFormulas.size <= listIndex) + } else if (listIndex < 0 || leaf.rightFormulas.size <= listIndex) { throw IllegalMove("listIndex out of bounds") + } } /** @@ -383,10 +384,11 @@ fun checkLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int) { state.checkNodeID(nodeID) val leaf = state.tree[nodeID] - if (!leaf.isLeaf) + if (!leaf.isLeaf) { throw IllegalMove("Rules can only be applied on leaf level") - else if (listIndex < 0 || leaf.leftFormulas.size <= listIndex) + } else if (listIndex < 0 || leaf.leftFormulas.size <= listIndex) { throw IllegalMove("listIndex out of bounds") + } } /** @@ -395,14 +397,14 @@ fun checkLeft(state: GenericSequentCalculusState, nodeID: Int, listIndex: Int) { * @return Equivalent state with the most recent rule application removed */ fun applyUndo(state: GenericSequentCalculusState): GenericSequentCalculusState { - if (state.tree.size <= 1) + if (state.tree.size <= 1) { throw IllegalMove("No move to undo") - + } val latestNode = state.tree.elementAt(state.tree.size - 1) - if (!latestNode.isLeaf) + if (!latestNode.isLeaf) { throw IllegalMove("Rules can only be applied on leaf level") - + } val parentID: Int? = latestNode.parent val parentNode = state.tree.elementAt(parentID!!) diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt index a5f1264e9..7b9393a98 100644 --- a/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/sequent/fo/BasicMoves.kt @@ -1,11 +1,21 @@ package kalkulierbar.sequent.fo import kalkulierbar.IllegalMove -import kalkulierbar.logic.* +import kalkulierbar.logic.Constant +import kalkulierbar.logic.ExistentialQuantifier +import kalkulierbar.logic.FirstOrderTerm +import kalkulierbar.logic.LogicNode +import kalkulierbar.logic.UniversalQuantifier import kalkulierbar.logic.transform.LogicNodeVariableInstantiator import kalkulierbar.logic.transform.Signature import kalkulierbar.parsers.FirstOrderParser -import kalkulierbar.sequent.* +import kalkulierbar.sequent.AllLeft +import kalkulierbar.sequent.AllRight +import kalkulierbar.sequent.ExLeft +import kalkulierbar.sequent.ExRight +import kalkulierbar.sequent.TreeNode +import kalkulierbar.sequent.checkLeft +import kalkulierbar.sequent.checkRight /** * Rule AllLeft is applied, if the LogicNode is the leftChild of node and is of type All(UniversalQuantifier). @@ -22,9 +32,9 @@ fun applyAllLeft(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, ins val node = state.tree[nodeID] val formula: LogicNode = node.leftFormulas[listIndex] - if (formula !is UniversalQuantifier) + if (formula !is UniversalQuantifier) { throw IllegalMove("Rule allLeft can only be applied on a universal quantifier") - + } val replaceWith = FirstOrderParser.parseTerm(instTerm) checkAdherenceToSignature(replaceWith, node) @@ -61,15 +71,20 @@ fun applyAllLeft(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, ins * @param instTerm The term to instantiate with. Must be a constant. * @return new state after applying move */ -fun applyAllRight(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, instTerm: String?): FirstOrderSequentState { +fun applyAllRight( + state: FirstOrderSequentState, + nodeID: Int, + listIndex: Int, + instTerm: String? +): FirstOrderSequentState { checkRight(state, nodeID, listIndex) val node = state.tree[nodeID] val formula: LogicNode = node.rightFormulas[listIndex] - if (formula !is UniversalQuantifier) + if (formula !is UniversalQuantifier) { throw IllegalMove("Rule allRight can only be applied on a universal quantifier") - + } // When swapVariable is not defined try to automatically find a fitting variableName val replaceWithString = instTerm ?: getFreshConstantName(node, formula.varName) @@ -77,9 +92,9 @@ fun applyAllRight(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, in val replaceWith = FirstOrderParser.parseConstant(replaceWithString) // Check if swapVariable is not already in use in the current sequence - if (checkIfVariableNameIsAlreadyInUse(node, replaceWithString)) + if (checkIfVariableNameIsAlreadyInUse(node, replaceWithString)) { throw IllegalMove("Identifier '$replaceWithString' is already in use") - + } // The newFormula which will be added to the right side of the sequence. This is the child of the quantifier var newFormula = formula.child.clone() @@ -120,9 +135,9 @@ fun applyExLeft(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, inst val node = state.tree[nodeID] val formula: LogicNode = node.leftFormulas[listIndex] - if (formula !is ExistentialQuantifier) + if (formula !is ExistentialQuantifier) { throw IllegalMove("Rule exLeft can only be applied on an existential quantifier") - + } // When swapVariable is not defined try to automatically find a fitting variableName val replaceWithString = instTerm ?: getFreshConstantName(node, formula.varName) @@ -130,9 +145,9 @@ fun applyExLeft(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, inst val replaceWith = FirstOrderParser.parseConstant(replaceWithString) // Check if swapVariable is not already in use in the current sequence - if (checkIfVariableNameIsAlreadyInUse(node, replaceWithString)) + if (checkIfVariableNameIsAlreadyInUse(node, replaceWithString)) { throw IllegalMove("Identifier '$replaceWithString' is already in use") - + } // The newFormula which will be added to the left side of the sequence. This is the child of the quantifier var newFormula = formula.child.clone() @@ -172,9 +187,9 @@ fun applyExRight(state: FirstOrderSequentState, nodeID: Int, listIndex: Int, ins val node = state.tree[nodeID] val formula: LogicNode = node.rightFormulas[listIndex] - if (formula !is ExistentialQuantifier) + if (formula !is ExistentialQuantifier) { throw IllegalMove("Rule exRight can only be applied on an existential quantifier") - + } val replaceWith = FirstOrderParser.parseTerm(instTerm) checkAdherenceToSignature(replaceWith, node) diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt b/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt index 1381eedd6..9c7c65c38 100644 --- a/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt +++ b/backend/src/main/kotlin/kalkulierbar/sequent/fo/FirstOrderSequent.kt @@ -7,8 +7,37 @@ import kalkulierbar.ScoredCalculus import kalkulierbar.logic.FoTermModule import kalkulierbar.logic.LogicModule import kalkulierbar.parsers.FirstOrderSequentParser -import kalkulierbar.sequent.* -import kotlinx.serialization.decodeFromString +import kalkulierbar.sequent.AllLeft +import kalkulierbar.sequent.AllRight +import kalkulierbar.sequent.AndLeft +import kalkulierbar.sequent.AndRight +import kalkulierbar.sequent.Ax +import kalkulierbar.sequent.ExLeft +import kalkulierbar.sequent.ExRight +import kalkulierbar.sequent.GenericSequentCalculus +import kalkulierbar.sequent.ImpLeft +import kalkulierbar.sequent.ImpRight +import kalkulierbar.sequent.NotLeft +import kalkulierbar.sequent.NotRight +import kalkulierbar.sequent.OrLeft +import kalkulierbar.sequent.OrRight +import kalkulierbar.sequent.PruneMove +import kalkulierbar.sequent.SequentCalculusMove +import kalkulierbar.sequent.SequentCalculusMoveModule +import kalkulierbar.sequent.SequentCalculusParam +import kalkulierbar.sequent.TreeNode +import kalkulierbar.sequent.UndoMove +import kalkulierbar.sequent.applyAndLeft +import kalkulierbar.sequent.applyAndRight +import kalkulierbar.sequent.applyAx +import kalkulierbar.sequent.applyImpLeft +import kalkulierbar.sequent.applyImpRight +import kalkulierbar.sequent.applyNotLeft +import kalkulierbar.sequent.applyNotRight +import kalkulierbar.sequent.applyOrLeft +import kalkulierbar.sequent.applyOrRight +import kalkulierbar.sequent.applyPrune +import kalkulierbar.sequent.applyUndo import kotlinx.serialization.json.Json import kotlinx.serialization.modules.plus @@ -56,10 +85,11 @@ class FirstOrderSequent : } override fun checkCloseOnState(state: FirstOrderSequentState): CloseMessage { - return if (state.tree.all { it.isClosed }) + return if (state.tree.all { it.isClosed }) { CloseMessage(true, "The proof is closed and valid in First Order Logic") - else + } else { CloseMessage(false, "Not all branches of the proof tree are closed") + } } /* @@ -77,6 +107,9 @@ class FirstOrderSequent : } } - override fun scoreFromState(state: FirstOrderSequentState, name: String?): Map = stateToStat(state, name) + override fun scoreFromState( + state: FirstOrderSequentState, + name: String? + ): Map = stateToStat(state, name) override fun formulaFromState(state: FirstOrderSequentState) = state.tree[0].toString() } diff --git a/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt b/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt index 3d334982b..61a360ce7 100644 --- a/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt +++ b/backend/src/main/kotlin/kalkulierbar/sequent/prop/PropositionalSequent.kt @@ -6,12 +6,38 @@ import kalkulierbar.JsonParseException import kalkulierbar.ScoredCalculus import kalkulierbar.logic.LogicModule import kalkulierbar.parsers.PropositionalSequentParser -import kalkulierbar.sequent.* -import kotlinx.serialization.decodeFromString +import kalkulierbar.sequent.AndLeft +import kalkulierbar.sequent.AndRight +import kalkulierbar.sequent.Ax +import kalkulierbar.sequent.GenericSequentCalculus +import kalkulierbar.sequent.ImpLeft +import kalkulierbar.sequent.ImpRight +import kalkulierbar.sequent.NotLeft +import kalkulierbar.sequent.NotRight +import kalkulierbar.sequent.OrLeft +import kalkulierbar.sequent.OrRight +import kalkulierbar.sequent.PruneMove +import kalkulierbar.sequent.SequentCalculusMove +import kalkulierbar.sequent.SequentCalculusMoveModule +import kalkulierbar.sequent.SequentCalculusParam +import kalkulierbar.sequent.TreeNode +import kalkulierbar.sequent.UndoMove +import kalkulierbar.sequent.applyAndLeft +import kalkulierbar.sequent.applyAndRight +import kalkulierbar.sequent.applyAx +import kalkulierbar.sequent.applyImpLeft +import kalkulierbar.sequent.applyImpRight +import kalkulierbar.sequent.applyNotLeft +import kalkulierbar.sequent.applyNotRight +import kalkulierbar.sequent.applyOrLeft +import kalkulierbar.sequent.applyOrRight +import kalkulierbar.sequent.applyPrune +import kalkulierbar.sequent.applyUndo import kotlinx.serialization.json.Json import kotlinx.serialization.modules.plus -class PropositionalSequent : GenericSequentCalculus, ScoredCalculus() { +class PropositionalSequent : GenericSequentCalculus, + ScoredCalculus() { override val identifier = "prop-sequent" override val serializer = Json { @@ -30,7 +56,10 @@ class PropositionalSequent : GenericSequentCalculus, ScoredCalculus applyAx(state, move.nodeID) as PropositionalSequentState @@ -49,10 +78,11 @@ class PropositionalSequent : GenericSequentCalculus, ScoredCalculus = stateToStat(state, name) + override fun scoreFromState( + state: PropositionalSequentState, + name: String? + ): Map = stateToStat(state, name) override fun formulaFromState(state: PropositionalSequentState) = state.tree[0].toString() } diff --git a/backend/src/main/kotlin/kalkulierbar/signedtableaux/BasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/signedtableaux/BasicMoves.kt index 86a3a759b..15fb5cfe5 100644 --- a/backend/src/main/kotlin/kalkulierbar/signedtableaux/BasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/signedtableaux/BasicMoves.kt @@ -2,7 +2,12 @@ package kalkulierbar.signedtableaux import kalkulierbar.IllegalMove -import kalkulierbar.logic.* +import kalkulierbar.logic.And +import kalkulierbar.logic.Box +import kalkulierbar.logic.Diamond +import kalkulierbar.logic.Impl +import kalkulierbar.logic.Not +import kalkulierbar.logic.Or /** * If the given node is negated, @@ -27,15 +32,16 @@ fun applyNegation(state: SignedModalTableauxState, nodeID: Int, leafID: Int?): S val node = nodes[nodeID] val formula = node.formula - if (formula !is Not) + if (formula !is Not) { throw IllegalMove("Negation rule can only be applied on a negation") - + } // new node with negated node sigh is added as a child of the given node state.addChildren(leafID, SignedModalTableauxNode(leafID, node.prefix, !node.sign, formula.child)) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(Negation(nodeID, leafID)) + } return state } @@ -71,22 +77,25 @@ fun applyAlpha(state: SignedModalTableauxState, nodeID: Int, leafID: Int?): Sign when (formula) { is And -> { // Alpha move can only be applied if the node sign is TRUE if the Formula is And - if (!node.sign) + if (!node.sign) { throw IllegalMove("Alpha rule can only be applied on a conjunction if the sign is True") + } alpha1 = SignedModalTableauxNode(leafID, node.prefix, true, formula.leftChild) alpha2 = SignedModalTableauxNode(nodes.size, node.prefix, true, formula.rightChild) } is Or -> { // Alpha move can only be applied if the node sign is FALSE if the Formula is OR - if (node.sign) + if (node.sign) { throw IllegalMove("Alpha rule can only be applied on a disjunction if the sign is False") + } alpha1 = SignedModalTableauxNode(leafID, node.prefix, false, formula.leftChild) alpha2 = SignedModalTableauxNode(nodes.size, node.prefix, false, formula.rightChild) } is Impl -> { // Alpha move can only be applied if the node sign is FALSE if the Formula is IMPL - if (node.sign) + if (node.sign) { throw IllegalMove("Alpha rule can only be applied on an implication if the sign is False") + } alpha1 = SignedModalTableauxNode(leafID, node.prefix, true, formula.leftChild) alpha2 = SignedModalTableauxNode(nodes.size, node.prefix, false, formula.rightChild) } @@ -98,8 +107,9 @@ fun applyAlpha(state: SignedModalTableauxState, nodeID: Int, leafID: Int?): Sign state.addChildren(nodes.size - 1, alpha2) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(AlphaMove(nodeID, leafID)) + } return state } @@ -133,20 +143,23 @@ fun applyBeta(state: SignedModalTableauxState, nodeID: Int, leafID: Int?): Signe // Check if the node is F And, T Or or T Impl: only then can be Beta move applied when (formula) { is And -> { - if (node.sign) + if (node.sign) { throw IllegalMove("Beta rule can only be applied on a conjunction if the sign is False") + } beta1 = SignedModalTableauxNode(leafID, node.prefix, false, formula.leftChild) beta2 = SignedModalTableauxNode(leafID, node.prefix, false, formula.rightChild) } is Or -> { - if (!node.sign) + if (!node.sign) { throw IllegalMove("Beta rule can only be applied on a disjunction if the sign is True") + } beta1 = SignedModalTableauxNode(leafID, node.prefix, true, formula.leftChild) beta2 = SignedModalTableauxNode(leafID, node.prefix, true, formula.rightChild) } is Impl -> { - if (!node.sign) + if (!node.sign) { throw IllegalMove("Beta rule can only be applied on an implication if the sign is True") + } beta1 = SignedModalTableauxNode(leafID, node.prefix, false, formula.leftChild) beta2 = SignedModalTableauxNode(leafID, node.prefix, true, formula.rightChild) } @@ -158,8 +171,9 @@ fun applyBeta(state: SignedModalTableauxState, nodeID: Int, leafID: Int?): Signe state.addChildren(leafID, beta1, beta2) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(BetaMove(nodeID, leafID)) + } return state } @@ -193,19 +207,21 @@ fun applyNu(state: SignedModalTableauxState, prefix: Int, nodeID: Int, leafID: I val newPrefix = node.prefix.toMutableList() newPrefix.add(prefix) - if (!state.prefixIsUsedOnBranch(leafID, newPrefix)) + if (!state.prefixIsUsedOnBranch(leafID, newPrefix)) { throw IllegalMove("Prefix has to be already in use on the selected branch") - + } // Check if the node is T Box ( [] ) or F DIAMOND ( <> ) : only then can be NU move applied val nu0 = when (formula) { is Box -> { - if (!node.sign) + if (!node.sign) { throw IllegalMove("Nu rule can only be applied on BOX if the sign is True") + } SignedModalTableauxNode(leafID, newPrefix, true, formula.child) } is Diamond -> { - if (node.sign) + if (node.sign) { throw IllegalMove("Nu rule can only be applied on DIAMOND if the sign is False") + } SignedModalTableauxNode(leafID, newPrefix, false, formula.child) } else -> throw IllegalMove("Nu rule can not be applied on the node '$node'") @@ -214,8 +230,9 @@ fun applyNu(state: SignedModalTableauxState, prefix: Int, nodeID: Int, leafID: I state.addChildren(leafID, nu0) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(NuMove(prefix, nodeID, leafID)) + } return state } @@ -250,18 +267,21 @@ fun applyPi(state: SignedModalTableauxState, prefix: Int, nodeID: Int, leafID: I val newPrefix = node.prefix.toMutableList() newPrefix.add(prefix) - if (state.prefixIsUsedOnBranch(leafID, newPrefix)) + if (state.prefixIsUsedOnBranch(leafID, newPrefix)) { throw IllegalMove("Prefix is already in use on the selected branch") + } // Check if the node is F Box ( [] ) or T DIAMOND ( <> ) : only then can be NU move applied val pi0 = when (formula) { is Box -> { - if (node.sign) + if (node.sign) { throw IllegalMove("Pi rule can only be applied on box if the sign is False") + } SignedModalTableauxNode(leafID, newPrefix, false, formula.child) } is Diamond -> { - if (!node.sign) + if (!node.sign) { throw IllegalMove("Pi rule can only be applied on diamond if the sign is True") + } SignedModalTableauxNode(leafID, newPrefix, true, formula.child) } else -> throw IllegalMove("Pi rule can not be applied on the node '$node'") @@ -270,8 +290,9 @@ fun applyPi(state: SignedModalTableauxState, prefix: Int, nodeID: Int, leafID: I state.addChildren(leafID, pi0) // Add move to history - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(PiMove(prefix, nodeID, leafID)) + } return state } @@ -282,9 +303,9 @@ fun applyPi(state: SignedModalTableauxState, prefix: Int, nodeID: Int, leafID: I * @return new state after applying move */ fun applyPrune(state: SignedModalTableauxState, nodeID: Int): SignedModalTableauxState { - if (!state.backtracking) + if (!state.backtracking) { throw IllegalMove("Backtracking is not enabled for this proof") - + } state.moveHistory.add(Prune(nodeID)) state.pruneBranch(nodeID) return state @@ -304,29 +325,29 @@ fun applyPrune(state: SignedModalTableauxState, nodeID: Int): SignedModalTableau fun applyClose(state: SignedModalTableauxState, nodeID: Int, closeID: Int): SignedModalTableauxState { val nodes = state.tree - if (closeID < nodeID) + if (closeID < nodeID) { return applyClose(state, closeID, nodeID) - + } checkCloseIDRestrictions(state, nodeID, closeID) val node = nodes[nodeID] val leaf = nodes[closeID] - if (node.sign == leaf.sign) + if (node.sign == leaf.sign) { throw IllegalMove("The selected formulas are not of opposite sign") - - if (node.prefix != leaf.prefix) + } + if (node.prefix != leaf.prefix) { throw IllegalMove("The selected formulas do not have the same prefix") - - if (!node.formula.synEq(leaf.formula)) + } + if (!node.formula.synEq(leaf.formula)) { throw IllegalMove("The selected formulas are not syntactically equivalent") - + } leaf.closeRef = nodeID state.setClosed(closeID) - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(CloseMove(nodeID, closeID)) - + } return state } @@ -338,8 +359,9 @@ private fun checkCloseIDRestrictions(state: SignedModalTableauxState, nodeID: In state.checkNodeID(closeID) // Verify that closeNode is transitive parent of node - if (!state.nodeIsParentOf(nodeID, closeID)) + if (!state.nodeIsParentOf(nodeID, closeID)) { throw IllegalMove("Node '${state.tree[closeID]}' is not an ancestor of node '${state.tree[nodeID]}'") + } } /** @@ -348,6 +370,7 @@ private fun checkCloseIDRestrictions(state: SignedModalTableauxState, nodeID: In fun checkNodeRestrictions(state: SignedModalTableauxState, nodeID: Int) { state.checkNodeID(nodeID) // Verify that node is not already closed - if (state.tree[nodeID].isClosed) + if (state.tree[nodeID].isClosed) { throw IllegalMove("Node '${state.tree[nodeID]}' is already closed") + } } diff --git a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt index 70e918e1d..c287e25b9 100644 --- a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt +++ b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableaux.kt @@ -37,7 +37,10 @@ class SignedModalTableaux : } @Suppress("ComplexMethod") - override fun applyMoveOnState(state: SignedModalTableauxState, move: SignedModalTableauxMove): SignedModalTableauxState { + override fun applyMoveOnState( + state: SignedModalTableauxState, + move: SignedModalTableauxMove + ): SignedModalTableauxState { // Clear status message state.statusMessage = null @@ -61,13 +64,13 @@ class SignedModalTableaux : * @return Equivalent state with the most recent rule application removed */ private fun applyUndo(state: SignedModalTableauxState): SignedModalTableauxState { - if (!state.backtracking) + if (!state.backtracking) { throw IllegalMove("Backtracking is not enabled for this proof") - + } // Can't undo any more moves in initial state - if (state.moveHistory.isEmpty()) + if (state.moveHistory.isEmpty()) { return state - + } // Create a fresh clone-state with the same parameters and input formula var freshState = SignedModalTableauxState(state.formula, state.assumption, state.backtracking) freshState.usedBacktracking = true diff --git a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt index bb2c7f477..552b9e93e 100644 --- a/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt +++ b/backend/src/main/kotlin/kalkulierbar/signedtableaux/SignedModalTableauxMisc.kt @@ -30,8 +30,10 @@ class SignedModalTableauxState( // Set isClosed to true for all nodes dominated by node in reverse tree while (node == tree[nodeID] || node.children.fold(true) { acc, e -> acc && tree[e].isClosed }) { node.isClosed = true - if (node.parent == null) + if (node.parent == null) { break + } + node = tree[node.parent!!] } node = tree[nodeID] @@ -51,12 +53,14 @@ class SignedModalTableauxState( @Suppress("ReturnCount") fun prefixIsUsedOnBranch(leafID: Int, prefix: List): Boolean { var node = tree[leafID] - if (prefix == node.prefix) + if (prefix == node.prefix) { return true + } while (node.parent != null) { node = tree[node.parent!!] - if (prefix == node.prefix) + if (prefix == node.prefix) { return true + } } return false } diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt index 233065816..bc3f7bfd8 100644 --- a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderBasicMoves.kt @@ -15,8 +15,9 @@ import kalkulierbar.logic.util.UnifierEquivalence * @return state with the close move applied */ fun applyAutoCloseBranch(state: FoTableauxState, leafID: Int, closeNodeID: Int): FoTableauxState { - if (state.manualVarAssign) + if (state.manualVarAssign) { throw IllegalMove("Auto-close is not enabled for this proof") + } ensureBasicCloseability(state, leafID, closeNodeID) val leaf = state.tree[leafID] @@ -51,8 +52,9 @@ fun applyMoveCloseBranch( val leaf = state.tree[leafID] val closeNode = state.tree[closeNodeID] // Check that given var assignment is a mgu, warn if not - if (!UnifierEquivalence.isMGUorNotUnifiable(varAssign, leaf.relation, closeNode.relation)) + if (!UnifierEquivalence.isMGUorNotUnifiable(varAssign, leaf.relation, closeNode.relation)) { state.statusMessage = "The unifier you specified is not an MGU" + } val sig = Signature.of(state.clauseSet) varAssign.values.forEach { sig.check(it) } @@ -83,12 +85,13 @@ private fun closeBranchCommon( // Apply all specified variable instantiations globally state.applyVarInstantiation(varAssign) - if (!leaf.relation.synEq(closeNode.relation)) + if (!leaf.relation.synEq(closeNode.relation)) { throw IllegalMove("Nodes '$leaf' and '$closeNode' are not equal after variable instantiation") - + } // Instantiating variables globally may violate regularity in unexpected places - if (state.regular && !checkRegularity(state)) + if (state.regular && !checkRegularity(state)) { throw IllegalMove("This variable instantiation would violate the proof regularity") + } // Close branch leaf.closeRef = closeNodeID @@ -133,8 +136,9 @@ fun applyMoveExpandLeaf(state: FoTableauxState, leafID: Int, clauseID: Int): FoT verifyExpandConnectedness(state, leafID) // Record expansion for backtracking - if (state.backtracking) + if (state.backtracking) { state.moveHistory.add(MoveExpand(leafID, clauseID)) + } state.expansionCounter += 1 diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt index 54c081da8..a890e5f84 100644 --- a/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt +++ b/backend/src/main/kotlin/kalkulierbar/tableaux/FirstOrderTableaux.kt @@ -26,9 +26,9 @@ class FirstOrderTableaux : GenericTableaux, JSONCalculus, JSONCalculus { @Suppress("ReturnCount") fun nodeIsParentOf(parentID: Int, childID: Int): Boolean { val child = tree[childID] - if (child.parent == parentID) + if (child.parent == parentID) { return true - if (child.parent == 0 || child.parent == null) + } + if (child.parent == 0 || child.parent == null) { return false + } return nodeIsParentOf(parentID, child.parent!!) } @@ -56,8 +58,9 @@ interface GenericTableauxState { // Set isClosed to true for all nodes dominated by leaf in reverse tree while (node.isLeaf || node.children.fold(true) { acc, e -> acc && tree[e].isClosed }) { node.isClosed = true - if (node.parent == null) + if (node.parent == null) { break + } node = tree[node.parent!!] } } @@ -72,11 +75,11 @@ interface GenericTableauxState { if (root.isClosed) { var connectedness = "unconnected" - if (checkConnectedness(this, TableauxType.STRONGLYCONNECTED)) + if (checkConnectedness(this, TableauxType.STRONGLYCONNECTED)) { connectedness = "strongly connected" - else if (checkConnectedness(this, TableauxType.WEAKLYCONNECTED)) + } else if (checkConnectedness(this, TableauxType.WEAKLYCONNECTED)) { connectedness = "weakly connected" - + } val regularity = if (checkRegularity(this)) "regular " else "" val withWithoutBT = if (usedBacktracking) "with" else "without" @@ -103,41 +106,45 @@ interface GenericTableauxState { @Suppress("ThrowsCount", "ComplexMethod") fun getLemma(leafID: Int, lemmaID: Int): Atom { // Verify that subtree root for lemma creation exists - if (lemmaID >= tree.size || lemmaID < 0) + if (lemmaID >= tree.size || lemmaID < 0) { throw IllegalMove("Node with ID $lemmaID does not exist") - // Verify that subtree root for lemma creation exists - if (leafID >= tree.size || leafID < 0) + } // Verify that subtree root for lemma creation exists + if (leafID >= tree.size || leafID < 0) { throw IllegalMove("Node with ID $leafID does not exist") - + } val leaf = tree[leafID] val lemmaNode = tree[lemmaID] - if (!leaf.isLeaf) + if (!leaf.isLeaf) { throw IllegalMove("Node '$leaf' is not a leaf") - - if (leaf.isClosed) + } + if (leaf.isClosed) { throw IllegalMove("Leaf '$leaf' is already closed") - - if (!lemmaNode.isClosed) + } + if (!lemmaNode.isClosed) { throw IllegalMove("Node '$lemmaNode' is not the root of a closed subtableaux") + } - if (lemmaNode.parent == null) + if (lemmaNode.parent == null) { throw IllegalMove("Root node cannot be used for lemma creation") + } - if (lemmaNode.isLeaf) + if (lemmaNode.isLeaf) { throw IllegalMove("Cannot create lemma from a leaf") + } val commonParent: Int = lemmaNode.parent!! - if (!nodeIsParentOf(commonParent, leafID)) + if (!nodeIsParentOf(commonParent, leafID)) { throw IllegalMove("Nodes '$leaf' and '$lemmaNode' are not siblings") + } val atom = lemmaNode.toAtom().not() // Verify compliance with regularity criteria - if (regular) + if (regular) { verifyExpandRegularity(this, leafID, Clause(mutableListOf(atom)), applyPreprocessing = false) - + } return atom } diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt index 3ab8c6fba..6deb1b70e 100644 --- a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt +++ b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalBasicMoves.kt @@ -95,14 +95,14 @@ fun applyMoveUseLemma(state: TableauxState, leafID: Int, lemmaID: Int): Tableaux */ @Suppress("ThrowsCount") fun applyMoveUndo(state: TableauxState): TableauxState { - if (!state.backtracking) + if (!state.backtracking) { throw IllegalMove("Backtracking is not enabled for this proof") - + } // Throw error if no moves were made already val history = state.moveHistory - if (history.isEmpty()) + if (history.isEmpty()) { throw IllegalMove("Can't undo in initial state") - + } // Retrieve and remove this undo from list val top = history.removeAt(state.moveHistory.size - 1) diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt index 29586685b..3f2718d9b 100644 --- a/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt +++ b/backend/src/main/kotlin/kalkulierbar/tableaux/PropositionalTableauxMisc.kt @@ -40,8 +40,9 @@ class TableauxState( */ override fun nodeIsDirectlyCloseable(nodeID: Int): Boolean { val node = tree[nodeID] - if (node.parent == null) + if (node.parent == null) { return false + } val parent = tree[node.parent] return node.isLeaf && node.toAtom() == parent.toAtom().not() @@ -67,8 +68,9 @@ class TableauxState( while (node.parent != null) { node = tree[node.parent!!] // Check if current node is identical to atom - if (node.toAtom() == atom) + if (node.toAtom() == atom) { return true + } } return false diff --git a/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt b/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt index a872eb68a..293fcd780 100644 --- a/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt +++ b/backend/src/main/kotlin/kalkulierbar/tableaux/RestrictionChecking.kt @@ -24,8 +24,9 @@ fun verifyExpandRegularity( // Check Leaf for having parent var predecessor: GenericTableauxNode? = null - if (leaf.parent != null) + if (leaf.parent != null) { predecessor = state.tree[leaf.parent!!] + } // Fill list of predecessor while (predecessor?.parent != null) { @@ -37,11 +38,12 @@ fun verifyExpandRegularity( val processedClause = if (applyPreprocessing) state.clauseExpandPreprocessing(clause) else clause.atoms for (atom in processedClause) { - if (lst.contains(atom)) + if (lst.contains(atom)) { throw IllegalMove( "Expanding this clause would introduce a duplicate " + "node '$atom' on the branch, making the tree irregular" ) + } } } @@ -56,20 +58,23 @@ fun verifyExpandConnectedness(state: GenericTableauxState, val children = leaf.children // Expansion on root does not need to fulfill connectedness - if (leafID == 0) + if (leafID == 0) { return + } if (state.type == TableauxType.WEAKLYCONNECTED) { - if (!children.fold(false) { acc, id -> acc || state.nodeIsCloseable(id) }) + if (!children.fold(false) { acc, id -> acc || state.nodeIsCloseable(id) }) { throw IllegalMove("No literal in this clause would be closeable, making the tree unconnected") + } } else if (state.type == TableauxType.STRONGLYCONNECTED) { - if (!children.fold(false) { acc, id -> acc || state.nodeIsDirectlyCloseable(id) }) + if (!children.fold(false) { acc, id -> acc || state.nodeIsDirectlyCloseable(id) }) { throw IllegalMove( """ No literal in this clause would be closeable with '$leaf', making the tree not strongly connected """ ) + } } } @@ -85,9 +90,9 @@ fun verifyExpandConnectedness(state: GenericTableauxState, fun checkConnectedness(state: GenericTableauxState, ctype: TableauxType): Boolean { val startNodes = state.root.children // root is excluded from connectedness criteria - if (ctype == TableauxType.UNCONNECTED) + if (ctype == TableauxType.UNCONNECTED) { return true - + } val strong = (ctype == TableauxType.STRONGLYCONNECTED) return startNodes.fold(true) { acc, id -> acc && checkConnectedSubtree(state, id, strong) } } @@ -118,9 +123,9 @@ private fun checkConnectedSubtree( // 2. All child-subtrees are weakly/strongly connected themselves // Leaves are trivially connected - if (node.isLeaf) + if (node.isLeaf) { return true - + } var hasDirectlyClosedChild = false var allChildrenConnected = true @@ -129,8 +134,9 @@ private fun checkConnectedSubtree( val closedCondition = child.isClosed && (!strong || child.closeRef == root) - if (child.isLeaf && closedCondition) + if (child.isLeaf && closedCondition) { hasDirectlyClosedChild = true + } // All children are connected themselves if (!checkConnectedSubtree(state, id, strong)) { allChildrenConnected = false @@ -170,9 +176,9 @@ private fun checkRegularitySubtree( val node = state.tree[root] // If node is in list of predecessors return false - if (lst.contains(node.toAtom())) + if (lst.contains(node.toAtom())) { return false - + } // Add node spelling to list of predecessors val lstCopy = mutableListOf>() lstCopy.addAll(lst) @@ -196,31 +202,33 @@ private fun checkRegularitySubtree( @Suppress("ThrowsCount") fun ensureExpandability(state: GenericTableauxState, leafID: Int, clauseID: Int) { // Don't allow further expand moves if connectedness requires close moves to be applied first - if (!checkConnectedness(state, state.type)) + if (!checkConnectedness(state, state.type)) { throw IllegalMove( "The proof tree is currently not sufficiently connected, " + "please close branches first to restore connectedness before expanding more leaves" ) - + } // Verify that both leaf and clause are valid - if (leafID >= state.tree.size || leafID < 0) + if (leafID >= state.tree.size || leafID < 0) { throw IllegalMove("Node with ID $leafID does not exist") - if (clauseID >= state.clauseSet.clauses.size || clauseID < 0) + } + if (clauseID >= state.clauseSet.clauses.size || clauseID < 0) { throw IllegalMove("Clause with ID $clauseID does not exist") - + } val leaf = state.tree[leafID] val clause = state.clauseSet.clauses[clauseID] // Verify that leaf is actually a leaf - if (!leaf.isLeaf) + if (!leaf.isLeaf) { throw IllegalMove("Node '$leaf' is not a leaf") - - if (leaf.isClosed) + } + if (leaf.isClosed) { throw IllegalMove("Node '$leaf' is already closed") - + } // Move should be compatible with regularity restriction - if (state.regular) + if (state.regular) { verifyExpandRegularity(state, leafID, clause) + } } /** @@ -240,26 +248,27 @@ fun ensureExpandability(state: GenericTableauxState, leafID @Suppress("ComplexMethod", "ThrowsCount") fun ensureBasicCloseability(state: GenericTableauxState, leafID: Int, closeNodeID: Int) { // Verify that both leaf and closeNode are valid nodes - if (leafID >= state.tree.size || leafID < 0) + if (leafID >= state.tree.size || leafID < 0) { throw IllegalMove("Node with ID $leafID does not exist") - if (closeNodeID >= state.tree.size || closeNodeID < 0) + } + if (closeNodeID >= state.tree.size || closeNodeID < 0) { throw IllegalMove("Node with ID $closeNodeID does not exist") - + } val leaf = state.tree[leafID] val closeNode = state.tree[closeNodeID] // Verify that leaf is actually a leaf - if (!leaf.isLeaf) + if (!leaf.isLeaf) { throw IllegalMove("Node '$leaf' is not a leaf") - + } // Verify that leaf is not already closed - if (leaf.isClosed) + if (leaf.isClosed) { throw IllegalMove("Leaf '$leaf' is already closed, no need to close again") - + } // Verify that leaf and closeNode reference the same literal - if (leaf.literalStem != closeNode.literalStem) + if (leaf.literalStem != closeNode.literalStem) { throw IllegalMove("Leaf '$leaf' and node '$closeNode' do not reference the same literal") - + } // Verify that negation checks out if (leaf.negated == closeNode.negated) { val noneOrBoth = if (leaf.negated) "both of them" else "neither of them" @@ -268,10 +277,11 @@ fun ensureBasicCloseability(state: GenericTableauxState, le } // Ensure that tree root node cannot be used to close literals of same spelling ('true') - if (closeNodeID == 0) + if (closeNodeID == 0) { throw IllegalMove("The root node cannot be used for branch closure") - + } // Verify that closeNode is transitive parent of leaf - if (!state.nodeIsParentOf(closeNodeID, leafID)) + if (!state.nodeIsParentOf(closeNodeID, leafID)) { throw IllegalMove("Node '$closeNode' is not an ancestor of leaf '$leaf'") + } } diff --git a/backend/src/main/kotlin/kalkulierbar/tamperprotect/TamperProtect.kt b/backend/src/main/kotlin/kalkulierbar/tamperprotect/TamperProtect.kt index ffbd51619..3aa9878c3 100644 --- a/backend/src/main/kotlin/kalkulierbar/tamperprotect/TamperProtect.kt +++ b/backend/src/main/kotlin/kalkulierbar/tamperprotect/TamperProtect.kt @@ -7,6 +7,7 @@ import org.komputing.khash.keccak.extensions.digestKeccak * Helper class to ensure state integrity * Calculates and verifies a cryptographic checksum over a state fingerprint * Technically a HMAC with a not strictly speaking secret key + * * Note: * This is designed to protect against semi-accidental misuse, _not_ active malicious interference */ diff --git a/backend/src/main/kotlin/kalkulierbar/tree/TreeGardener.kt b/backend/src/main/kotlin/kalkulierbar/tree/TreeGardener.kt index f2106e021..bbaf752e6 100644 --- a/backend/src/main/kotlin/kalkulierbar/tree/TreeGardener.kt +++ b/backend/src/main/kotlin/kalkulierbar/tree/TreeGardener.kt @@ -15,8 +15,9 @@ interface TreeGardener { fun checkNodeID(vararg ids: Int) { for (id in ids) { - if (id < 0 || tree.size <= id) + if (id < 0 || tree.size <= id) { throw IllegalMove("Node with ID $id does not exist") + } } } @@ -29,10 +30,12 @@ interface TreeGardener { @Suppress("ReturnCount") fun nodeIsParentOf(parentID: Int, childID: Int): Boolean { val child = tree[childID] - if (child.parent == parentID) + if (child.parent == parentID) { return true - if (child.parent == 0 || child.parent == null) + } + if (child.parent == 0 || child.parent == null) { return false + } return nodeIsParentOf(parentID, child.parent!!) } @@ -61,8 +64,9 @@ interface TreeGardener { val index = worklist.removeAt(0) val node = tree[index] worklist.addAll(node.children) - if (node.isLeaf) + if (node.isLeaf) { leaves.add(index) + } } return leaves @@ -109,8 +113,9 @@ interface TreeGardener { private fun removeNodeInconsistent(id: Int) { tree.removeAt(id) tree.forEach { - if (it.parent != null && it.parent!! > id) + if (it.parent != null && it.parent!! > id) { it.parent = it.parent!! - 1 + } } } @@ -121,8 +126,9 @@ interface TreeGardener { tree.forEach { it.children.clear() } for (i in tree.indices) { - if (tree[i].parent != null) + if (tree[i].parent != null) { tree[tree[i].parent!!].children.add(i) + } } } @@ -133,10 +139,11 @@ interface TreeGardener { */ fun getWidth(nodeID: Int): Int { val node = tree[nodeID] - return if (node.children.isEmpty()) + return if (node.children.isEmpty()) { 1 - else + } else { node.children.sumOf { getWidth(it) } + } } /** @@ -146,9 +153,10 @@ interface TreeGardener { */ fun getDepth(nodeID: Int): Int { val node = tree[nodeID] - return if (node.children.isEmpty()) + return if (node.children.isEmpty()) { 1 - else + } else { node.children.maxByOrNull { getDepth(it) }!! + 1 + } } } diff --git a/backend/src/main/kotlin/statekeeper/constants.kt b/backend/src/main/kotlin/statekeeper/Constants.kt similarity index 100% rename from backend/src/main/kotlin/statekeeper/constants.kt rename to backend/src/main/kotlin/statekeeper/Constants.kt diff --git a/backend/src/main/kotlin/statekeeper/Scoreboard.kt b/backend/src/main/kotlin/statekeeper/Scoreboard.kt index 550b1b4cc..00d4475ba 100644 --- a/backend/src/main/kotlin/statekeeper/Scoreboard.kt +++ b/backend/src/main/kotlin/statekeeper/Scoreboard.kt @@ -27,10 +27,11 @@ object Scoreboard { init { @Suppress("TooGenericExceptionCaught") data = try { - if (READONLY || !storage.exists()) + if (READONLY || !storage.exists()) { mutableMapOf() - else + } else { Json.decodeFromString(storage.readText()) + } } catch (e: Exception) { val msg = "Could not parse stored scoreboard: " throw JsonParseException(msg + (e.message ?: "Unknown error")) @@ -44,13 +45,14 @@ object Scoreboard { } fun addScore(calculus: String, formula: String, score: Map) { - if (READONLY) + if (READONLY) { return + } checkSanity(calculus, formula, score) - if (scoreboardCounter >= SCORE_MAX_NUM_SCOREBOARDS) + if (scoreboardCounter >= SCORE_MAX_NUM_SCOREBOARDS) { cleanScoreboards() - + } val calculusScores = data.getOrPut(calculus) { mutableMapOf() } val formulaScores = calculusScores.getOrPut(formula) { scoreboardCounter += 1; mutableListOf() } @@ -73,8 +75,9 @@ object Scoreboard { scoreboard.sortByDescending { it["Score"]?.toInt() ?: 0 } - if (scoreboard.size > SCORE_MAX_ENTRIES_PER_FORMULA) + if (scoreboard.size > SCORE_MAX_ENTRIES_PER_FORMULA) { scoreboard.removeLast() + } } /** @@ -83,24 +86,30 @@ object Scoreboard { */ @Suppress("ThrowsCount") private fun checkSanity(calculus: String, formula: String, score: Map) { - if (score.size > SCORE_MAX_FIELD_COUNT) + if (score.size > SCORE_MAX_FIELD_COUNT) { throw StorageLimitHit("Score objects exceeds field limit of $SCORE_MAX_FIELD_COUNT fields") - if (formula.length > SCORE_MAX_FORMULA_SIZE) + } + if (formula.length > SCORE_MAX_FORMULA_SIZE) { throw StorageLimitHit("Formula exceed size limit of $SCORE_MAX_FORMULA_SIZE B") - if (calculus.length > SCORE_MAX_CALC_NAME_SIZE) + } + if (calculus.length > SCORE_MAX_CALC_NAME_SIZE) { throw StorageLimitHit("Example calculus name exceeds size limit of $SCORE_MAX_CALC_NAME_SIZE B") - if (score.keys.any { it.length > SCORE_MAX_KEY_SIZE }) + } + if (score.keys.any { it.length > SCORE_MAX_KEY_SIZE }) { throw StorageLimitHit("Score object key exceeds size limit of $SCORE_MAX_KEY_SIZE B") - if (score.values.any { it.length > SCORE_MAX_VALUE_SIZE }) + } + if (score.values.any { it.length > SCORE_MAX_VALUE_SIZE }) { throw StorageLimitHit("Score object value exceeds size limit of $SCORE_MAX_VALUE_SIZE B") + } } /** * Save the current scoreboard data to the scoreboard file */ private fun flush() { - if (!storage.exists()) + if (!storage.exists()) { storage.createNewFile() + } storage.writeText(Json.encodeToString(data)) flushScheduled = false } @@ -114,7 +123,8 @@ object Scoreboard { }.toMutableMap() scoreboardCounter = data.values.sumOf { it.size } - if (scoreboardCounter >= SCORE_MAX_NUM_SCOREBOARDS) + if (scoreboardCounter >= SCORE_MAX_NUM_SCOREBOARDS) { throw StorageLimitHit("Maximum scoreboard count of $SCORE_MAX_NUM_SCOREBOARDS exceeded") + } } } diff --git a/backend/src/main/kotlin/statekeeper/statekeeper.kt b/backend/src/main/kotlin/statekeeper/Statekeeper.kt similarity index 91% rename from backend/src/main/kotlin/statekeeper/statekeeper.kt rename to backend/src/main/kotlin/statekeeper/Statekeeper.kt index 1685a2fd9..5ef1cae2c 100644 --- a/backend/src/main/kotlin/statekeeper/statekeeper.kt +++ b/backend/src/main/kotlin/statekeeper/Statekeeper.kt @@ -3,7 +3,6 @@ package statekeeper import kalkulierbar.JsonParseException import kalkulierbar.KalkulierbarException import kotlinx.serialization.Serializable -import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString import kotlinx.serialization.json.Json import org.komputing.khash.keccak.KeccakParameter @@ -33,8 +32,9 @@ object StateKeeper { if (storage.createNewFile()) { state = AppState() flush() - } else + } else { state = Json.decodeFromString(storage.readText()) + } } catch (e: Exception) { val msg = "Could not parse stored state: " throw JsonParseException(msg + (e.message ?: "Unknown error")) @@ -67,8 +67,9 @@ object StateKeeper { */ fun checkCredentials(mac: String): String { val fingerprint = "kbcc" - if (!verifyMAC(fingerprint, mac)) + if (!verifyMAC(fingerprint, mac)) { throw AuthenticationException("Invalid password") + } return "true" } @@ -85,8 +86,9 @@ object StateKeeper { */ fun setCalculusState(calculus: String, enableString: String, mac: String): String { val fingerprint = "kbsc|$calculus|$enableString" - if (!verifyMAC(fingerprint, mac)) + if (!verifyMAC(fingerprint, mac)) { throw AuthenticationException("Invalid password") + } val enable = (enableString == "true") @@ -113,8 +115,9 @@ object StateKeeper { val fingerprint = "kbae|$example" val parsedExample: Example - if (!verifyMAC(fingerprint, mac)) + if (!verifyMAC(fingerprint, mac)) { throw AuthenticationException("Invalid password") + } try { parsedExample = Json.decodeFromString(example) @@ -143,13 +146,15 @@ object StateKeeper { @Suppress("ThrowsCount") fun delExample(exampleIdString: String, mac: String): String { val fingerprint = "kbde|$exampleIdString" - if (!verifyMAC(fingerprint, mac)) + if (!verifyMAC(fingerprint, mac)) { throw AuthenticationException("Invalid password") + } try { val id = exampleIdString.toInt() - if (id < 0 || id >= state.examples.size) + if (id < 0 || id >= state.examples.size) { throw JsonParseException("Example with ID $id does not exist") + } state.examples.removeAt(id) flush() } catch (e: NumberFormatException) { @@ -201,19 +206,24 @@ object StateKeeper { */ @Suppress("ThrowsCount") private fun checkSanity(ex: Example) { - if (ex.name.length > EXAMPLE_NAME_SIZE) + if (ex.name.length > EXAMPLE_NAME_SIZE) { throw StorageLimitHit("Example name exceeds size limit of $EXAMPLE_NAME_SIZE B") - if (ex.description.length > EXAMPLE_DESC_SIZE) + } + if (ex.description.length > EXAMPLE_DESC_SIZE) { throw StorageLimitHit("Example description exceeds size limit of $EXAMPLE_DESC_SIZE B") - if (ex.formula.length > EXAMPLE_FORMULA_SIZE) + } + if (ex.formula.length > EXAMPLE_FORMULA_SIZE) { throw StorageLimitHit("Example formula exceeds size limit of $EXAMPLE_FORMULA_SIZE B") - if (ex.params.length > EXAMPLE_PARAM_SIZE) + } + if (ex.params.length > EXAMPLE_PARAM_SIZE) { throw StorageLimitHit("Example parameters exceed size limit of $EXAMPLE_PARAM_SIZE B") - if (ex.calculus.length > EXAMPLE_CALC_NAME_SIZE) + } + if (ex.calculus.length > EXAMPLE_CALC_NAME_SIZE) { throw StorageLimitHit("Example calculus name exceeds size limit of $EXAMPLE_CALC_NAME_SIZE B") - - if (state.examples.size >= MAX_EXAMPLE_COUNT) + } + if (state.examples.size >= MAX_EXAMPLE_COUNT) { throw StorageLimitHit("Maximum number of stored examples ($MAX_EXAMPLE_COUNT) exceeded") + } } } diff --git a/backend/src/main/kotlin/statekeeper/Stats.kt b/backend/src/main/kotlin/statekeeper/Stats.kt index c80be827a..69002d066 100644 --- a/backend/src/main/kotlin/statekeeper/Stats.kt +++ b/backend/src/main/kotlin/statekeeper/Stats.kt @@ -27,10 +27,11 @@ object Stats { init { @Suppress("TooGenericExceptionCaught") data = try { - if (!storage.exists()) + if (!storage.exists()) { StatContainer() - else + } else { Json.decodeFromString(storage.readText()) + } } catch (e: Exception) { val msg = "Could not parse stored stats: " throw JsonParseException(msg + (e.message ?: "Unknown error")) @@ -52,8 +53,9 @@ object Stats { * Save the current stats to the stat file */ private fun flush() { - if (!storage.exists()) + if (!storage.exists()) { storage.createNewFile() + } storage.writeText(Json.encodeToString(data)) flushScheduled = false } diff --git a/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt b/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt index dec4c779a..018acff4b 100644 --- a/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt +++ b/backend/src/test/kotlin/kalkulierbar/TestTamperProtect.kt @@ -10,7 +10,21 @@ class TestTamperProtect { private val tv1 = Pair("", "0D9A6E6CCA519AEFA10F211186D8F4F8BCC5132816027D6260134B59A440CA6C") private val tv2 = Pair("smoke&mirrors", "7323EC61EE548AF565BA2D874AD8E9FC3F363E4726833283B25B9AC9F54E42EF") - private val words = listOf("fog", "haze", "watermelon", "zombie", "factory", "dance", "dream", "silent", "weep", "lightbulb", "shine", "dim", "utopia") + private val words = listOf( + "fog", + "haze", + "watermelon", + "zombie", + "factory", + "dance", + "dream", + "silent", + "weep", + "lightbulb", + "shine", + "dim", + "utopia" + ) @Test fun testSealGeneration() { diff --git a/backend/src/test/kotlin/kalkulierbar/dpll/TestDpllJson.kt b/backend/src/test/kotlin/kalkulierbar/dpll/TestDpllJson.kt index 679e89793..0e0f26885 100644 --- a/backend/src/test/kotlin/kalkulierbar/dpll/TestDpllJson.kt +++ b/backend/src/test/kotlin/kalkulierbar/dpll/TestDpllJson.kt @@ -58,7 +58,12 @@ class TestDpllJson { @Test fun testStateToJson() { - val expected = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true},{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"},"children":[],"modelVerified":null}],"seal":"9A2C06A4018F47568B0F64B3A9BEA68FE6F83C3CD7E1F45D8B1E925E162E1BA1"}""" + val expected = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true}, + |{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT", + |"label":"true","diff":{"type":"cd-identity"},"children":[],"modelVerified":null}], + |"seal":"9A2C06A4018F47568B0F64B3A9BEA68FE6F83C3CD7E1F45D8B1E925E162E1BA1"}""" + .trimMargin().replace("\n", "") val got = dpll.parseFormula("!a,c;a,!c", null) assertEquals(expected, got) } @@ -69,15 +74,46 @@ class TestDpllJson { @Test fun testJsonToState() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true},{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"},"children":[1,2],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}},"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}},"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}},"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[],"modelVerified":null}],"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true}, + |{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT", + |"label":"true","diff":{"type":"cd-identity"},"children":[1,2], + |"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff": + |{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}}, + |"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label": + |"¬a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a", + |"negated":true}]}},"children":[3,4],"modelVerified":null},{"parent":2, + |"type":"SPLIT","label":"c","diff":{"type":"cd-addclause","clause": + |{"atoms":[{"lit":"c","negated":false}]}},"children":[],"modelVerified":null}, + |{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause", + |"clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[], + |"modelVerified":null}], + |"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + .trimMargin() val state = dpll.jsonToState(json) - val expected = "pdpll|{!a, c}, {a, !c}|[(null|[1, 2]|ROOT|true|identity|null), (0|[]|SPLIT|a|add-{a}|null), (0|[3, 4]|SPLIT|¬a|add-{!a}|null), (2|[]|SPLIT|c|add-{c}|null), (2|[]|SPLIT|¬c|add-{!c}|null)]" + val expected = "pdpll|{!a, c}, {a, !c}|[(null|[1, 2]|ROOT|true|identity|null), " + + "(0|[]|SPLIT|a|add-{a}|null), (0|[3, 4]|SPLIT|¬a|add-{!a}|null), " + + "(2|[]|SPLIT|c|add-{c}|null), (2|[]|SPLIT|¬c|add-{!c}|null)]" assertEquals(expected, state.getHash()) } @Test fun testJsonStateCorrupt() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true},{"litc","negated":false}]},{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"},"children":[1,2],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}},"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}},"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}},"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[],"modelVerified":null}],"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true}, + |{"litc","negated":false}]},{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT", + |"label":"true","diff":{"type":"cd-identity"},"children":[1,2], + |"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff": + |{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}}, + |"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}}, + |"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}}, + |"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}}, + |"children":[],"modelVerified":null}], + |"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + .trimMargin() assertFailsWith { dpll.jsonToState(json) } @@ -85,7 +121,21 @@ class TestDpllJson { @Test fun testJsonStateMissingField() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"negated":true},{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"},"children":[1,2],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}},"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}},"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}},"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[],"modelVerified":null}],"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"negated":true}, + |{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT", + |"label":"true","diff":{"type":"cd-identity"},"children":[1,2], + |"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff": + |{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}}, + |"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}}, + |"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}}, + |"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}}, + |"children":[],"modelVerified":null}], + |"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + .trimMargin() assertFailsWith { dpll.jsonToState(json) } @@ -93,7 +143,22 @@ class TestDpllJson { @Test fun testJsonStateModify() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"},"children":[1,2],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}},"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}},"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}},"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[],"modelVerified":null}],"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT", + |"label":"true","diff":{"type":"cd-identity"},"children":[1,2],"modelVerified":null}, + |{"parent":0,"type":"SPLIT","label":"a","diff":{"type":"cd-addclause", + |"clause":{"atoms":[{"lit":"a","negated":false}]}},"children":[], + |"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}}, + |"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT", + |"label":"c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c", + |"negated":false}]}},"children":[],"modelVerified":null}, + |{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause", + |"clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[], + |"modelVerified":null}], + |"seal":"A8651499DDF3E5E9D724CB4E7F35F318FA2559DBE0945B38BCD64A6806D6C1AD"}""" + .trimMargin() assertFailsWith { dpll.jsonToState(json) } @@ -101,7 +166,22 @@ class TestDpllJson { @Test fun testJsonStateSeal() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true},{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":true}]}]},"tree":[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"},"children":[1,2],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":false}]}},"children":[],"modelVerified":null},{"parent":0,"type":"SPLIT","label":"¬a","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"a","negated":true}]}},"children":[3,4],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}},"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c","diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}},"children":[],"modelVerified":null}],"seal":"A8651499DDF3E5E9D724CB4E7F35F318FAFAFAFADBE0945B38BCD64A6806D6C1AD"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true}, + |{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":false}, + |{"lit":"c","negated":true}]}]},"tree": + |[{"parent":null,"type":"ROOT","label":"true","diff":{"type":"cd-identity"}, + |"children":[1,2],"modelVerified":null},{"parent":0,"type":"SPLIT", + |"label":"a","diff":{"type":"cd-addclause","clause":{"atoms": + |[{"lit":"a","negated":false}]}},"children":[],"modelVerified":null}, + |{"parent":0,"type":"SPLIT","label":"¬a","diff":{"type":"cd-addclause", + |"clause":{"atoms":[{"lit":"a","negated":true}]}},"children":[3,4], + |"modelVerified":null},{"parent":2,"type":"SPLIT","label":"c","diff": + |{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":false}]}}, + |"children":[],"modelVerified":null},{"parent":2,"type":"SPLIT","label":"¬c", + |"diff":{"type":"cd-addclause","clause":{"atoms":[{"lit":"c","negated":true}]}}, + |"children":[],"modelVerified":null}], + |"seal":"A8651499DDF3E5E9D724CB4E7F35F318FAFAFAFADBE0945B38BCD64A6806D6C1AD"}""" + .trimMargin() assertFailsWith { dpll.jsonToState(json) } diff --git a/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestAndRight.kt b/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestAndRight.kt index 9f06c97ee..b37baa8c5 100644 --- a/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestAndRight.kt +++ b/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestAndRight.kt @@ -4,7 +4,11 @@ import kalkulierbar.IllegalMove import kalkulierbar.parsers.FirstOrderParser import kalkulierbar.sequent.AndRight import kalkulierbar.sequent.fo.FirstOrderSequent -import kotlin.test.* +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotNull +import kotlin.test.assertTrue class TestAndRight { diff --git a/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestUndo.kt b/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestUndo.kt index 17abff2b6..13a3eb95f 100644 --- a/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestUndo.kt +++ b/backend/src/test/kotlin/kalkulierbar/firstordersequent/TestUndo.kt @@ -1,7 +1,11 @@ package kalkulierbar.firstordersequent import kalkulierbar.IllegalMove -import kalkulierbar.sequent.* +import kalkulierbar.sequent.AndRight +import kalkulierbar.sequent.Ax +import kalkulierbar.sequent.NotRight +import kalkulierbar.sequent.OrRight +import kalkulierbar.sequent.UndoMove import kalkulierbar.sequent.fo.FirstOrderSequent import kotlin.test.Test import kotlin.test.assertEquals diff --git a/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt b/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt index c02f1ed68..52d6556dc 100644 --- a/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt +++ b/backend/src/test/kotlin/kalkulierbar/logic/TestPropositionalLogic.kt @@ -101,11 +101,15 @@ class TestPropositionalLogic { fun testNotTseytin() { assertEquals("{not0}, {!vara, !not0}, {vara, not0}", TseytinCNF.transform(n1).toString()) assertEquals( - "{not0}, {!varb, !not3}, {varb, not3}, {!not3, !not2}, {not3, not2}, {not2, !vara, !equiv1}, {!not2, vara, !equiv1}, {!not2, !vara, equiv1}, {not2, vara, equiv1}, {!equiv1, !not0}, {equiv1, not0}", + "{not0}, {!varb, !not3}, {varb, not3}, {!not3, !not2}, {not3, not2}, " + + "{not2, !vara, !equiv1}, {!not2, vara, !equiv1}, {!not2, !vara, equiv1}, " + + "{not2, vara, equiv1}, {!equiv1, !not0}, {equiv1, not0}", TseytinCNF.transform(n2).toString() ) assertEquals( - "{not0}, {!vara, !not4}, {vara, not4}, {!vara, or2}, {!not4, or2}, {vara, not4, !or2}, {!varc, !not6}, {varc, not6}, {or2, !and1}, {not6, !and1}, {!or2, !not6, and1}, {!and1, !not0}, {and1, not0}", + "{not0}, {!vara, !not4}, {vara, not4}, {!vara, or2}, {!not4, or2}, " + + "{vara, not4, !or2}, {!varc, !not6}, {varc, not6}, {or2, !and1}, " + + "{not6, !and1}, {!or2, !not6, and1}, {!and1, !not0}, {and1, not0}", TseytinCNF.transform(n3).toString() ) } @@ -127,15 +131,19 @@ class TestPropositionalLogic { @Test fun testAndTseytin() { assertEquals( - "{and0}, {!vara, !not1}, {vara, not1}, {varb, impl5}, {!vara, impl5}, {!varb, vara, !impl5}, {varb, !and3}, {impl5, !and3}, {!varb, !impl5, and3}, {not1, !and0}, {and3, !and0}, {!not1, !and3, and0}", + "{and0}, {!vara, !not1}, {vara, not1}, {varb, impl5}, {!vara, impl5}," + + " {!varb, vara, !impl5}, {varb, !and3}, {impl5, !and3}, {!varb, !impl5, and3}," + + " {not1, !and0}, {and3, !and0}, {!not1, !and3, and0}", TseytinCNF.transform(a1).toString() ) assertEquals( - "{and0}, {!vara, !not2}, {vara, not2}, {vara, !and0}, {not2, !and0}, {!vara, !not2, and0}", + "{and0}, {!vara, !not2}, {vara, not2}, {vara, !and0}, {not2, !and0}, " + + "{!vara, !not2, and0}", TseytinCNF.transform(a2).toString() ) assertEquals( - "{and0}, {!vara, !not3}, {vara, not3}, {!vara, or1}, {!not3, or1}, {vara, not3, !or1}, {or1, !and0}, {varb, !and0}, {!or1, !varb, and0}", + "{and0}, {!vara, !not3}, {vara, not3}, {!vara, or1}, {!not3, or1}, " + + "{vara, not3, !or1}, {or1, !and0}, {varb, !and0}, {!or1, !varb, and0}", TseytinCNF.transform(a3).toString() ) } @@ -150,7 +158,10 @@ class TestPropositionalLogic { @Test fun testOrNaiveCNF() { assertEquals("{a, b}", NaiveCNF.transform(o1).toString()) - assertEquals("{a, !b, a, !a}, {a, !b, a, !b}, {a, !b, b, !a}, {a, !b, b, !b}", NaiveCNF.transform(o2).toString()) + assertEquals( + "{a, !b, a, !a}, {a, !b, a, !b}, {a, !b, b, !a}, {a, !b, b, !b}", + NaiveCNF.transform(o2).toString() + ) assertEquals("{!a, !b, b}, {!a, !b, b}", NaiveCNF.transform(o3).toString()) } @@ -161,11 +172,17 @@ class TestPropositionalLogic { TseytinCNF.transform(o1).toString() ) assertEquals( - "{or0}, {!varb, !not3}, {varb, not3}, {!vara, or1}, {!not3, or1}, {vara, not3, !or1}, {vara, !varb, !equiv5}, {!vara, varb, !equiv5}, {!vara, !varb, equiv5}, {vara, varb, equiv5}, {!or1, or0}, {!equiv5, or0}, {or1, equiv5, !or0}", + "{or0}, {!varb, !not3}, {varb, not3}, {!vara, or1}, {!not3, or1}, " + + "{vara, not3, !or1}, {vara, !varb, !equiv5}, {!vara, varb, !equiv5}, " + + "{!vara, !varb, equiv5}, {vara, varb, equiv5}, {!or1, or0}, " + + "{!equiv5, or0}, {or1, equiv5, !or0}", TseytinCNF.transform(o2).toString() ) assertEquals( - "{or0}, {vara, !and2}, {varb, !and2}, {!vara, !varb, and2}, {!and2, !not1}, {and2, not1}, {!varb, !not8}, {varb, not8}, {varb, impl6}, {!not8, impl6}, {!varb, not8, !impl6}, {!impl6, !not5}, {impl6, not5}, {!not1, or0}, {!not5, or0}, {not1, not5, !or0}", + "{or0}, {vara, !and2}, {varb, !and2}, {!vara, !varb, and2}, " + + "{!and2, !not1}, {and2, not1}, {!varb, !not8}, {varb, not8}, " + + "{varb, impl6}, {!not8, impl6}, {!varb, not8, !impl6}, {!impl6, !not5}, " + + "{impl6, not5}, {!not1, or0}, {!not5, or0}, {not1, not5, !or0}", TseytinCNF.transform(o3).toString() ) } diff --git a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt index ca7686881..51ce51fb9 100644 --- a/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt +++ b/backend/src/test/kotlin/kalkulierbar/logic/transform/TestSignature.kt @@ -8,8 +8,10 @@ import kotlin.test.assertFails class TestSignature { private val validFormulas = mapOf( "P(f(a, b))" to "Σ(constants={a, b}, functions={f(2)}, relations={P(1)}, bound={})", - "P(a, g(f(f(f(a))), b, f(c))) & Q(a, b, c)" to "Σ(constants={a, b, c}, functions={f(1), g(3)}, relations={P(2), Q(3)}, bound={})", - "/all X: /all Y: /all Z: (P(X, Y) & P(Y, Z) -> P(X, Z)) & P(a, f(a, a)) & P(f(a, a), g(a, a, a, a))" to "Σ(constants={a}, functions={f(2), g(4)}, relations={P(2)}, bound={X, Y, Z})" + "P(a, g(f(f(f(a))), b, f(c))) & Q(a, b, c)" + to "Σ(constants={a, b, c}, functions={f(1), g(3)}, relations={P(2), Q(3)}, bound={})", + "/all X: /all Y: /all Z: (P(X, Y) & P(Y, Z) -> P(X, Z)) & P(a, f(a, a)) & P(f(a, a), g(a, a, a, a))" + to "Σ(constants={a}, functions={f(2), g(4)}, relations={P(2)}, bound={X, Y, Z})" ) private val mixedArity = listOf( @@ -59,11 +61,13 @@ class TestSignature { val cs = FirstOrderCNF.transform(formula) val csSig = Signature.of(cs) - if (csSig.boundVariables.isEmpty()) + if (csSig.boundVariables.isEmpty()) { assertEquals(signature(expected), csSig) - else assertEquals( - signature(expected), csSig - ) + } else { + assertEquals( + signature(expected), csSig + ) + } } } diff --git a/backend/src/test/kotlin/kalkulierbar/nonclausaltableaux/TestBeta.kt b/backend/src/test/kotlin/kalkulierbar/nonclausaltableaux/TestBeta.kt index 239a368b7..0898930d8 100644 --- a/backend/src/test/kotlin/kalkulierbar/nonclausaltableaux/TestBeta.kt +++ b/backend/src/test/kotlin/kalkulierbar/nonclausaltableaux/TestBeta.kt @@ -74,7 +74,9 @@ class TestBeta { state = instance.applyMoveOnState(state, AlphaMove(0)) state = instance.applyMoveOnState(state, BetaMove(2)) - val expected = "[(null|[1]|false|null|((P(c) ∨ (P(d) ∧ Q(c))) ∧ Q(c))), (0|[2]|false|null|Q(c)), (1|[3, 4]|false|null|(P(c) ∨ (P(d) ∧ Q(c)))), (2|[]|false|null|(P(d) ∧ Q(c))), (2|[]|false|null|P(c))]" + val expected = "[(null|[1]|false|null|((P(c) ∨ (P(d) ∧ Q(c))) ∧ Q(c))), " + + "(0|[2]|false|null|Q(c)), (1|[3, 4]|false|null|(P(c) ∨ (P(d) ∧ Q(c)))), " + + "(2|[]|false|null|(P(d) ∧ Q(c))), (2|[]|false|null|P(c))]" assertEquals(expected, state.tree.map { it.getHash() }.toString()) } } diff --git a/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt b/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt index 0390610ac..cb9ccd741 100644 --- a/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt +++ b/backend/src/test/kotlin/kalkulierbar/parsers/TestFirstOrderSequentParser.kt @@ -65,7 +65,10 @@ class TestFirstOrderSequentParser { "!(/ex X: (P(X) <-> !P(X))) |- " to "¬(∃X: ((P(X) → ¬P(X)) ∧ (¬P(X) → P(X)))) ⊢ ", "/ex Xyz: P(Xyz) & /all X: P(X) |- " to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X))) ⊢ ", - "\\ex Xyz: P(Xyz) & \\all X: P(X), P(c) |- /ex Xyz: P(Xyz) & /all X: P(X), \\all X: \\all Y: \\all Z: R(m(X, m(Y, Z)), m(m(X,Y), Z))" to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X))), P(c) ⊢ ((∃Xyz: P(Xyz)) ∧ (∀X: P(X))), (∀X: (∀Y: (∀Z: R(m(X, m(Y, Z)), m(m(X, Y), Z)))))" + "\\ex Xyz: P(Xyz) & \\all X: P(X), P(c) |- /ex Xyz: P(Xyz) & " + + "/all X: P(X), \\all X: \\all Y: \\all Z: R(m(X, m(Y, Z)), m(m(X,Y), Z))" + to "((∃Xyz: P(Xyz)) ∧ (∀X: P(X))), P(c) ⊢ ((∃Xyz: P(Xyz)) ∧ (∀X: P(X))), " + + "(∀X: (∀Y: (∀Z: R(m(X, m(Y, Z)), m(m(X, Y), Z)))))" ) @Test diff --git a/backend/src/test/kotlin/kalkulierbar/propsequent/TestAndRight.kt b/backend/src/test/kotlin/kalkulierbar/propsequent/TestAndRight.kt index dfcd79aa4..b70a28cfa 100644 --- a/backend/src/test/kotlin/kalkulierbar/propsequent/TestAndRight.kt +++ b/backend/src/test/kotlin/kalkulierbar/propsequent/TestAndRight.kt @@ -4,7 +4,11 @@ import kalkulierbar.IllegalMove import kalkulierbar.parsers.PropositionalParser import kalkulierbar.sequent.AndRight import kalkulierbar.sequent.prop.PropositionalSequent -import kotlin.test.* +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotNull +import kotlin.test.assertTrue class TestAndRight { diff --git a/backend/src/test/kotlin/kalkulierbar/propsequent/TestUndo.kt b/backend/src/test/kotlin/kalkulierbar/propsequent/TestUndo.kt index 4b2b2131e..2ce5f8008 100644 --- a/backend/src/test/kotlin/kalkulierbar/propsequent/TestUndo.kt +++ b/backend/src/test/kotlin/kalkulierbar/propsequent/TestUndo.kt @@ -1,7 +1,11 @@ package kalkulierbar.propsequent import kalkulierbar.IllegalMove -import kalkulierbar.sequent.* +import kalkulierbar.sequent.AndRight +import kalkulierbar.sequent.Ax +import kalkulierbar.sequent.NotRight +import kalkulierbar.sequent.OrRight +import kalkulierbar.sequent.UndoMove import kalkulierbar.sequent.prop.PropositionalSequent import kotlin.test.Test import kotlin.test.assertEquals diff --git a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt index bcaf5e089..b22418297 100644 --- a/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt +++ b/backend/src/test/kotlin/kalkulierbar/regression/TestIssue50.kt @@ -11,6 +11,13 @@ class TestIssue50 { @Test fun testSuffixes() { val state = inst.parseFormulaToState("/all M: /all N: (Subset(M, N) <-> /all A: (In(A, M) -> In(A, N)))", null) - assertEquals("{Subset(M_1, N_1), !Subset(M_1, N_1)}, {Subset(M_2, N_2), In(sk1(M_2, N_2), M_2)}, {Subset(M_3, N_3), !In(sk1(M_3, N_3), N_3)}, {!In(A_4, M_4), In(A_4, N_4), !Subset(M_4, N_4)}, {!In(A_5, M_5), In(A_5, N_5), In(sk1(M_5, N_5), M_5)}, {!In(A_6, M_6), In(A_6, N_6), !In(sk1(M_6, N_6), N_6)}", state.clauseSet.toString()) + assertEquals( + "{Subset(M_1, N_1), !Subset(M_1, N_1)}, {Subset(M_2, N_2), " + + "In(sk1(M_2, N_2), M_2)}, {Subset(M_3, N_3), !In(sk1(M_3, N_3), N_3)}, " + + "{!In(A_4, M_4), In(A_4, N_4), !Subset(M_4, N_4)}, {!In(A_5, M_5), " + + "In(A_5, N_5), In(sk1(M_5, N_5), M_5)}, " + + "{!In(A_6, M_6), In(A_6, N_6), !In(sk1(M_6, N_6), N_6)}", + state.clauseSet.toString() + ) } } diff --git a/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt b/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt index 807d58a0f..398582b0e 100644 --- a/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt +++ b/backend/src/test/kotlin/kalkulierbar/resolution/TestFOResolveUnify.kt @@ -40,12 +40,30 @@ class TestFOResolveUnify { @Test fun testValid() { - testFormula(valid1, MoveResolveUnify(0, 1, 0, 0), "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3") - testFormula(valid2, MoveResolveUnify(0, 1, 0, 0), "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3") - testFormula(valid3, MoveResolveUnify(0, 1, 0, 0), "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(sk1, c), sk1)}, {}||NONE|2|3") - testFormula(valid4, MoveResolveUnify(0, 1, 0, 0), "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4") - testFormula(valid4, MoveResolveUnify(2, 1, 0, 0), "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4") - testFormula(valid5, MoveResolveUnify(2, 1, 1, 0), "resolutionstate|{!R(a), R(c)}, {R(X_2)}, {T(a), !R(f(g(h(a))))}, {T(a)}||NONE|3|4") + testFormula( + valid1, MoveResolveUnify(0, 1, 0, 0), + "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3" + ) + testFormula( + valid2, MoveResolveUnify(0, 1, 0, 0), + "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3" + ) + testFormula( + valid3, MoveResolveUnify(0, 1, 0, 0), + "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(sk1, c), sk1)}, {}||NONE|2|3" + ) + testFormula( + valid4, MoveResolveUnify(0, 1, 0, 0), + "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4" + ) + testFormula( + valid4, MoveResolveUnify(2, 1, 0, 0), + "resolutionstate|{!R(a)}, {R(X_2)}, {!R(f(g(h(a))))}, {}||NONE|3|4" + ) + testFormula( + valid5, MoveResolveUnify(2, 1, 1, 0), + "resolutionstate|{!R(a), R(c)}, {R(X_2)}, {T(a), !R(f(g(h(a))))}, {T(a)}||NONE|3|4" + ) } @Test @@ -68,8 +86,14 @@ class TestFOResolveUnify { @Test fun testManual() { - testFormula(valid1, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "a")), "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3") - testFormula(valid2, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "Y_2")), "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3") + testFormula( + valid1, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "a")), + "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(a, c), a)}, {}||NONE|2|3" + ) + testFormula( + valid2, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "Y_2")), + "resolutionstate|{R(f(X_1, c), X_1)}, {!R(f(Y_2, c), Y_2)}, {}||NONE|2|3" + ) testFormula(valid3, MoveResolveCustom(0, 1, 0, 0, mapOf("X_1" to "f(nope)"))) } } diff --git a/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt b/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt index b6ea68682..ac28c79b0 100644 --- a/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt +++ b/backend/src/test/kotlin/kalkulierbar/resolution/TestHyperResolution.kt @@ -110,7 +110,11 @@ class TestHyperResolution { @Test fun testFoIndexChecks() { - val state = fo.parseFormulaToState("(S(a) | !S(b) | !S(c) | !S(d)) & (R(b) | R(c)) & (Q(c) | Q(k)) & (P(d) | P(g) | P(h))", null) + val state = fo.parseFormulaToState( + "(S(a) | !S(b) | !S(c) | !S(d)) & (R(b) " + + "| R(c)) & (Q(c) | Q(k)) & (P(d) | P(g) | P(h))", + null + ) assertFailsWith { fo.applyMoveOnState(state, MoveHyper(-1, mapOf())) @@ -173,17 +177,35 @@ class TestHyperResolution { @Test fun testFoValidB() { - var state = fo.parseFormulaToState("/all X: (R(a) | !R(X) | R(X) | R(d)) & (R(e) | R(f) | R(b) | R(g))", null) + var state = fo.parseFormulaToState( + "/all X: (R(a) | !R(X) | R(X) | R(d)) & (R(e) " + + "| R(f) | R(b) | R(g))", + null + ) state = fo.applyMoveOnState(state, MoveHyper(0, mapOf(1 to Pair(1, 2)))) - assertEquals("{R(a), !R(X_1), R(X_1), R(d)}, {R(e), R(f), R(b), R(g)}, {R(a), R(b), R(d), R(e), R(f), R(g)}", state.clauseSet.toString()) + assertEquals( + "{R(a), !R(X_1), R(X_1), R(d)}, {R(e), R(f), R(b), R(g)}, " + + "{R(a), R(b), R(d), R(e), R(f), R(g)}", + state.clauseSet.toString() + ) } @Test fun aTPError() { - var state = fo.parseFormulaToState("F(a) & !G(a) & /all W:(!F(W) | H(W)) & /all Z:(!J(Z) | !I(Z) | F(Z)) & /all X: /all Y:(!H(X) | G(X) | !H(Y) | !I(Y)) & J(b) & I(b)", null) + var state = fo.parseFormulaToState( + "F(a) & !G(a) & /all W:(!F(W) " + + "| H(W)) & /all Z:(!J(Z) | !I(Z) | F(Z)) & /all X: /all Y:(!H(X) " + + "| G(X) | !H(Y) | !I(Y)) & J(b) & I(b)", + null + ) state = fo.applyMoveOnState(state, MoveHyper(3, mapOf(0 to Pair(5, 0), 1 to Pair(6, 0)))) - assertEquals("{F(a)}, {!G(a)}, {!F(W_3), H(W_3)}, {!J(Z_4), !I(Z_4), F(Z_4)}, {!H(X_5), G(X_5), !H(Y_5), !I(Y_5)}, {J(b)}, {I(b)}, {F(b)}", state.clauseSet.toString()) + assertEquals( + "{F(a)}, {!G(a)}, {!F(W_3), H(W_3)}, " + + "{!J(Z_4), !I(Z_4), F(Z_4)}, {!H(X_5), G(X_5), !H(Y_5), !I(Y_5)}, " + + "{J(b)}, {I(b)}, {F(b)}", + state.clauseSet.toString() + ) } } diff --git a/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt b/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt index 114b8038a..461f282ff 100644 --- a/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt +++ b/backend/src/test/kotlin/kalkulierbar/resolution/TestResolutionJson.kt @@ -110,7 +110,13 @@ class TestResolutionJson { @Test fun testJsonState() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false},{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms":[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms":[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1,"hiddenClauses":{"clauses":[]},"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false}, + |{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms": + |[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms": + |[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1, + |"hiddenClauses":{"clauses":[]}, + |"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + .trimMargin() val state = instance.jsonToState(json) assertEquals("resolutionstate|{a, b, c}, {!b, d}, {!c}||NONE|-1", state.getHash()) @@ -118,7 +124,13 @@ class TestResolutionJson { @Test fun testJsonStateCorrupt() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"anegated":false},{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms":[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms":[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1,"hiddenClauses":{"clauses":[]},"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"anegated":false}, + |{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms": + |[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms": + |[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1, + |"hiddenClauses":{"clauses":[]}, + |"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) } @@ -126,7 +138,13 @@ class TestResolutionJson { @Test fun testJsonStateMissingField() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{negated":false},{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms":[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms":[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1,"hiddenClauses":{"clauses":[]},"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{negated":false}, + |{"lit":"b","negated":false},{"lit":"c","negated":false}]}, + |{"atoms":[{"lit":"b","negated":true},{"lit":"d","negated":false}]}, + |{"atoms":[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1, + |"hiddenClauses":{"clauses":[]}, + |"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) } @@ -134,7 +152,13 @@ class TestResolutionJson { @Test fun testJsonStateModify() { - val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true},{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms":[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms":[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1,"hiddenClauses":{"clauses":[]},"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + val json = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":true}, + |{"lit":"b","negated":false},{"lit":"c","negated":false}]},{"atoms": + |[{"lit":"b","negated":true},{"lit":"d","negated":false}]},{"atoms": + |[{"lit":"c","negated":true}]}]},"visualHelp":"NONE","newestNode":-1, + |"hiddenClauses":{"clauses":[]}, + |"seal":"C8BB7816176F4DDFE33206C21D4466380D798276E649D48DDA1DD80D48CE9273"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) } @@ -146,7 +170,11 @@ class TestResolutionJson { @Test fun testStateToJson() { - val expected = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false}]},{"atoms":[{"lit":"a","negated":true}]}]},"visualHelp":"NONE","newestNode":-1,"hiddenClauses":{"clauses":[]},"lastMove":null,"seal":"C0C4AC36F24D4CE8C65D8108D2E2493D451F005BF5AC1BD00D8E153969952A36"}""" + val expected = """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false}]}, + |{"atoms":[{"lit":"a","negated":true}]}]},"visualHelp":"NONE","newestNode":-1, + |"hiddenClauses":{"clauses":[]},"lastMove":null, + |"seal":"C0C4AC36F24D4CE8C65D8108D2E2493D451F005BF5AC1BD00D8E153969952A36"}""" + .trimMargin().replace("\n", "") val param = "{\"cnfStrategy\": \"NAIVE\", \"visualHelp\": \"NONE\"}" val got = instance.parseFormula("a;!a", param) assertEquals(expected, got) @@ -154,14 +182,114 @@ class TestResolutionJson { @Test fun testJsonToState() { - val json1 = """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable","spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"a"}]}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"QuantifiedVariable","spelling":"Y_7"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]}]},"visualHelp":"HIGHLIGHT","newestNode":-1,"hiddenClauses":{"clauses":[]},"clauseCounter":8,"statusMessage":null,"lastMove":null,"seal":"196976513C2CF3237A499CE786D476733DF97B1199D8C7E26EAB89A210144A7F"}""" - val json2 = """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable","spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"a"}]}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"QuantifiedVariable","spelling":"Y_7"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[]},{"atoms":[]}]},"visualHelp":"HIGHLIGHT","newestNode":10,"hiddenClauses":{"clauses":[]},"clauseCounter":11,"statusMessage":null,"lastMove":null,"seal":"73B2B4074EAAD533D36972CFB6AE9BA81AF3E3C492CC09B0D86125EBB6C4723F"}""" - val jsonInvalid1 = """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable","spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"a"}]}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"QuantifiedVariable","spelling":"Y_7"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]}]},"visualHelp":"HIGHLIGHT","newestNode":-1,"hiddenClauses":{"clauses":[]},"clauseCounter":8,"statusMessage":null,"lastMove":null,"seal":"196976513C2CF3237A499CE786D4HELLODF97B1199D8C7E26EAB89A210144A7F"}""" - val jsonInvalid2 = """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable","spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"a"}]}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"QuantifiedVariable","spelling":"Y_7"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[]},{"atoms":[]}]},"visualHelp":"HIGHLIGHT","newestNode":10,"hiddenClauses":{"clauses":[]},"clauseCounter":11,"statusMessage":null,"lastMove":null,"seal":"73B2B4074EAAD533D36972CFB6AE9BA81AF3E3C492CC09B0D86125EBB6C4723F"}""" + val json1 = """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"b"}]},"negated":false}]},{"atoms":[{"lit": + |{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms": + |[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f", + |"arguments":[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable", + |"spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R", + |"arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant", + |"spelling":"b"},{"type":"Constant","spelling":"a"}]}]},"negated":true},{"lit": + |{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments": + |[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]}, + |"negated":true}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type": + |"Constant","spelling":"a"}]},"negated":true},{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"b"}]},"negated":true},{"lit":{"spelling":"R", + |"arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms": + |[{"lit":{"spelling":"Q","arguments":[{"type":"QuantifiedVariable","spelling": + |"Y_7"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"Q","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":true}]}]},"visualHelp": + |"HIGHLIGHT","newestNode":-1,"hiddenClauses":{"clauses":[]},"clauseCounter":8, + |"statusMessage":null,"lastMove":null, + |"seal":"196976513C2CF3237A499CE786D476733DF97B1199D8C7E26EAB89A210144A7F"}""" + .trimMargin() + val json2 = """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"b"}]},"negated":false}]},{"atoms": + |[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms":[{"lit": + |{"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments": + |[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable", + |"spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R", + |"arguments":[{"type":"Function","spelling":"f","arguments":[{"type": + |"Constant","spelling":"b"},{"type":"Constant","spelling":"a"}]}]}, + |"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Function", + |"spelling":"f","arguments":[{"type":"Constant","spelling":"b"},{"type": + |"Constant","spelling":"b"}]}]},"negated":true}]},{"atoms":[{"lit": + |{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]}, + |"negated":true},{"lit":{"spelling":"R","arguments":[{"type":"Constant", + |"spelling":"b"}]},"negated":true},{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit": + |{"spelling":"Q","arguments":[{"type":"QuantifiedVariable","spelling":"Y_7"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"Q","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":true}]},{"atoms":[{"lit":{ + |"spelling":"R","arguments":[{"type":"Function","spelling":"f","arguments": + |[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]}, + |"negated":true}]},{"atoms":[]},{"atoms":[]}]},"visualHelp":"HIGHLIGHT", + |"newestNode":10,"hiddenClauses":{"clauses":[]},"clauseCounter":11, + |"statusMessage":null,"lastMove":null, + |"seal":"73B2B4074EAAD533D36972CFB6AE9BA81AF3E3C492CC09B0D86125EBB6C4723F"}""" + .trimMargin() + val jsonInvalid1 = """{"clauseSet":{"clauses":[{"atoms":[{"lit": + |{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":false}]},{"atoms": + |[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Function","spelling":"f","arguments":[{"type":"Constant","spelling":"b"}, + |{"type":"QuantifiedVariable","spelling":"X_4"}]}]},"negated":false}]}, + |{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f", + |"arguments":[{"type":"Constant","spelling":"b"},{"type":"Constant", + |"spelling":"a"}]}]},"negated":true},{"lit":{"spelling":"R","arguments": + |[{"type":"Function","spelling":"f","arguments":[{"type":"Constant", + |"spelling":"b"},{"type":"Constant","spelling":"b"}]}]},"negated":true}]}, + |{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"a"}]}, + |"negated":true},{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"b"}]},"negated":true},{"lit": + |{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]}, + |{"atoms":[{"lit":{"spelling":"Q","arguments":[{"type":"QuantifiedVariable", + |"spelling":"Y_7"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"Q", + |"arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]}]}, + |"visualHelp":"HIGHLIGHT","newestNode":-1,"hiddenClauses":{"clauses":[]}, + |"clauseCounter":8,"statusMessage":null,"lastMove":null, + |"seal":"196976513C2CF3237A499CE786D4HELLODF97B1199D8C7E26EAB89A210144A7F"}""" + .trimMargin() + val jsonInvalid2 = """{"clauseSet":{"clauses":[{"atoms":[{"lit": + |{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]},false}]}, + |{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"a"}]},"negated":false}]},{"atoms": + |[{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f", + |"arguments":[{"type":"Constant","spelling":"b"},{"type":"QuantifiedVariable", + |"spelling":"X_4"}]}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R", + |"arguments":[{"type":"Function","spelling":"f","arguments":[{"type":"Constant", + |"spelling":"b"},{"type":"Constant","spelling":"a"}]}]},"negated":true}, + |{"lit":{"spelling":"R","arguments":[{"type":"Function","spelling":"f", + |"arguments":[{"type":"Constant","spelling":"b"}, + |{"type":"Constant","spelling":"b"}]}]},"negated":true}]}, + |{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"a"}]},"negated":true}, + |{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"b"}]}, + |"negated":true},{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":true}]}, + |{"atoms":[{"lit":{"spelling":"Q","arguments": + |[{"type":"QuantifiedVariable","spelling":"Y_7"}]},"negated":false}]}, + |{"atoms":[{"lit":{"spelling":"Q","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":true}]}, + |{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Function","spelling":"f","arguments": + |[{"type":"Constant","spelling":"b"},{"type":"Constant","spelling":"b"}]}]}, + |"negated":true}]},{"atoms":[]},{"atoms":[]}]},"visualHelp":"HIGHLIGHT", + |"newestNode":10,"hiddenClauses":{"clauses":[]},"clauseCounter":11, + |"statusMessage":null,"lastMove":null, + |"seal":"73B2B4074EAAD533D36972CFB6AE9BA81AF3E3C492CC09B0D86125EBB6C4723F"}""" + .trimMargin() val state1 = foInstance.jsonToState(json1) val state2 = foInstance.jsonToState(json2) - assertEquals(json1, foInstance.stateToJson(state1)) - assertEquals(json2, foInstance.stateToJson(state2)) + assertEquals(json1.replace("\n", ""), foInstance.stateToJson(state1)) + assertEquals(json2.replace("\n", ""), foInstance.stateToJson(state2)) assertFailsWith { foInstance.jsonToState(jsonInvalid1) } diff --git a/backend/src/test/kotlin/kalkulierbar/signedtableaux/TestPrune.kt b/backend/src/test/kotlin/kalkulierbar/signedtableaux/TestPrune.kt index 17b4062d0..b8aa65830 100644 --- a/backend/src/test/kotlin/kalkulierbar/signedtableaux/TestPrune.kt +++ b/backend/src/test/kotlin/kalkulierbar/signedtableaux/TestPrune.kt @@ -6,7 +6,7 @@ import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertFailsWith -class TestPruneMove { +class TestPrune { val instance = SignedModalTableaux() val parser = ModalLogicParser() diff --git a/backend/src/test/kotlin/kalkulierbar/statekeeper/TestAdmin.kt b/backend/src/test/kotlin/kalkulierbar/statekeeper/TestAdmin.kt index 69cea236d..7ee3c904d 100644 --- a/backend/src/test/kotlin/kalkulierbar/statekeeper/TestAdmin.kt +++ b/backend/src/test/kotlin/kalkulierbar/statekeeper/TestAdmin.kt @@ -125,20 +125,32 @@ class TestAdmin { @Test fun testExamples() { - var example = """{"name": "example1", "description": "Does some stuff", "calculus": "fo-resolution","formula": "/ex X: R(X)", "params": "Some params here"}""" + var example = """{"name": "example1", "description": "Does some stuff", + |"calculus": "fo-resolution","formula": "/ex X: R(X)", "params": "Some params here"}""" + .trimMargin() var fingerprint = "kbae|$example" var payloadWithKey = "$fingerprint|$date|$key" var mac = toHex(payloadWithKey.digestKeccak(parameter = KeccakParameter.SHA3_256)) StateKeeper.addExample(example, mac) - var expected = """{"disabled": [], "examples": [{"name":"example1","description":"Does some stuff","calculus":"fo-resolution","formula":"/ex X: R(X)","params":"Some params here"}]}""" + var expected = """{"disabled": [], "examples": + |[{"name":"example1","description":"Does some stuff", + |"calculus":"fo-resolution","formula":"/ex X: R(X)","params":"Some params here"}]}""" + .trimMargin().replace("\n", "") assertEquals(expected, StateKeeper.getConfig()) - example = """{"name": "example2", "description": "Does some crazy stuff", "calculus": "fo-tableaux","formula": "/all X: P(X)", "params": "Some params here"}""" + example = """{"name": "example2", "description": "Does some crazy stuff", + |"calculus": "fo-tableaux","formula": "/all X: P(X)", "params": "Some params here"}""" + .trimMargin() fingerprint = "kbae|$example" payloadWithKey = "$fingerprint|$date|$key" mac = toHex(payloadWithKey.digestKeccak(parameter = KeccakParameter.SHA3_256)) StateKeeper.addExample(example, mac) - expected = """{"disabled": [], "examples": [{"name":"example1","description":"Does some stuff","calculus":"fo-resolution","formula":"/ex X: R(X)","params":"Some params here"}, {"name":"example2","description":"Does some crazy stuff","calculus":"fo-tableaux","formula":"/all X: P(X)","params":"Some params here"}]}""" + expected = """{"disabled": [], "examples": + | [{"name":"example1","description":"Does some stuff","calculus":"fo-resolution", + |"formula":"/ex X: R(X)","params":"Some params here"}, + |{"name":"example2","description":"Does some crazy stuff", + |"calculus":"fo-tableaux","formula":"/all X: P(X)","params":"Some params here"}]}""" + .trimMargin().replace("\n", "") assertEquals(expected, StateKeeper.getConfig()) // Wrong ID @@ -172,14 +184,19 @@ class TestAdmin { payloadWithKey = "$fingerprint|$date|$key" mac = toHex(payloadWithKey.digestKeccak(parameter = KeccakParameter.SHA3_256)) StateKeeper.delExample(exampleIdString, mac) - expected = """{"disabled": [], "examples": [{"name":"example2","description":"Does some crazy stuff","calculus":"fo-tableaux","formula":"/all X: P(X)","params":"Some params here"}]}""" + expected = """{"disabled": [], "examples": + |[{"name":"example2","description":"Does some crazy stuff", + |"calculus":"fo-tableaux","formula":"/all X: P(X)","params":"Some params here"}]}""" + .trimMargin().replace("\n", "") assertEquals(expected, StateKeeper.getConfig()) } @Test fun testInvalidExample() { // Missing field - var example = """{"name": "example1", "calculus": "fo-resolution","formula": "/ex X: R(X)", "params": "Some params here"}""" + var example = """{"name": "example1", "calculus": "fo-resolution", + |"formula": "/ex X: R(X)", "params": "Some params here"} + """.trimMargin() var fingerprint = "kbae|$example" var payloadWithKey = "$fingerprint|$date|$key" var mac = toHex(payloadWithKey.digestKeccak(parameter = KeccakParameter.SHA3_256)) @@ -188,7 +205,9 @@ class TestAdmin { } // Wrong mac - example = """{"name": "example1", "description": "Does some stuff", "calculus": "fo-resolution","formula": "/ex X: R(X)", "params": "Some params here"}""" + example = """{"name": "example1", "description": "Does some stuff", + |"calculus": "fo-resolution","formula": "/ex X: R(X)", "params": "Some params here"}""" + .trimMargin() fingerprint = "kbae|$example" payloadWithKey = "$fingerprint|20200101|$key" mac = toHex(payloadWithKey.digestKeccak(parameter = KeccakParameter.SHA3_256)) diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt index 47dbbdf21..bf541eec8 100644 --- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt +++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestFirstOrderJson.kt @@ -51,17 +51,41 @@ class TestFirstOrderJson { @Test fun testJsonStateEmpty() { val json = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"QuantifiedVariable","spelling":"X"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"c"}]},"negated":true}]}]},"formula":"\\all X: R(X) & !R(c)","type":"UNCONNECTED","regular":false,"backtracking":false,"manualVarAssign":false,"tree":[{"parent":null,"relation":{"spelling":"true","arguments":[]},"negated":false,"isClosed":false,"closeRef":null,"children":[],"spelling":"true()"}],"moveHistory":[],"usedBacktracking":false,"expansionCounter":0,"seal":"47E0E51B486CDF0FEB644B195CFBCB08E61C2556BD67D84B86B08CB658055ACB","renderedClauseSet":["R(X)","!R(c)"]}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"QuantifiedVariable","spelling":"X"}]},"negated":false}]}, + |{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"c"}]},"negated":true}]}]}, + |"formula":"\\all X: R(X) & !R(c)","type":"UNCONNECTED","regular":false, + |"backtracking":false,"manualVarAssign":false,"tree": + |[{"parent":null,"relation":{"spelling":"true","arguments":[]}, + |"negated":false,"isClosed":false,"closeRef":null,"children":[], + |"spelling":"true()"}],"moveHistory":[],"usedBacktracking":false, + |"expansionCounter":0, + |"seal":"47E0E51B486CDF0FEB644B195CFBCB08E61C2556BD67D84B86B08CB658055ACB", + |"renderedClauseSet":["R(X)","!R(c)"]}""" + .trimMargin() val state = instance.jsonToState(json) val hash = - "fotableaux|\\all X: R(X) & !R(c)|0|UNCONNECTED|false|false|false|false|{R(X)}, {!R(c)}|[true();p;null;-;o;()]|[]" + "fotableaux|\\all X: R(X) & !R(c)|0|UNCONNECTED|false|false|false|false|{R(X)}, " + + "{!R(c)}|[true();p;null;-;o;()]|[]" assertEquals(hash, state.getHash()) } @Test fun testJsonStateModification() { val json = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"QuantifiedVariable","spelling":"X"}]},"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"q"}]},"negated":true}]}]},"formula":"\\all X: R(X) & !R(c)","type":"UNCONNECTED","regular":false,"backtracking":false,"manualVarAssign":false,"tree":[{"parent":null,"relation":{"spelling":"true","arguments":[]},"negated":false,"isClosed":false,"closeRef":null,"children":[],"spelling":"true()"}],"moveHistory":[],"usedBacktracking":false,"expansionCounter":0,"seal":"47E0E51B486CDF0FEB644B195CFBCB08E61C2556BD67D84B86B08CB658055ACB","renderedClauseSet":["R(X)","!R(c)"]}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit": + |{"spelling":"R","arguments":[{"type":"QuantifiedVariable","spelling":"X"}]}, + |"negated":false}]},{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"q"}]},"negated":true}]}]}, + |"formula":"\\all X: R(X) & !R(c)","type":"UNCONNECTED","regular":false, + |"backtracking":false,"manualVarAssign":false,"tree":[{"parent":null,"relation": + |{"spelling":"true","arguments":[]},"negated":false,"isClosed":false, + |"closeRef":null,"children":[],"spelling":"true()"}],"moveHistory":[], + |"usedBacktracking":false,"expansionCounter":0, + |"seal":"47E0E51B486CDF0FEB644B195CFBCB08E61C2556BD67D84B86B08CB658055ACB", + |"renderedClauseSet":["R(X)","!R(c)"]}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) } @@ -75,7 +99,17 @@ class TestFirstOrderJson { fun testStateToJson() { val json = instance.parseFormula("\\ex X: R(X)", null) val expected = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments":[{"type":"Constant","spelling":"sk1"}]},"negated":false}]}]},"formula":"\\ex X: R(X)","type":"UNCONNECTED","regular":false,"backtracking":false,"manualVarAssign":false,"tree":[{"parent":null,"relation":{"spelling":"true","arguments":[]},"negated":false,"lemmaSource":null,"isClosed":false,"closeRef":null,"children":[],"spelling":"true()"}],"moveHistory":[],"usedBacktracking":false,"expansionCounter":0,"seal":"22B8CEDC626EBF36DAAA3E50356CD328C075805A0538EA0F91B4C88658D8C465","renderedClauseSet":["R(sk1)"],"statusMessage":null}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit":{"spelling":"R","arguments": + |[{"type":"Constant","spelling":"sk1"}]},"negated":false}]}]}, + |"formula":"\\ex X: R(X)","type":"UNCONNECTED","regular":false, + |"backtracking":false,"manualVarAssign":false,"tree": + |[{"parent":null,"relation":{"spelling":"true","arguments":[]}, + |"negated":false,"lemmaSource":null,"isClosed":false,"closeRef":null, + |"children":[],"spelling":"true()"}],"moveHistory":[], + |"usedBacktracking":false,"expansionCounter":0, + |"seal":"22B8CEDC626EBF36DAAA3E50356CD328C075805A0538EA0F91B4C88658D8C465", + |"renderedClauseSet":["R(sk1)"],"statusMessage":null} + """.trimMargin().replace("\n", "") assertEquals(expected, json) } diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt index 07aab2033..58fba8d11 100644 --- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt +++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestPropositionalJson.kt @@ -51,10 +51,19 @@ class TestPropositionalJson { @Test fun testJsonStateEmpty() { val json = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false},{"lit":"b","negated":false}]},{"atoms":[{"lit":"a","negated":true}]},{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false,"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false,"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[],"backtracking":false,"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false}, + |{"lit":"b","negated":false}]},{"atoms":[{"lit":"a","negated":true}]}, + |{"atoms":[{"lit":"b","negated":true}]}]}, + |"type":"UNCONNECTED","regular":false,"backtracking":false, + |"tree":[{"parent":null,"spelling":"true","negated":false, + |"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[], + |"backtracking":false, + |"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + .trimMargin() val state = instance.jsonToState(json) assertEquals( - "tableauxstate|UNCONNECTED|false|false|false|{a, b}, {!a}, {!b}|[true;p;null;-;l;o;()]|[]", + "tableauxstate|UNCONNECTED|false|false|false|{a, b}, {!a}, {!b}|" + + "[true;p;null;-;l;o;()]|[]", state.getHash() ) } @@ -62,7 +71,15 @@ class TestPropositionalJson { @Test fun testJsonStateCorrupt() { val json = - """{"clauseSet":{"clauses":"atoms":[{"lit":"a","negated":false},{"lit":"b","negated":false}]},{"atoms":[{"lit":"a","negated":true}]},{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false,"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false,"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[],"backtracking":false,"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + """{"clauseSet":{"clauses":"atoms":[{"lit":"a","negated":false}, + |{"lit":"b","negated":false}]},{"atoms":[{"lit":"a","negated":true}]}, + |{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED", + |"regular":false,"backtracking":false,"tree": + |[{"parent":null,"spelling":"true","negated":false, + |"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[], + |"backtracking":false, + |"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) @@ -72,7 +89,15 @@ class TestPropositionalJson { @Test fun testJsonStateMissingField() { val json = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false},{negated":false}]},{"atoms":[{"lit":"a","negated":true}]},{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false,"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false,"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[],"backtracking":false,"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false}, + |{negated":false}]},{"atoms":[{"lit":"a","negated":true}]}, + |{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED", + |"regular":false,"backtracking":false,"tree": + |[{"parent":null,"spelling":"true","negated":false, + |"isClosed":false,"closeRef":null,"children":[]}], + |"moveHistory":[],"backtracking":false, + |"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) @@ -82,7 +107,14 @@ class TestPropositionalJson { @Test fun testJsonStateModify() { val json = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false},{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":true}]},{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false,"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false,"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[],"backtracking":false,"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit":"a","negated":false} + |,{"lit":"c","negated":false}]},{"atoms":[{"lit":"a","negated":true}]}, + |{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false, + |"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false, + |"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[], + |"backtracking":false, + |"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) } @@ -91,7 +123,14 @@ class TestPropositionalJson { @Test fun testJsonStateTypeMismatch() { val json = - """{"clauseSet":{"clauses":[{"atoms":[{"lit":3,"negated":false},{"lit":"b","negated":false}]},{"atoms":[{"lit":"a","negated":true}]},{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false,"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false,"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[],"backtracking":false,"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + """{"clauseSet":{"clauses":[{"atoms":[{"lit":3,"negated":false}, + |{"lit":"b","negated":false}]},{"atoms":[{"lit":"a","negated":true}]}, + |{"atoms":[{"lit":"b","negated":true}]}]},"type":"UNCONNECTED","regular":false, + |"backtracking":false,"tree":[{"parent":null,"spelling":"true","negated":false, + |"isClosed":false,"closeRef":null,"children":[]}],"moveHistory":[], + |"backtracking":false, + |"seal":"9FB4C2B77422E91BAEB40529CEEBB8660F54A2DA64E0E27BAAFD41E61819D9A1"}""" + .trimMargin() assertFailsWith { instance.jsonToState(json) diff --git a/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt b/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt index 7c631d97e..3107c6ecd 100644 --- a/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt +++ b/backend/src/test/kotlin/kalkulierbar/tableaux/TestUndoFO.kt @@ -7,7 +7,12 @@ import kotlin.test.assertEquals class TestUndoFO { val instance = FirstOrderTableaux() - private val param = FoTableauxParam(TableauxType.UNCONNECTED, regular = false, backtracking = true, manualVarAssign = false) + private val param = FoTableauxParam( + TableauxType.UNCONNECTED, + regular = false, + backtracking = true, + manualVarAssign = false + ) private val paramManual = FoTableauxParam( TableauxType.UNCONNECTED, regular = false,