proof.rb revision a5e53dbef6b3edf62bcb2f94bad010bf7cd2442d
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek# The Proof class is not supposed to be stored in the database. Its purpose is
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek# to allow for an easy way to create proving commands in the RESTful manner.
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek# It is called Proof to comply with the ProofsController which in turn gets
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek# called on */proofs routes.
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek# This class prepares the proving procedure and creates the models which are
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek# presented in the UI (ProofAttempt).
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek class ProversValidator < ActiveModel::EachValidator
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek not_provers = value.reject { |id| Prover.where(id: id).any? }
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek record.errors.add attribute, "#{not_provers} are not provers"
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek TIMEOUT_RANGE = [5.seconds, 10.seconds, 30.seconds,
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek attr_reader :axiom_selection_method, :specific_axiom_selection, :axioms
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek validates :axiom_selection_method, inclusion: {in: AxiomSelection::METHODS}
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek inclusion: {in: (TIMEOUT_RANGE.first..TIMEOUT_RANGE.last)},
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek def initialize(opts, prove_asynchronously: true)
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek @timeout = opts[:proof][:timeout].to_i if opts[:proof][:timeout].present?
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek proof_attempt.proof_attempt_configuration.save!
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek @prover_ids = normalize_check_box_ids(opts[:proof][:prover_ids])
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek @provers = @prover_ids.map { |prover| Prover.where(id: prover).first }
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek # Rails 4.2 introduces the html form option :include_hidden for this task.
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek collection.select(&:present?).map(&:to_i) if collection
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek axiom_ids = normalize_check_box_ids(opts[:proof][:axioms])
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek @axioms = axiom_ids.map { |id| Axiom.find(id) } if axiom_ids
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek @axiom_selection_method = opts[:proof][:axiom_selection_method].try(:to_sym)
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek initialize_proof_attempts_for_theorem(opts, proof_obligation)
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek initialize_proof_attempts_for_theorem(opts, theorem)
b4f87b42b18888c396e44e7359f7aafb092221bfJakub Hrozek def initialize_proof_attempts_for_theorem(opts, theorem)
16cb0969f0a9ea71524d852077d6a480740d4f12Jakub Hrozek proof_attempt.proof_attempt_configuration = pac
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek @proof_attempts << proof_attempt
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek def build_axiom_selection(opts)
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek if AxiomSelection::METHODS.include?(axiom_selection_method)
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek send("build_#{axiom_selection_method}", opts)
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek def build_manual_axiom_selection(opts)
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek axiom_ids = normalize_check_box_ids(opts[:proof][:axioms])
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek @specific_axiom_selection = ManualAxiomSelection.new
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek if axiom_ids
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek specific_axiom_selection.axioms =
e00c2b5ac4963de9521599c88597b7fb97339d0eJakub Hrozek axiom_ids.map { |id| Axiom.unscoped.find(id) }
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek def build_sine_axiom_selection(opts)
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek @specific_axiom_selection =
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek SineAxiomSelection.new(opts[:proof][:sine_axiom_selection])
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek def timeout_present?
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek timeout.present?
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek proof_attempts.each do |proof_attempt|
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek if prove_asynchronously
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek ProofExecutionWorker.perform_async(proof_attempt.id)
44703b84feaafa4f0a4f8df11c5a503dcf48616eJakub Hrozek ProofExecutionWorker.new.perform(proof_attempt.id)