proof_attempt.rb revision 353f5670601cd45216a420745dded50a73ac5616
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch belongs_to :theorem, foreign_key: 'sentence_id'
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch has_one :axiom_selection, through: :proof_attempt_configuration
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch has_many :generated_axioms, dependent: :destroy
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch validates :state, inclusion: {in: State::STATES}
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch self.proof_status ||= ProofStatus.find(ProofStatus::DEFAULT_OPEN_STATUS)
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch "#{theorem.locid}//#{self.class.to_s.underscore.dasherize}-#{number}"
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch ontology_version = theorem.ontology.current_version
49fc09f995183d44e004bbc3eb9b6c6c7b6cae7fTimo Sirainen unless ontology_version.provers.include?(prover)
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch ontology_version.save!
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch def retry_failed
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch ProofExecutionWorker.perform_async(id)
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch def proper_subset_of_axioms_selected?
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch selected = proof_attempt_configuration.axiom_selection.axioms
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch available = theorem.ontology.axioms
1b81b28b2e7856748cffd7d01052a944b6c80b23Timo Sirainen selected.any? && selected.count < available.count
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch def prove_options_from_configuration
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch pac = proof_attempt_configuration
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch Hets::ProveOptions.new({prover: pac.prover,
ab90f702ceedb7ba445a9a592be0b213b27cbafaStephan Bosch timeout: pac.timeout})