Module: ADSL::Spass::SpassTranslator

Defined in:
lib/adsl/spass/spass_translator.rb

Defined Under Namespace

Classes: ChainedContext, ContextCommon, FlatContext, Predicate, Translation

Instance Method Summary collapse

Instance Method Details

#replace_conjecture(input, conjecture) ⇒ Object 



8
9
10
11
12
13
14
 
# File 'lib/adsl/spass/spass_translator.rb', line 8

def replace_conjecture(input, conjecture)
  input.gsub(/list_of_formulae\s*\(\s*conjectures\s*\)\s*\..*?end_of_list\./m, <<-SPASS)
  list_of_formulae(conjectures).
    formula(#{conjecture.resolve_spass}).
  end_of_list.
  SPASS
end