patrick/ask-dracula-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Support right-to-left implications

Browse Source
This commit is contained in:
Patrick Lühne
2019-11-06 19:05:04 -06:00
parent 7da722aeec
commit fa2110294a
2 changed files with 8 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
foliage

Submodule foliage updated: 9076ecd95d...8870cee179

10
src/format_tptp.rs
View File

@@ -62,7 +62,7 @@ fn collect_predicate_declarations_in_formula<'a>(
{
collect_predicate_declarations_in_formula(predicate_declarations, argument);
},
foliage::Formula::Implies(ref left, ref right) =>
foliage::Formula::Implies(ref left, ref right, _) =>
{
collect_predicate_declarations_in_formula(predicate_declarations, left);
collect_predicate_declarations_in_formula(predicate_declarations, right);
@@ -162,7 +162,7 @@ fn collect_symbolic_constants_in_formula<'a>(
{
collect_symbolic_constants_in_formula(symbolic_constants, argument);
},
foliage::Formula::Implies(ref left, ref right) =>
foliage::Formula::Implies(ref left, ref right, _) =>
{
collect_symbolic_constants_in_formula(symbolic_constants, left);
collect_symbolic_constants_in_formula(symbolic_constants, right);
@@ -515,7 +515,11 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
write!(format, ")")
},
foliage::Formula::Implies(ref left, ref right) => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()),
foliage::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction
{
foliage::ImplicationDirection::LeftToRight => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()),
foliage::ImplicationDirection::RightToLeft => write!(format, "({:?} <= {:?})", left.display_tptp(), right.display_tptp()),
},
foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()),
foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", Some("p__less__"), left, right),
foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", Some("p__less_equal__"), left, right),