Module: Bparity::Formal::Deductive::ProductProgram

Defined in:
lib/bparity/formal/deductive.rb

Class Method Summary collapse

Class Method Details

.call(old_translation, new_translation) ⇒ Object 



252
253
254
255
256
257
258
259
260
261
262
 
# File 'lib/bparity/formal/deductive.rb', line 252

def call(old_translation, new_translation)
  unless old_translation.parameters == new_translation.parameters &&
         old_translation.term.sort == new_translation.term.sort
    raise ConfigurationError, "The F4 translations have incompatible input or output sorts."
  end

  declarations = old_translation.parameters.map { |name, sort| "(declare-const #{name} #{sort})" }
  (["(set-logic ALL)"] + declarations +
    ["(assert (not (= #{old_translation.term.smt} #{new_translation.term.smt})))", "(check-sat)",
     "(get-model)"]).join("\n") << "\n"
end