Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Zach/simplifications #149

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 54 additions & 0 deletions src/convenience/mod.rs
Original file line number Diff line number Diff line change
@@ -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
}
626 changes: 613 additions & 13 deletions src/simplifying/fol/ht.rs

Large diffs are not rendered by default.

384 changes: 384 additions & 0 deletions src/simplifying/fol/mod.rs
Original file line number Diff line number Diff line change
@@ -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}")
}
}
45 changes: 45 additions & 0 deletions src/syntax_tree/fol.rs
Original file line number Diff line number Diff line change
@@ -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
39 changes: 4 additions & 35 deletions src/translating/tau_star.rs
Original file line number Diff line number Diff line change
@@ -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 {