Skip to content

Commit

Permalink
Add missing error messages and rework translation
Browse files Browse the repository at this point in the history
  • Loading branch information
@aannleax
aannleax committed Apr 25, 2024
1 parent 2e6f69b commit 54677de
Show file tree
Hide file tree
Showing 5 changed files with 208 additions and 168 deletions.
39 changes: 15 additions & 24 deletions nemo/src/io/parser/types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,33 +143,27 @@ pub enum ParseError {
/// A wildcard pattern was used inside of the rule head.
#[error(r#"rule head must not contain unnamed variables "_""#)]
UnnamedInHead,
/// The universal variable does not occur in a positive body literal.
#[error(r#"the universal variable "{0}" must occur in a positive body literal"#)]
/// The universal variable is not safe or derived.
#[error(r#"variable "{0}" appears in the head but cannot be derived from the body"#)]
UnsafeHeadVariable(Variable),
/// The variable must only depend on variables that occur in a positive body literal.
#[error(r#"the variable "{0}" must only depend on variables that occur in a positive body literals"#)]
UnsafeDefinition(Variable),
/// Negated literal uses a complex term.
#[error(r#"negated literal "{0}" uses the complex term "{1}""#)]
NegatedLiteralComplex(String, String),
/// Negated literal uses a derived variable.
#[error(r#"negated literal "{0}" uses a derived variable "{1}""#)]
NegatedLiteralDerived(String, Variable),
/// Complex term uses a derived variable.
#[error(r#"complex term "{0}" uses a derived variable "{1}""#)]
ComplexTermDerived(String, Variable),
/// Complex term uses an unsafe variable.
#[error(r#"complex term "{0}" uses an unsafe variable "{1}""#)]
#[error(r#"the value of variable "{1}" contained in term "{0}" cannot be derived"#)]
UnsafeComplexTerm(String, Variable),
/// Variable has been defined multiple times.
#[error(r#"the variable "{0}" has been used in multiple equalities"#)]
MultipleDefinitions(Variable),
/// The unsafe variable appears in multiple negative body literals.
#[error(r#"the unsafe variable "{0}" appears in multiple negative body literals"#)]
UnsafeVariableInMultipleNegativeLiterals(Variable),
/// A variable used in a comparison does not occur in a positive body literal.
#[error(r#"the variable "{0}" used in a comparison; must occur in a positive body literal"#)]
UnsafeFilterVariable(Variable),
/// Constraint on unsafe unsafe variable may only use variables from that negated literal
#[error(r#"Term "{0}" uses variable {1} from negated literal {2} but also the variable {3}, which does not appear in it."#)]
ConstraintOutsideVariable(String, Variable, String, Variable),
/// An aggregate term occurs in the body of a rule.
#[error(r#"An aggregate term ("{0}") occurs in the body of a rule"#)]
AggregateInBody(Aggregate),
/// Multiple aggregates in one rule
#[error("Currently, only one aggregate per rule is supported.")]
MultipleAggregates,
/// Aggregates cannot be used within existential rules
#[error("Aggregates may not appear in existential rules.")]
AggregatesPlusExistentials,
/// A variable is both existentially and universally quantified
#[error(r#"variables named "{0}" occur with existential and universal quantification"#)]
BothQuantifiers(String),
Expand Down Expand Up @@ -317,9 +311,6 @@ pub enum ParseError {
/// Expected an parenthesised term tree.
#[error("Expected an parenthesised term tree")]
ExpectedParenthesisedTerm,
/// An aggregate term occurs in the body of a rule.
#[error(r#"An term ("{0}") occurs in the body of a rule"#)]
AggregateInBody(Aggregate),
/// Unknown aggregate operation
#[error(r#"Aggregate operation "{0}" is not known"#)]
UnknownAggregateOperation(String),
Expand Down
206 changes: 89 additions & 117 deletions nemo/src/model/chase_model/rule.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -455,149 +455,121 @@ impl ChaseRule {
new_constraints
}

/// Seperate different [Constraint]s of the given [Rule] into several categories.
fn seperate_constraints(
fn compute_derived_variables(
rule: &Rule,
aggregate: &Option<ChaseAggregate>,
negative_body: &[VariableAtom],
constraints: &mut ConstraintCategories,
) {
let safe_variables = rule.safe_variables();
let mut known_variables = safe_variables.clone();

let mut negative_variables = HashMap::<Variable, usize>::new();
for (body_index, negative_atom) in negative_body.iter().enumerate() {
for variable in negative_atom.terms() {
if !safe_variables.contains(variable) {
negative_variables.insert(variable.clone(), body_index);
known_variables.insert(variable.clone());
}
}
}

assigned_constraints: &mut HashSet<usize>,
) -> HashSet<Variable> {
let mut derived_variables = rule.safe_variables();
let mut aggregate_variables = HashSet::<Variable>::new();
if let Some(aggregate) = aggregate {
aggregate_variables.insert(aggregate.output_variable.clone());
known_variables.insert(aggregate.output_variable.clone());
}

let mut positive_variables = safe_variables.clone();
let mut update = true;
while update {
let num_assigned_constraints = assigned_constraints.len();

let mut assigned_constraints = HashSet::<usize>::new();
while assigned_constraints.len() < rule.constraints().len() {
let num_assigned = assigned_constraints.len();

for current_constraint_index in 0..rule.constraints().len() {
if assigned_constraints.contains(&current_constraint_index) {
for (constraint_index, constraint) in rule.constraints().iter().enumerate() {
if assigned_constraints.contains(&constraint_index) {
continue;
}
let current_constraint = &rule.constraints()[current_constraint_index];

if let Some((variable, term)) = current_constraint.has_form_assignment() {
if !positive_variables.contains(variable)
&& !aggregate_variables.contains(variable)
if let Some((variable, term)) = constraint.has_form_assignment() {
if derived_variables.contains(variable)
|| aggregate_variables.contains(variable)
{
enum TermStatus {
Undefined,
Positive,
Aggregate,
}
let mut status = TermStatus::Positive;

for subvariable in term.variables() {
if aggregate_variables.contains(subvariable) {
status = TermStatus::Aggregate;
break;
} else if !known_variables.contains(subvariable) {
status = TermStatus::Undefined;
break;
}
}

match status {
TermStatus::Undefined => {
continue;
}
TermStatus::Positive => {
constraints
.positive_constructors
.push(Constructor::new(variable.clone(), term.clone()));
positive_variables.insert(variable.clone());
known_variables.insert(variable.clone());

assigned_constraints.insert(current_constraint_index);
continue;
}
TermStatus::Aggregate => {
constraints
.aggregate_constructors
.push(Constructor::new(variable.clone(), term.clone()));
aggregate_variables.insert(variable.clone());
known_variables.insert(variable.clone());

assigned_constraints.insert(current_constraint_index);
continue;
}
}
}
}

enum TermLayer {
Positive,
Aggregate,
Undefined,
}

enum TermNegation {
None,
Negated(usize),
}

let mut layer = TermLayer::Positive;
let mut negation = TermNegation::None;

for subvariable in current_constraint.variables() {
if aggregate_variables.contains(subvariable) {
layer = TermLayer::Aggregate;
} else if let Some(atom_index) = negative_variables.get(subvariable) {
negation = TermNegation::Negated(*atom_index);
} else if !known_variables.contains(subvariable) {
layer = TermLayer::Undefined;
break;
continue;
}
}

match layer {
TermLayer::Positive => {
if !derived_variables.contains(variable)
&& term
.variables()
.all(|variable| derived_variables.contains(variable))
{
derived_variables.insert(variable.clone());
constraints
.positive_constraints
.push(current_constraint.clone());
assigned_constraints.insert(current_constraint_index);
.positive_constructors
.push(Constructor::new(variable.clone(), term.clone()));
assigned_constraints.insert(constraint_index);
continue;
}
TermLayer::Aggregate => {

if !aggregate_variables.contains(variable)
&& term.variables().all(|variable| {
derived_variables.contains(variable)
|| aggregate_variables.contains(variable)
})
{
aggregate_variables.insert(variable.clone());
constraints
.aggregate_constraints
.push(current_constraint.clone());
assigned_constraints.insert(current_constraint_index);
.aggregate_constructors
.push(Constructor::new(variable.clone(), term.clone()));
assigned_constraints.insert(constraint_index);
continue;
}
TermLayer::Undefined => {}
}
}

if !matches!(layer, TermLayer::Undefined) {
match negation {
TermNegation::None => {}
TermNegation::Negated(index) => {
constraints.negative_constraints[index]
.push(current_constraint.clone());
}
}
update = num_assigned_constraints != assigned_constraints.len();
}

derived_variables
}

/// Seperate different [Constraint]s of the given [Rule] into several categories.
fn seperate_constraints(
rule: &Rule,
aggregate: &Option<ChaseAggregate>,
negative_body: &[VariableAtom],
constraints: &mut ConstraintCategories,
) {
let mut assigned_constraints = HashSet::<usize>::new();
let derived_variables = Self::compute_derived_variables(
rule,
aggregate,
constraints,
&mut assigned_constraints,
);

let mut negative_variables = HashMap::<Variable, usize>::new();
for (body_index, negative_atom) in negative_body.iter().enumerate() {
for variable in negative_atom.terms() {
if !derived_variables.contains(variable) {
negative_variables.insert(variable.clone(), body_index);
}
}
}

if assigned_constraints.len() == num_assigned {
unreachable!("A well-formed rule should have no cyclic dependencies");
for (constraint_index, constraint) in rule.constraints().iter().enumerate() {
if assigned_constraints.contains(&constraint_index) {
continue;
}

// Constraint on derived variables
if constraint
.variables()
.all(|variable| derived_variables.contains(variable))
{
constraints.positive_constraints.push(constraint.clone());
assigned_constraints.insert(constraint_index);
continue;
}

// Constraint on negative variables
for variable in constraint.variables() {
if let Some(negative_index) = negative_variables.get(variable) {
constraints.negative_constraints[*negative_index].push(constraint.clone());
assigned_constraints.insert(constraint_index);
continue;
}
}

// Constraints on aggregates are currently not expressible
}

debug_assert!(assigned_constraints.len() == rule.constraints().len());
}
}

Expand Down
Loading

0 comments on commit 54677de

Please sign in to comment.