Skip to content

Commit

Permalink
Evolog Modules: Parsing of module literals
Browse files Browse the repository at this point in the history
  • Loading branch information
madmike200590 committed Jul 24, 2024
1 parent 2b4f19d commit 49233d9
Show file tree
Hide file tree
Showing 13 changed files with 446 additions and 54 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ default Literal toLiteral() {

Set<VariableTerm> getOccurringVariables();

Atom substitute(Substitution substitution); // Introduce parameterized interface Substituable<A extends Atom> to get atom types right?
Atom substitute(Substitution substitution); // Introduce parameterized interface Substitutable<A extends Atom> to get atom types right?

Atom renameVariables(String newVariablePrefix);

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
package at.ac.tuwien.kr.alpha.api.programs.atoms;

import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.terms.Term;

import java.util.List;
import java.util.Optional;

/**
* An atom that is implemented using an additional ASP program (i.e. a module).
* Note that a module atom itself can not be instantiated, but needs to be compiled
* into some kind of instantiable atom by linking it to an ASP program that implements
* the referenced module.
*/
public interface ModuleAtom extends Atom {

String getModuleName();

List<Term> getInput();

List<Term> getOutput();

ModuleInstantiationMode getInstantiationMode();

@Override
ModuleAtom substitute(Substitution substitution);

interface ModuleInstantiationMode {
Optional<Integer> requestedAnswerSets();

ModuleInstantiationMode ALL = Optional::empty;

static ModuleInstantiationMode forNumAnswerSets(int answerSets) {
return () -> Optional.of(answerSets);
}

}

}
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
package at.ac.tuwien.kr.alpha.api.programs.literals;

import java.util.List;
import java.util.Set;

import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.Predicate;
import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm;

import java.util.List;
import java.util.Set;

/**
* A literal according to the ASP Core 2 Standard.
* <p>A literal according to the ASP Core 2 Standard.
* Wraps an {@link Atom} that may or may not be negated.
*
* </p>
* Copyright (c) 2017-2021, the Alpha Team.
*/
// TODO go through implementations and pull out stuff that can be default-implemented here
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
package at.ac.tuwien.kr.alpha.api.programs.literals;

import at.ac.tuwien.kr.alpha.api.programs.atoms.ModuleAtom;
import at.ac.tuwien.kr.alpha.api.grounder.Substitution;

public interface ModuleLiteral extends Literal{

@Override
ModuleAtom getAtom();

@Override
ModuleLiteral negate();

@Override
ModuleLiteral substitute(Substitution substitution);

}
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ public Set<VariableTerm> getOccurringVariables() {
/**
* Returns whether this atom is ground, i.e., variable-free.
*
* @return true iff the terms of this atom contain no {@link VariableTermImpl}.
* @return true iff the terms of this atom contain no {@link VariableTerm}.
*/
@Override
public abstract boolean isGround();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,9 @@
import at.ac.tuwien.kr.alpha.api.ComparisonOperator;
import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation;
import at.ac.tuwien.kr.alpha.api.programs.Predicate;
import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.*;
import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom.AggregateElement;
import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom.AggregateFunctionSymbol;
import at.ac.tuwien.kr.alpha.api.programs.atoms.AtomQuery;
import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.ComparisonAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.ExternalAtom;
import at.ac.tuwien.kr.alpha.api.programs.literals.Literal;
import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
import at.ac.tuwien.kr.alpha.commons.programs.atoms.AggregateAtomImpl.AggregateElementImpl;
Expand Down Expand Up @@ -63,6 +59,10 @@ public static ExternalAtom newExternalAtom(Predicate predicate, PredicateInterpr
return new ExternalAtomImpl(predicate, interpretation, input, output);
}

public static ModuleAtom newModuleAtom(String moduleName, ModuleAtom.ModuleInstantiationMode instantiationMode, List<Term> input, List<Term> output) {
return new ModuleAtomImpl(moduleName, input, output, instantiationMode);
}

public static AtomQuery query(Predicate predicate) {
return AtomQueryImpl.forPredicate(predicate);
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,132 @@
package at.ac.tuwien.kr.alpha.commons.programs.atoms;

import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.Predicate;
import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.ModuleAtom;
import at.ac.tuwien.kr.alpha.api.programs.literals.ModuleLiteral;
import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
import at.ac.tuwien.kr.alpha.commons.Predicates;
import at.ac.tuwien.kr.alpha.commons.programs.literals.Literals;
import at.ac.tuwien.kr.alpha.commons.util.Util;
import org.apache.commons.collections4.ListUtils;

import java.util.List;
import java.util.Objects;
import java.util.stream.Collectors;

class ModuleAtomImpl extends AbstractAtom implements ModuleAtom {

private final String moduleName;
private final List<Term> input;
private final List<Term> output;
private final ModuleInstantiationMode instantiationMode;

ModuleAtomImpl(String moduleName, List<Term> input, List<Term> output, ModuleInstantiationMode instantiationMode) {
this.moduleName = Objects.requireNonNull(moduleName);
this.input = Objects.requireNonNull(input);
this.output = Objects.requireNonNull(output);
this.instantiationMode = Objects.requireNonNull(instantiationMode);
}

@Override
public String getModuleName() {
return moduleName;
}

@Override
public List<Term> getInput() {
return input;
}

@Override
public List<Term> getOutput() {
return output;
}

@Override
public ModuleInstantiationMode getInstantiationMode() {
return instantiationMode;
}

@Override
public Atom withTerms(List<Term> terms) {
if (terms.size() != this.input.size() + this.output.size()) {
throw new IllegalArgumentException(
"Cannot apply term list " + terms + " to module atom " + this + ", terms has invalid size!");
}
List<Term> newInput = terms.subList(0, this.input.size());
List<Term> newOutput = terms.subList(this.input.size(), terms.size());
return new ModuleAtomImpl(this.moduleName, newInput, newOutput, this.instantiationMode);
}

@Override
public ModuleAtom substitute(Substitution substitution) {
List<Term> substitutedInput = this.input.stream().map(t -> t.substitute(substitution)).collect(Collectors.toList());
List<Term> substitutedOutput = this.output.stream().map(t -> t.substitute(substitution)).collect(Collectors.toList());
return new ModuleAtomImpl(this.moduleName, substitutedInput, substitutedOutput, this.instantiationMode);
}

@Override
public List<Term> getTerms() {
return ListUtils.union(input, output);
}

@Override
public Predicate getPredicate() {
return Predicates.getPredicate(moduleName, output.size());
}

@Override
public boolean isGround() {
for (Term t : input) {
if (!t.isGround()) {
return false;
}
}
for (Term t : output) {
if (!t.isGround()) {
return false;
}
}
return true;
}

@Override
public ModuleLiteral toLiteral(boolean positive) {
return Literals.fromAtom(this, positive);
}

@Override
public boolean equals(Object o) {
if (this == o) {
return true;
}
if (o == null || getClass() != o.getClass()) {
return false;
}
ModuleAtomImpl that = (ModuleAtomImpl) o;
return Objects.equals(moduleName, that.moduleName)
&& Objects.equals(input, that.input)
&& Objects.equals(output, that.output)
&& Objects.equals(instantiationMode, that.instantiationMode);
}

@Override
public int hashCode() {
return Objects.hash(moduleName, input, output, instantiationMode);
}

@Override
public String toString() {
String result = "#" + moduleName;
if (!input.isEmpty()) {
result += Util.join("[", input, "]");
}
if (!output.isEmpty()) {
result += Util.join("(", output, ")");
}
return result;
}

}
Original file line number Diff line number Diff line change
@@ -1,13 +1,7 @@
package at.ac.tuwien.kr.alpha.commons.programs.literals;

import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.ComparisonAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.ExternalAtom;
import at.ac.tuwien.kr.alpha.api.programs.literals.AggregateLiteral;
import at.ac.tuwien.kr.alpha.api.programs.literals.BasicLiteral;
import at.ac.tuwien.kr.alpha.api.programs.literals.ComparisonLiteral;
import at.ac.tuwien.kr.alpha.api.programs.literals.ExternalLiteral;
import at.ac.tuwien.kr.alpha.api.programs.atoms.*;
import at.ac.tuwien.kr.alpha.api.programs.literals.*;

public final class Literals {

Expand All @@ -30,7 +24,11 @@ public static ComparisonLiteral fromAtom(ComparisonAtom atom, boolean positive)
public static ExternalLiteral fromAtom(ExternalAtom atom, boolean positive) {
return new ExternalLiteralImpl(atom, positive);
}


public static ModuleLiteral fromAtom(ModuleAtom atom, boolean positive) {
return new ModuleLiteralImpl(atom, positive);
}

public static ComparisonLiteral newComparisonLiteral(ComparisonAtom atom, boolean positive) {
return new ComparisonLiteralImpl(atom, positive);
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
package at.ac.tuwien.kr.alpha.commons.programs.literals;

import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.atoms.ModuleAtom;
import at.ac.tuwien.kr.alpha.api.programs.literals.ModuleLiteral;
import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm;

import java.util.Collections;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

class ModuleLiteralImpl extends AbstractLiteral implements ModuleLiteral {

ModuleLiteralImpl(ModuleAtom atom, boolean positive) {
super(atom, positive);
}

@Override
public ModuleAtom getAtom() {
return (ModuleAtom) atom;
}

@Override
public ModuleLiteral negate() {
return new ModuleLiteralImpl(getAtom(), isNegated());
}

@Override
public ModuleLiteral substitute(Substitution substitution) {
return new ModuleLiteralImpl(getAtom().substitute(substitution), positive);
}

// TODO introduce common abstract supertype for external an module literals to avoid code duplication (same goes for atoms!)
@Override
public Set<VariableTerm> getBindingVariables() {
// If the external atom is negative, then all variables of input and output are non-binding
// and there are no binding variables (like for ordinary atoms).
// If the external atom is positive, then variables of output are binding.

if (this.isNegated()) {
return Collections.emptySet();
}

List<Term> output = getAtom().getOutput();

Set<VariableTerm> binding = new HashSet<>(output.size());

for (Term out : output) {
if (out instanceof VariableTerm) {
binding.add((VariableTerm) out);
}
}

return binding;
}

@Override
public Set<VariableTerm> getNonBindingVariables() {
List<Term> input = getAtom().getInput();
List<Term> output = getAtom().getOutput();

// External atoms have their input always non-binding, since they cannot
// be queried without some concrete input.
Set<VariableTerm> nonbindingVariables = new HashSet<>();
for (Term term : input) {
nonbindingVariables.addAll(term.getOccurringVariables());
}

// If the external atom is negative, then all variables of input and output are
// non-binding.
if (this.isNegated()) {
for (Term out : output) {
if (out instanceof VariableTerm) {
nonbindingVariables.add((VariableTerm) out);
}
}
}

return nonbindingVariables;
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ weight_at_level : term (AT term)? (COMMA terms)?;

naf_literals : naf_literal (COMMA naf_literals)?;

naf_literal : NAF? (external_atom | classical_literal | builtin_atom);
naf_literal : NAF? (external_atom | module_atom | classical_literal | builtin_atom);

id : ID | TEST_EXPECT | TEST_UNSAT | TEST_GIVEN | TEST_ASSERT_ALL | TEST_ASSERT_SOME | DIRECTIVE_ENUM | DIRECTIVE_TEST;

Expand Down Expand Up @@ -87,6 +87,8 @@ interval_bound : numeral | VARIABLE;

external_atom : MINUS? AMPERSAND id (SQUARE_OPEN input = terms SQUARE_CLOSE)? (PAREN_OPEN output = terms PAREN_CLOSE)?; // NOT Core2 syntax.

module_atom : SHARP id (CURLY_OPEN NUMBER CURLY_CLOSE)? (SQUARE_OPEN input = terms SQUARE_CLOSE)? (PAREN_OPEN output = terms PAREN_CLOSE)?; // NOT Core2 syntax.

directive : directive_enumeration | directive_test | directive_module; // NOT Core2 syntax, allows solver specific directives. Further directives shall be added here.

directive_enumeration : SHARP DIRECTIVE_ENUM id DOT; // NOT Core2 syntax, used for aggregate translation.
Expand Down
Loading

0 comments on commit 49233d9

Please sign in to comment.