diff --git a/src/common/statement.ts b/src/common/statement.ts index 4a548fc..46bf53b 100644 --- a/src/common/statement.ts +++ b/src/common/statement.ts @@ -462,7 +462,6 @@ export class ExistenceStatement extends QuantifierStatement { symbolized(variables: Formula[] = []): Statement { if (variables.length === 0) { - // not a nested quantifier return this.formula.symbolized(this.variables, REPLACEMENT_SYMBOL); } @@ -488,7 +487,6 @@ export class UniversalStatement extends QuantifierStatement { symbolized(variables: Formula[] = []): Statement { if (variables.length === 0) { - // not a nested quantifier return this.formula.symbolized(this.variables, REPLACEMENT_SYMBOL); } diff --git a/src/common/tree.ts b/src/common/tree.ts index dc79145..b4cfe10 100644 --- a/src/common/tree.ts +++ b/src/common/tree.ts @@ -307,6 +307,8 @@ export class TruthTreeNode { universe = this.tree.nodes[this.parent].universe!; } + console.log(this.statement.getNewConstants(universe)); + return this.statement.getNewConstants(universe); } @@ -392,7 +394,14 @@ export class TruthTreeNode { } if (this.statement instanceof UniversalStatement) { - console.log('Universal statements do not have correct decompositions'); + // This will occur due to the way that get/set are implemented under + // the hood. When a setter is called, it attempts to access the old + // value using the getter, which will trigger this code flow. + // It is not harmful but still not intended. + console.error( + 'This error can likely be ignored: Universal statements do ' + + 'not have correct decompositions' + ); return new Set(); } @@ -829,6 +838,29 @@ export class TruthTreeNode { break; } + if ( + Object.keys(assignment).length !== this.statement.variables.length + ) { + // If the assignment does not have an assignment for every variable + // then arbitrarily assign a value from the universe. If one doesn't + // exist then arbitrarily assign the constant 'x' + + let value: Formula; + // Check universe for arbitrarily value + if (leafNode.universe!.length > 0) { + value = leafNode.universe!.values().next().value; + } else { + value = new Formula('x'); + } + + for (const variable of this.statement.variables) { + if (Object.keys(assignment).includes(variable.toString())) { + continue; + } + assignment[variable.toString()] = value; + } + } + deleteMapping(uninstantiated, assignment, this.statement.variables); } diff --git a/src/common/util.ts b/src/common/util.ts index 2957a53..4d95673 100644 --- a/src/common/util.ts +++ b/src/common/util.ts @@ -19,8 +19,8 @@ export interface EvaluationResponse { * Effectively, if there are |U| elements in the universe, then the N-dimensional * map will have |U|^N elements. * - * @param num_dims N - the number of dimensions (variables) - * @param universe U - the set of constants + * @param num_dims the number of dimensions N, typically the number of variables + * @param universe the set of constants U * @returns an N-dimensional map representing every N-tuple of the elements in the universe */ export function createNDimensionalMapping(