Added automatic value assignment, fixes #69

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);
 		}
 

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<number>();
 		}
 
@@ -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);
 				}
 

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(