Package ch.so.agi.mcp.constraint

Class ConstraintGoalSolver

java.lang.Object

ch.so.agi.mcp.constraint.ConstraintGoalSolver

public final class ConstraintGoalSolver
extends Object

Small deterministic finite-domain solver for semantic constraint test goals.

The solver derives interesting values from INTERLIS model domains and IR literals, searches a bounded cartesian product and validates every candidate assignment through ConstraintModelSynthesizer. Simple numeric equalities additionally drive candidate derivation backwards through ADD/SUB/MUL/DIV and COLLECTION_SUM instead of relying on unrelated literal/pivot guesses. It is deliberately not a complete SMT solver. Search exhaustion is reported explicitly so a later solver strategy (for example Z3) can replace or complement it without changing the IR or object-graph layers.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final record	ConstraintGoalSolver.Solution

Method Summary

Modifier and Type	Method	Description
static ConstraintGoalSolver.Solution	solve(ConstraintExpressionEngine.TestGoal goal, ConstraintModelSynthesizer.ModelBinding binding)
static ConstraintGoalSolver.Solution	solve(ConstraintExpressionEngine.TestGoal goal, ConstraintModelSynthesizer.ModelBinding binding, Map<String,Object> fixed)	Existing key and reference assignments are immutable during scoped population search.
static ConstraintGoalSolver.Solution	solve(ConstraintExpressionEngine.TestGoal goal, ConstraintModelSynthesizer.ModelBinding binding, Map<String,Object> fixed, ConstraintModelSynthesizer.CountShape shape)
static List<ConstraintGoalSolver.Solution>	solveAll(ConstraintExpression expression, ConstraintModelSynthesizer.ModelBinding binding)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

solve

public static ConstraintGoalSolver.Solution solve(ConstraintExpressionEngine.TestGoal goal,
 ConstraintModelSynthesizer.ModelBinding binding)

solve

public static ConstraintGoalSolver.Solution solve(ConstraintExpressionEngine.TestGoal goal,
 ConstraintModelSynthesizer.ModelBinding binding,
 Map<String,Object> fixed)

Existing key and reference assignments are immutable during scoped population search.

solve

public static ConstraintGoalSolver.Solution solve(ConstraintExpressionEngine.TestGoal goal,
 ConstraintModelSynthesizer.ModelBinding binding,
 Map<String,Object> fixed,
 ConstraintModelSynthesizer.CountShape shape)

solveAll

public static List<ConstraintGoalSolver.Solution> solveAll(ConstraintExpression expression,
 ConstraintModelSynthesizer.ModelBinding binding)