diff --git a/src/convenience/mod.rs b/src/convenience/mod.rs
index ea89163d..3756831e 100644
--- a/src/convenience/mod.rs
+++ b/src/convenience/mod.rs
@@ -1,3 +1,57 @@
pub mod apply;
pub mod unbox;
pub mod with_warnings;
+
+use {crate::syntax_tree::fol, indexmap::IndexSet};
+
+/// True if v1 is subsorteq to v2 and False otherwise
+pub fn subsort(v1: &fol::Variable, v2: &fol::Variable) -> bool {
+ match v1.sort {
+ fol::Sort::General => match v2.sort {
+ fol::Sort::General => true,
+ fol::Sort::Integer | fol::Sort::Symbol => false,
+ },
+ fol::Sort::Integer => match v2.sort {
+ fol::Sort::General | fol::Sort::Integer => true,
+ fol::Sort::Symbol => false,
+ },
+ fol::Sort::Symbol => match v2.sort {
+ fol::Sort::General | fol::Sort::Symbol => true,
+ fol::Sort::Integer => false,
+ },
+ }
+}
+
+/// Choose `arity` variable names by incrementing `variant`, disjoint from `variables`
+pub fn choose_fresh_variable_names(
+ variables: &IndexSet<fol::Variable>,
+ variant: &str,
+ arity: usize,
+) -> Vec<String> {
+ let mut taken_vars = Vec::<String>::new();
+ for var in variables.iter() {
+ taken_vars.push(var.name.to_string());
+ }
+ let mut fresh_vars = Vec::<String>::new();
+ let arity_bound = match taken_vars.contains(&variant.to_string()) {
+ true => arity + 1,
+ false => {
+ fresh_vars.push(variant.to_string());
+ arity
+ }
+ };
+ for n in 1..arity_bound {
+ let mut candidate: String = variant.to_owned();
+ let number: &str = &n.to_string();
+ candidate.push_str(number);
+ let mut m = n;
+ while taken_vars.contains(&candidate) || fresh_vars.contains(&candidate) {
+ variant.clone_into(&mut candidate);
+ m += 1;
+ let number = &m.to_string();
+ candidate.push_str(number);
+ }
+ fresh_vars.push(candidate.to_string());
+ }
+ fresh_vars
+}
diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs
index 31207bcc..00d493ba 100644
--- a/src/simplifying/fol/ht.rs
+++ b/src/simplifying/fol/ht.rs
@@ -1,9 +1,15 @@
-use crate::{
- convenience::{
- apply::Apply as _,
- unbox::{fol::UnboxedFormula, Unbox as _},
+use {
+ super::{replacement_helper, simplify_conjunction_tree_with_equality, transitive_equality},
+ crate::{
+ convenience::{
+ apply::Apply as _,
+ unbox::{fol::UnboxedFormula, Unbox as _},
+ },
+ syntax_tree::fol::{
+ AtomicFormula, BinaryConnective, Formula, GeneralTerm, IntegerTerm, Quantification,
+ Quantifier, Sort, SymbolicTerm, Theory,
+ },
},
- syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory},
};
pub fn simplify(theory: Theory) -> Theory {
@@ -12,16 +18,25 @@ pub fn simplify(theory: Theory) -> Theory {
}
}
-fn simplify_formula(formula: Formula) -> Formula {
+pub fn simplify_formula(formula: Formula) -> Formula {
formula.apply_all(&mut vec![
Box::new(remove_identities),
Box::new(remove_annihilations),
Box::new(remove_idempotences),
Box::new(join_nested_quantifiers),
+ Box::new(extend_quantifier_scope),
+ Box::new(restrict_quantifier_domain),
+ // cleanup
+ Box::new(simplify_variable_lists),
+ Box::new(simplify_empty_quantifiers),
+ Box::new(simplify_transitive_equality),
+ // cleanup
+ Box::new(simplify_variable_lists),
+ Box::new(simplify_empty_quantifiers),
])
}
-fn remove_identities(formula: Formula) -> Formula {
+pub fn remove_identities(formula: Formula) -> Formula {
// Remove identities
// e.g. F op E => F
@@ -58,7 +73,7 @@ fn remove_identities(formula: Formula) -> Formula {
}
}
-fn remove_annihilations(formula: Formula) -> Formula {
+pub fn remove_annihilations(formula: Formula) -> Formula {
// Remove annihilations
// e.g. F op E => E
@@ -95,7 +110,7 @@ fn remove_annihilations(formula: Formula) -> Formula {
}
}
-fn remove_idempotences(formula: Formula) -> Formula {
+pub fn remove_idempotences(formula: Formula) -> Formula {
// Remove idempotences
// e.g. F op F => F
@@ -112,7 +127,7 @@ fn remove_idempotences(formula: Formula) -> Formula {
}
}
-pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
+pub fn join_nested_quantifiers(formula: Formula) -> Formula {
// Remove nested quantifiers
// e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y)
@@ -138,14 +153,461 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
}
}
+pub fn extend_quantifier_scope(formula: Formula) -> Formula {
+ match formula.clone().unbox() {
+ // Bring a conjunctive or disjunctive term into the scope of a quantifer
+ // e.g. exists X ( F(X) ) & G => exists X ( F(X) & G )
+ // where X does not occur free in G
+ UnboxedFormula::BinaryFormula {
+ connective,
+ lhs:
+ Formula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier,
+ variables,
+ },
+ formula: f,
+ },
+ rhs,
+ } => match connective {
+ BinaryConnective::Conjunction | BinaryConnective::Disjunction => {
+ let mut collision = false;
+ for var in variables.iter() {
+ if rhs.free_variables().contains(var) {
+ collision = true;
+ break;
+ }
+ }
+
+ match collision {
+ true => formula,
+ false => Formula::QuantifiedFormula {
+ quantification: Quantification {
+ quantifier,
+ variables,
+ },
+ formula: Formula::BinaryFormula {
+ connective,
+ lhs: f,
+ rhs: rhs.into(),
+ }
+ .into(),
+ },
+ }
+ }
+ _ => formula,
+ },
+
+ UnboxedFormula::BinaryFormula {
+ connective,
+ lhs,
+ rhs:
+ Formula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier,
+ variables,
+ },
+ formula: f,
+ },
+ } => match connective {
+ BinaryConnective::Conjunction | BinaryConnective::Disjunction => {
+ let mut collision = false;
+ for var in variables.iter() {
+ if lhs.free_variables().contains(var) {
+ collision = true;
+ break;
+ }
+ }
+
+ match collision {
+ true => formula,
+ false => Formula::QuantifiedFormula {
+ quantification: Quantification {
+ quantifier,
+ variables,
+ },
+ formula: Formula::BinaryFormula {
+ connective,
+ lhs: lhs.into(),
+ rhs: f,
+ }
+ .into(),
+ },
+ }
+ }
+ _ => formula,
+ },
+
+ x => x.rebox(),
+ }
+}
+
+pub fn simplify_variable_lists(formula: Formula) -> Formula {
+ match formula.clone().unbox() {
+ // Removes variables from quantifiers when they do not occur in the quantified formula
+ // e.g. exists X Y ( q(Y) ) => exists Y ( q(Y) )
+ UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ mut variables,
+ quantifier,
+ },
+ formula,
+ } => {
+ let fvars = formula.variables();
+ variables.retain(|x| fvars.contains(x));
+ Formula::QuantifiedFormula {
+ quantification: Quantification {
+ variables,
+ quantifier,
+ },
+ formula: formula.into(),
+ }
+ }
+
+ x => x.rebox(),
+ }
+}
+
+pub fn simplify_empty_quantifiers(formula: Formula) -> Formula {
+ match formula.clone().unbox() {
+ // Remove quantifiers with no variables
+ // e.g. exists ( F ) => F
+ UnboxedFormula::QuantifiedFormula {
+ quantification: Quantification { variables, .. },
+ formula: f,
+ } => {
+ if variables.is_empty() {
+ f
+ } else {
+ formula
+ }
+ }
+
+ x => x.rebox(),
+ }
+}
+
+pub fn restrict_quantifier_domain(formula: Formula) -> Formula {
+ let mut simplified_formula = formula.clone();
+ match formula.clone().unbox() {
+ // Replace a general variable in an outer quantification with a fresh integer variable capturing an inner quantification
+ // e.g. exists Z$g (exists I$i J$i (I$i = Z$g & G) & H) => exists K$i (exists I$i J$i (I$i = K$i & G) & H)
+ // or forall Z$g (exists I$i J$i (I$i = Z$g & G) -> H) => forall K$i (exists I$i J$i (I$i = K$i & G) -> H)
+ UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Exists,
+ variables: outer_vars,
+ },
+ formula:
+ Formula::BinaryFormula {
+ connective: BinaryConnective::Conjunction,
+ lhs,
+ rhs,
+ },
+ } => {
+ let mut replaced = false;
+ let mut conjunctive_terms = Formula::conjoin_invert(*lhs);
+ conjunctive_terms.extend(Formula::conjoin_invert(*rhs));
+ for ct in conjunctive_terms.iter() {
+ if let Formula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Exists,
+ variables: inner_vars,
+ },
+ formula: inner_formula,
+ } = ct
+ {
+ let inner_ct = Formula::conjoin_invert(*inner_formula.clone());
+ for ict in inner_ct.iter() {
+ if let Formula::AtomicFormula(AtomicFormula::Comparison(comp)) = ict {
+ if comp.equality_comparison() {
+ for ovar in outer_vars.iter() {
+ for ivar in inner_vars.iter() {
+ if ovar.sort == Sort::General && ivar.sort == Sort::Integer
+ {
+ let replacement_result =
+ replacement_helper(ivar, ovar, comp, &formula);
+
+ if replacement_result.1 {
+ simplified_formula = replacement_result.0;
+ replaced = true;
+ break;
+ }
+ }
+ }
+ if replaced {
+ break;
+ }
+ }
+ }
+ if replaced {
+ break;
+ }
+ }
+ }
+ }
+ if replaced {
+ break;
+ }
+ }
+ }
+
+ UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Forall,
+ variables: outer_vars,
+ },
+ formula:
+ Formula::BinaryFormula {
+ connective: BinaryConnective::Implication,
+ lhs,
+ rhs,
+ },
+ } => {
+ if let UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Exists,
+ variables: inner_vars,
+ },
+ formula: inner_formula,
+ } = lhs.unbox()
+ {
+ let mut replaced = false;
+ let conjunctive_terms = Formula::conjoin_invert(inner_formula);
+ for ct in conjunctive_terms.iter() {
+ if let Formula::AtomicFormula(AtomicFormula::Comparison(comp)) = ct {
+ if comp.equality_comparison() {
+ for ovar in outer_vars.iter() {
+ for ivar in inner_vars.iter() {
+ if ovar.sort == Sort::General
+ && ivar.sort == Sort::Integer
+ && !rhs.free_variables().contains(ovar)
+ {
+ let replacement_result =
+ replacement_helper(ivar, ovar, comp, &formula);
+ if replacement_result.1 {
+ simplified_formula = replacement_result.0;
+ replaced = true;
+ break;
+ }
+ }
+ if replaced {
+ break;
+ }
+ }
+ }
+ if replaced {
+ break;
+ }
+ }
+ }
+ if replaced {
+ break;
+ }
+ }
+ }
+ }
+
+ _ => (),
+ }
+ simplified_formula
+}
+
+pub fn eliminate_redundant_quantifiers(formula: Formula) -> Formula {
+ match formula.clone().unbox() {
+ // Remove redundant existentials
+ // e.g. exists Z$g (Z$g = X$g and F(Z$g)) => F(X$g)
+ UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Exists,
+ mut variables,
+ },
+ formula: f,
+ } => match f.clone().unbox() {
+ UnboxedFormula::BinaryFormula {
+ connective: BinaryConnective::Conjunction,
+ ..
+ } => {
+ let simplification_result =
+ simplify_conjunction_tree_with_equality(f, variables.clone());
+ match simplification_result.1 {
+ Some(sub_pair) => {
+ variables.retain(|v| v != &sub_pair.0);
+ Formula::QuantifiedFormula {
+ quantification: Quantification {
+ quantifier: Quantifier::Exists,
+ variables,
+ },
+ formula: simplification_result.0.into(),
+ }
+ }
+ None => formula,
+ }
+ }
+ _ => formula,
+ },
+
+ // A universally quantified implication can sometimes be simplified
+ // e.g. forall X1 .. Xj .. Xn (F1 and .. Fi .. and Fm -> G), where Fi is Xj=t, and Xj doesn’t occur in t, and free variables occurring in t are not bound by quantifiers in F1, F2, ..
+ // becomes forall X1 .. Xn (F1 and .. and Fm -> G)
+ UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Forall,
+ mut variables,
+ },
+ formula:
+ Formula::BinaryFormula {
+ connective: BinaryConnective::Implication,
+ lhs,
+ rhs,
+ },
+ } => match lhs.clone().unbox() {
+ UnboxedFormula::BinaryFormula {
+ connective: BinaryConnective::Conjunction,
+ ..
+ } => {
+ let mut f = formula;
+ let lhs_simplify = simplify_conjunction_tree_with_equality(*lhs, variables.clone());
+ match lhs_simplify.1 {
+ Some(sub_pair) => {
+ if !rhs.clone().unsafe_substitution(&sub_pair.0, &sub_pair.1) {
+ variables.retain(|v| v != &sub_pair.0);
+ f = Formula::QuantifiedFormula {
+ quantification: Quantification {
+ quantifier: Quantifier::Forall,
+ variables,
+ },
+ formula: Formula::BinaryFormula {
+ connective: BinaryConnective::Implication,
+ lhs: lhs_simplify.0.into(),
+ rhs: rhs.substitute(sub_pair.0, sub_pair.1).into(),
+ }
+ .into(),
+ };
+ }
+ f
+ }
+ None => f,
+ }
+ }
+
+ _ => formula,
+ },
+
+ _ => formula,
+ }
+}
+
+pub fn simplify_transitive_equality(formula: Formula) -> Formula {
+ match formula.clone().unbox() {
+ // When X is a subsort of Y (or sort(X) = sort(Y)) and t is a term:
+ // exists X Y (X = t and Y = t and F)
+ // =>
+ // exists X (X = t and F(X))
+ // Replace Y with X within F
+ UnboxedFormula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier: Quantifier::Exists,
+ mut variables,
+ },
+ formula: f,
+ } => match f.clone().unbox() {
+ UnboxedFormula::BinaryFormula {
+ connective: BinaryConnective::Conjunction,
+ ..
+ } => {
+ let mut simplified = formula.clone();
+ let mut simplify = false;
+ let conjunctive_terms = Formula::conjoin_invert(f.clone());
+ let mut ct_copy = conjunctive_terms.clone();
+ for (i, ct1) in conjunctive_terms.iter().enumerate() {
+ // Search for an equality formula
+ if let Formula::AtomicFormula(AtomicFormula::Comparison(c1)) = ct1 {
+ if c1.equality_comparison() {
+ for (j, ct2) in conjunctive_terms.iter().enumerate() {
+ // Search for a second equality formula
+ if let Formula::AtomicFormula(AtomicFormula::Comparison(c2)) = ct2 {
+ if c2.equality_comparison() && i != j {
+ if let Some((keep_var, drop_var, drop_term)) =
+ transitive_equality(
+ c1.clone(),
+ c2.clone(),
+ variables.clone(),
+ )
+ {
+ variables.retain(|x| x != &drop_var);
+ ct_copy.retain(|t| {
+ t != &Formula::AtomicFormula(
+ AtomicFormula::Comparison(drop_term.clone()),
+ )
+ });
+ let keep = match keep_var.sort {
+ Sort::General => {
+ GeneralTerm::Variable(keep_var.name)
+ }
+ Sort::Integer => GeneralTerm::IntegerTerm(
+ IntegerTerm::Variable(keep_var.name),
+ ),
+ Sort::Symbol => GeneralTerm::SymbolicTerm(
+ SymbolicTerm::Variable(keep_var.name),
+ ),
+ };
+ let inner = Formula::conjoin(ct_copy.clone())
+ .substitute(drop_var, keep);
+ simplified = Formula::QuantifiedFormula {
+ quantification: Quantification {
+ quantifier: Quantifier::Exists,
+ variables: variables.clone(),
+ },
+ formula: inner.into(),
+ };
+ simplify = true;
+ }
+ }
+ }
+ if simplify {
+ break;
+ }
+ }
+ }
+ }
+ if simplify {
+ break;
+ }
+ }
+ simplified
+ }
+
+ _ => formula,
+ },
+
+ x => x.rebox(),
+ }
+}
+
#[cfg(test)]
mod tests {
use {
super::{
- join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities,
- simplify_formula,
+ eliminate_redundant_quantifiers, extend_quantifier_scope, join_nested_quantifiers,
+ remove_annihilations, remove_idempotences, remove_identities,
+ simplify_empty_quantifiers, simplify_formula, simplify_transitive_equality,
+ simplify_variable_lists,
+ },
+ crate::{
+ convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain,
+ syntax_tree::fol::Formula,
},
- crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
};
#[test]
@@ -240,4 +702,142 @@ mod tests {
)
}
}
+
+ #[test]
+ fn test_extend_quantification_scope() {
+ for (src, target) in [
+ (
+ "exists X (q(X) and 1 < 3) and p(Z)",
+ "exists X (q(X) and 1 < 3 and p(Z))",
+ ),
+ (
+ "exists X (q(X) and 1 < 3) and p(X)",
+ "exists X (q(X) and 1 < 3) and p(X)",
+ ),
+ (
+ "forall Z X (q(X) and 1 < Z) or p(Y,Z$)",
+ "forall Z X (q(X) and 1 < Z or p(Y,Z$))",
+ ),
+ (
+ "p(Z) and exists X (q(X) and 1 < 3)",
+ "exists X (p(Z) and (q(X) and 1 < 3))",
+ ),
+ ] {
+ let result = extend_quantifier_scope(src.parse().unwrap());
+ let target = target.parse().unwrap();
+ assert_eq!(result, target, "{result} != {target}")
+ }
+ }
+
+ #[test]
+ fn test_simplify_variable_lists() {
+ for (src, target) in [
+ (
+ "exists X Y ( q or (t and q(Y)))",
+ "exists Y ( q or (t and q(Y)))",
+ ),
+ (
+ "exists Y V ( q or forall X (t(Y) and q(X)))",
+ "exists Y ( q or forall X (t(Y) and q(X)))",
+ ),
+ ] {
+ assert_eq!(
+ simplify_variable_lists(src.parse().unwrap()),
+ target.parse().unwrap()
+ )
+ }
+ }
+
+ #[test]
+ fn test_simplify_empty_quantifiers() {
+ for (src, target) in [("exists Y (1 < 2)", "1 < 2"), ("forall Z #true", "#true")] {
+ assert_eq!(
+ simplify_empty_quantifiers(simplify_variable_lists(src.parse().unwrap())),
+ target.parse().unwrap()
+ )
+ }
+ }
+
+ #[test]
+ fn test_restrict_quantifiers() {
+ for (src, target) in [
+ (
+ "exists Z Z1 ( exists I$i J$i ( Z = J$i and q(I$i, J$i) ) and Z = Z1 )",
+ "exists Z1 J1$i ( exists I$i J$i ( J1$i = J$i and q(I$i, J$i) ) and J1$i = Z1 )",
+ ),
+ (
+ "exists Z Z1 ( exists I$i J$i ( q(I$i, J$i) and Z = J$i) and Z = Z1 )",
+ "exists Z1 J1$i ( exists I$i J$i ( q(I$i, J$i) and J1$i = J$i) and J1$i = Z1 )",
+ ),
+ (
+ "exists Z Z1 ( Z = Z1 and exists I$i J$i ( q(I$i, J$i) and Z = J$i) )",
+ "exists Z1 J1$i ( J1$i = Z1 and exists I$i J$i ( q(I$i, J$i) and J1$i = J$i) )",
+ ),
+ (
+ "exists Z Z1 ( Z = Z1 and exists I$i J$i ( q(I$i, J$i) and Z = J$i and 3 > 2) and 1 < 5 )",
+ "exists Z1 J1$i ( J1$i = Z1 and exists I$i J$i ( q(I$i, J$i) and J1$i = J$i and 3 > 2) and 1 < 5 )",
+ ),
+ (
+ "forall X Y ( exists Z I$i (p(X) and p(Z) and Y = I$i) -> q(X) )",
+ "forall X I1$i ( exists Z I$i (p(X) and p(Z) and I1$i = I$i) -> q(X) )",
+ ),
+ (
+ "forall X Y ( exists Z I$i (p(X) and p(Z) and Y = I$i) -> q(Y) )",
+ "forall X Y ( exists Z I$i (p(X) and p(Z) and Y = I$i) -> q(Y) )",
+ ),
+ (
+ "forall X Y ( exists I$i J$i (Y = J$i and p(I$i, J$i) and I$i = X) -> q(Z) )",
+ "forall X J1$i ( exists I$i J$i (J1$i = J$i and p(I$i, J$i) and I$i = X) -> q(Z) )",
+ ),
+ (
+ "forall X Y ( exists Z I$i (p(X,Z) or Y = I$i) -> q(X) )",
+ "forall X Y ( exists Z I$i (p(X,Z) or Y = I$i) -> q(X) )",
+ ),
+ (
+ "forall X Y ( exists Z I$i (p(X,Z) and I$i = X) -> exists A X (q(A,X)) )",
+ "forall Y I1$i ( exists Z I$i (p(I1$i,Z) and I$i = I1$i) -> exists A X (q(A,X)) )",
+ ),
+ ] {
+ let src =
+ restrict_quantifier_domain(src.parse().unwrap());
+ let target = target.parse().unwrap();
+ assert_eq!(src, target, "{src} != {target}")
+ }
+ }
+
+ #[test]
+ fn test_eliminate_redundant_quantifiers() {
+ for (src, target) in [
+ ("exists X ( X = Z and not q(X) )", "not q(Z)"),
+ (
+ "exists Y ( Y = X and forall V (p(Y,V) -> q(X)) )",
+ "forall V (p(X,V) -> q(X))",
+ ),
+ (
+ "exists Z Z1 ( Z = I and (exists K$i (K$i = I) and Z = Z1) )",
+ "exists Z1 ( exists K$i (K$i = I) and I = Z1)",
+ ),
+ (
+ "forall X V (p(X) and X = V -> q(V))",
+ "forall V (p(V) -> q(V))",
+ ),
+ ] {
+ let src =
+ simplify_empty_quantifiers(eliminate_redundant_quantifiers(src.parse().unwrap()));
+ let target = target.parse().unwrap();
+ assert_eq!(src, target, "{src} != {target}")
+ }
+ }
+
+ #[test]
+ fn test_simplify_transitive_equality() {
+ for (src, target) in [(
+ "exists X Y Z ( X = 5 and Y = 5 and not p(X,Y))",
+ "exists X Z ( X = 5 and not p(X,X))",
+ )] {
+ let src = simplify_transitive_equality(src.parse().unwrap());
+ let target = target.parse().unwrap();
+ assert_eq!(src, target, "{src} != {target}")
+ }
+ }
}
diff --git a/src/simplifying/fol/mod.rs b/src/simplifying/fol/mod.rs
index 284456e7..e73b2e2a 100644
--- a/src/simplifying/fol/mod.rs
+++ b/src/simplifying/fol/mod.rs
@@ -1,2 +1,386 @@
pub mod classic;
pub mod ht;
+
+use crate::{
+ convenience::{
+ choose_fresh_variable_names, subsort,
+ unbox::{fol::UnboxedFormula, Unbox as _},
+ },
+ syntax_tree::fol::{
+ AtomicFormula, BinaryConnective, Comparison, Formula, GeneralTerm, Guard, IntegerTerm,
+ Quantification, Relation, Sort, SymbolicTerm, Variable,
+ },
+};
+
+// ASSUMES ivar is an integer variable and ovar is a general variable
+// This function checks if the comparison `ivar = ovar` or `ovar = ivar` matches the comparison `comp`
+// If so, it replaces ovar with a fresh integer variable within `formula`
+// Otherwise it returns `formula`
+fn replacement_helper(
+ ivar: &Variable,
+ ovar: &Variable,
+ comp: &Comparison,
+ formula: &Formula,
+) -> (Formula, bool) {
+ let mut simplified_formula = formula.clone();
+ let ivar_term = GeneralTerm::IntegerTerm(IntegerTerm::Variable(ivar.name.clone()));
+ let candidate = Comparison {
+ term: GeneralTerm::Variable(ovar.name.clone()),
+ guards: vec![Guard {
+ relation: Relation::Equal,
+ term: ivar_term.clone(),
+ }],
+ };
+ let mut replace = false;
+ if comp == &candidate {
+ replace = true;
+ } else {
+ let candidate = Comparison {
+ term: ivar_term.clone(),
+ guards: vec![Guard {
+ relation: Relation::Equal,
+ term: GeneralTerm::Variable(ovar.name.clone()),
+ }],
+ };
+ if comp == &candidate {
+ replace = true;
+ }
+ }
+
+ if replace {
+ let varnames = choose_fresh_variable_names(
+ &formula.variables(),
+ &ivar.name.chars().next().unwrap().to_string(),
+ 1,
+ );
+ let fvar = varnames[0].clone();
+ let fvar_term = GeneralTerm::IntegerTerm(IntegerTerm::Variable(fvar.clone()));
+ match formula.clone() {
+ Formula::QuantifiedFormula {
+ quantification:
+ Quantification {
+ quantifier,
+ mut variables,
+ },
+ formula: f,
+ } => {
+ variables.retain(|x| x != ovar); // Drop ovar from the outer quantification, leaving ovar free within formula
+ variables.push(Variable {
+ // Add the new integer variable to replace ovar
+ name: fvar,
+ sort: Sort::Integer,
+ });
+ simplified_formula = Formula::QuantifiedFormula {
+ quantification: Quantification {
+ quantifier: quantifier.clone(),
+ variables,
+ },
+ formula: f.substitute(ovar.clone(), fvar_term).into(), // Replace all free occurences of ovar with fvar_term
+ };
+ }
+
+ _ => panic!("You are using the replacement helper function wrong"),
+ }
+ }
+ (simplified_formula, replace)
+}
+
+// ASSUMES formula has the form:
+// F(var) & var = term OR
+// F(var) & term = var
+// If var is a variable of sort S and term is a term of a subsort of S,
+// and term doesn't contain variables quantified within F, return `F(term)`
+// Otherwise, return the original formula
+fn subsort_equality(var: Variable, term: GeneralTerm, formula: Formula) -> (Formula, bool) {
+ let mut modified = false;
+ let mut simplified_formula = formula.clone();
+ match formula.clone().unbox() {
+ UnboxedFormula::BinaryFormula {
+ connective: BinaryConnective::Conjunction,
+ lhs,
+ ..
+ } => {
+ let term_vars = term.variables(); // term must not contain var
+ match var.sort {
+ Sort::General => {
+ if !term_vars.contains(&var) && !lhs.clone().unsafe_substitution(&var, &term) {
+ modified = true;
+ simplified_formula = lhs.substitute(var, term);
+ }
+ }
+ Sort::Integer => match term.clone() {
+ GeneralTerm::IntegerTerm(_) => {
+ if !term_vars.contains(&var)
+ && !lhs.clone().unsafe_substitution(&var, &term)
+ {
+ modified = true;
+ simplified_formula = lhs.substitute(var, term);
+ }
+ }
+ _ => {
+ simplified_formula = formula;
+ }
+ },
+ Sort::Symbol => match term.clone() {
+ GeneralTerm::SymbolicTerm(_) => {
+ if !term_vars.contains(&var)
+ && !lhs.clone().unsafe_substitution(&var, &term)
+ {
+ modified = true;
+ simplified_formula = lhs.substitute(var, term);
+ }
+ }
+ _ => {
+ simplified_formula = formula;
+ }
+ },
+ }
+ }
+
+ _ => panic!("you're using the subsort equality fn wrong"),
+ }
+ (simplified_formula, modified)
+}
+
+// Given a tree of conjunctions, F1, .. Fi, .. Fn, identify an equality formula Fi: X = t or t = X
+// If possible, substitute t for X within the tree and drop Fi
+// Return the original formula and None if not possible
+// Otherwise, return the simplified formula and the (X, t) substitution pair
+fn simplify_conjunction_tree_with_equality(
+ formula: Formula,
+ enclosing_variables: Vec<Variable>,
+) -> (Formula, Option<(Variable, GeneralTerm)>) {
+ let mut result = (formula.clone(), None);
+ let conjunctive_terms = Formula::conjoin_invert(formula.clone());
+ for ct in conjunctive_terms.iter() {
+ // Search for an equality formula
+ if let Formula::AtomicFormula(AtomicFormula::Comparison(comp)) = ct {
+ if comp.equality_comparison() {
+ let term = &comp.term;
+ let g = comp.guards[0].clone();
+ let lhs_is_var = match term.clone() {
+ GeneralTerm::Variable(v) => Some(Variable {
+ sort: Sort::General,
+ name: v,
+ }),
+ GeneralTerm::IntegerTerm(IntegerTerm::Variable(v)) => Some(Variable {
+ sort: Sort::Integer,
+ name: v,
+ }),
+ GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(v)) => Some(Variable {
+ sort: Sort::Symbol,
+ name: v,
+ }),
+ _ => None,
+ };
+ let rhs_is_var = match g.term.clone() {
+ GeneralTerm::Variable(v) => Some(Variable {
+ sort: Sort::General,
+ name: v,
+ }),
+ GeneralTerm::IntegerTerm(IntegerTerm::Variable(v)) => Some(Variable {
+ sort: Sort::Integer,
+ name: v,
+ }),
+ GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(v)) => Some(Variable {
+ sort: Sort::Symbol,
+ name: v,
+ }),
+ _ => None,
+ };
+
+ let mut safety = true; // Simplify var = term or term = var but not both
+ // Don't restructure the conjunction tree unless simplification occurs
+ let mut restructured = vec![]; // Make the equality formula the top rhs leaf of a new conjunction tree
+ // for i in 0..conjunctive_terms.len() {
+ // if conjunctive_terms[i] != *ct {
+ // restructured.push(conjunctive_terms[i].clone());
+ // }
+ // }
+ for alt_ct in conjunctive_terms.clone() {
+ if alt_ct != *ct {
+ restructured.push(alt_ct);
+ }
+ }
+ restructured.push(ct.clone());
+
+ let simplified = Formula::conjoin(restructured);
+
+ if let Some(v1) = lhs_is_var {
+ if enclosing_variables.contains(&v1) {
+ let simplification_result =
+ subsort_equality(v1.clone(), g.term.clone(), simplified.clone());
+ if simplification_result.1 {
+ result = (simplification_result.0, Some((v1, g.term)));
+ safety = false;
+ }
+ }
+ }
+ if let Some(v2) = rhs_is_var {
+ if enclosing_variables.contains(&v2) && safety {
+ let simplification_result =
+ subsort_equality(v2.clone(), term.clone(), simplified);
+ if simplification_result.1 {
+ result = (simplification_result.0, Some((v2, term.clone())));
+ safety = false;
+ }
+ }
+ }
+ if !safety {
+ break;
+ }
+ }
+ }
+ }
+ result
+}
+
+// Checks if two equality comparisons V1 = t1 (t1 = V1) and V2 = t2 (t2 = V2)
+// satisfy that V1 is subsorteq to V2 and t1 = t2 and V1 and V2 occur in variables
+// Returns keep_var, drop_var, drop_term
+pub fn transitive_equality(
+ c1: Comparison,
+ c2: Comparison,
+ variables: Vec<Variable>,
+) -> Option<(Variable, Variable, Comparison)> {
+ let lhs1 = c1.term.clone();
+ let rhs1 = c1.guards[0].term.clone();
+ let lhs2 = c2.term.clone();
+ let rhs2 = c2.guards[0].term.clone();
+
+ let is_var = |term: GeneralTerm| match term {
+ GeneralTerm::Variable(ref v) => {
+ let var = Variable {
+ sort: Sort::General,
+ name: v.to_string(),
+ };
+ match variables.contains(&var) {
+ true => Some(var),
+ false => None,
+ }
+ }
+ GeneralTerm::IntegerTerm(IntegerTerm::Variable(ref v)) => {
+ let var = Variable {
+ sort: Sort::Integer,
+ name: v.to_string(),
+ };
+ match variables.contains(&var) {
+ true => Some(var),
+ false => None,
+ }
+ }
+ GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(ref v)) => {
+ let var = Variable {
+ sort: Sort::Symbol,
+ name: v.to_string(),
+ };
+ match variables.contains(&var) {
+ true => Some(var),
+ false => None,
+ }
+ }
+ _ => None,
+ };
+
+ // Is V1 a variable?
+ let lhs1_is_var = is_var(lhs1.clone());
+
+ // Is V2 a variable?
+ let lhs2_is_var = is_var(lhs2.clone());
+
+ // Is t1 a variable?
+ let rhs1_is_var = is_var(rhs1.clone());
+
+ // Is t2 a variable?
+ let rhs2_is_var = is_var(rhs2.clone());
+
+ let mut result = None;
+ match lhs1_is_var {
+ Some(v1) => match lhs2_is_var {
+ // v1 = rhs1
+ Some(v2) => {
+ // v1 = rhs1, v2 = rhs2
+ if rhs1 == rhs2 {
+ if subsort(&v1, &v2) {
+ result = Some((v1, v2, c2));
+ } else if subsort(&v2, &v1) {
+ result = Some((v2, v1, c1));
+ }
+ }
+ }
+ None => match rhs2_is_var {
+ Some(v2) => {
+ // v1 = rhs1, lhs2 = v2
+ if rhs1 == lhs2 {
+ if subsort(&v1, &v2) {
+ result = Some((v1, v2, c2));
+ } else if subsort(&v2, &v1) {
+ result = Some((v2, v1, c1));
+ }
+ }
+ }
+ None => result = None,
+ },
+ },
+ None => match rhs1_is_var {
+ Some(v1) => {
+ // lhs1 = v1
+ match lhs2_is_var {
+ Some(v2) => {
+ // lhs1 = v1, v2 = rhs2
+ if lhs1 == rhs2 {
+ if subsort(&v1, &v2) {
+ result = Some((v1, v2, c2));
+ } else if subsort(&v2, &v1) {
+ result = Some((v2, v1, c1));
+ }
+ }
+ }
+ None => match rhs2_is_var {
+ Some(v2) => {
+ // lhs1 = v1, lhs2 = v2
+ if lhs1 == lhs2 {
+ if subsort(&v1, &v2) {
+ result = Some((v1, v2, c2));
+ } else if subsort(&v2, &v1) {
+ result = Some((v2, v1, c1));
+ }
+ }
+ }
+ None => {
+ result = None;
+ }
+ },
+ }
+ }
+ None => {
+ result = None;
+ }
+ },
+ }
+ result
+}
+
+#[test]
+fn test_simplify_conjunction_tree() {
+ for (src, target) in [(
+ (
+ "X = Z and not q(X)",
+ vec![
+ Variable {
+ name: "X".to_string(),
+ sort: Sort::General,
+ },
+ Variable {
+ name: "Y".to_string(),
+ sort: Sort::General,
+ },
+ ],
+ ),
+ "not q(Z)",
+ )] {
+ let result = simplify_conjunction_tree_with_equality(src.0.parse().unwrap(), src.1).0;
+ let target = target.parse().unwrap();
+ assert_eq!(result, target, "{result} != {target}")
+ }
+}
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index c501ecbd..53d471f4 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -419,6 +419,12 @@ impl Comparison {
.collect(),
}
}
+
+ pub fn equality_comparison(&self) -> bool {
+ let guards = &self.guards;
+ let first = &guards[0];
+ guards.len() == 1 && first.relation == Relation::Equal
+ }
}
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
@@ -668,6 +674,24 @@ impl Formula {
.unwrap_or_else(|| Formula::AtomicFormula(AtomicFormula::Truth))
}
+ /// Inverse function to conjoin
+ pub fn conjoin_invert(formula: Formula) -> Vec<Formula> {
+ match formula {
+ Formula::BinaryFormula {
+ connective: BinaryConnective::Conjunction,
+ lhs,
+ rhs,
+ } => {
+ let mut formulas = Self::conjoin_invert(*lhs);
+ formulas.append(&mut Self::conjoin_invert(*rhs));
+ formulas
+ }
+ _ => {
+ vec![formula]
+ }
+ }
+ }
+
/// Recursively turn a list of formulas into a tree of disjunctions
pub fn disjoin(formulas: impl IntoIterator<Item = Formula>) -> Formula {
/*
@@ -801,6 +825,27 @@ impl Formula {
}
}
+ // Replacing var with term within self is unsafe if self contains a subformula
+ // of the form QxF, where var is free in F and a variable in term occurs in x
+ pub fn unsafe_substitution(self, var: &Variable, term: &GeneralTerm) -> bool {
+ match self {
+ Formula::AtomicFormula(_) => false,
+ Formula::UnaryFormula { formula, .. } => formula.unsafe_substitution(var, term),
+ Formula::BinaryFormula { lhs, rhs, .. } => {
+ lhs.unsafe_substitution(var, term) || rhs.unsafe_substitution(var, term)
+ }
+ Formula::QuantifiedFormula {
+ quantification,
+ formula,
+ } => {
+ let tvars = term.variables();
+ let qvars: IndexSet<Variable> = IndexSet::from_iter(quantification.variables);
+ let overlap: IndexSet<&Variable> = tvars.intersection(&qvars).collect();
+ formula.free_variables().contains(var) && !overlap.is_empty()
+ }
+ }
+ }
+
pub fn quantify(self, quantifier: Quantifier, variables: Vec<Variable>) -> Formula {
if variables.is_empty() {
self
diff --git a/src/translating/tau_star.rs b/src/translating/tau_star.rs
index 5510dbf4..62f07b65 100644
--- a/src/translating/tau_star.rs
+++ b/src/translating/tau_star.rs
@@ -1,5 +1,8 @@
use {
- crate::syntax_tree::{asp, fol},
+ crate::{
+ convenience::choose_fresh_variable_names,
+ syntax_tree::{asp, fol},
+ },
indexmap::IndexSet,
lazy_static::lazy_static,
regex::Regex,
@@ -39,40 +42,6 @@ fn choose_fresh_global_variables(program: &asp::Program) -> Vec<String> {
globals
}
-/// Choose `arity` variable names by incrementing `variant`, disjoint from `variables`
-fn choose_fresh_variable_names(
- variables: &IndexSet<fol::Variable>,
- variant: &str,
- arity: usize,
-) -> Vec<String> {
- let mut taken_vars = Vec::<String>::new();
- for var in variables.iter() {
- taken_vars.push(var.name.to_string());
- }
- let mut fresh_vars = Vec::<String>::new();
- let arity_bound = match taken_vars.contains(&variant.to_string()) {
- true => arity + 1,
- false => {
- fresh_vars.push(variant.to_string());
- arity
- }
- };
- for n in 1..arity_bound {
- let mut candidate: String = variant.to_owned();
- let number: &str = &n.to_string();
- candidate.push_str(number);
- let mut m = n;
- while taken_vars.contains(&candidate) || fresh_vars.contains(&candidate) {
- variant.clone_into(&mut candidate);
- m += 1;
- let number = &m.to_string();
- candidate.push_str(number);
- }
- fresh_vars.push(candidate.to_string());
- }
- fresh_vars
-}
-
// Z = t
fn construct_equality_formula(term: asp::Term, z: fol::Variable) -> fol::Formula {
let z_var_term = match z.sort {