|
| 1 | +import Logic from 'logic-solver'; |
| 2 | +import { match } from 'ts-pattern'; |
| 3 | +import type { |
| 4 | + CheckerConstraint, |
| 5 | + ComparisonConstraint, |
| 6 | + ComparisonTerm, |
| 7 | + LogicalConstraint, |
| 8 | + ValueConstraint, |
| 9 | + VariableConstraint, |
| 10 | +} from '../types'; |
| 11 | + |
| 12 | +/** |
| 13 | + * A boolean constraint solver based on `logic-solver`. Only boolean and integer types are supported. |
| 14 | + */ |
| 15 | +export class ConstraintSolver { |
| 16 | + // a table for internalizing string literals |
| 17 | + private stringTable: string[] = []; |
| 18 | + |
| 19 | + // a map for storing variable names and their corresponding formulas |
| 20 | + private variables: Map<string, Logic.Formula> = new Map<string, Logic.Formula>(); |
| 21 | + |
| 22 | + /** |
| 23 | + * Check the satisfiability of the given constraint. |
| 24 | + */ |
| 25 | + checkSat(constraint: CheckerConstraint): boolean { |
| 26 | + // reset state |
| 27 | + this.stringTable = []; |
| 28 | + this.variables = new Map<string, Logic.Formula>(); |
| 29 | + |
| 30 | + // convert the constraint to a "logic-solver" formula |
| 31 | + const formula = this.buildFormula(constraint); |
| 32 | + |
| 33 | + // solve the formula |
| 34 | + const solver = new Logic.Solver(); |
| 35 | + solver.require(formula); |
| 36 | + |
| 37 | + // DEBUG: |
| 38 | + // const solution = solver.solve(); |
| 39 | + // if (solution) { |
| 40 | + // console.log('Solution:'); |
| 41 | + // this.variables.forEach((v, k) => console.log(`\t${k}=${solution?.evaluate(v)}`)); |
| 42 | + // } else { |
| 43 | + // console.log('No solution'); |
| 44 | + // } |
| 45 | + |
| 46 | + return !!solver.solve(); |
| 47 | + } |
| 48 | + |
| 49 | + private buildFormula(constraint: CheckerConstraint): Logic.Formula { |
| 50 | + return match(constraint) |
| 51 | + .when( |
| 52 | + (c): c is ValueConstraint => c.kind === 'value', |
| 53 | + (c) => this.buildValueFormula(c) |
| 54 | + ) |
| 55 | + .when( |
| 56 | + (c): c is VariableConstraint => c.kind === 'variable', |
| 57 | + (c) => this.buildVariableFormula(c) |
| 58 | + ) |
| 59 | + .when( |
| 60 | + (c): c is ComparisonConstraint => ['eq', 'ne', 'gt', 'gte', 'lt', 'lte'].includes(c.kind), |
| 61 | + (c) => this.buildComparisonFormula(c) |
| 62 | + ) |
| 63 | + .when( |
| 64 | + (c): c is LogicalConstraint => ['and', 'or', 'not'].includes(c.kind), |
| 65 | + (c) => this.buildLogicalFormula(c) |
| 66 | + ) |
| 67 | + .otherwise(() => { |
| 68 | + throw new Error(`Unsupported constraint format: ${JSON.stringify(constraint)}`); |
| 69 | + }); |
| 70 | + } |
| 71 | + |
| 72 | + private buildLogicalFormula(constraint: LogicalConstraint) { |
| 73 | + return match(constraint.kind) |
| 74 | + .with('and', () => this.buildAndFormula(constraint)) |
| 75 | + .with('or', () => this.buildOrFormula(constraint)) |
| 76 | + .with('not', () => this.buildNotFormula(constraint)) |
| 77 | + .exhaustive(); |
| 78 | + } |
| 79 | + |
| 80 | + private buildAndFormula(constraint: LogicalConstraint): Logic.Formula { |
| 81 | + if (constraint.children.some((c) => this.isFalse(c))) { |
| 82 | + // short-circuit |
| 83 | + return Logic.FALSE; |
| 84 | + } |
| 85 | + return Logic.and(...constraint.children.map((c) => this.buildFormula(c))); |
| 86 | + } |
| 87 | + |
| 88 | + private buildOrFormula(constraint: LogicalConstraint): Logic.Formula { |
| 89 | + if (constraint.children.some((c) => this.isTrue(c))) { |
| 90 | + // short-circuit |
| 91 | + return Logic.TRUE; |
| 92 | + } |
| 93 | + return Logic.or(...constraint.children.map((c) => this.buildFormula(c))); |
| 94 | + } |
| 95 | + |
| 96 | + private buildNotFormula(constraint: LogicalConstraint) { |
| 97 | + if (constraint.children.length !== 1) { |
| 98 | + throw new Error('"not" constraint must have exactly one child'); |
| 99 | + } |
| 100 | + return Logic.not(this.buildFormula(constraint.children[0])); |
| 101 | + } |
| 102 | + |
| 103 | + private isTrue(constraint: CheckerConstraint): unknown { |
| 104 | + return constraint.kind === 'value' && constraint.value === true; |
| 105 | + } |
| 106 | + |
| 107 | + private isFalse(constraint: CheckerConstraint): unknown { |
| 108 | + return constraint.kind === 'value' && constraint.value === false; |
| 109 | + } |
| 110 | + |
| 111 | + private buildComparisonFormula(constraint: ComparisonConstraint) { |
| 112 | + if (constraint.left.kind === 'value' && constraint.right.kind === 'value') { |
| 113 | + // constant comparison |
| 114 | + const left: ValueConstraint = constraint.left; |
| 115 | + const right: ValueConstraint = constraint.right; |
| 116 | + return match(constraint.kind) |
| 117 | + .with('eq', () => (left.value === right.value ? Logic.TRUE : Logic.FALSE)) |
| 118 | + .with('ne', () => (left.value !== right.value ? Logic.TRUE : Logic.FALSE)) |
| 119 | + .with('gt', () => (left.value > right.value ? Logic.TRUE : Logic.FALSE)) |
| 120 | + .with('gte', () => (left.value >= right.value ? Logic.TRUE : Logic.FALSE)) |
| 121 | + .with('lt', () => (left.value < right.value ? Logic.TRUE : Logic.FALSE)) |
| 122 | + .with('lte', () => (left.value <= right.value ? Logic.TRUE : Logic.FALSE)) |
| 123 | + .exhaustive(); |
| 124 | + } |
| 125 | + |
| 126 | + return match(constraint.kind) |
| 127 | + .with('eq', () => this.transformEquality(constraint.left, constraint.right)) |
| 128 | + .with('ne', () => this.transformInequality(constraint.left, constraint.right)) |
| 129 | + .with('gt', () => |
| 130 | + this.transformComparison(constraint.left, constraint.right, (l, r) => Logic.greaterThan(l, r)) |
| 131 | + ) |
| 132 | + .with('gte', () => |
| 133 | + this.transformComparison(constraint.left, constraint.right, (l, r) => Logic.greaterThanOrEqual(l, r)) |
| 134 | + ) |
| 135 | + .with('lt', () => |
| 136 | + this.transformComparison(constraint.left, constraint.right, (l, r) => Logic.lessThan(l, r)) |
| 137 | + ) |
| 138 | + .with('lte', () => |
| 139 | + this.transformComparison(constraint.left, constraint.right, (l, r) => Logic.lessThanOrEqual(l, r)) |
| 140 | + ) |
| 141 | + .exhaustive(); |
| 142 | + } |
| 143 | + |
| 144 | + private buildVariableFormula(constraint: VariableConstraint) { |
| 145 | + return ( |
| 146 | + match(constraint.type) |
| 147 | + .with('boolean', () => this.booleanVariable(constraint.name)) |
| 148 | + .with('number', () => this.intVariable(constraint.name)) |
| 149 | + // strings are internalized and represented by their indices |
| 150 | + .with('string', () => this.intVariable(constraint.name)) |
| 151 | + .exhaustive() |
| 152 | + ); |
| 153 | + } |
| 154 | + |
| 155 | + private buildValueFormula(constraint: ValueConstraint) { |
| 156 | + return match(constraint.value) |
| 157 | + .when( |
| 158 | + (v): v is boolean => typeof v === 'boolean', |
| 159 | + (v) => (v === true ? Logic.TRUE : Logic.FALSE) |
| 160 | + ) |
| 161 | + .when( |
| 162 | + (v): v is number => typeof v === 'number', |
| 163 | + (v) => Logic.constantBits(v) |
| 164 | + ) |
| 165 | + .when( |
| 166 | + (v): v is string => typeof v === 'string', |
| 167 | + (v) => { |
| 168 | + // internalize the string and use its index as formula representation |
| 169 | + const index = this.stringTable.indexOf(v); |
| 170 | + if (index === -1) { |
| 171 | + this.stringTable.push(v); |
| 172 | + return Logic.constantBits(this.stringTable.length - 1); |
| 173 | + } else { |
| 174 | + return Logic.constantBits(index); |
| 175 | + } |
| 176 | + } |
| 177 | + ) |
| 178 | + .exhaustive(); |
| 179 | + } |
| 180 | + |
| 181 | + private booleanVariable(name: string) { |
| 182 | + this.variables.set(name, name); |
| 183 | + return name; |
| 184 | + } |
| 185 | + |
| 186 | + private intVariable(name: string) { |
| 187 | + const r = Logic.variableBits(name, 32); |
| 188 | + this.variables.set(name, r); |
| 189 | + return r; |
| 190 | + } |
| 191 | + |
| 192 | + private transformEquality(left: ComparisonTerm, right: ComparisonTerm) { |
| 193 | + if (left.type !== right.type) { |
| 194 | + throw new Error(`Type mismatch in equality constraint: ${JSON.stringify(left)}, ${JSON.stringify(right)}`); |
| 195 | + } |
| 196 | + |
| 197 | + const leftFormula = this.buildFormula(left); |
| 198 | + const rightFormula = this.buildFormula(right); |
| 199 | + if (left.type === 'boolean' && right.type === 'boolean') { |
| 200 | + // logical equivalence |
| 201 | + return Logic.equiv(leftFormula, rightFormula); |
| 202 | + } else { |
| 203 | + // integer equality |
| 204 | + return Logic.equalBits(leftFormula, rightFormula); |
| 205 | + } |
| 206 | + } |
| 207 | + |
| 208 | + private transformInequality(left: ComparisonTerm, right: ComparisonTerm) { |
| 209 | + return Logic.not(this.transformEquality(left, right)); |
| 210 | + } |
| 211 | + |
| 212 | + private transformComparison( |
| 213 | + left: ComparisonTerm, |
| 214 | + right: ComparisonTerm, |
| 215 | + func: (left: Logic.Formula, right: Logic.Formula) => Logic.Formula |
| 216 | + ) { |
| 217 | + return func(this.buildFormula(left), this.buildFormula(right)); |
| 218 | + } |
| 219 | +} |
0 commit comments