proof.rb revision 54f2fe542bbb8735c8c4aa653e01f72f9cc88122
970N/A# The Proof class is not supposed to be stored in the database. Its purpose is
970N/A# to allow for an easy way to create proving commands in the RESTful manner.
970N/A# It is called Proof to comply with the ProofsController which in turn gets
970N/A# called on */proofs routes.
1072N/A# This class prepares the proving procedure and creates the models which are
970N/A# presented in the UI (ProofAttempt).
970N/Aclass Proof < FakeRecord
970N/A class ProversValidator < ActiveModel::EachValidator
970N/A def validate_each(record, attribute, value)
970N/A not_provers = value.reject { |id| Prover.where(id: id).any? }
970N/A if not_provers.any?
970N/A record.errors.add attribute, "#{not_provers} are not provers"
970N/A end
970N/A end
970N/A end
970N/A
970N/A TIMEOUT_RANGE = [5.seconds, 10.seconds, 30.seconds,
970N/A 1.minutes, 5.minutes, 10.minutes, 30.minutes,
970N/A 1.hours, 6.hours,
970N/A 1.days, 2.days, 7.days]
970N/A
970N/A # flags
970N/A attr_reader :prove_asynchronously
970N/A # ontology related
970N/A attr_reader :ontology, :proof_obligation
970N/A # prover related
970N/A attr_reader :prover_ids, :provers
970N/A # axiom related
970N/A attr_reader :axiom_selection_method, :axiom_selection, :specific_axiom_selection, :axioms
970N/A # timeout
970N/A attr_reader :timeout
970N/A # result related
970N/A attr_reader :proof_attempts
970N/A
970N/A validates :prover_ids, provers: true
970N/A validates :axiom_selection_method, inclusion: {in: AxiomSelection::METHODS}
970N/A validates :timeout,
970N/A inclusion: {in: (TIMEOUT_RANGE.first..TIMEOUT_RANGE.last)},
970N/A if: :timeout_present?
970N/A
970N/A delegate :to_s, to: :proof_obligation
970N/A
970N/A def initialize(opts, prove_asynchronously: true)
1105N/A prepare_options(opts)
970N/A @prove_asynchronously = prove_asynchronously
970N/A @ontology = Ontology.find(opts[:ontology_id])
970N/A @timeout = opts[:proof][:timeout].to_i if opts[:proof][:timeout].present?
970N/A initialize_proof_obligation(opts)
970N/A initialize_provers(opts)
970N/A initialize_axiom_selection(opts)
970N/A initialize_proof_attempts(opts)
970N/A end
970N/A
970N/A def save!
970N/A ActiveRecord::Base.transaction do
970N/A specific_axiom_selection.save!
970N/A proof_attempts.each do |proof_attempt|
970N/A proof_attempt.save!
970N/A proof_attempt.proof_attempt_configuration.save!
970N/A end
970N/A end
970N/A prove
970N/A end
970N/A
970N/A def theorem?
970N/A proof_obligation.is_a?(Theorem)
970N/A end
970N/A
970N/A protected
970N/A
970N/A # This is needed for the validations to run.
970N/A def prepare_options(opts)
970N/A opts[:proof] ||= {}
970N/A opts[:proof][:prover_ids] ||= []
970N/A end
970N/A
970N/A def ontology_version
970N/A @ontology_version ||= ontology.current_version
970N/A end
970N/A
970N/A def initialize_proof_obligation(opts)
970N/A @proof_obligation ||=
970N/A if opts[:theorem_id]
970N/A Theorem.find(opts[:theorem_id])
970N/A else
970N/A ontology_version
970N/A end
970N/A end
970N/A
970N/A def initialize_provers(opts)
970N/A @prover_ids = normalize_check_box_ids(opts[:proof][:prover_ids])
970N/A @provers = @prover_ids.map { |prover| Prover.where(id: prover).first }
970N/A @provers.compact!
970N/A @provers = [nil] if @provers.blank?
970N/A end
970N/A
970N/A # HACK: Remove the empty string from params.
1105N/A # Rails 4.2 introduces the html form option :include_hidden for this task.
1105N/A def normalize_check_box_ids(collection)
970N/A collection.select(&:present?).map(&:to_i) if collection
1105N/A end
970N/A
970N/A def initialize_axioms(opts)
970N/A axiom_ids = normalize_check_box_ids(opts[:proof][:axioms])
970N/A @axioms = axiom_ids.map { |id| Axiom.find(id) } if axiom_ids
970N/A end
970N/A
977N/A def initialize_axiom_selection(opts)
970N/A @axiom_selection_method = opts[:proof][:axiom_selection_method].try(:to_sym)
970N/A build_axiom_selection(opts)
970N/A end
970N/A
970N/A def initialize_proof_attempts(opts)
970N/A @proof_attempts = []
970N/A if theorem?
970N/A initialize_proof_attempts_for_theorem(opts, proof_obligation)
970N/A else
982N/A proof_obligation.theorems.each do |theorem|
970N/A initialize_proof_attempts_for_theorem(opts, theorem)
970N/A end
970N/A end
970N/A end
970N/A
970N/A def initialize_proof_attempts_for_theorem(opts, theorem)
970N/A provers.each do |prover|
970N/A pac = ProofAttemptConfiguration.new
970N/A pac.prover = prover
970N/A pac.timeout = timeout
970N/A pac.axiom_selection = axiom_selection
970N/A
970N/A proof_attempt = ProofAttempt.new
982N/A proof_attempt.theorem = theorem
970N/A proof_attempt.proof_attempt_configuration = pac
970N/A pac.proof_attempt = proof_attempt
970N/A
970N/A @proof_attempts << proof_attempt
1105N/A end
970N/A end
970N/A
1105N/A def build_axiom_selection(opts)
970N/A send("build_#{axiom_selection_method}", opts) if AxiomSelection::METHODS.include?(axiom_selection_method)
970N/A end
970N/A
970N/A def build_manual_axiom_selection(opts)
970N/A axiom_ids = normalize_check_box_ids(opts[:proof][:axioms])
970N/A @specific_axiom_selection = ManualAxiomSelection.new
970N/A if axiom_ids
970N/A specific_axiom_selection.axioms =
970N/A axiom_ids.map { |id| Axiom.unscoped.find(id) }
970N/A end
1105N/A @axiom_selection = @specific_axiom_selection.axiom_selection
1105N/A end
1105N/A
970N/A def build_sine_axiom_selection(opts)
970N/A SineAxiomSelection.new(opts[:proof][:sine_axiom_selection])
970N/A end
1105N/A
970N/A def timeout_present?
970N/A timeout.present?
970N/A end
970N/A
970N/A def prove
970N/A proof_attempts.each do |proof_attempt|
970N/A if prove_asynchronously
970N/A ProofExecutionWorker.perform_async(proof_attempt.id)
970N/A else
970N/A ProofExecutionWorker.new.perform(proof_attempt.id)
970N/A end
970N/A end
970N/A end
970N/Aend
970N/A