Class: Kumi::Core::Analyzer::Passes::UnsatDetector

Inherits:
VisitorPass show all
Includes:
Syntax
Defined in:
lib/kumi/core/analyzer/passes/unsat_detector.rb

Overview

RESPONSIBILITY: Detect unsatisfiable constraints using formal constraint semantics DEPENDENCIES: :declarations, :input_metadata, :registry, SNAST representation INTERFACE: new(schema, state).run(errors)

Detects when constraints are clearly unsatisfiable using constraint propagation:

  1. Same variable with contradicting equality values (v == 5 AND v == 10)

  2. Values violating input domain constraints

  3. Constraints derived through arithmetic operations that violate domains

Constant Summary collapse

COMPARATORS = 
i[> < >= <= == !=].freeze

Instance Method Summary collapse

Methods inherited from VisitorPass

#visit

Methods inherited from PassBase

#debug, #debug_enabled?, #initialize

Methods included from ErrorReporting

#inferred_location, #raise_localized_error, #raise_syntax_error, #raise_type_error, #report_enhanced_error, #report_error, #report_semantic_error, #report_syntax_error, #report_type_error

Constructor Details

This class inherits a constructor from Kumi::Core::Analyzer::Passes::PassBase

Instance Method Details

#run(errors) ⇒ Object 



20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
 
# File 'lib/kumi/core/analyzer/passes/unsat_detector.rb', line 20

def run(errors)
  definitions = get_state(:declarations)
  input_meta = get_state(:input_metadata) || {}
  registry = get_state(:registry)

  @propagator = FormalConstraintPropagator.new(schema, state)

  each_decl do |decl|
    # Only check trait declarations for obvious contradictions
    next unless decl.is_a?(TraitDeclaration)

    atoms = extract_equality_atoms(decl.expression, definitions)
    next if atoms.empty?

    # Check for formal, obvious contradictions
    next unless contradicting_equalities?(atoms) || domain_violations?(atoms, input_meta) ||
                propagated_violations?(atoms, definitions, input_meta, registry)

    report_error(
      errors,
      "conjunction `#{decl.name}` is impossible",
      location: decl.loc
    )
  end

  state
end