Remove unused code
This commit is contained in:
parent
37f1b301b5
commit
e03628ec66
GPG Key ID:
05F3611E97A70ABF
165
src/problem.rs
165
src/problem.rs
|
|
@ -369,171 +369,6 @@ impl Problem
|
|||
Ok(())
|
||||
}
|
||||
|
||||
fn display(&self, output_format: crate::output::Format)
|
||||
{
|
||||
let format_context = FormatContext
|
||||
{
|
||||
program_variable_declaration_ids:
|
||||
std::cell::RefCell::new(VariableDeclarationIDs::new()),
|
||||
integer_variable_declaration_ids:
|
||||
std::cell::RefCell::new(VariableDeclarationIDs::new()),
|
||||
input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(),
|
||||
variable_declaration_domains: &self.variable_declaration_domains.borrow(),
|
||||
};
|
||||
|
||||
let print_title = |title, section_separator|
|
||||
{
|
||||
print!("{}{}", section_separator, "%".repeat(72));
|
||||
print!("\n% {}", title);
|
||||
println!("\n{}", "%".repeat(72));
|
||||
};
|
||||
|
||||
let print_formula = |formula: &foliage::Formula|
|
||||
{
|
||||
match output_format
|
||||
{
|
||||
crate::output::Format::HumanReadable => print!("{}",
|
||||
foliage::format::display_formula(formula, &format_context)),
|
||||
crate::output::Format::TPTP => print!("{}",
|
||||
crate::output::tptp::display_formula(formula, &format_context)),
|
||||
}
|
||||
};
|
||||
|
||||
let mut section_separator = "";
|
||||
|
||||
if output_format == crate::output::Format::TPTP
|
||||
{
|
||||
print_title("anthem types", section_separator);
|
||||
section_separator = "\n";
|
||||
|
||||
let tptp_preamble_anthem_types
|
||||
= include_str!("output/tptp/preamble_types.tptp").trim_end();
|
||||
println!("{}", tptp_preamble_anthem_types);
|
||||
|
||||
print_title("anthem axioms", section_separator);
|
||||
|
||||
let tptp_preamble_anthem_types
|
||||
= include_str!("output/tptp/preamble_axioms.tptp").trim_end();
|
||||
println!("{}", tptp_preamble_anthem_types);
|
||||
|
||||
if !self.predicate_declarations.borrow().is_empty()
|
||||
|| !self.function_declarations.borrow().is_empty()
|
||||
{
|
||||
print_title("types", section_separator);
|
||||
|
||||
if !self.predicate_declarations.borrow().is_empty()
|
||||
{
|
||||
println!("% predicate types")
|
||||
}
|
||||
|
||||
for predicate_declaration in self.predicate_declarations.borrow().iter()
|
||||
{
|
||||
println!("tff(type, type, {}).",
|
||||
crate::output::tptp::display_predicate_declaration(predicate_declaration));
|
||||
}
|
||||
|
||||
if !self.function_declarations.borrow().is_empty()
|
||||
{
|
||||
println!("% function types")
|
||||
}
|
||||
|
||||
for function_declaration in self.function_declarations.borrow().iter()
|
||||
{
|
||||
println!("tff(type, type, {}).",
|
||||
crate::output::tptp::display_function_declaration(function_declaration,
|
||||
&format_context));
|
||||
}
|
||||
}
|
||||
|
||||
let function_declarations = self.function_declarations.borrow();
|
||||
let symbolic_constants = function_declarations.iter().filter(
|
||||
|x| !self.input_constant_declaration_domains.borrow().contains_key(*x));
|
||||
|
||||
let mut last_symbolic_constant: Option<std::rc::Rc<foliage::FunctionDeclaration>> =
|
||||
None;
|
||||
|
||||
for (i, symbolic_constant) in symbolic_constants.enumerate()
|
||||
{
|
||||
// Order axioms are only necessary with two or more symbolic constants
|
||||
if i == 1
|
||||
{
|
||||
println!("% axioms for order of symbolic constants")
|
||||
}
|
||||
|
||||
if symbolic_constant.arity > 0
|
||||
{
|
||||
// TODO: refactor
|
||||
panic!("unexpected n-ary function declaration");
|
||||
}
|
||||
|
||||
if let Some(last_symbolic_constant) = last_symbolic_constant
|
||||
{
|
||||
println!("tff(symbolic_constant_order, axiom, p__less__({}, {})).",
|
||||
last_symbolic_constant.name, symbolic_constant.name);
|
||||
}
|
||||
|
||||
last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant));
|
||||
}
|
||||
}
|
||||
|
||||
for (section_kind, statements) in self.statements.borrow().iter()
|
||||
{
|
||||
if statements.is_empty()
|
||||
{
|
||||
continue;
|
||||
}
|
||||
|
||||
let title = match section_kind
|
||||
{
|
||||
SectionKind::CompletedDefinitions => "completed definitions",
|
||||
SectionKind::IntegrityConstraints => "integrity constraints",
|
||||
SectionKind::Axioms => "axioms",
|
||||
SectionKind::Assumptions => "assumptions",
|
||||
SectionKind::Lemmas => "lemmas",
|
||||
SectionKind::Assertions => "assertions",
|
||||
};
|
||||
|
||||
print_title(title, section_separator);
|
||||
section_separator = "\n";
|
||||
|
||||
let mut i = 0;
|
||||
|
||||
for statement in statements.iter()
|
||||
{
|
||||
if let Some(ref description) = statement.description
|
||||
{
|
||||
println!("% {}", description);
|
||||
}
|
||||
|
||||
let name = match &statement.name
|
||||
{
|
||||
// TODO: refactor
|
||||
Some(name) => name.clone(),
|
||||
None =>
|
||||
{
|
||||
i += 1;
|
||||
format!("statement_{}", i)
|
||||
},
|
||||
};
|
||||
|
||||
if output_format == crate::output::Format::TPTP
|
||||
{
|
||||
// TODO: add proper statement type
|
||||
print!("tff({}, axiom, ", name);
|
||||
}
|
||||
|
||||
print_formula(&statement.formula);
|
||||
|
||||
if output_format == crate::output::Format::TPTP
|
||||
{
|
||||
print!(").");
|
||||
}
|
||||
|
||||
println!("");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn write_tptp_problem_to_prove_next_statement(&self, formatter: &mut String) -> std::fmt::Result
|
||||
{
|
||||
use std::fmt::Write as _;
|
||||
|
|
|
|||
Loading…
Reference in New Issue