Class: Kumi::Core::Analyzer::Passes::UnsatDetectorPass

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

Constant Summary collapse

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

Constants inherited from PassBase

PassBase::HALT

Instance Method Summary collapse

Methods inherited from VisitorPass

#visit

Methods inherited from PassBase

contract_declared?, #debug, #debug_enabled?, declared_optional_reads, declared_reads, declared_writes, #initialize, optional_reads, reads, writes

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 



14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
 
# File 'lib/kumi/core/analyzer/passes/unsat_detector_pass.rb', line 14

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