numeric

package
v1.5.4 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Feb 7, 2026 License: MIT Imports: 5 Imported by: 0

Documentation

Overview

domain.go implements the numeric subdomain for the flow solver's ProductDomain.

The numeric Domain tracks integer constraints (bounds, orderings, modular residues) and integrates State (compact storage) with TheorySolver (transitive inference). It satisfies the domain.Domain interface for use in the constraint solving framework.

Package numeric provides abstract interpretation for numeric constraints.

This package implements a theory solver for integer arithmetic, tracking:

  • Interval bounds: lower and upper limits for variables
  • Modular residues: congruence relations (x % m == r)
  • Difference constraints: relationships between pairs (x - y <= c)
  • Symbolic length bounds: array length references

The solver uses Bellman-Ford to detect unsatisfiable constraint sets via negative cycle detection in the difference constraint graph.

theory.go provides SMT-style theory solving for numeric constraints.

The TheorySolver bridges the compact State representation to more sophisticated theory solvers that can perform transitive inference and consistency checking. It wraps two solvers:

  • DifferenceGraph: Implements difference-bound matrix (DBM) analysis for transitive reasoning about inequalities. Detects unsatisfiability via negative cycle detection.

  • ModularSolver: Handles modular arithmetic constraints (x % m == r) and range-modular consistency checking.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func BoundsForWithTheory 

func BoundsForWithTheory(s *State, key constraint.PathKey) (lower, upper int64, ok bool)

BoundsForWithTheory returns bounds using theory solver for transitive inference.

This combines direct bounds from the State with transitive bounds inferred by the theory solver. The result is the tightest bounds available from both sources.

More expensive than State.BoundsFor due to solver construction, but may produce tighter bounds when variables are constrained relative to each other.

func CountModularValues 

func CountModularValues(s *State, key constraint.PathKey, modulus, residue int64) int64

CountModularValues counts values in a variable's range satisfying x % m == r.

Uses the theory solver to count how many integers in the variable's range satisfy the modular constraint. Returns -1 if the count cannot be determined (e.g., modulus <= 0 or state is nil).

func InferRelationalBound 

func InferRelationalBound(s *State, x, y constraint.PathKey) (int64, bool)

InferRelationalBound derives the tightest x - y <= c from transitive constraints.

Convenience function that creates a theory solver from the state and queries for the relational bound. Returns (0, false) if the state has no relations or if no bound can be inferred.

Types

type Domain 

type Domain struct {
	// contains filtered or unexported fields
}

Domain implements the numeric subdomain for ProductDomain.

Domain tracks numeric constraints and bounds for variables. It combines two complementary analysis components:

  • State: Tracks bounds (lower/upper), orderings (x < y), and modular constraints (x ≡ r mod m) for each path key.

  • TheorySolver: Implements difference-bound matrix (DBM) analysis for transitive reasoning about inequalities. Detects unsatisfiability when constraints form negative cycles.

Supported constraints:

  • Lt (x < y): Strict ordering, translated to difference constraint x - y ≤ -1
  • Le (x ≤ y): Non-strict ordering, translated to x - y ≤ 0
  • Gt (x > y): Strict ordering, translated to y - x ≤ -1
  • Ge (x ≥ y): Non-strict ordering, translated to y - x ≤ 0
  • Eq (x = c): Exact value, sets both lower and upper bounds to c
  • ModEq (x ≡ r mod m): Modular arithmetic constraint

When combined with type narrowing, numeric domain enables patterns like: 

if x >= 0 and x <= 10 then
    -- x is known to be in range [0, 10]
end

The domain maintains soundness by eagerly checking the theory solver after each constraint application. If constraints are mutually unsatisfiable (e.g., x > 10 and x < 5), the domain becomes UNSAT.

func NewDomain 

func NewDomain(env constraint.Env) *Domain

NewDomain creates a new numeric Domain with empty state.

Both State and TheorySolver are initialized empty. Constraints are added via ApplyAtom calls.

func (*Domain) ApplyAtom 

func (d *Domain) ApplyAtom(atom constraint.Atom) bool

ApplyAtom applies a numeric constraint atom to the domain.

The atom is applied to both State (for bounds tracking) and TheorySolver (for transitive reasoning). After application, satisfiability is checked.

Supported atoms:

  • AtomKindLt: x < y (variable-variable comparison)
  • AtomKindLe: x ≤ y or x ≤ c (variable-variable or variable-constant)
  • AtomKindGe: x ≥ y or x ≥ c (variable-variable or variable-constant)
  • AtomKindGt: x > y (variable-variable comparison)
  • AtomKindEq: x = c or x = y (equality constraint)
  • AtomKindModEq: x ≡ r (mod m) (modular arithmetic)

Returns false if the constraint makes the domain unsatisfiable.

func (*Domain) BoundsForWithTheory 

func (d *Domain) BoundsForWithTheory(key constraint.PathKey) (lower, upper int64, ok bool)

BoundsForWithTheory returns bounds after transitive inference via the theory solver.

This method uses the difference graph to derive tighter bounds from ordering constraints. For example, if x <= y and y <= 10, the method infers x <= 10 even without a direct bound on x.

Returns (lower, upper, true) if bounds exist (direct or inferred), or (0, 0, false) if no bounds are known or can be inferred.

func (*Domain) Clone 

func (d *Domain) Clone() domain.Domain

Clone creates a deep copy of the Domain for speculative evaluation.

Both State and TheorySolver are cloned to ensure independent modification.

func (*Domain) IsUnsat 

func (d *Domain) IsUnsat() bool

IsUnsat returns true if numeric constraints are unsatisfiable.

func (*Domain) Join 

func (d *Domain) Join(other domain.Domain) domain.Domain

Join computes the least upper bound of two numeric domains.

Join semantics for numeric constraints:

  • Bounds are widened: lower = min(d.lower, o.lower), upper = max(d.upper, o.upper)
  • Only orderings present in BOTH domains are preserved
  • Modular constraints are intersected

The TheorySolver is rebuilt from the joined State to ensure consistency.

func (*Domain) State 

func (d *Domain) State() *State

State returns the underlying State for direct inspection.

Provides access to the compact constraint storage for debugging, testing, or advanced queries. The returned State should not be modified directly; use Domain methods for constraint application.

func (*Domain) Theory 

func (d *Domain) Theory() *TheorySolver

Theory returns the underlying TheorySolver for direct inspection.

Provides access to the theory solver for debugging, testing, or advanced queries. The returned solver should not be modified directly outside of Domain method calls.

func (*Domain) TightenWithTheory 

func (d *Domain) TightenWithTheory() *Domain

TightenWithTheory returns a new Domain with bounds tightened via transitive closure.

Applies the theory solver's transitive inference to compute tighter bounds for all variables. The original domain is not modified.

This is useful for producing a "final" domain with maximum precision before querying bounds. Note that this can be expensive for large constraint sets.

type Interval 

type Interval struct {
	Lower int64
	Upper int64
}

Interval represents a closed integer interval [lower, upper].

Special values:

  • Lower = MinInt64: unbounded below (negative infinity)
  • Upper = MaxInt64: unbounded above (positive infinity)

An interval with Lower > Upper represents an empty (unsatisfiable) set.

type ModResidue 

type ModResidue struct {
	Modulus int64
	Residue int64
}

ModResidue represents a modular arithmetic constraint: x % modulus == residue.

For example, ModResidue{Modulus: 2, Residue: 0} represents even numbers.

type State 

type State struct {
	// contains filtered or unexported fields
}

State represents a compact abstract state for numeric constraints.

Uses interval bounds and modular residues instead of storing raw constraints. All maps use constraint.PathKey for versioned variable identity.

The state supports lattice operations: Join computes the intersection of facts (for control flow merge), and constraint application refines the state.

func Bottom 

func Bottom() *State

Bottom returns the unsatisfiable state (bottom of the lattice).

A Bottom state represents a contradiction: the constraints are mutually unsatisfiable. Any path condition that reaches Bottom is unreachable.

func Join 

func Join(a, b *State) *State

Join computes the intersection of two states for control flow merge.

At join points (phi nodes), we keep only facts that hold on all incoming paths. This is the meet operation in the abstract interpretation lattice:

  • Bounds: Keep variables present in both, take interval intersection. If Lower > Upper after intersection, result is Bottom (unsatisfiable).

  • Modular: Keep only identical modular constraints from both states. Different modular constraints on the same variable are incompatible.

  • Relations: Keep constraints present in both, take maximum (loosest) bound. max(a.relations[k], b.relations[k]) represents the weakest constraint that holds on both paths.

  • LenRefs: Keep only identical length references from both states.

If both states are nil or Bottom, returns the non-Bottom one. If the result is Top (empty maps), returns nil to save memory.

func NewState 

func NewState() *State

NewState creates an empty (top) numeric state.

func TightenWithTheory 

func TightenWithTheory(s *State) *State

TightenWithTheory uses theory solvers to compute tighter bounds via transitive closure.

The theory solver can derive bounds that aren't directly stored in the State. This function applies those inferences to produce a new State with tighter bounds.

Returns:

  • A new State with improved bounds (if any tightening occurred)
  • Bottom state if transitive closure proves unsatisfiability
  • The original state if no improvement is possible

func (*State) ApplyConstraintWithResolver 

func (s *State) ApplyConstraintWithResolver(c constraint.NumericConstraint, resolve constraint.PathResolver)

ApplyConstraintWithResolver refines the state with a numeric constraint.

Uses the provided resolver to convert constraint paths to versioned PathKeys. The resolver maps paths to their SSA versions at the current CFG point, ensuring constraints bind to the correct variable incarnation. If resolution fails (returns empty key), the constraint is silently skipped.

func (*State) ApplyEq 

func (s *State) ApplyEq(x, y constraint.PathKey)

func (*State) ApplyEqConst 

func (s *State) ApplyEqConst(v constraint.PathKey, c int64)

func (*State) ApplyGe 

func (s *State) ApplyGe(x, y constraint.PathKey)

func (*State) ApplyGeConst 

func (s *State) ApplyGeConst(v constraint.PathKey, c int64)

func (*State) ApplyGt 

func (s *State) ApplyGt(x, y constraint.PathKey)

func (*State) ApplyLe 

func (s *State) ApplyLe(x, y constraint.PathKey)

func (*State) ApplyLeConst 

func (s *State) ApplyLeConst(v constraint.PathKey, c int64)

func (*State) ApplyLeLenOf 

func (s *State) ApplyLeLenOf(v, arr constraint.PathKey)

func (*State) ApplyLt 

func (s *State) ApplyLt(x, y constraint.PathKey)

func (*State) ApplyModEq 

func (s *State) ApplyModEq(v constraint.PathKey, m, r int64)

func (*State) Bounds 

func (s *State) Bounds() map[constraint.PathKey]Interval

Bounds returns the raw bounds map for theory solver initialization.

This provides direct access to the bounds map for building the theory solver's difference graph. The returned map should not be modified.

func (*State) BoundsFor 

func (s *State) BoundsFor(key constraint.PathKey) (lower, upper int64, ok bool)

BoundsFor returns the interval bounds for a PathKey.

Returns (lower, upper, true) if the key has known bounds, or (0, 0, false) if the key has no constraints. This is the direct lookup without transitive inference; use BoundsForWithTheory for tighter bounds via transitive closure.

func (*State) CheckSatisfiability 

func (s *State) CheckSatisfiability() bool

CheckSatisfiability verifies the state has no contradictions.

Checks interval bounds for consistency (lower <= upper) and uses Bellman-Ford to detect negative cycles in the difference constraint graph. A negative cycle indicates an unsatisfiable constraint set.

func (*State) Clone 

func (s *State) Clone() *State

Clone creates a deep copy of the state for speculative evaluation.

All internal maps are copied so modifications to the clone don't affect the original. Used during disjunction evaluation where each branch needs its own independent state.

func (*State) Equals 

func (s *State) Equals(other *State) bool

Equals checks if two states are semantically equal.

Two states are equal if they have the same unsat flag and identical maps for bounds, modular constraints, relations, and length references. nil and Top (empty maps) states are considered equal.

func (*State) IsTop 

func (s *State) IsTop() bool

IsTop returns true if the state is Top (no constraints, all values possible).

func (*State) IsUnsat 

func (s *State) IsUnsat() bool

IsUnsat returns true if the state represents a contradiction.

An unsatisfiable state indicates that the combination of numeric constraints has no solution. This can happen when bounds conflict (x > 5 AND x < 3) or when difference constraints form a negative cycle.

func (*State) LenRefFor 

func (s *State) LenRefFor(key constraint.PathKey) (arrKey constraint.PathKey, ok bool)

LenRefFor returns the array key if variable has a symbolic length bound.

A length reference means "key <= #arrKey" (variable is bounded by array length). This is used to prove array access safety when the index is bounded by the array.

func (*State) Modular 

func (s *State) Modular() map[constraint.PathKey]ModResidue

Modular returns the raw modular constraints map.

Each entry maps a path key to its modular residue constraint. The returned map should not be modified.

func (*State) Rekey 

func (s *State) Rekey(remap map[constraint.PathKey]constraint.PathKey) *State

Rekey creates a new state with keys remapped according to the provided mapping.

At phi nodes, SSA versions from different predecessors merge into new versions. This method renames constraints to use the merged version keys, enabling proper constraint propagation across phi boundaries.

func (*State) Relations 

func (s *State) Relations() map[constraint.PathKey]map[constraint.PathKey]int64

Relations returns the raw relations map for theory solver initialization.

The map is transformed from the internal flat format (relationKey -> int64) to a nested format (X -> Y -> int64) for easier iteration. Each entry represents a difference constraint X - Y <= C.

func (*State) SetUnsat 

func (s *State) SetUnsat()

SetUnsat marks the state as unsatisfiable (contradiction detected).

Once unsat, the state remains unsat regardless of further constraint applications. This is used when external analysis (theory solver) detects unsatisfiability that wasn't caught by local constraint application.

type TheorySolver 

type TheorySolver struct {
	// contains filtered or unexported fields
}

TheorySolver bridges State to SMT-style theory solvers.

The solver maintains two components:

  • diff: DifferenceGraph for inequality reasoning (x - y <= c)
  • mod: ModularSolver for modular arithmetic (x % m == r)

These are kept synchronized with State constraints and provide additional inference capabilities beyond what State tracks directly.

func NewTheorySolver 

func NewTheorySolver() *TheorySolver

NewTheorySolver creates a new TheorySolver with empty solvers.

The solvers must be populated via LoadFromState or individual Add* methods before queries will return meaningful results.

func ToTheorySolver 

func ToTheorySolver(s *State) *TheorySolver

ToTheorySolver creates a TheorySolver initialized with a state's constraints.

This is a convenience function that creates a new solver and loads all constraints from the given state in one operation.

func (*TheorySolver) AddBounds 

func (t *TheorySolver) AddBounds(key constraint.PathKey, lower, upper int64)

AddBounds adds lower and upper bounds for a variable.

If lower == upper, the variable has a known constant value, which is also added as a modular equality for enhanced modular reasoning.

Bounds at +/- maxWeight are treated as unbounded and not added.

func (*TheorySolver) AddConstraintWithResolver 

func (t *TheorySolver) AddConstraintWithResolver(nc constraint.NumericConstraint, resolve constraint.PathResolver)

AddConstraintWithResolver adds a numeric constraint using versioned keys.

The resolver converts constraint paths to versioned PathKeys at a specific CFG point, ensuring constraints bind to the correct SSA versions. If any path resolution fails (returns empty key), the constraint is silently skipped.

Supports all standard numeric constraint types: Le, Lt, Ge, Gt, Eq, EqConst, LeConst, GeConst. Each is translated to appropriate difference graph operations.

func (*TheorySolver) AddDifferenceConstraint 

func (t *TheorySolver) AddDifferenceConstraint(x, y constraint.PathKey, c int64)

AddDifferenceConstraint adds a difference constraint x - y <= c directly.

This is the primitive operation for the difference graph. All comparison operators are translated to this form:

  • x < y becomes x - y <= -1
  • x <= y becomes x - y <= 0
  • x > y becomes y - x <= -1
  • x >= y becomes y - x <= 0
  • x == y becomes both x - y <= 0 and y - x <= 0

func (*TheorySolver) AddModular 

func (t *TheorySolver) AddModular(key constraint.PathKey, modulus, residue int64)

AddModular adds a modular constraint x % m == r.

Modular constraints are tracked for consistency checking and cardinality reasoning but don't feed directly into the difference graph. They are used in combination with range bounds for modular-range consistency.

func (*TheorySolver) CheckModularConsistency 

func (t *TheorySolver) CheckModularConsistency(key constraint.PathKey, modulus, residue int64) bool

CheckModularConsistency checks if x % modulus == residue is consistent with known bounds.

The modular solver checks if there exists at least one value in the variable's range that satisfies the modular constraint. Returns false if no such value exists.

func (*TheorySolver) CheckSatisfiability 

func (t *TheorySolver) CheckSatisfiability() bool

CheckSatisfiability checks if the current constraints are satisfiable.

Uses the difference graph's negative cycle detection. A negative cycle in the constraint graph means the constraints are mutually unsatisfiable (e.g., x > y > z > x implies x > x, a contradiction).

func (*TheorySolver) Clone 

func (t *TheorySolver) Clone() *TheorySolver

Clone creates a deep copy of the solver for speculative evaluation.

Both underlying solvers are cloned to ensure independent modification.

func (*TheorySolver) CountModularInRange 

func (t *TheorySolver) CountModularInRange(key constraint.PathKey, modulus, residue int64) int64

CountModularInRange counts values in a variable's range satisfying x % m == r.

This is used for cardinality reasoning: if the count is 0, the constraint is unsatisfiable; if the count is 1, the variable is uniquely determined.

func (*TheorySolver) InferBounds 

func (t *TheorySolver) InferBounds(key constraint.PathKey) (lower, upper int64, ok bool)

InferBounds uses the difference graph to derive tighter bounds via transitive closure.

The difference graph can infer bounds that aren't directly stored. For example, if x <= y and y <= 10, then x <= 10 even without a direct bound on x.

Returns the inferred interval (lower, upper, true) or (0, 0, false) if no bounds can be derived for the key.

func (*TheorySolver) InferRelationalBound 

func (t *TheorySolver) InferRelationalBound(x, y constraint.PathKey) (int64, bool)

InferRelationalBound derives the tightest x - y <= c from transitive constraints.

This uses the difference graph's transitive closure to find the minimum value of c such that x - y <= c is implied by all constraints. This is stronger than just looking up direct relations.

func (*TheorySolver) LoadFromState 

func (t *TheorySolver) LoadFromState(s *State)

LoadFromState populates theory solvers from a numeric State.

Transfers all constraints from the State to the theory solvers:

  • Bounds become upper/lower bound constraints in the difference graph
  • Exact bounds (lower == upper) also become modular equality constraints
  • Relations become difference constraints in the graph
  • Modular constraints are noted but handled via range+residue

This enables transitive inference not available in the raw State.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.