proof_attempt.rb revision 80d7c205926c3c8b9869082cc4eb0760e54e0aee
2ronwalfclass ProofAttempt < ActiveRecord::Base
2ronwalf include Numbering
2ronwalf include StateUpdater
2ronwalf
2ronwalf numbering_parent_column 'sentence_id'
2ronwalf
2ronwalf belongs_to :theorem, foreign_key: 'sentence_id'
2ronwalf belongs_to :proof_status
2ronwalf belongs_to :prover
2ronwalf belongs_to :proof_attempt_configuration
2ronwalf has_one :prover_output
2ronwalf has_one :tactic_script
2ronwalf has_many :generated_axioms, dependent: :destroy
2ronwalf has_and_belongs_to_many :used_axioms,
2ronwalf class_name: 'Axiom',
2ronwalf association_foreign_key: 'sentence_id',
2ronwalf join_table: 'used_axioms_proof_attempts'
2ronwalf has_and_belongs_to_many :used_theorems,
2ronwalf class_name: 'Theorem',
2ronwalf association_foreign_key: 'sentence_id',
2ronwalf join_table: 'used_axioms_proof_attempts'
2ronwalf
2ronwalf attr_accessible :locid
2ronwalf attr_accessible :time_taken,
2ronwalf :number,
2ronwalf :state,
2ronwalf :state_updated_at,
2ronwalf :last_error
2ronwalf
2ronwalf validates :state, inclusion: {in: State::STATES}
2ronwalf validates :theorem, presence: true
2ronwalf
2ronwalf before_create :generate_locid
2ronwalf before_save :set_default_proof_status
2ronwalf after_save :update_theorem_status
2ronwalf
2ronwalf scope :latest, order('number DESC')
2ronwalf
2ronwalf delegate :ontology, to: :theorem
2ronwalf
2ronwalf def self.find_with_locid(locid, _iri = nil)
2ronwalf where(locid: locid).first
2ronwalf end
2ronwalf
2ronwalf def used_sentences
2ronwalf @used_sentences ||= used_axioms + used_theorems
2ronwalf end
2ronwalf
2ronwalf def set_default_proof_status
2ronwalf self.proof_status ||= ProofStatus.find(ProofStatus::DEFAULT_OPEN_STATUS)
2ronwalf end
2ronwalf
2ronwalf def generate_locid
2ronwalf self.locid =
2ronwalf "#{theorem.locid}//#{self.class.to_s.underscore.dasherize}-#{number}"
2ronwalf end
2ronwalf
2ronwalf def update_theorem_status
2ronwalf theorem.update_proof_status(proof_status)
2ronwalf end
2ronwalf
2ronwalf def associate_prover_with_ontology_version
ontology_version = theorem.ontology.current_version
unless ontology_version.provers.include?(prover)
ontology_version.provers << prover
ontology_version.save!
end
end
def retry_failed
options_to_attempts = CollectiveProofAttemptWorker.
normalize_for_async_call({prove_options_from_configuration => [self]})
CollectiveProofAttemptWorker.
perform_async(Theorem.to_s, theorem.id, options_to_attempts)
end
protected
def prove_options_from_configuration
pac = proof_attempt_configuration
Hets::ProveOptions.new({prover: pac.prover,
timeout: pac.timeout})
end
end