diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/AnswerSetToXlsxWriterTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/AnswerSetToXlsxWriterTest.java index f1bf9e441..c3887321f 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/AnswerSetToXlsxWriterTest.java +++ b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/AnswerSetToXlsxWriterTest.java @@ -19,6 +19,7 @@ import at.ac.tuwien.kr.alpha.app.mappers.AnswerSetToWorkbookMapperTest; import at.ac.tuwien.kr.alpha.commons.AnswerSetBuilder; +// TODO this is an integration test public class AnswerSetToXlsxWriterTest { @Test diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/MainTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/MainTest.java index a6b26f307..97fec5bee 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/MainTest.java +++ b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/MainTest.java @@ -39,6 +39,7 @@ import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; +// TODO this is an end-to-end test public class MainTest { private static final String INPUT = "p(a). " + System.lineSeparator() + " b :- p(X)." + System.lineSeparator(); diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/ComponentGraphWriterTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/ComponentGraphWriterTest.java index fff165831..39273cf20 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/ComponentGraphWriterTest.java +++ b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/ComponentGraphWriterTest.java @@ -11,6 +11,7 @@ import at.ac.tuwien.kr.alpha.api.impl.AlphaImpl; import at.ac.tuwien.kr.alpha.api.programs.analysis.ComponentGraph; +// TODO This is a functional test and should not be run with standard unit tests public class ComponentGraphWriterTest { private static final String LS = System.lineSeparator(); diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/DependencyGraphWriterTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/DependencyGraphWriterTest.java index b487e8479..942da90a5 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/DependencyGraphWriterTest.java +++ b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/DependencyGraphWriterTest.java @@ -11,6 +11,7 @@ import at.ac.tuwien.kr.alpha.api.impl.AlphaImpl; import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph; +// TODO This is a functional test and should not be run with standard unit tests public class DependencyGraphWriterTest { private static final String LS = System.lineSeparator(); diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/mappers/AnswerSetToWorkbookMapperTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/mappers/AnswerSetToWorkbookMapperTest.java index a2433d692..b528cd500 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/mappers/AnswerSetToWorkbookMapperTest.java +++ b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/mappers/AnswerSetToWorkbookMapperTest.java @@ -22,6 +22,7 @@ import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.commons.AnswerSetBuilder; +// TODO This is a functional test and should not be run with standard unit tests public class AnswerSetToWorkbookMapperTest { private AnswerSetToWorkbookMapper mapper = new AnswerSetToWorkbookMapper(); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/externals/AspStandardLibrary.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/AspStandardLibrary.java similarity index 99% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/externals/AspStandardLibrary.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/AspStandardLibrary.java index 30aad5eed..14142ed62 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/externals/AspStandardLibrary.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/AspStandardLibrary.java @@ -23,7 +23,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.externals; +package at.ac.tuwien.kr.alpha.commons.externals; import java.time.LocalDateTime; import java.time.format.DateTimeFormatter; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/BinaryPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/BinaryPredicateInterpretation.java similarity index 96% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/BinaryPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/BinaryPredicateInterpretation.java index d0f62b756..22150b49f 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/BinaryPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/BinaryPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import java.util.List; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/BindingMethodPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/BindingMethodPredicateInterpretation.java similarity index 98% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/BindingMethodPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/BindingMethodPredicateInterpretation.java index a73aae4b2..a12c6f44d 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/BindingMethodPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/BindingMethodPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import org.apache.commons.lang3.ClassUtils; import org.apache.commons.lang3.StringUtils; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/externals/Externals.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/Externals.java similarity index 90% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/externals/Externals.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/Externals.java index a4e02806a..386c8c983 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/externals/Externals.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/Externals.java @@ -23,7 +23,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.externals; +package at.ac.tuwien.kr.alpha.commons.externals; import java.lang.reflect.Method; import java.util.ArrayList; @@ -44,13 +44,6 @@ import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.BinaryPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.BindingMethodPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.IntPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.LongPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.MethodPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.SuppliedPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.UnaryPredicateInterpretation; public final class Externals { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/IntPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/IntPredicateInterpretation.java similarity index 96% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/IntPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/IntPredicateInterpretation.java index dd8acc05e..36d0a06bc 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/IntPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/IntPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import java.util.List; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/LongPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/LongPredicateInterpretation.java similarity index 96% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/LongPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/LongPredicateInterpretation.java index e5ef94663..e7978f3c8 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/LongPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/LongPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import java.util.List; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/MethodPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/MethodPredicateInterpretation.java similarity index 97% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/MethodPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/MethodPredicateInterpretation.java index ff7dc78f6..c4aaacbdc 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/MethodPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/MethodPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import org.apache.commons.lang3.ClassUtils; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/NonBindingPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/NonBindingPredicateInterpretation.java similarity index 97% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/NonBindingPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/NonBindingPredicateInterpretation.java index 53ad2350b..7a065aa7c 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/NonBindingPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/NonBindingPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/PredicateInterpretationImpl.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/PredicateInterpretationImpl.java new file mode 100644 index 000000000..8e52bfacb --- /dev/null +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/PredicateInterpretationImpl.java @@ -0,0 +1,14 @@ +package at.ac.tuwien.kr.alpha.commons.externals; + +import java.util.List; +import java.util.Set; + +import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; +import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.api.terms.Term; + +// TODO this looks like a duplicate +public interface PredicateInterpretationImpl extends PredicateInterpretation { + @Override + Set>> evaluate(List terms); +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/SuppliedPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/SuppliedPredicateInterpretation.java similarity index 97% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/SuppliedPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/SuppliedPredicateInterpretation.java index a29adffbf..1efa81425 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/SuppliedPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/SuppliedPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.BindingPredicateInterpretation; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/UnaryPredicateInterpretation.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/UnaryPredicateInterpretation.java similarity index 96% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/UnaryPredicateInterpretation.java rename to alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/UnaryPredicateInterpretation.java index 5e90b4712..10611bcdc 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/fixedinterpretations/UnaryPredicateInterpretation.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/externals/UnaryPredicateInterpretation.java @@ -25,7 +25,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.common.fixedinterpretations; +package at.ac.tuwien.kr.alpha.commons.externals; import java.util.List; diff --git a/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/atoms/BasicAtomImplTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/atoms/BasicAtomImplTest.java new file mode 100644 index 000000000..275aa413e --- /dev/null +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/atoms/BasicAtomImplTest.java @@ -0,0 +1,67 @@ +package at.ac.tuwien.kr.alpha.commons.atoms; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import org.junit.jupiter.api.Test; + +import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.terms.Terms; + +/** + * Test for basic functionality of various implementations of {@link Atom}. + * + * Copyright (c) 2019-2021, the Alpha Team. + */ +public class BasicAtomImplTest { + + @Test + public void testIsBasicAtomGround() { + BasicAtomImpl a = new BasicAtomImpl(Predicates.getPredicate("bla", 2), Terms.newSymbolicConstant("blubb"), + Terms.newFunctionTerm("foo", Terms.newSymbolicConstant("bar"))); + assertTrue(a.isGround()); + BasicAtomImpl a1 = new BasicAtomImpl(Predicates.getPredicate("foo", 4), Terms.newConstant(1), Terms.newConstant(2), Terms.newConstant(3), + Terms.newConstant("bar")); + assertTrue(a1.isGround()); + BasicAtomImpl a2 = new BasicAtomImpl(Predicates.getPredicate("foo", 1), Terms.newVariable("BAR")); + assertFalse(a2.isGround()); + BasicAtomImpl a3 = new BasicAtomImpl(Predicates.getPredicate("foo", 3), Terms.newSymbolicConstant("b"), Terms.newSymbolicConstant("a"), + Terms.newFunctionTerm("r", Terms.newConstant("bla"), Terms.newVariable("BLUBB"))); + assertFalse(a3.isGround()); + } + + @Test + public void testAreBasicAtomsEqual() { + BasicAtomImpl a1 = new BasicAtomImpl(Predicates.getPredicate("bla", 2), Terms.newSymbolicConstant("blubb"), + Terms.newFunctionTerm("foo", Terms.newSymbolicConstant("bar"))); + BasicAtomImpl a2 = new BasicAtomImpl(Predicates.getPredicate("bla", 2), Terms.newSymbolicConstant("blubb"), + Terms.newFunctionTerm("foo", Terms.newSymbolicConstant("bar"))); + assertEquals(a1, a2); + + BasicAtomImpl a3 = new BasicAtomImpl(Predicates.getPredicate("foo", 4), Terms.newConstant(1), Terms.newConstant(2), Terms.newConstant(3), + Terms.newConstant("bar")); + BasicAtomImpl a4 = new BasicAtomImpl(Predicates.getPredicate("foo", 4), Terms.newConstant(1), Terms.newConstant(2), Terms.newConstant(3), + Terms.newConstant("bar")); + assertEquals(a3, a4); + + BasicAtomImpl a5 = new BasicAtomImpl(Predicates.getPredicate("foo", 1), Terms.newVariable("BAR")); + BasicAtomImpl a6 = new BasicAtomImpl(Predicates.getPredicate("foo", 1), Terms.newVariable("BAR")); + assertEquals(a5, a6); + + BasicAtomImpl a7 = new BasicAtomImpl(Predicates.getPredicate("foo", 3), Terms.newSymbolicConstant("b"), Terms.newSymbolicConstant("a"), + Terms.newFunctionTerm("r", Terms.newConstant("bla"), Terms.newVariable("BLUBB"))); + BasicAtomImpl a8 = new BasicAtomImpl(Predicates.getPredicate("foo", 3), Terms.newSymbolicConstant("b"), Terms.newSymbolicConstant("a"), + Terms.newFunctionTerm("r", Terms.newConstant("bla"), Terms.newVariable("BLUBB"))); + assertEquals(a7, a8); + + assertFalse(a1.equals(a3)); + assertFalse(a3.equals(a1)); + assertFalse(a1.equals(a5)); + assertFalse(a5.equals(a1)); + assertFalse(a1.equals(a7)); + assertFalse(a7.equals(a1)); + } + +} diff --git a/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/atoms/ExternalAtomImplTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/atoms/ExternalAtomImplTest.java new file mode 100644 index 000000000..d762709b5 --- /dev/null +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/atoms/ExternalAtomImplTest.java @@ -0,0 +1,104 @@ +package at.ac.tuwien.kr.alpha.commons.atoms; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; +import at.ac.tuwien.kr.alpha.api.externals.Predicate; +import at.ac.tuwien.kr.alpha.api.programs.atoms.ExternalAtom; +import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.api.terms.Term; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; +import at.ac.tuwien.kr.alpha.commons.terms.Terms; + +public class ExternalAtomImplTest { + + private Map externals; + + public ExternalAtomImplTest() throws NoSuchMethodException, SecurityException { + externals = new HashMap<>(); + externals.put("isFoo", Externals.processPredicateMethod(ExternalAtomImplTest.class.getMethod("isFoo", int.class))); + externals.put("extWithOutput", Externals.processPredicateMethod(ExternalAtomImplTest.class.getMethod("extWithOutput", int.class))); + } + + @Predicate + public static final boolean isFoo(int bar) { + return 0xF00 == bar; + } + + @Predicate + public static final Set>> extWithOutput(int in) { + Set>> retVal = new HashSet<>(); + List> lst = new ArrayList<>(); + lst.add(Terms.newConstant(in)); + retVal.add(lst); + return retVal; + } + + @Test + public void testIsExternalAtomGround() { + List ext1Input = new ArrayList<>(); + ext1Input.add(Terms.newConstant(1)); + // ext1 := &isFoo[1] + ExternalAtom ext1 = Atoms.newExternalAtom(Predicates.getPredicate("isFoo", 1), externals.get("isFoo"), ext1Input, Collections.emptyList()); + assertTrue(ext1.isGround()); + + // ext2 := &isFoo[bar(1)] + List ext2Input = new ArrayList<>(); + ext2Input.add(Terms.newFunctionTerm("bar", Terms.newConstant(1))); + ExternalAtom ext2 = Atoms.newExternalAtom(Predicates.getPredicate("isFoo", 1), externals.get("isFoo"), ext2Input, Collections.emptyList()); + assertTrue(ext2.isGround()); + + // ext3 := &isFoo[BLA] + List ext3Input = new ArrayList<>(); + ext3Input.add(Terms.newVariable("BLA")); + ExternalAtom ext3 = Atoms.newExternalAtom(Predicates.getPredicate("isFoo", 1), externals.get("isFoo"), ext3Input, Collections.emptyList()); + assertFalse(ext3.isGround()); + } + + @Test + @SuppressWarnings("unlikely-arg-type") + public void testAreExternalAtomsEqual() { + // ext1 := &isFoo[1] + List ext1Input = new ArrayList<>(); + ext1Input.add(Terms.newConstant(1)); + ExternalAtom ext1 = Atoms.newExternalAtom(Predicates.getPredicate("isFoo", 1), externals.get("isFoo"), ext1Input, Collections.emptyList()); + // ext2 := &isFoo[1] + List ext2Input = new ArrayList<>(); + ext2Input.add(Terms.newConstant(1)); + ExternalAtom ext2 = Atoms.newExternalAtom(Predicates.getPredicate("isFoo", 1), externals.get("isFoo"), ext2Input, Collections.emptyList()); + + assertEquals(ext1, ext2); + assertEquals(ext2, ext1); + + assertFalse(ext1.equals(null)); + assertFalse(ext1.equals("bla")); + assertTrue(ext1.hashCode() == ext2.hashCode()); + } + + @Test + public void testExternalHasOutput() { + // ext := &extWithOutput[1](OUT) + List input = new ArrayList<>(); + List output = new ArrayList<>(); + input.add(Terms.newConstant(1)); + output.add(Terms.newVariable("OUT")); + ExternalAtom ext = Atoms.newExternalAtom(Predicates.getPredicate("extWithOutput", 2), externals.get("extWithOutput"), input, output); + + assertFalse(ext.isGround()); + assertTrue(ext.hasOutput()); + } + +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/externals/AspStandardLibraryTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/externals/AspStandardLibraryTest.java similarity index 98% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/externals/AspStandardLibraryTest.java rename to alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/externals/AspStandardLibraryTest.java index 2e2e954ce..75efaa200 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/externals/AspStandardLibraryTest.java +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/externals/AspStandardLibraryTest.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.externals; +package at.ac.tuwien.kr.alpha.commons.externals; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertFalse; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/atoms/LiteralBindingNonBindingVariablesTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/literals/LiteralBindingNonBindingVariablesTest.java similarity index 61% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/atoms/LiteralBindingNonBindingVariablesTest.java rename to alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/literals/LiteralBindingNonBindingVariablesTest.java index 5b0370e9e..e60887fed 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/atoms/LiteralBindingNonBindingVariablesTest.java +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/literals/LiteralBindingNonBindingVariablesTest.java @@ -23,30 +23,29 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.atoms; +package at.ac.tuwien.kr.alpha.commons.literals; import static org.junit.jupiter.api.Assertions.assertEquals; +import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; -import java.util.HashMap; -import java.util.Map; +import java.util.List; import java.util.Set; import java.util.stream.Collectors; import org.junit.jupiter.api.Disabled; import org.junit.jupiter.api.Test; -import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; -import at.ac.tuwien.kr.alpha.api.rules.Rule; -import at.ac.tuwien.kr.alpha.api.rules.heads.Head; +import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.IntPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; +import at.ac.tuwien.kr.alpha.commons.externals.IntPredicateInterpretation; +import at.ac.tuwien.kr.alpha.commons.terms.Terms; /** * Tests the behaviour of {@link Literal#getBindingVariables()} and {@link Literal#getNonBindingVariables()} @@ -55,12 +54,10 @@ */ public class LiteralBindingNonBindingVariablesTest { - private final Map externals = new HashMap<>(); - private final ProgramParser parser = new ProgramParserImpl(); - @Test public void testPositiveBasicLiteral() { - Literal literal = parser.parse("p(X,Y) :- q(X,Y).").getRules().get(0).getBody().stream().findFirst().get(); + // literal := q(X, Y) + Literal literal = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("q", 2), Terms.newVariable("X"), Terms.newVariable("Y")), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables(), "X", "Y"); expectVariables(literal.getNonBindingVariables()); @@ -68,7 +65,8 @@ public void testPositiveBasicLiteral() { @Test public void testNegativeBasicLiteral() { - Literal literal = parser.parse("p(X,Y) :- q(X,Y), not r(X,Y).").getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := not r(X, Y) + Literal literal = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("r", 2), Terms.newVariable("X"), Terms.newVariable("Y")), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "X", "Y"); @@ -76,8 +74,8 @@ public void testNegativeBasicLiteral() { @Test public void testPositiveComparisonLiteral_EQ_LeftAssigning() { - Rule rule = parser.parse("p(X) :- q(X,Y), Y = 5.").getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate() == ComparisonOperators.EQ.toPredicate()).findFirst().get(); + // literal := Y = 5 + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("Y"), Terms.newConstant(5), ComparisonOperators.EQ), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables(), "Y"); expectVariables(literal.getNonBindingVariables()); @@ -85,8 +83,8 @@ public void testPositiveComparisonLiteral_EQ_LeftAssigning() { @Test public void testNegativeComparisonLiteral_EQ_LeftAssigning() { - Rule rule = parser.parse("p(X) :- q(X,Y), not Y = 5.").getRules().get(0); - Literal literal = rule.getNegativeBody().stream().findFirst().get(); + // literal := not Y = 5 + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("Y"), Terms.newConstant(5), ComparisonOperators.EQ), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "Y"); @@ -94,8 +92,8 @@ public void testNegativeComparisonLiteral_EQ_LeftAssigning() { @Test public void testPositiveComparisonLiteral_EQ_RightAssigning() { - Rule rule = parser.parse("p(X) :- q(X,Y), 5 = Y.").getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate() == ComparisonOperators.EQ.toPredicate()).findFirst().get(); + // literal := 5 = Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newConstant(5), Terms.newVariable("Y"), ComparisonOperators.EQ), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables(), "Y"); expectVariables(literal.getNonBindingVariables()); @@ -103,25 +101,17 @@ public void testPositiveComparisonLiteral_EQ_RightAssigning() { @Test public void testNegativeComparisonLiteral_EQ_RightAssigning() { - Literal literal = parser.parse("p(X) :- q(X,Y), not 5 = Y.").getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := 5 = Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newConstant(5), Terms.newVariable("Y"), ComparisonOperators.EQ), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "Y"); } - @Test - @Disabled("Literals of this kind are compiled away by VariableEqualityRemoval") - public void testPositiveComparisonLiteral_EQ_Bidirectional() { - Rule rule = parser.parse("p(X) :- q(X,Y), X = Y.").getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate() == ComparisonOperators.EQ.toPredicate()).findFirst().get(); - assertEquals(false, literal.isNegated()); - expectVariables(literal.getBindingVariables()); - expectVariables(literal.getNonBindingVariables(), "X", "Y"); - } - @Test public void testNegativeComparisonLiteral_EQ_Bidirectional() { - Literal literal = parser.parse("p(X) :- q(X,Y), not X = Y.").getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := not X = Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("X"), Terms.newVariable("Y"), ComparisonOperators.EQ), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "X", "Y"); @@ -129,8 +119,8 @@ public void testNegativeComparisonLiteral_EQ_Bidirectional() { @Test public void testPositiveComparisonLiteral_NEQ_LeftAssigning() { - Rule rule = parser.parse("p(X) :- q(X,Y), Y != 5.").getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate() == ComparisonOperators.NE.toPredicate()).findFirst().get(); + // literal := Y != 5 + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("Y"), Terms.newConstant(5), ComparisonOperators.NE), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "Y"); @@ -138,7 +128,8 @@ public void testPositiveComparisonLiteral_NEQ_LeftAssigning() { @Test public void testNegativeComparisonLiteral_NEQ_LeftAssigning() { - Literal literal = parser.parse("p(X) :- q(X,Y), not Y != 5.").getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := not Y != 5 + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("Y"), Terms.newConstant(5), ComparisonOperators.NE), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables(), "Y"); expectVariables(literal.getNonBindingVariables()); @@ -146,8 +137,8 @@ public void testNegativeComparisonLiteral_NEQ_LeftAssigning() { @Test public void testPositiveComparisonLiteral_NEQ_RightAssigning() { - Rule rule = parser.parse("p(X) :- q(X,Y), 5 != Y.").getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate() == ComparisonOperators.NE.toPredicate()).findFirst().get(); + // literal := 5 != Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newConstant(5), Terms.newVariable("Y"), ComparisonOperators.NE), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "Y"); @@ -155,7 +146,8 @@ public void testPositiveComparisonLiteral_NEQ_RightAssigning() { @Test public void testNegativeComparisonLiteral_NEQ_RightAssigning() { - Literal literal = parser.parse("p(X) :- q(X,Y), not 5 != Y.").getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := not 5 != Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newConstant(5), Terms.newVariable("Y"), ComparisonOperators.NE), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables(), "Y"); expectVariables(literal.getNonBindingVariables()); @@ -163,8 +155,8 @@ public void testNegativeComparisonLiteral_NEQ_RightAssigning() { @Test public void testPositiveComparisonLiteral_NEQ_Bidirectional() { - Rule rule = parser.parse("p(X) :- q(X,Y), X != Y.").getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate() == ComparisonOperators.NE.toPredicate()).findFirst().get(); + // literal := X != Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("X"), Terms.newVariable("Y"), ComparisonOperators.NE), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "X", "Y"); @@ -173,7 +165,8 @@ public void testPositiveComparisonLiteral_NEQ_Bidirectional() { @Test @Disabled("Literals of this kind are compiled away by VariableEqualityRemoval") public void testNegativeComparisonLiteral_NEQ_Bidirectional() { - Literal literal = parser.parse("p(X) :- q(X,Y), not X != Y.").getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := not X != Y + Literal literal = Literals.fromAtom(Atoms.newComparisonAtom(Terms.newVariable("X"), Terms.newVariable("Y"), ComparisonOperators.NE), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables(), "X", "Y"); expectVariables(literal.getNonBindingVariables()); @@ -181,9 +174,12 @@ public void testNegativeComparisonLiteral_NEQ_Bidirectional() { @Test public void testPositiveExternalLiteral() { - externals.put("ext", new IntPredicateInterpretation(i -> i > 0)); - Rule rule = parser.parse("p(X) :- q(Y), &ext[Y](X).", externals).getRules().get(0); - Literal literal = rule.getBody().stream().filter((lit) -> lit.getPredicate().getName().equals("ext")).findFirst().get(); + // literal := &ext[Y](X) + List extInput = new ArrayList<>(); + List extOutput = new ArrayList<>(); + extInput.add(Terms.newVariable("Y")); + extOutput.add(Terms.newVariable("X")); + Literal literal = Literals.fromAtom(Atoms.newExternalAtom(Predicates.getPredicate("ext", 2), new IntPredicateInterpretation(i -> i > 0), extInput, extOutput), true); assertEquals(false, literal.isNegated()); expectVariables(literal.getBindingVariables(), "X"); expectVariables(literal.getNonBindingVariables(), "Y"); @@ -191,8 +187,12 @@ public void testPositiveExternalLiteral() { @Test public void testNegativeExternalLiteral() { - externals.put("ext", new IntPredicateInterpretation(i -> i > 0)); - Literal literal = parser.parse("p(X) :- q(Y), not &ext[Y](X).", externals).getRules().get(0).getNegativeBody().stream().findFirst().get(); + // literal := not &ext[Y](X) + List extInput = new ArrayList<>(); + List extOutput = new ArrayList<>(); + extInput.add(Terms.newVariable("Y")); + extOutput.add(Terms.newVariable("X")); + Literal literal = Literals.fromAtom(Atoms.newExternalAtom(Predicates.getPredicate("ext", 2), new IntPredicateInterpretation(i -> i > 0), extInput, extOutput), false); assertEquals(true, literal.isNegated()); expectVariables(literal.getBindingVariables()); expectVariables(literal.getNonBindingVariables(), "X", "Y"); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/SimpleAnswerSetFormatterTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/util/SimpleAnswerSetFormatterTest.java similarity index 85% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/SimpleAnswerSetFormatterTest.java rename to alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/util/SimpleAnswerSetFormatterTest.java index 0b14388ad..b187bc242 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/SimpleAnswerSetFormatterTest.java +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/util/SimpleAnswerSetFormatterTest.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.common; +package at.ac.tuwien.kr.alpha.commons.util; import static org.junit.jupiter.api.Assertions.assertEquals; @@ -7,7 +7,6 @@ import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.util.AnswerSetFormatter; import at.ac.tuwien.kr.alpha.commons.AnswerSetBuilder; -import at.ac.tuwien.kr.alpha.commons.util.SimpleAnswerSetFormatter; public class SimpleAnswerSetFormatterTest { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java index e55c6fcfb..eeaa2f024 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java @@ -116,4 +116,8 @@ default String noGoodToString(T noGood) { } AtomCounter getAtomCounter(); + + static boolean isAtom(int atom) { + return atom >= 0; + } } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ProgramParserImpl.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ProgramParserImpl.java index 2b7d82905..a0a71d8a5 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ProgramParserImpl.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ProgramParserImpl.java @@ -19,9 +19,9 @@ import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2Lexer; import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2Parser; -import at.ac.tuwien.kr.alpha.core.externals.Externals; import at.ac.tuwien.kr.alpha.core.programs.InputProgram; public class ProgramParserImpl implements ProgramParser { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/BasicRule.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/BasicRule.java index 1a2cab45e..1c218769a 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/BasicRule.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/BasicRule.java @@ -27,6 +27,7 @@ */ package at.ac.tuwien.kr.alpha.core.rules; +import java.util.Arrays; import java.util.List; import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; @@ -45,4 +46,7 @@ public BasicRule(Head head, List body) { super(head, body); } + public BasicRule(Head head, Literal... body) { + this(head, Arrays.asList(body)); + } } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/InternalRule.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/InternalRule.java index 9a72fca12..3283ac64f 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/InternalRule.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/InternalRule.java @@ -28,6 +28,7 @@ package at.ac.tuwien.kr.alpha.core.rules; import java.util.ArrayList; +import java.util.Arrays; import java.util.List; import com.google.common.annotations.VisibleForTesting; @@ -59,6 +60,10 @@ public class InternalRule extends NormalRuleImpl implements CompiledRule { private final RuleGroundingInfoImpl groundingOrders; + public InternalRule(NormalHead head, Literal... body) { + this(head, Arrays.asList(body)); + } + public InternalRule(NormalHead head, List body) { super(head, body); if (body.isEmpty()) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/Rules.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/Rules.java new file mode 100644 index 000000000..7666ba84a --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/rules/Rules.java @@ -0,0 +1,28 @@ +package at.ac.tuwien.kr.alpha.core.rules; + +import java.util.ArrayList; +import java.util.List; + +import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; +import at.ac.tuwien.kr.alpha.api.rules.Rule; +import at.ac.tuwien.kr.alpha.api.rules.heads.Head; +import at.ac.tuwien.kr.alpha.api.rules.heads.NormalHead; +import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; + +public final class Rules { + + private Rules() { + throw new AssertionError("Cannot instantiate utility class!"); + } + + public static Rule newRule(BasicAtom headAtom, Literal... body) { + NormalHead head = Heads.newNormalHead(headAtom); + List bodyLiterals = new ArrayList<>(); + for (Literal lit : body) { + bodyLiterals.add(lit); + } + return new BasicRule(head, bodyLiterals); + } + +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/Atoms.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/Atoms.java deleted file mode 100644 index 9ba91dbfa..000000000 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/Atoms.java +++ /dev/null @@ -1,9 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.solver; - -public final class Atoms { - - public static boolean isAtom(int atom) { - return atom >= 0; - } - -} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java index 8d8edcbb3..8e800b953 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java @@ -205,7 +205,7 @@ public Choice backtrack() { return choice; } - void addChoiceInformation(Pair, Map> choiceAtoms, Map> headsToBodies) { + public void addChoiceInformation(Pair, Map> choiceAtoms, Map> headsToBodies) { choicePointInfluenceManager.addInformation(choiceAtoms); addHeadsToBodies(headsToBodies); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java index 9194925d8..929b904f3 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java @@ -32,7 +32,6 @@ import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.isPositive; -import static at.ac.tuwien.kr.alpha.core.solver.Atoms.isAtom; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.FALSE; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE; @@ -335,7 +334,7 @@ private boolean assignmentsConsistent(ThriceTruth oldTruth, ThriceTruth value) { } private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent impliedBy) { - if (!isAtom(atom)) { + if (!AtomStore.isAtom(atom)) { throw new IllegalArgumentException("not an atom"); } if (value == null) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaRandomSignHeuristic.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaRandomSignHeuristic.java index 4e2cbc238..e2b539dc4 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaRandomSignHeuristic.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaRandomSignHeuristic.java @@ -25,15 +25,14 @@ */ package at.ac.tuwien.kr.alpha.core.solver.heuristics; +import java.util.Random; + import at.ac.tuwien.kr.alpha.core.common.Assignment; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; import at.ac.tuwien.kr.alpha.core.solver.heuristics.activity.BodyActivityProviderFactory.BodyActivityType; -import static at.ac.tuwien.kr.alpha.core.solver.Atoms.isAtom; - -import java.util.Random; - public class AlphaRandomSignHeuristic extends DependencyDrivenHeuristic { public AlphaRandomSignHeuristic(Assignment assignment, ChoiceManager choiceManager, int decayPeriod, double decayFactor, Random random) { @@ -51,7 +50,7 @@ protected void incrementSignCounter(Integer literal) { @Override public boolean chooseSign(int atom) { - if (!isAtom(atom)) { + if (!AtomStore.isAtom(atom)) { throw new IllegalArgumentException("Atom must be a positive integer."); } diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/atoms/AtomsTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/atoms/AtomsTest.java deleted file mode 100644 index 602bb960f..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/atoms/AtomsTest.java +++ /dev/null @@ -1,148 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.atoms; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertFalse; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import java.util.ArrayList; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; -import at.ac.tuwien.kr.alpha.api.externals.Predicate; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; -import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.api.programs.atoms.ExternalAtom; -import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.externals.Externals; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; - -/** - * Test for basic functionality of various implementations of {@link Atom}. - * - * Copyright (c) 2019-2020, the Alpha Team. - */ -public class AtomsTest { - - private final ProgramParser parser; - private Map externals; - - public AtomsTest() throws NoSuchMethodException, SecurityException { - externals = new HashMap<>(); - externals.put("isFoo", Externals.processPredicateMethod(AtomsTest.class.getMethod("isFoo", int.class))); - externals.put("extWithOutput", Externals.processPredicateMethod(AtomsTest.class.getMethod("extWithOutput", int.class))); - parser = new ProgramParserImpl(); - } - - @Predicate - public static final boolean isFoo(int bar) { - return 0xF00 == bar; - } - - @Predicate - public static final Set>> extWithOutput(int in) { - Set>> retVal = new HashSet<>(); - List> lst = new ArrayList<>(); - lst.add(Terms.newConstant(in)); - retVal.add(lst); - return retVal; - } - - @Test - public void testIsBasicAtomGround() { - ASPCore2Program p = parser.parse("bla(blubb, foo(bar))."); - Atom a = p.getFacts().get(0); - assertBasicAtomGround(a, true); - ASPCore2Program p1 = parser.parse("foo(1, 2, 3, \"bar\")."); - Atom a1 = p1.getFacts().get(0); - assertBasicAtomGround(a1, true); - ASPCore2Program p2 = parser.parse("foo(BAR)."); - Atom a2 = p2.getFacts().get(0); - assertBasicAtomGround(a2, false); - ASPCore2Program p3 = parser.parse("foo(b, a, r(\"bla\", BLUBB))."); - Atom a3 = p3.getFacts().get(0); - assertBasicAtomGround(a3, false); - } - - @Test - public void testAreBasicAtomsEqual() { - ASPCore2Program p1 = parser.parse("bla(blubb, foo(bar)). bla(blubb, foo(bar))."); - Atom a1 = p1.getFacts().get(0); - Atom a2 = p1.getFacts().get(1); - assertEquals(a1, a2); - ASPCore2Program p2 = parser.parse("foo(1, 2, 3, \"bar\"). foo(1, 2, 3, \"bar\")."); - Atom a3 = p2.getFacts().get(0); - Atom a4 = p2.getFacts().get(1); - assertEquals(a3, a4); - ASPCore2Program p3 = parser.parse("foo(BAR). foo(BAR)."); - Atom a5 = p3.getFacts().get(0); - Atom a6 = p3.getFacts().get(1); - assertEquals(a5, a6); - ASPCore2Program p4 = parser.parse("foo(b, a, r(\"bla\", BLUBB)). foo(b, a, r(\"bla\", BLUBB))."); - Atom a7 = p4.getFacts().get(0); - Atom a8 = p4.getFacts().get(1); - assertEquals(a7, a8); - - assertFalse(a1.equals(a3)); - assertFalse(a3.equals(a1)); - assertFalse(a1.equals(a5)); - assertFalse(a5.equals(a1)); - assertFalse(a1.equals(a7)); - assertFalse(a7.equals(a1)); - } - - @Test - public void testIsExternalAtomGround() { - ASPCore2Program p1 = parser.parse("a :- &isFoo[1].", externals); - Atom ext1 = p1.getRules().get(0).getBody().stream().findFirst().get().getAtom(); - assertExternalAtomGround(ext1, true); - ASPCore2Program p2 = parser.parse("a :- &isFoo[bar(1)].", externals); - Atom ext2 = p2.getRules().get(0).getBody().stream().findFirst().get().getAtom(); - assertExternalAtomGround(ext2, true); - ASPCore2Program p3 = parser.parse("a :- &isFoo[BLA].", externals); - Atom ext3 = p3.getRules().get(0).getBody().stream().findFirst().get().getAtom(); - assertExternalAtomGround(ext3, false); - } - - @Test - @SuppressWarnings("unlikely-arg-type") - public void testAreExternalAtomsEqual() { - ASPCore2Program p1 = parser.parse("a :- &isFoo[1].", externals); - Atom ext1 = p1.getRules().get(0).getBody().stream().findFirst().get().getAtom(); - ASPCore2Program p2 = parser.parse("a :- &isFoo[1].", externals); - Atom ext2 = p2.getRules().get(0).getBody().stream().findFirst().get().getAtom(); - assertEquals(ext1, ext2); - assertEquals(ext2, ext1); - - assertFalse(ext1.equals(null)); - assertFalse(ext1.equals("bla")); - assertTrue(ext1.hashCode() == ext2.hashCode()); - } - - @Test - public void testExternalHasOutput() { - ASPCore2Program p = parser.parse("a:- &extWithOutput[1](OUT).", externals); - Atom ext = p.getRules().get(0).getBody().stream().findFirst().get().getAtom(); - assertExternalAtomGround(ext, false); - assertTrue(((ExternalAtom) ext).hasOutput()); - } - - private void assertBasicAtomGround(Atom a, boolean expectedGround) { - assertTrue(a instanceof BasicAtom); - assertEquals(expectedGround, a.isGround()); - } - - private void assertExternalAtomGround(Atom a, boolean expectedGround) { - assertTrue(a instanceof ExternalAtom); - assertEquals(expectedGround, a.isGround()); - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/ProgramTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/ProgramTest.java index 9ced45803..0bd692dda 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/ProgramTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/ProgramTest.java @@ -27,23 +27,43 @@ import static org.junit.jupiter.api.Assertions.assertEquals; +import java.util.ArrayList; +import java.util.List; + import org.junit.jupiter.api.Test; import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; +import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; +import at.ac.tuwien.kr.alpha.api.rules.Rule; +import at.ac.tuwien.kr.alpha.api.rules.heads.Head; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.literals.Literals; +import at.ac.tuwien.kr.alpha.commons.terms.Terms; +import at.ac.tuwien.kr.alpha.core.programs.InputProgram; +import at.ac.tuwien.kr.alpha.core.rules.Rules; public class ProgramTest { - + @Test public void testToString() { - ASPCore2Program parsedProgram = new ProgramParserImpl().parse( - "p(a)." + System.lineSeparator() + - "q(X) :- p(X)." + System.lineSeparator() + - "p(b)."); + ASPCore2Program program; + // rule := q(X) :- p(X). + List body = new ArrayList<>(); + body.add(Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Terms.newVariable("X")), true)); + Rule rule = Rules.newRule( + Atoms.newBasicAtom(Predicates.getPredicate("q", 1), Terms.newVariable("X")), + Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Terms.newVariable("X")).toLiteral()); + List facts = new ArrayList<>(); + facts.add(Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Terms.newSymbolicConstant("a"))); + facts.add(Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Terms.newSymbolicConstant("b"))); + // program := p(a). p(b). q(X) :- p(X). + program = InputProgram.builder().addFacts(facts).addRule(rule).build(); assertEquals( "p(a)." + System.lineSeparator() + - "p(b)." + System.lineSeparator() + - "q(X) :- p(X)." + System.lineSeparator(), - parsedProgram.toString()); + "p(b)." + System.lineSeparator() + + "q(X) :- p(X)." + System.lineSeparator(), + program.toString()); } -} \ No newline at end of file +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/RuleTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/RuleTest.java index 0c637cb1a..9359bb09c 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/RuleTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/common/RuleTest.java @@ -1,46 +1,76 @@ package at.ac.tuwien.kr.alpha.core.common; - import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertFalse; import static org.junit.jupiter.api.Assertions.assertTrue; import org.junit.jupiter.api.Test; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; +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.rules.Rule; import at.ac.tuwien.kr.alpha.api.rules.heads.Head; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; +import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; import at.ac.tuwien.kr.alpha.core.rules.InternalRule; import at.ac.tuwien.kr.alpha.core.rules.NormalRuleImpl; +import at.ac.tuwien.kr.alpha.core.rules.Rules; /** - * Copyright (c) 2018, the Alpha Team. + * Copyright (c) 2018 - 2021, the Alpha Team. */ public class RuleTest { - private final ProgramParserImpl parser = new ProgramParserImpl(); - @Test public void renameVariables() { - String originalRule = "p(X,Y) :- a, f(Z) = 1, q(X,g(Y),Z), dom(A)."; - Rule rule = parser.parse(originalRule).getRules().get(0); - CompiledRule normalRule = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(rule)); - CompiledRule renamedRule = normalRule.renameVariables("_13"); - Rule expectedRenamedRule = parser.parse("p(X_13, Y_13) :- a, f(Z_13) = 1, q(X_13, g(Y_13), Z_13), dom(A_13).").getRules().get(0); - CompiledRule expectedRenamedNormalRule = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(expectedRenamedRule)); - assertEquals(expectedRenamedNormalRule.toString(), renamedRule.toString()); + // rule := p(X,Y) :- a, f(Z) = 1, q(X,g(Y),Z), dom(A). + BasicAtom headAtom = Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")); + BasicAtom bodyAtom1 = Atoms.newBasicAtom(Predicates.getPredicate("a", 0)); + ComparisonAtom bodyAtom2 = Atoms.newComparisonAtom(Terms.newFunctionTerm("f", Terms.newVariable("Z")), Terms.newConstant(1), ComparisonOperators.EQ); + BasicAtom bodyAtom3 = Atoms.newBasicAtom(Predicates.getPredicate("q", 3), + Terms.newVariable("X"), Terms.newFunctionTerm("g", Terms.newVariable("Y")), Terms.newVariable("Z")); + BasicAtom bodyAtom4 = Atoms.newBasicAtom(Predicates.getPredicate("dom", 1), Terms.newVariable("A")); + CompiledRule rule = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule( + Rules.newRule(headAtom, bodyAtom1.toLiteral(), bodyAtom2.toLiteral(), bodyAtom3.toLiteral(), bodyAtom4.toLiteral()))); + + // ruleWithRenamedVars := p(X_13, Y_13) :- a, f(Z_13) = 1, q(X_13, g(Y_13), Z_13), dom(A_13). + BasicAtom headAtomRenamed = Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X_13"), Terms.newVariable("Y_13")); + BasicAtom bodyAtom1Renamed = Atoms.newBasicAtom(Predicates.getPredicate("a", 0)); + ComparisonAtom bodyAtom2Renamed = Atoms.newComparisonAtom(Terms.newFunctionTerm("f", Terms.newVariable("Z_13")), Terms.newConstant(1), + ComparisonOperators.EQ); + BasicAtom bodyAtom3Renamed = Atoms.newBasicAtom(Predicates.getPredicate("q", 3), + Terms.newVariable("X_13"), Terms.newFunctionTerm("g", Terms.newVariable("Y_13")), Terms.newVariable("Z_13")); + BasicAtom bodyAtom4Renamed = Atoms.newBasicAtom(Predicates.getPredicate("dom", 1), Terms.newVariable("A_13")); + CompiledRule ruleWithRenamedVars = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule( + Rules.newRule(headAtomRenamed, bodyAtom1Renamed.toLiteral(), bodyAtom2Renamed.toLiteral(), bodyAtom3Renamed.toLiteral(), + bodyAtom4Renamed.toLiteral()))); + + assertEquals(ruleWithRenamedVars, rule.renameVariables("_13")); } @Test public void testRulesEqual() { - ASPCore2Program p1 = parser.parse("p(X, Y) :- bla(X), blub(Y), foo(X, Y), not bar(X)."); - Rule r1 = p1.getRules().get(0); - ASPCore2Program p2 = parser.parse("p(X, Y) :- bla(X), blub(Y), foo(X, Y), not bar(X)."); - Rule r2 = p2.getRules().get(0); - ASPCore2Program p3 = parser.parse("p(X, Y) :- bla(X), blub(X), foo(X, X), not bar(X)."); - Rule r3 = p3.getRules().get(0); + // r1 := p(X, Y) :- bla(X), blub(Y), foo(X, Y), not bar(X). + Rule r1 = Rules.newRule(Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")), + Atoms.newBasicAtom(Predicates.getPredicate("bla", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("blub", 1), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("foo", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("bar", 1), Terms.newVariable("X")).toLiteral(false)); + // r2 := p(X, Y) :- bla(X), blub(Y), foo(X, Y), not bar(X). + Rule r2 = Rules.newRule(Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")), + Atoms.newBasicAtom(Predicates.getPredicate("bla", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("blub", 1), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("foo", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("bar", 1), Terms.newVariable("X")).toLiteral(false)); + // r3 := p(X, Y) :- bla(X), blub(X), foo(X, X), not bar(X). + Rule r3 = Rules.newRule(Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")), + Atoms.newBasicAtom(Predicates.getPredicate("bla", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("blub", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("foo", 2), Terms.newVariable("X"), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("bar", 1), Terms.newVariable("X")).toLiteral(false)); assertTrue(r1.equals(r2)); assertTrue(r2.equals(r1)); assertTrue(r1.hashCode() == r2.hashCode()); @@ -52,4 +82,4 @@ public void testRulesEqual() { assertTrue(r2.hashCode() != r3.hashCode()); } -} \ No newline at end of file +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/depgraph/DependencyGraphImplTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/depgraph/DependencyGraphImplTest.java deleted file mode 100644 index 65e4f32ae..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/depgraph/DependencyGraphImplTest.java +++ /dev/null @@ -1,276 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.depgraph; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertFalse; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import java.util.ArrayList; -import java.util.List; -import java.util.Map; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; -import at.ac.tuwien.kr.alpha.api.programs.Predicate; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph; -import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph.Node; -import at.ac.tuwien.kr.alpha.commons.Predicates; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; -import at.ac.tuwien.kr.alpha.core.programs.AnalyzedProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; -import at.ac.tuwien.kr.alpha.core.test.util.DependencyGraphUtils; - -public class DependencyGraphImplTest { - - private ProgramParser parser = new ProgramParserImpl(); - private NormalizeProgramTransformation normalizeTransform = new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - - // Currently not used anywhere, but keep as it might come in handy - @SuppressWarnings("unused") - private static String generateRandomProgram(int numRules, int numPredicates, int maxRuleBodyLiterals) { - String[] predicates = new String[numPredicates]; - for (int i = 0; i < predicates.length; i++) { - predicates[i] = "p" + Integer.toString(i + 1); - } - - StringBuilder prgBuilder = new StringBuilder(); - String tmpAtom; - int tmpBodyLiterals; - for (int i = 0; i < numRules; i++) { - tmpBodyLiterals = 1 + ((int) (Math.random() * maxRuleBodyLiterals)); - tmpAtom = predicates[(int) (Math.random() * predicates.length)]; - prgBuilder.append(tmpAtom).append(" :- "); - for (int j = 0; j < tmpBodyLiterals; j++) { - tmpAtom = predicates[(int) (Math.random() * predicates.length)]; - prgBuilder.append(tmpAtom); - if (j < (tmpBodyLiterals - 1)) { - prgBuilder.append(", "); - } - } - prgBuilder.append("."); - prgBuilder.append("\n"); - } - return prgBuilder.toString(); - } - - @Test - public void edgesEqualTest() { - Predicate testPredicate = Predicates.getPredicate("test", 2, false, false); - EdgeImpl e1 = new EdgeImpl(new NodeImpl(testPredicate), true); - EdgeImpl e2 = new EdgeImpl(new NodeImpl(testPredicate), true); - assertEquals(e1, e2); - } - - @Test - public void reachabilityCheckSimpleTest() { - ASPCore2Program prog = parser.parse("b :- a."); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - - Node a = dg.getNodeForPredicate(Predicates.getPredicate("a", 0)); - Node b = dg.getNodeForPredicate(Predicates.getPredicate("b", 0)); - - NodeImpl nonExistent = new NodeImpl(Predicates.getPredicate("notHere", 0)); - - assertTrue(DependencyGraphUtils.isReachableFrom(a, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(b, a, dg)); - assertFalse(DependencyGraphUtils.isReachableFrom(a, b, dg)); - assertFalse(DependencyGraphUtils.isReachableFrom(nonExistent, a, dg)); - assertFalse(DependencyGraphUtils.isReachableFrom(nonExistent, b, dg)); - } - - @Test - public void reachabilityCheckWithHopsTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a.").append("\n"); - bld.append("c :- b.").append("\n"); - bld.append("d :- c.").append("\n"); - - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - Node a = dg.getNodeForPredicate(Predicates.getPredicate("a", 0)); - Node b = dg.getNodeForPredicate(Predicates.getPredicate("b", 0)); - Node c = dg.getNodeForPredicate(Predicates.getPredicate("c", 0)); - Node d = dg.getNodeForPredicate(Predicates.getPredicate("d", 0)); - - assertTrue(DependencyGraphUtils.isReachableFrom(d, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(b, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(a, a, dg)); - - assertTrue(DependencyGraphUtils.isReachableFrom(d, b, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, b, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(b, b, dg)); - - assertTrue(DependencyGraphUtils.isReachableFrom(d, c, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, c, dg)); - - assertFalse(DependencyGraphUtils.isReachableFrom(a, d, dg)); - assertFalse(DependencyGraphUtils.isReachableFrom(a, c, dg)); - assertFalse(DependencyGraphUtils.isReachableFrom(a, b, dg)); - } - - @Test - public void reachabilityWithCyclesTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a, f1.").append("\n"); - bld.append("c :- b.").append("\n"); - bld.append("d :- c.").append("\n"); - bld.append("a :- d.").append("\n"); - bld.append("x :- d, f1."); - - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - Node a = dg.getNodeForPredicate(Predicates.getPredicate("a", 0)); - Node b = dg.getNodeForPredicate(Predicates.getPredicate("b", 0)); - Node c = dg.getNodeForPredicate(Predicates.getPredicate("c", 0)); - Node d = dg.getNodeForPredicate(Predicates.getPredicate("d", 0)); - Node f1 = dg.getNodeForPredicate(Predicates.getPredicate("f1", 0)); - Node x = dg.getNodeForPredicate(Predicates.getPredicate("x", 0)); - Node notInGraph = new NodeImpl(Predicates.getPredicate("notInGraph", 0)); - - assertTrue(DependencyGraphUtils.isReachableFrom(d, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(b, a, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(a, a, dg)); - - assertTrue(DependencyGraphUtils.isReachableFrom(d, b, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, b, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(b, b, dg)); - - assertTrue(DependencyGraphUtils.isReachableFrom(d, c, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, c, dg)); - - assertTrue(DependencyGraphUtils.isReachableFrom(a, d, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(a, c, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(a, b, dg)); - - assertTrue(DependencyGraphUtils.isReachableFrom(x, f1, dg)); - assertTrue(DependencyGraphUtils.isReachableFrom(c, f1, dg)); - - assertFalse(DependencyGraphUtils.isReachableFrom(notInGraph, a, dg)); - } - - @Test - public void stronglyConnectedComponentsSimpleTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a.").append("\n"); - bld.append("a :- b.").append("\n"); - - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - Node a = dg.getNodeForPredicate(Predicates.getPredicate("a", 0)); - Node b = dg.getNodeForPredicate(Predicates.getPredicate("b", 0)); - - List componentA = new ArrayList<>(); - componentA.add(a); - assertTrue(DependencyGraphUtils.areStronglyConnected(componentA, dg)); - assertFalse(DependencyGraphUtils.isStronglyConnectedComponent(componentA, dg)); - - - List componentB = new ArrayList<>(); - componentB.add(b); - assertTrue(DependencyGraphUtils.areStronglyConnected(componentB, dg)); - assertFalse(DependencyGraphUtils.isStronglyConnectedComponent(componentB, dg)); - - List componentAll = new ArrayList<>(); - componentAll.add(a); - componentAll.add(b); - assertTrue(DependencyGraphUtils.areStronglyConnected(componentAll, dg)); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(componentAll, dg)); - } - - @Test - public void stronglyConnectedComponentsMultipleComponentsTest() { - String inputProgram = "f0.\n" + - "f1.\n" + - "f2.\n" + - "f3.\n" + - "a :- f0, f1, not b.\n" + - "b :- f0, f1, not a.\n" + - "c :- f2, f3, not d.\n" + - "d :- f2, f3, not c.\n" + - "x :- a, c, y.\n" + - "y :- b, d, x.\n" + - "z :- x, y, z."; - - ASPCore2Program prog = parser.parse(inputProgram); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - - Node f0 = dg.getNodeForPredicate(Predicates.getPredicate("f0", 0)); - Node f1 = dg.getNodeForPredicate(Predicates.getPredicate("f1", 0)); - Node f2 = dg.getNodeForPredicate(Predicates.getPredicate("f2", 0)); - Node f3 = dg.getNodeForPredicate(Predicates.getPredicate("f3", 0)); - Node a = dg.getNodeForPredicate(Predicates.getPredicate("a", 0)); - Node b = dg.getNodeForPredicate(Predicates.getPredicate("b", 0)); - Node c = dg.getNodeForPredicate(Predicates.getPredicate("c", 0)); - Node d = dg.getNodeForPredicate(Predicates.getPredicate("d", 0)); - Node x = dg.getNodeForPredicate(Predicates.getPredicate("x", 0)); - Node y = dg.getNodeForPredicate(Predicates.getPredicate("y", 0)); - Node z = dg.getNodeForPredicate(Predicates.getPredicate("z", 0)); - - StronglyConnectedComponentsAlgorithm.SccResult sccResult = StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg); - Map nodesByComponent = sccResult.nodesByComponentId; - List> stronglyConnectedComponents = sccResult.stronglyConnectedComponents; - assertEquals(8, stronglyConnectedComponents.size()); - - for (int i = 0; i < stronglyConnectedComponents.size(); i++) { - List stronglyConnectedComponent = stronglyConnectedComponents.get(i); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(stronglyConnectedComponent, dg)); - for (Node node : stronglyConnectedComponent) { - assertEquals(Integer.valueOf(i), nodesByComponent.get(node)); - } - } - - List c1 = new ArrayList<>(); - c1.add(a); - c1.add(b); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c1, dg)); - assertEquals(nodesByComponent.get(a), nodesByComponent.get(b)); - - List c2 = new ArrayList<>(); - c2.add(c); - c2.add(d); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c2, dg)); - assertEquals(nodesByComponent.get(c), nodesByComponent.get(d)); - - List c3 = new ArrayList<>(); - c3.add(x); - c3.add(y); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c3, dg)); - assertEquals(nodesByComponent.get(x), nodesByComponent.get(y)); - - List c4 = new ArrayList<>(); - c4.add(z); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c4, dg)); - - List c5 = new ArrayList<>(); - c5.add(f0); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c5, dg)); - - List c6 = new ArrayList<>(); - c6.add(f1); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c6, dg)); - - List c7 = new ArrayList<>(); - c7.add(f2); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c7, dg)); - - List c8 = new ArrayList<>(); - c8.add(f3); - assertTrue(DependencyGraphUtils.isStronglyConnectedComponent(c8, dg)); - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/depgraph/StratificationAlgorithmTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/depgraph/StratificationAlgorithmTest.java deleted file mode 100644 index c50acaf9b..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/depgraph/StratificationAlgorithmTest.java +++ /dev/null @@ -1,241 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.depgraph; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import java.util.List; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; -import at.ac.tuwien.kr.alpha.api.programs.Predicate; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.analysis.ComponentGraph; -import at.ac.tuwien.kr.alpha.api.programs.analysis.ComponentGraph.SCComponent; -import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph; -import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph.Node; -import at.ac.tuwien.kr.alpha.commons.Predicates; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; -import at.ac.tuwien.kr.alpha.core.programs.AnalyzedProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; - -public class StratificationAlgorithmTest { - - private ProgramParser parser = new ProgramParserImpl(); - private NormalizeProgramTransformation normalizeTransform = new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - - private boolean predicateIsBeforePredicateInOrder(Predicate predBefore, Predicate predAfter, List order) { - boolean foundPredBefore = false; - for (SCComponent component : order) { - for (Node node : component.getNodes()) { - if (node.getPredicate() == predBefore) { - foundPredBefore = true; - } - if (node.getPredicate() == predAfter) { - // Found second predicate, return true if we already found the first predicate. - return foundPredBefore; - } - } - } - return false; - } - - @Test - public void stratifyOneRuleTest() { - ASPCore2Program prog = parser.parse("a :- b."); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate a = Predicates.getPredicate("a", 0); - Predicate b = Predicates.getPredicate("b", 0); - - assertEquals(2, strata.size()); - assertTrue(predicateIsBeforePredicateInOrder(b, a, strata)); - } - - @Test - public void stratifyTwoRulesTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a.").append("\n"); - bld.append("c :- b.").append("\n"); - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate a = Predicates.getPredicate("a", 0); - Predicate b = Predicates.getPredicate("b", 0); - Predicate c = Predicates.getPredicate("c", 0); - - assertEquals(3, strata.size()); - assertTrue(predicateIsBeforePredicateInOrder(a, b, strata)); - assertTrue(predicateIsBeforePredicateInOrder(b, c, strata)); - assertTrue(predicateIsBeforePredicateInOrder(a, c, strata)); - } - - @Test - public void stratifyWithNegativeDependencyTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a.").append("\n"); - bld.append("c :- b.").append("\n"); - bld.append("d :- not c.").append("\n"); - bld.append("e :- d.").append("\n"); - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate a = Predicates.getPredicate("a", 0); - Predicate b = Predicates.getPredicate("b", 0); - Predicate c = Predicates.getPredicate("c", 0); - Predicate d = Predicates.getPredicate("d", 0); - Predicate e = Predicates.getPredicate("e", 0); - - assertEquals(5, strata.size()); - assertTrue(predicateIsBeforePredicateInOrder(a, b, strata)); - assertTrue(predicateIsBeforePredicateInOrder(b, c, strata)); - assertTrue(predicateIsBeforePredicateInOrder(c, d, strata)); - assertTrue(predicateIsBeforePredicateInOrder(d, e, strata)); - } - - @Test - public void stratifyWithPositiveCycleTest() { - StringBuilder bld = new StringBuilder(); - bld.append("ancestor_of(X, Y) :- parent_of(X, Y)."); - bld.append("ancestor_of(X, Z) :- parent_of(X, Y), ancestor_of(Y, Z)."); - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate ancestorOf = Predicates.getPredicate("ancestor_of", 2); - Predicate parentOf = Predicates.getPredicate("parent_of", 2); - - assertEquals(2, strata.size()); - assertTrue(predicateIsBeforePredicateInOrder(parentOf, ancestorOf, strata)); - } - - @Test - public void stratifyLargeGraphTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a."); - bld.append("c :- b."); - bld.append("d :- c."); - bld.append("e :- d."); - bld.append("f :- not e."); - bld.append("g :- d, j, not f."); - bld.append("h :- not c."); - bld.append("i :- h, not j."); - bld.append("j :- h, not i."); - bld.append("k :- g, not l."); - bld.append("l :- g, not k."); - bld.append("m :- not k, not l."); - bld.append("n :- m, not i, not j."); - bld.append("p :- not m, not n."); - - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate a = Predicates.getPredicate("a", 0); - Predicate b = Predicates.getPredicate("b", 0); - Predicate c = Predicates.getPredicate("c", 0); - Predicate d = Predicates.getPredicate("d", 0); - Predicate e = Predicates.getPredicate("e", 0); - Predicate f = Predicates.getPredicate("f", 0); - Predicate h = Predicates.getPredicate("h", 0); - - assertTrue(predicateIsBeforePredicateInOrder(a, h, strata)); - assertTrue(predicateIsBeforePredicateInOrder(b, h, strata)); - assertTrue(predicateIsBeforePredicateInOrder(c, h, strata)); - - assertTrue(predicateIsBeforePredicateInOrder(a, f, strata)); - assertTrue(predicateIsBeforePredicateInOrder(b, f, strata)); - assertTrue(predicateIsBeforePredicateInOrder(c, f, strata)); - assertTrue(predicateIsBeforePredicateInOrder(d, f, strata)); - assertTrue(predicateIsBeforePredicateInOrder(e, f, strata)); - } - - @Test - public void stratifyAvoidDuplicatesTest() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a."); - bld.append("c :- b."); - bld.append("d :- c."); - bld.append("e :- d."); - bld.append("f :- not e."); - bld.append("g :- d, j, not f."); - bld.append("h :- not c."); - bld.append("i :- h, not j."); - bld.append("j :- h, not i."); - bld.append("k :- g, not l."); - bld.append("l :- g, not k."); - bld.append("m :- not k, not l."); - bld.append("n :- m, not i, not j."); - bld.append("p :- not m, not n."); - - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate a = Predicates.getPredicate("a", 0); - Predicate b = Predicates.getPredicate("b", 0); - Predicate c = Predicates.getPredicate("c", 0); - Predicate d = Predicates.getPredicate("d", 0); - Predicate e = Predicates.getPredicate("e", 0); - Predicate f = Predicates.getPredicate("f", 0); - Predicate h = Predicates.getPredicate("h", 0); - - assertEquals(7, strata.size()); - assertTrue(predicateIsBeforePredicateInOrder(a, b, strata)); - assertTrue(predicateIsBeforePredicateInOrder(b, c, strata)); - assertTrue(predicateIsBeforePredicateInOrder(c, h, strata)); - assertTrue(predicateIsBeforePredicateInOrder(c, d, strata)); - assertTrue(predicateIsBeforePredicateInOrder(d, e, strata)); - assertTrue(predicateIsBeforePredicateInOrder(e, f, strata)); - assertTrue(predicateIsBeforePredicateInOrder(d, f, strata)); - } - - @Test - public void avoidDuplicatesTest1() { - StringBuilder bld = new StringBuilder(); - bld.append("b :- a."); - bld.append("c :- b."); - bld.append("c :- a."); - - ASPCore2Program prog = parser.parse(bld.toString()); - NormalProgram normalProg = normalizeTransform.apply(prog); - AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalProg); - DependencyGraph dg = analyzed.getDependencyGraph(); - ComponentGraph cg = ComponentGraphImpl.buildComponentGraph(dg, StronglyConnectedComponentsAlgorithm.findStronglyConnectedComponents(dg)); - List strata = StratificationAlgorithm.calculateStratification(cg); - - Predicate a = Predicates.getPredicate("a", 0); - Predicate b = Predicates.getPredicate("b", 0); - Predicate c = Predicates.getPredicate("c", 0); - - assertTrue(predicateIsBeforePredicateInOrder(a, b, strata)); - assertTrue(predicateIsBeforePredicateInOrder(b, c, strata)); - assertTrue(predicateIsBeforePredicateInOrder(a, c, strata)); - - assertEquals(3, strata.size()); - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/GrounderMockWithBasicProgram.java similarity index 96% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java rename to alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/GrounderMockWithBasicProgram.java index 669e6037f..7950b90dd 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/GrounderMockWithBasicProgram.java @@ -71,7 +71,7 @@ * * Copyright (c) 2016, the Alpha Team. */ -public class DummyGrounder implements Grounder { +public class GrounderMockWithBasicProgram implements Grounder { public static final Set EXPECTED = new HashSet<>(singletonList(new AnswerSetBuilder() .predicate("a") .predicate("b") @@ -98,11 +98,11 @@ public class DummyGrounder implements Grounder { private static Atom rule1 = new RuleAtom(InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(ruleABC)), new BasicSubstitution()); private Set returnedNogoods = new HashSet<>(); - public DummyGrounder(AtomStore atomStore) { + public GrounderMockWithBasicProgram(AtomStore atomStore) { this(atomStore, p -> true); } - public DummyGrounder(AtomStore atomStore, java.util.function.Predicate filter) { + public GrounderMockWithBasicProgram(AtomStore atomStore, java.util.function.Predicate filter) { this.atomStore = atomStore; this.filter = filter; Arrays.asList(atomAA, atomBB, rule1, atomCC).forEach(atomStore::putIfAbsent); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/GrounderMockWithChoice.java similarity index 97% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java rename to alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/GrounderMockWithChoice.java index 66374d312..bda74f709 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/GrounderMockWithChoice.java @@ -70,7 +70,7 @@ /** * Represents a small ASP program with choices {@code { aa :- not bb. bb :- not aa. }}. */ -public class ChoiceGrounder implements Grounder { +public class GrounderMockWithChoice implements Grounder { public static final Set EXPECTED = new HashSet<>(asList( new AnswerSetBuilder() .predicate("aa") @@ -129,11 +129,11 @@ public class ChoiceGrounder implements Grounder { private final java.util.function.Predicate filter; - public ChoiceGrounder(AtomStore atomStore) { + public GrounderMockWithChoice(AtomStore atomStore) { this(atomStore, p -> true); } - public ChoiceGrounder(AtomStore atomStore, java.util.function.Predicate filter) { + public GrounderMockWithChoice(AtomStore atomStore, java.util.function.Predicate filter) { this.atomStore = atomStore; this.filter = filter; Arrays.asList(atomAA, atomBB, rule1, rule2, atomEnBR1, atomEnBR2, atomDisBR1, atomDisBR2).forEach(atomStore::putIfAbsent); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounderTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounderTest.java deleted file mode 100644 index 4321d27da..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounderTest.java +++ /dev/null @@ -1,460 +0,0 @@ -/* - * Copyright (c) 2018-2020 Siemens AG - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * 1) Redistributions of source code must retain the above copyright notice, this - * list of conditions and the following disclaimer. - * - * 2) Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE - * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR - * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER - * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, - * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ -package at.ac.tuwien.kr.alpha.core.grounder; - -import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.atom; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; -import static org.junit.jupiter.api.Assertions.fail; - -import java.util.Arrays; -import java.util.Collection; -import java.util.Collections; -import java.util.List; -import java.util.Map; - -import org.junit.jupiter.api.BeforeEach; -import org.junit.jupiter.api.Disabled; -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.config.GrounderHeuristicsConfiguration; -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.grounder.Substitution; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; -import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution; -import at.ac.tuwien.kr.alpha.commons.substitutions.Instance; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.atoms.Literals; -import at.ac.tuwien.kr.alpha.core.common.Assignment; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.common.NoGood; -import at.ac.tuwien.kr.alpha.core.grounder.instantiation.BindingResult; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; -import at.ac.tuwien.kr.alpha.core.parser.ProgramPartParser; -import at.ac.tuwien.kr.alpha.core.programs.AnalyzedProgram; -import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; -import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; -import at.ac.tuwien.kr.alpha.core.programs.transformation.StratifiedEvaluation; -import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; -import at.ac.tuwien.kr.alpha.core.rules.InternalRule; -import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; -import at.ac.tuwien.kr.alpha.core.solver.TrailAssignment; - -/** - * Tests {@link NaiveGrounder} - * - * Some test cases use atoms of the something/1 predicate to trick the grounder - * into believing that other atoms might become true. This is fragile because future implementations - * of preprocessing techniques might render this trick useless. - * If unit tests in this class begin to fail due to such improvements to preprocessing, this issue must be addressed. - */ -public class NaiveGrounderTest { - private static final ProgramParser PROGRAM_PARSER = new ProgramParserImpl(); - private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser(); - private static final NormalizeProgramTransformation NORMALIZE_TRANSFORM = new NormalizeProgramTransformation( - SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - - final Literal litP1X = PROGRAM_PART_PARSER.parseLiteral("p1(X)"); - final Literal litP2X = PROGRAM_PART_PARSER.parseLiteral("p2(X)"); - final Literal litQ2Y = PROGRAM_PART_PARSER.parseLiteral("q2(Y)"); - final Literal litQ1Y = PROGRAM_PART_PARSER.parseLiteral("q1(Y)"); - final Literal litAX = PROGRAM_PART_PARSER.parseLiteral("a(X)"); - final Literal litA1 = PROGRAM_PART_PARSER.parseLiteral("a(1)"); - - @BeforeEach - public void resetRuleIdGenerator() { - InternalRule.resetIdGenerator(); - } - - /** - * Asserts that a ground rule whose positive body is not satisfied by the empty assignment - * is grounded immediately. - */ - @Test - public void groundRuleAlreadyGround() { - ASPCore2Program program = PROGRAM_PARSER.parse("a :- not b. " - + "b :- not a. " - + "c :- b."); - NormalProgram normal = NORMALIZE_TRANSFORM.apply(program); - CompiledProgram prog = new StratifiedEvaluation().apply(AnalyzedProgram.analyzeNormalProgram(normal)); - - AtomStore atomStore = new AtomStoreImpl(); - Grounder grounder = GrounderFactory.getInstance("naive", prog, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); - int litCNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("c")), false); - int litB = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("b"))); - assertExistsNoGoodContaining(noGoods.values(), litCNeg); - assertExistsNoGoodContaining(noGoods.values(), litB); - } - - /** - * Asserts that a ground rule whose positive non-unary body is not satisfied by the empty assignment - * is grounded immediately. - */ - @Test - public void groundRuleWithLongerBodyAlreadyGround() { - ASPCore2Program program = PROGRAM_PARSER.parse("a :- not b. " - + "b :- not a. " - + "c :- b. " - + "d :- b, c. "); - NormalProgram normal = NORMALIZE_TRANSFORM.apply(program); - InternalProgram prog = new StratifiedEvaluation().apply(AnalyzedProgram.analyzeNormalProgram(normal)); - - AtomStore atomStore = new AtomStoreImpl(); - Grounder grounder = GrounderFactory.getInstance("naive", prog, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); - int litANeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("a")), false); - int litBNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("b")), false); - int litCNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("c")), false); - int litDNeg = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("d")), false); - assertExistsNoGoodContaining(noGoods.values(), litANeg); - assertExistsNoGoodContaining(noGoods.values(), litBNeg); - assertExistsNoGoodContaining(noGoods.values(), litCNeg); - assertExistsNoGoodContaining(noGoods.values(), litDNeg); - } - - /** - * Asserts that a ground constraint whose positive body is not satisfied by the empty assignment - * is grounded immediately. - */ - @Test - public void groundConstraintAlreadyGround() { - ASPCore2Program program = PROGRAM_PARSER.parse("a :- not b. " - + "b :- not a. " - + ":- b."); - NormalProgram normal = NORMALIZE_TRANSFORM.apply(program); - InternalProgram prog = new StratifiedEvaluation().apply(AnalyzedProgram.analyzeNormalProgram(normal)); - - AtomStore atomStore = new AtomStoreImpl(); - Grounder grounder = GrounderFactory.getInstance("naive", prog, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); - int litB = Literals.atomToLiteral(atomStore.get(PROGRAM_PART_PARSER.parseBasicAtom("b"))); - assertTrue(noGoods.containsValue(NoGood.fromConstraint(Collections.singletonList(litB), Collections.emptyList()))); - } - - @Test - public void avoidDeadEndsWithPermissiveGrounderHeuristicForP1() { - RuleGroundingOrderImpl groundingOrderP1 = new RuleGroundingOrderImpl(litP1X, - Arrays.asList(litP2X, litQ2Y, litQ1Y), -1, false); - testDeadEnd("p1", groundingOrderP1, true); - } - - @Test - public void avoidDeadEndsWithPermissiveGrounderHeuristicForQ1() { - RuleGroundingOrderImpl groundingOrderQ1 = new RuleGroundingOrderImpl(litQ1Y, - Arrays.asList(litQ2Y, litP2X, litP1X), -1, false); - testDeadEnd("q1", groundingOrderQ1, true); - } - - @Test - public void noDeadEndWithPermissiveGrounderHeuristicForP1() { - RuleGroundingOrderImpl groundingOrderP1 = new RuleGroundingOrderImpl(litP1X, - Arrays.asList(litP2X, litQ1Y, litQ2Y), -1, false); - testDeadEnd("p1", groundingOrderP1, true); - } - - @Test - public void noDeadEndWithPermissiveGrounderHeuristicForQ1() { - RuleGroundingOrderImpl groundingOrderQ1 = new RuleGroundingOrderImpl(litQ1Y, - Arrays.asList(litQ2Y, litP1X, litP2X), -1, false); - testDeadEnd("q1", groundingOrderQ1, true); - } - - /** - * Tests the method {@link NaiveGrounder#getGroundInstantiations(InternalRule, RuleGroundingOrder, Substitution, Assignment)} on a - * predefined program: - * - * p1(1). q1(1).
- * x :- p1(X), p2(X), q1(Y), q2(Y).
- * p2(X) :- something(X).
- * q2(X) :- something(X).
- * - * Given one grounding order {@code groundingOrder} for the first rule in this program which starts with - * the literal whose predicate name is {@code predicateNameOfStartingLiteral} and a substitution substituting - * the variable in this literal by 1 it is attempted to ground the rule. - * It is then asserted that ground instantiations are produced if and only if {@code expectNoGoods} is true. - * - * @param predicateNameOfStartingLiteral the predicate name of the starting literal, either "p1" or "q1". - * @param groundingOrder a grounding order for the first rule in the predefined program that starts with the literal - * whose predicate name is {@code predicateNameOfStartingLiteral}. - * @param expectNoGoods {@code true} iff ground instantiations are expected to be produced under the conditions - * described above. - */ - private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrderImpl groundingOrder, boolean expectNoGoods) { - String aspStr = "p1(1). q1(1). " - + "x :- p1(X), p2(X), q1(Y), q2(Y). " - + "p2(X) :- something(X). " - + "q2(X) :- something(X). "; - CompiledProgram program = InternalProgram.fromNormalProgram( - NORMALIZE_TRANSFORM.apply( - PROGRAM_PARSER.parse(aspStr))); - - AtomStore atomStore = new AtomStoreImpl(); - NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, - GrounderHeuristicsConfiguration.permissive(), true); - - CompiledRule nonGroundRule = grounder.getNonGroundRule(0); - String strLiteral = "p1".equals(predicateNameOfStartingLiteral) ? "p1(X)" : "p1(Y)"; - final Literal startingLiteral = PROGRAM_PART_PARSER.parseLiteral(strLiteral); - ((RuleGroundingInfoImpl) nonGroundRule.getGroundingInfo()).groundingOrders.put(startingLiteral, groundingOrder); - - grounder.bootstrap(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore); - final Substitution subst1 = BasicSubstitution.specializeSubstitution(startingLiteral, new Instance(Terms.newConstant(1)), - BasicSubstitution.EMPTY_SUBSTITUTION); - final BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, groundingOrder, subst1, currentAssignment); - - assertEquals(expectNoGoods, bindingResult.size() > 0); - } - - @Test - public void testGroundingOfRuleSwitchedOffByFalsePositiveBody() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X). " - + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.FALSE, false); - } - - @Test - public void testGroundingOfRuleNotSwitchedOffByTruePositiveBody() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X). " - + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.TRUE, true); - } - - @Test - @Disabled("Currently, rule grounding is not switched off by a true negative body atom") - public void testGroundingOfRuleSwitchedOffByTrueNegativeBody() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), not b(X). " - + "b(X) :- something(X). "); - testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.TRUE, false); - } - - @Test - public void testGroundingOfRuleNotSwitchedOffByFalseNegativeBody() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), not b(X). " - + "b(X) :- something(X). "); - - testIfGrounderGroundsRule(program, 0, litAX, 1, ThriceTruth.FALSE, true); - } - - /** - * Tests if {@link NaiveGrounder#getGroundInstantiations(InternalRule, RuleGroundingOrder, Substitution, Assignment)} - * produces ground instantiations for the rule with ID {@code ruleID} in {@code program} when {@code startingLiteral} - * unified with the numeric instance {@code startingInstance} is used as starting literal and {@code b(1)} is assigned - * {@code bTruth}. - * It is asserted that ground instantiations are produced if and only if {@code expectNoGoods} is true. - */ - private void testIfGrounderGroundsRule(ASPCore2Program program, int ruleID, Literal startingLiteral, int startingInstance, ThriceTruth bTruth, - boolean expectNoGoods) { - CompiledProgram internalPrg = InternalProgram.fromNormalProgram(NORMALIZE_TRANSFORM.apply(program)); - AtomStore atomStore = new AtomStoreImpl(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore); - NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", internalPrg, atomStore, p -> true, - GrounderHeuristicsConfiguration.permissive(), true); - - int b = atomStore.putIfAbsent(atom("b", 1)); - currentAssignment.growForMaxAtomId(); - currentAssignment.assign(b, bTruth); - - grounder.bootstrap(); - final CompiledRule nonGroundRule = grounder.getNonGroundRule(ruleID); - final Substitution substStartingLiteral = BasicSubstitution.specializeSubstitution(startingLiteral, new Instance(Terms.newConstant(startingInstance)), - BasicSubstitution.EMPTY_SUBSTITUTION); - final BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, nonGroundRule.getGroundingInfo().orderStartingFrom(startingLiteral), - substStartingLiteral, currentAssignment); - assertEquals(expectNoGoods, bindingResult.size() > 0); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_0_reject() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X). " - + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 0, false, Arrays.asList(1)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_1_accept() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X). " - + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 1, true, Arrays.asList(1)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_1_reject() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X), b(X+1). " - + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 1, false, Arrays.asList(2)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_2_accept() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X), b(X+1). " - + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 2, true, Arrays.asList(2)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_1_accept_two_substitutions() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X,Y). " - + "b(X,Y) :- something(X,Y)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 1, new ThriceTruth[] {ThriceTruth.TRUE, ThriceTruth.TRUE }, 2, true, - Arrays.asList(0, 0)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_1_accept_accept_two_substitutions_with_different_remaining_tolerances() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(1), b(X,Y). " - + "b(X,Y) :- something(X,Y)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litA1, 1, 1, new ThriceTruth[] {null, null }, 2, true, Arrays.asList(1, 1)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_2_reject() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). " - + "c(X) :- a(X), b(X), b(X+1), b(X+2). " - + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 2, false, Arrays.asList(3)); - } - - @Test - public void testPermissiveGrounderHeuristicTolerance_2_accept_multiple_facts_of_same_variable() { - ASPCore2Program program = PROGRAM_PARSER.parse("a(1). b(1). " - + "c(X) :- a(X), b(X), b(X+1), b(X+2). " - + "b(X) :- something(X)."); - testPermissiveGrounderHeuristicTolerance(program, 0, litAX, 1, 2, true, Arrays.asList(2)); - } - - private void testPermissiveGrounderHeuristicTolerance(ASPCore2Program program, int ruleID, Literal startingLiteral, int startingInstance, int tolerance, - boolean expectNoGoods, List expectedNumbersOfUnassignedPositiveBodyAtoms) { - testPermissiveGrounderHeuristicTolerance(program, ruleID, startingLiteral, startingInstance, tolerance, new ThriceTruth[] {}, 1, expectNoGoods, - expectedNumbersOfUnassignedPositiveBodyAtoms); - } - - /** - * Tests if {@link NaiveGrounder#getGroundInstantiations(InternalRule, RuleGroundingOrder, Substitution, Assignment)} - * produces ground instantiations for the rule with ID {@code ruleID} in {@code program} when {@code startingLiteral} - * unified with the numeric instance {@code startingInstance} is used as starting literal and the following - * additional conditions are established: - *
    - *
  • The atoms {@code b([startingInstance], 1), ..., b([startingInstance], n)} are added to the grounder's - * working memory without changing the assignment, where {@code arityOfB-1} occurences of {@code startingInstance} - * are used instead of {@code [startingInstance]} and {@code n} is the length of the {@code truthsOfB} array. - * For example, if the length of {@code truthsOfB} is 2 and {@code arityOfB} is also 2, these atoms are - * {@code b(1,1), b(1,2)}. - *
    • - *
  • The same atoms are assigned the truth values in the {@code truthsOfB} array.
    • - *
- * It is asserted that ground instantiations are produced if and only if {@code expectNoGoods} is true. - * If ground instantiations are produced, it is also asserted that the numbers of unassigned positive body atoms - * determined by {@code getGroundInstantiations} match those given in {@code expectedNumbersOfUnassignedPositiveBodyAtoms}. - */ - private void testPermissiveGrounderHeuristicTolerance(ASPCore2Program program, int ruleID, Literal startingLiteral, int startingInstance, int tolerance, - ThriceTruth[] truthsOfB, int arityOfB, boolean expectNoGoods, List expectedNumbersOfUnassignedPositiveBodyAtoms) { - CompiledProgram internalPrg = InternalProgram.fromNormalProgram(NORMALIZE_TRANSFORM.apply(program)); - AtomStore atomStore = new AtomStoreImpl(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore); - GrounderHeuristicsConfiguration heuristicConfiguration = GrounderHeuristicsConfiguration.getInstance(tolerance, tolerance); - NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", internalPrg, atomStore, p -> true, heuristicConfiguration, true); - - int[] bAtomIDs = new int[truthsOfB.length]; - for (int i = 0; i < truthsOfB.length; i++) { - int[] bTerms = new int[arityOfB]; - for (int n = 0; n < arityOfB; n++) { - bTerms[n] = (n == arityOfB - 1) ? i + 1 : startingInstance; - } - bAtomIDs[i] = atomStore.putIfAbsent(atom("b", bTerms)); - } - addAtomsToWorkingMemoryWithoutChangingTheAssignment(atomStore, grounder, bAtomIDs); - assign(currentAssignment, bAtomIDs, truthsOfB); - - grounder.bootstrap(); - final CompiledRule nonGroundRule = grounder.getNonGroundRule(ruleID); - final Substitution substStartingLiteral = BasicSubstitution.specializeSubstitution(startingLiteral, new Instance(Terms.newConstant(startingInstance)), - BasicSubstitution.EMPTY_SUBSTITUTION); - final BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, nonGroundRule.getGroundingInfo().orderStartingFrom(startingLiteral), - substStartingLiteral, currentAssignment); - assertEquals(expectNoGoods, bindingResult.size() > 0); - if (bindingResult.size() > 0) { - assertEquals(expectedNumbersOfUnassignedPositiveBodyAtoms, bindingResult.getNumbersOfUnassignedPositiveBodyAtoms()); - } else { - assertTrue(bindingResult.getNumbersOfUnassignedPositiveBodyAtoms().isEmpty()); - } - } - - /** - * Assigns {@code truthValues} to atoms {@code atomIDs} in {@code currentAssignment}. - */ - private void assign(TrailAssignment currentAssignment, int[] atomIDs, ThriceTruth[] truthValues) { - currentAssignment.growForMaxAtomId(); - for (int i = 0; i < truthValues.length; i++) { - int atomID = atomIDs[i]; - if (truthValues[i] != null) { - currentAssignment.assign(atomID, truthValues[i]); - } - } - } - - /** - * Adds atoms {@code atomIDs} to {@code grounder}'s working memory without changing the assignment. - * This is achieved by creating a temporary assignment on {@code atomStore} in which those atoms are assigned true - * and using this temporary assignment to update the grounder's working memory. - */ - private void addAtomsToWorkingMemoryWithoutChangingTheAssignment(AtomStore atomStore, NaiveGrounder grounder, int[] atomIDs) { - TrailAssignment temporaryAssignment = new TrailAssignment(atomStore); - temporaryAssignment.growForMaxAtomId(); - for (int b : atomIDs) { - temporaryAssignment.assign(b, ThriceTruth.TRUE); - } - grounder.updateAssignment(temporaryAssignment.getNewPositiveAssignmentsIterator()); - } - - private void assertExistsNoGoodContaining(Collection noGoods, int literal) { - for (NoGood noGood : noGoods) { - for (int literalInNoGood : noGood) { - if (literalInNoGood == literal) { - return; - } - } - } - fail("No NoGood exists that contains literal " + literal); - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGeneratorTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGeneratorTest.java deleted file mode 100644 index e5d44ded9..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGeneratorTest.java +++ /dev/null @@ -1,93 +0,0 @@ -/** - * Copyright (c) 2018 Siemens AG - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * 1) Redistributions of source code must retain the above copyright notice, this - * list of conditions and the following disclaimer. - * - * 2) Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE - * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR - * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER - * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, - * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ -package at.ac.tuwien.kr.alpha.core.grounder; - -import static org.junit.jupiter.api.Assertions.assertEquals; - -import java.util.List; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.grounder.Substitution; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; -import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.atoms.Literals; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; -import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; -import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; -import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; -import at.ac.tuwien.kr.alpha.core.rules.InternalRule; - -/** - * Tests {@link NoGoodGenerator} - */ -public class NoGoodGeneratorTest { - - private static final ProgramParser PARSER = new ProgramParserImpl(); - private static final NormalizeProgramTransformation NORMALIZE_TRANSFORM = new NormalizeProgramTransformation( - SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - - private static final ConstantTerm A = Terms.newSymbolicConstant("a"); - private static final ConstantTerm B = Terms.newSymbolicConstant("b"); - - private static final VariableTerm X = Terms.newVariable("X"); - private static final VariableTerm Y = Terms.newVariable("Y"); - - /** - * Calls {@link NoGoodGenerator#collectNegLiterals(InternalRule, Substitution)}, which puts the atom occurring - * negatively in a rule into the atom store. It is then checked whether the atom in the atom store is positive. - */ - @Test - public void collectNeg_ContainsOnlyPositiveLiterals() { - ASPCore2Program input = PARSER.parse("p(a,b). " - + "q(a,b) :- not nq(a,b). " - + "nq(a,b) :- not q(a,b)."); - NormalProgram normal = NORMALIZE_TRANSFORM.apply(input); - CompiledProgram program = InternalProgram.fromNormalProgram(normal); - - CompiledRule rule = program.getRules().get(1); - AtomStore atomStore = new AtomStoreImpl(); - Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - NoGoodGenerator noGoodGenerator = ((NaiveGrounder) grounder).noGoodGenerator; - Substitution substitution = new BasicSubstitution(); - substitution.put(X, A); - substitution.put(Y, B); - List collectedNeg = noGoodGenerator.collectNegLiterals(rule, substitution); - assertEquals(1, collectedNeg.size()); - String negAtomString = atomStore.atomToString(Literals.atomOf(collectedNeg.get(0))); - assertEquals("q(a, b)", negAtomString); - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleGroundingInfoTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleGroundingInfoTest.java new file mode 100644 index 000000000..4f95d0f2c --- /dev/null +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleGroundingInfoTest.java @@ -0,0 +1,199 @@ +/* + * Copyright (c) 2017-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * 1) Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * 2) Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ +package at.ac.tuwien.kr.alpha.core.grounder; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.junit.jupiter.api.Assertions.fail; + +import org.junit.jupiter.api.Test; + +import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; +import at.ac.tuwien.kr.alpha.api.terms.ArithmeticOperator; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; +import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; +import at.ac.tuwien.kr.alpha.commons.terms.Terms; +import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; +import at.ac.tuwien.kr.alpha.core.rules.InternalRule; + +/** + * Copyright (c) 2017-2021, the Alpha Team. + */ +public class RuleGroundingInfoTest { + + @Test + public void groundingOrder() { + // r1 := h(X,C) :- p(X,Y), q(A,B), r(Y,A), s(C). + CompiledRule r1 = new InternalRule( + Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("h", 2), Terms.newVariable("X"), Terms.newVariable("C"))), + Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("q", 2), Terms.newVariable("A"), Terms.newVariable("B")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("r", 2), Terms.newVariable("Y"), Terms.newVariable("A")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("s", 1), Terms.newVariable("C")).toLiteral()); + RuleGroundingInfo rgo1 = new RuleGroundingInfoImpl(r1); + rgo1.computeGroundingOrders(); + assertEquals(4, rgo1.getStartingLiterals().size()); + + // r2 := j(A,A,X,Y) :- r1(A,A), r1(X,Y), r1(A,X), r1(A,Y). + CompiledRule r2 = new InternalRule( + Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("j", 4), Terms.newVariable("A"), Terms.newVariable("A"), Terms.newVariable("X"), + Terms.newVariable("Y"))), + Atoms.newBasicAtom(Predicates.getPredicate("r1", 2), Terms.newVariable("A"), Terms.newVariable("A")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("r1", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("r1", 2), Terms.newVariable("A"), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("r1", 2), Terms.newVariable("A"), Terms.newVariable("Y")).toLiteral()); + RuleGroundingInfo rgo2 = new RuleGroundingInfoImpl(r2); + rgo2.computeGroundingOrders(); + assertEquals(4, rgo2.getStartingLiterals().size()); + + // r3 := p(a) :- b = a. + CompiledRule r3 = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Terms.newSymbolicConstant("a"))), + Atoms.newComparisonAtom(Terms.newSymbolicConstant("b"), Terms.newSymbolicConstant("a"), ComparisonOperators.EQ).toLiteral()); + RuleGroundingInfo rgo3 = new RuleGroundingInfoImpl(r3); + rgo3.computeGroundingOrders(); + assertTrue(rgo3.hasFixedInstantiation()); + } + + /** + * Tests that an exception is thrown when trying to compute grounding orders for a rule that is not safe due to cyclic dependencies between + * body variables. + */ + @Test + public void groundingOrderUnsafe() { + assertThrows(RuntimeException.class, () -> { + // rule := h(X, Z) :- Y = X + 1, X = Z + 1, Z = Y - 2. + CompiledRule rule = new InternalRule( + Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("h", 2), Terms.newVariable("X"), Terms.newVariable("Z"))), + Atoms.newComparisonAtom( + Terms.newVariable("Y"), + Terms.newArithmeticTerm(Terms.newVariable("Y"), ArithmeticOperator.PLUS, Terms.newConstant(1)), + ComparisonOperators.EQ).toLiteral(), + Atoms.newComparisonAtom( + Terms.newVariable("X"), + Terms.newArithmeticTerm(Terms.newVariable("Z"), ArithmeticOperator.PLUS, Terms.newConstant(1)), + ComparisonOperators.EQ).toLiteral(), + Atoms.newComparisonAtom( + Terms.newVariable("Z"), + Terms.newArithmeticTerm(Terms.newVariable("Y"), ArithmeticOperator.MINUS, Terms.newConstant(2)), + ComparisonOperators.EQ).toLiteral()); + computeGroundingOrdersForRule(rule); + }); + } + + @Test + public void testPositionFromWhichAllVarsAreBound_ground() { + // rule := a :- b, not c. + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("a", 0))), + Atoms.newBasicAtom(Predicates.getPredicate("b", 0)).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("c", 0)).toLiteral(false)); + RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(rule); + assertEquals(0, rgo0.getFixedGroundingOrder().getPositionFromWhichAllVarsAreBound()); + } + + @Test + public void testPositionFromWhichAllVarsAreBound_simpleNonGround() { + // rule := a(X) :- b(X), not c(X). + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("a", 1), Terms.newVariable("X"))), + Atoms.newBasicAtom(Predicates.getPredicate("b", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("c", 1), Terms.newVariable("X")).toLiteral(false)); + RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(rule); + assertEquals(1, rgo0.getStartingLiterals().size()); + for (Literal startingLiteral : rgo0.getStartingLiterals()) { + assertEquals(0, rgo0.orderStartingFrom(startingLiteral).getPositionFromWhichAllVarsAreBound()); + } + } + + @Test + public void testPositionFromWhichAllVarsAreBound_longerSimpleNonGround() { + // rule := a(X) :- b(X), c(X), d(X), not e(X). + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("a", 1), Terms.newVariable("X"))), + Atoms.newBasicAtom(Predicates.getPredicate("b", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("c", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("d", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("e", 1), Terms.newVariable("X")).toLiteral(false)); + RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(rule); + assertEquals(3, rgo0.getStartingLiterals().size()); + for (Literal startingLiteral : rgo0.getStartingLiterals()) { + assertEquals(0, rgo0.orderStartingFrom(startingLiteral).getPositionFromWhichAllVarsAreBound()); + } + } + + @Test + public void testToString_longerSimpleNonGround() { + // rule := a(X) :- b(X), c(X), d(X), not e(X). + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("a", 1), Terms.newVariable("X"))), + Atoms.newBasicAtom(Predicates.getPredicate("b", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("c", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("d", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("e", 1), Terms.newVariable("X")).toLiteral(false)); + RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(rule); + assertEquals(3, rgo0.getStartingLiterals().size()); + for (Literal startingLiteral : rgo0.getStartingLiterals()) { + switch (startingLiteral.getPredicate().getName()) { + case "b": + assertEquals("b(X) : | c(X), d(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); + break; + case "c": + assertEquals("c(X) : | b(X), d(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); + break; + case "d": + assertEquals("d(X) : | b(X), c(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); + break; + default: + fail("Unexpected starting literal: " + startingLiteral); + } + } + } + + @Test + public void testPositionFromWhichAllVarsAreBound_joinedNonGround() { + // rule := a(X) :- b(X), c(X, Y), d(X, Z), not e(X). + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("a", 1), Terms.newVariable("X"))), + Atoms.newBasicAtom(Predicates.getPredicate("b", 1), Terms.newVariable("X")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("c", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("d", 2), Terms.newVariable("X"), Terms.newVariable("Z")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("e", 1), Terms.newVariable("X")).toLiteral(false)); + RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(rule); + final Literal litBX = Atoms.newBasicAtom(Predicates.getPredicate("b", 1), Terms.newVariable("X")).toLiteral(); + final Literal litCXY = Atoms.newBasicAtom(Predicates.getPredicate("c", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(); + final Literal litDXZ = Atoms.newBasicAtom(Predicates.getPredicate("d", 2), Terms.newVariable("X"), Terms.newVariable("Z")).toLiteral(); + assertTrue(2 <= rgo0.orderStartingFrom(litBX).getPositionFromWhichAllVarsAreBound()); + assertTrue(1 <= rgo0.orderStartingFrom(litCXY).getPositionFromWhichAllVarsAreBound()); + assertTrue(1 <= rgo0.orderStartingFrom(litDXZ).getPositionFromWhichAllVarsAreBound()); + } + + private RuleGroundingInfo computeGroundingOrdersForRule(CompiledRule rule) { + RuleGroundingInfo rgo = new RuleGroundingInfoImpl(rule); + rgo.computeGroundingOrders(); + return rgo; + } + +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleGroundingOrderTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleGroundingOrderTest.java deleted file mode 100644 index b8964e9b6..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleGroundingOrderTest.java +++ /dev/null @@ -1,167 +0,0 @@ -/* - * Copyright (c) 2017-2020, the Alpha Team. - * All rights reserved. - * - * Additional changes made by Siemens. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * 1) Redistributions of source code must retain the above copyright notice, this - * list of conditions and the following disclaimer. - * - * 2) Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE - * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR - * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER - * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, - * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ -package at.ac.tuwien.kr.alpha.core.grounder; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertThrows; -import static org.junit.jupiter.api.Assertions.assertTrue; -import static org.junit.jupiter.api.Assertions.fail; - -import java.util.function.Function; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; -import at.ac.tuwien.kr.alpha.core.parser.ProgramPartParser; -import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; -import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; -import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; - -/** - * Copyright (c) 2017-2019, the Alpha Team. - */ -public class RuleGroundingOrderTest { - - private static final ProgramParser PARSER = new ProgramParserImpl(); - private static final NormalizeProgramTransformation NORMALIZE_TRANSFORM = new NormalizeProgramTransformation( - SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - private static final Function PARSE_AND_PREPROCESS = (str) -> { - return InternalProgram.fromNormalProgram(NORMALIZE_TRANSFORM.apply(PARSER.parse(str))); - }; - - private static final ProgramPartParser PROGRAM_PART_PARSER = new ProgramPartParser(); - - @Test - public void groundingOrder() { - String aspStr = "h(X,C) :- p(X,Y), q(A,B), r(Y,A), s(C)." + - "j(A,B,X,Y) :- r1(A,B), r1(X,Y), r1(A,X), r1(B,Y), A = B." + - "p(a) :- b = a."; - CompiledProgram prog = PARSE_AND_PREPROCESS.apply(aspStr); - CompiledRule rule0 = prog.getRules().get(0); - RuleGroundingInfo rgo0 = new RuleGroundingInfoImpl(rule0); - rgo0.computeGroundingOrders(); - assertEquals(4, rgo0.getStartingLiterals().size()); - - CompiledRule rule1 = prog.getRules().get(1); - RuleGroundingInfo rgo1 = new RuleGroundingInfoImpl(rule1); - rgo1.computeGroundingOrders(); - assertEquals(4, rgo1.getStartingLiterals().size()); - - CompiledRule rule2 = prog.getRules().get(2); - RuleGroundingInfo rgo2 = new RuleGroundingInfoImpl(rule2); - rgo2.computeGroundingOrders(); - assertTrue(rgo2.hasFixedInstantiation()); - } - - @Test - public void groundingOrderUnsafe() { - assertThrows(RuntimeException.class, () -> { - String aspStr = "h(X,C) :- X = Y, Y = C .. 3, C = X."; - CompiledProgram prog = PARSE_AND_PREPROCESS.apply(aspStr); - computeGroundingOrdersForRule(prog, 0); - }); - } - - @Test - public void testPositionFromWhichAllVarsAreBound_ground() { - String aspStr = "a :- b, not c."; - CompiledProgram internalPrg = PARSE_AND_PREPROCESS.apply(aspStr); - RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(internalPrg, 0); - assertEquals(0, rgo0.getFixedGroundingOrder().getPositionFromWhichAllVarsAreBound()); - } - - @Test - public void testPositionFromWhichAllVarsAreBound_simpleNonGround() { - String aspStr = "a(X) :- b(X), not c(X)."; - CompiledProgram internalPrg = PARSE_AND_PREPROCESS.apply(aspStr); - RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(internalPrg, 0); - assertEquals(1, rgo0.getStartingLiterals().size()); - for (Literal startingLiteral : rgo0.getStartingLiterals()) { - assertEquals(0, rgo0.orderStartingFrom(startingLiteral).getPositionFromWhichAllVarsAreBound()); - } - } - - @Test - public void testPositionFromWhichAllVarsAreBound_longerSimpleNonGround() { - String aspStr = "a(X) :- b(X), c(X), d(X), not e(X)."; - CompiledProgram internalPrg = PARSE_AND_PREPROCESS.apply(aspStr); - RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(internalPrg, 0); - assertEquals(3, rgo0.getStartingLiterals().size()); - for (Literal startingLiteral : rgo0.getStartingLiterals()) { - assertEquals(0, rgo0.orderStartingFrom(startingLiteral).getPositionFromWhichAllVarsAreBound()); - } - } - - @Test - public void testToString_longerSimpleNonGround() { - String aspStr = "a(X) :- b(X), c(X), d(X), not e(X)."; - CompiledProgram internalPrg = PARSE_AND_PREPROCESS.apply(aspStr); - RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(internalPrg, 0); - assertEquals(3, rgo0.getStartingLiterals().size()); - for (Literal startingLiteral : rgo0.getStartingLiterals()) { - switch (startingLiteral.getPredicate().getName()) { - case "b": - assertEquals("b(X) : | c(X), d(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); - break; - case "c": - assertEquals("c(X) : | b(X), d(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); - break; - case "d": - assertEquals("d(X) : | b(X), c(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); - break; - default: - fail("Unexpected starting literal: " + startingLiteral); - } - } - } - - @Test - public void testPositionFromWhichAllVarsAreBound_joinedNonGround() { - String aspStr = "a(X) :- b(X), c(X,Y), d(X,Z), not e(X)."; - CompiledProgram internalPrg = PARSE_AND_PREPROCESS.apply(aspStr); - RuleGroundingInfo rgo0 = computeGroundingOrdersForRule(internalPrg, 0); - final Literal litBX = PROGRAM_PART_PARSER.parseLiteral("b(X)"); - final Literal litCXY = PROGRAM_PART_PARSER.parseLiteral("c(X,Y)"); - final Literal litDXZ = PROGRAM_PART_PARSER.parseLiteral("d(X,Z)"); - assertTrue(2 <= rgo0.orderStartingFrom(litBX).getPositionFromWhichAllVarsAreBound()); - assertTrue(1 <= rgo0.orderStartingFrom(litCXY).getPositionFromWhichAllVarsAreBound()); - assertTrue(1 <= rgo0.orderStartingFrom(litDXZ).getPositionFromWhichAllVarsAreBound()); - } - - private RuleGroundingInfo computeGroundingOrdersForRule(CompiledProgram program, int ruleIndex) { - CompiledRule rule = program.getRules().get(ruleIndex); - RuleGroundingInfo rgo = new RuleGroundingInfoImpl(rule); - rgo.computeGroundingOrders(); - return rgo; - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/SubstitutionTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/SubstitutionTest.java index 2fc8f87a2..24c2aceea 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/SubstitutionTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/SubstitutionTest.java @@ -35,11 +35,8 @@ 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.ProgramParser; import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; -import at.ac.tuwien.kr.alpha.api.rules.Rule; -import at.ac.tuwien.kr.alpha.api.rules.heads.Head; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.api.terms.FunctionTerm; import at.ac.tuwien.kr.alpha.api.terms.Term; @@ -47,19 +44,17 @@ import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.literals.Literals; +import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution; import at.ac.tuwien.kr.alpha.commons.substitutions.Instance; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.atoms.RuleAtom; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; import at.ac.tuwien.kr.alpha.core.rules.InternalRule; -import at.ac.tuwien.kr.alpha.core.rules.NormalRuleImpl; import at.ac.tuwien.kr.alpha.core.test.util.SubstitutionTestUtil; import at.ac.tuwien.kr.alpha.core.util.Substitutions; public class SubstitutionTest { - private static final ProgramParser PARSER = new ProgramParserImpl(); private static final ConstantTerm A = Terms.newSymbolicConstant("a"); private static final ConstantTerm B = Terms.newSymbolicConstant("b"); @@ -113,11 +108,13 @@ public void substituteNegativeBasicAtom() { @Test public void groundAndPrintRule() { - Rule rule = PARSER.parse("x :- p(X,Y), not q(X,Y).").getRules().get(0); - CompiledRule nonGroundRule = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(rule)); + // rule := x :- p(X,Y), not q(X,Y). + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("x", 0))), + Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("q", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(false)); Substitution substitution1 = BasicSubstitution.specializeSubstitution(PX, PA, BasicSubstitution.EMPTY_SUBSTITUTION); Substitution substitution2 = BasicSubstitution.specializeSubstitution(PY, PB, substitution1); - String printedString = SubstitutionTestUtil.groundAndPrintRule(nonGroundRule, substitution2); + String printedString = SubstitutionTestUtil.groundAndPrintRule(rule, substitution2); assertEquals("x :- p(a, b), not q(a, b).", printedString); } @@ -168,11 +165,13 @@ private void groundLiteralToString(boolean negated) { @Test public void substitutionFromString() { - Rule rule = PARSER.parse("x :- p(X,Y), not q(X,Y).").getRules().get(0); - CompiledRule nonGroundRule = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(rule)); + // rule := x :- p(X,Y), not q(X,Y). + CompiledRule rule = new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("x", 0))), + Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("q", 2), Terms.newVariable("X"), Terms.newVariable("Y")).toLiteral(false)); Substitution substitution1 = BasicSubstitution.specializeSubstitution(PX, PA, BasicSubstitution.EMPTY_SUBSTITUTION); Substitution substitution = BasicSubstitution.specializeSubstitution(PY, PB, substitution1); - RuleAtom ruleAtom = new RuleAtom(nonGroundRule, substitution); + RuleAtom ruleAtom = new RuleAtom(rule, substitution); String substitutionString = (String) ((ConstantTerm) ruleAtom.getTerms().get(1)).getObject(); Substitution fromString = Substitutions.fromString(substitutionString); assertEquals(substitution, fromString); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/UnificationTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/UnificationTest.java deleted file mode 100644 index 7492fc3d7..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/UnificationTest.java +++ /dev/null @@ -1,111 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.grounder; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertNotNull; -import static org.junit.jupiter.api.Assertions.assertNull; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; -import at.ac.tuwien.kr.alpha.commons.substitutions.Unifier; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.parser.ProgramPartParser; - -/** - * Copyright (c) 2021, the Alpha Team. - */ -public class UnificationTest { - - private ProgramPartParser partsParser = new ProgramPartParser(); - - @Test - public void simpleGroundUnification() { - Atom pX = partsParser.parseLiteral("p(X)").getAtom(); - Atom pa = partsParser.parseLiteral("p(abc)").getAtom(); - Unifier unifier = Unification.unifyAtoms(pa, pX); - assertNotNull(unifier); - assertEquals(1, unifier.getMappedVariables().size()); - assertEquals("abc", unifier.eval(Terms.newVariable("X")).toString()); - } - - @Test - public void unificationBothSides() { - Atom left = partsParser.parseLiteral("p(X, 1)").getAtom(); - Atom right = partsParser.parseLiteral("p(d, Y)").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNotNull(unifier); - assertEquals(2, unifier.getMappedVariables().size()); - assertEquals("d", unifier.eval(Terms.newVariable("X")).toString()); - assertEquals("1", unifier.eval(Terms.newVariable("Y")).toString()); - } - - @Test - public void unificationNonGround() { - Atom left = partsParser.parseLiteral("p(X, 13)").getAtom(); - Atom right = partsParser.parseLiteral("p(Z, Y)").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNotNull(unifier); - assertEquals(3, unifier.getMappedVariables().size()); - assertEquals("13", unifier.eval(Terms.newVariable("Y")).toString()); - // Check that the unifier sets X=Z by either mapping X -> Z or Z -> X. - if (unifier.eval(Terms.newVariable("X")) != null) { - // X is mapped, it must map to Z now. - assertEquals("Z", unifier.eval(Terms.newVariable("X")).toString()); - } else { - // X is not mapped, so Z must map to X. - assertEquals("X", unifier.eval(Terms.newVariable("Z")).toString()); - } - } - - @Test - public void unificationWithFunctionTerms() { - Atom left = partsParser.parseLiteral("a(b, f(X, 13), g(Z), d)").getAtom(); - Atom right = partsParser.parseLiteral("a(b, A, g(e), d)").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNotNull(unifier); - assertEquals(3, unifier.getMappedVariables().size()); - assertEquals(left.substitute(unifier).toString(), right.substitute(unifier).toString()); - } - - @Test - public void unificationWithArithmeticTerms() { - Atom left = partsParser.parseLiteral("a(X - (3 * Y))").getAtom(); - Atom right = partsParser.parseLiteral("a(15 - Z)").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNotNull(unifier); - assertEquals(3, unifier.getMappedVariables().size()); - assertEquals(left.substitute(unifier).toString(), right.substitute(unifier).toString()); - } - - @Test - public void nonunificationWithArithmeticTerms() { - Atom left = partsParser.parseLiteral("a(X + 4)").getAtom(); - Atom right = partsParser.parseLiteral("a(Y - 4)").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNull(unifier); - } - - @Test - public void nonunificationWithArithmeticTermsNested() { - Atom left = partsParser.parseLiteral("a(X + 7)").getAtom(); - Atom right = partsParser.parseLiteral("a(Y + (Z - 2))").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNull(unifier); - } - - @Test - public void nonunificationSimple() { - Atom left = partsParser.parseLiteral("a(b,X)").getAtom(); - Atom right = partsParser.parseLiteral("a(c,Y)").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNull(unifier); - } - - @Test - public void nonunificationNested() { - Atom left = partsParser.parseLiteral("a(f(X,a))").getAtom(); - Atom right = partsParser.parseLiteral("a(f(a,b))").getAtom(); - Unifier unifier = Unification.unifyAtoms(left, right); - assertNull(unifier); - } -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/UnifierTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/UnifierTest.java deleted file mode 100644 index d0a0aaf62..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/UnifierTest.java +++ /dev/null @@ -1,84 +0,0 @@ -/* - * Copyright (c) 2018, 2020, the Alpha Team. - * All rights reserved. - * - * Additional changes made by Siemens. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * 1) Redistributions of source code must retain the above copyright notice, this - * list of conditions and the following disclaimer. - * - * 2) Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE - * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR - * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER - * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, - * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ - -package at.ac.tuwien.kr.alpha.core.grounder; - -import static org.junit.jupiter.api.Assertions.assertEquals; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; -import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.api.terms.Term; -import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.commons.substitutions.Unifier; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; - -public class UnifierTest extends SubstitutionTest { - - @Test - public void extendUnifier() { - VariableTerm varX = Terms.newVariable("X"); - VariableTerm varY = Terms.newVariable("Y"); - Unifier sub1 = new Unifier(); - sub1.put(varX, varY); - Unifier sub2 = new Unifier(); - sub2.put(varY, Terms.newConstant("a")); - - sub1.extendWith(sub2); - BasicAtom atom1 = parseAtom("p(X)"); - - Atom atomSubstituted = atom1.substitute(sub1); - assertEquals(Terms.newConstant("a"), atomSubstituted.getTerms().get(0)); - } - - @Test - public void mergeUnifierIntoLeft() { - VariableTerm varX = Terms.newVariable("X"); - VariableTerm varY = Terms.newVariable("Y"); - VariableTerm varZ = Terms.newVariable("Z"); - Term constA = Terms.newConstant("a"); - Unifier left = new Unifier(); - left.put(varX, varY); - left.put(varZ, varY); - Unifier right = new Unifier(); - right.put(varX, constA); - Unifier merged = Unifier.mergeIntoLeft(left, right); - assertEquals(constA, merged.eval(varY)); - assertEquals(constA, merged.eval(varZ)); - } - - private BasicAtom parseAtom(String atom) { - ProgramParser programParser = new ProgramParserImpl(); - ASPCore2Program program = programParser.parse(atom + "."); - return (BasicAtom) program.getFacts().get(0); - } -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustifiedTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustifiedTest.java deleted file mode 100644 index 87097ecad..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustifiedTest.java +++ /dev/null @@ -1,215 +0,0 @@ -/** - * Copyright (c) 2018-2019, the Alpha Team. - * All rights reserved. - * - * Additional changes made by Siemens. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * 1) Redistributions of source code must retain the above copyright notice, this - * list of conditions and the following disclaimer. - * - * 2) Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE - * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR - * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER - * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, - * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ -package at.ac.tuwien.kr.alpha.core.grounder.structure; - -import static org.junit.jupiter.api.Assertions.assertFalse; -import static org.junit.jupiter.api.Assertions.assertNotEquals; - -import java.util.Arrays; -import java.util.Collections; -import java.util.Set; -import java.util.function.Function; - -import org.junit.jupiter.api.Test; - -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.programs.Predicate; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; -import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; -import at.ac.tuwien.kr.alpha.commons.Predicates; -import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.grounder.NaiveGrounder; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; -import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; -import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; -import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; -import at.ac.tuwien.kr.alpha.core.solver.TrailAssignment; - -/** - * Copyright (c) 2018-2020, the Alpha Team. - */ -public class AnalyzeUnjustifiedTest { - - private final ProgramParser parser = new ProgramParserImpl(); - private final NormalizeProgramTransformation normalize = new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - private final Function parseAndPreprocess = (str) -> { - return InternalProgram.fromNormalProgram(normalize.apply(parser.parse(str))); - }; - - @Test - public void justifySimpleRules() { - String program = "p(X) :- q(X)." + - "q(X) :- p(X)." + - "q(5) :- r." + - "r :- not nr." + - "nr :- not r." + - ":- not p(5)."; - CompiledProgram internalProgram = parseAndPreprocess.apply(program); - AtomStore atomStore = new AtomStoreImpl(); - NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true); - grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); - int rId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("r", 0))); - int nrId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("nr", 0))); - assignment.growForMaxAtomId(); - assignment.assign(rId, ThriceTruth.FALSE); - assignment.assign(nrId, ThriceTruth.TRUE); - BasicAtom p5 = Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Collections.singletonList(Terms.newConstant(5))); - assignment.assign(atomStore.get(p5), ThriceTruth.MBT); - Set reasons = grounder.justifyAtom(atomStore.get(p5), assignment); - assertFalse(reasons.isEmpty()); - } - - @Test - public void justifyLargerRules() { - String program = "p(X) :- q(X,Y), r(Y), not s(X,Y)." + - "{ q(1,X)} :- dom(X)." + - "dom(1..3)." + - "{r(X)} :- p(X)." + - "{r(2)}." + - "{s(1,2)}." + - ":- not p(1)."; - CompiledProgram internalProgram = parseAndPreprocess.apply(program); - AtomStore atomStore = new AtomStoreImpl(); - NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true); - grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); - Atom p1 = parser.parse("p(1).").getFacts().get(0); - Atom r2 = parser.parse("r(2).").getFacts().get(0); - Atom s12 = parser.parse("s(1,2).").getFacts().get(0); - Atom q11 = parser.parse("q(1,1).").getFacts().get(0); - Atom q12 = parser.parse("q(1,2).").getFacts().get(0); - Atom q13 = parser.parse("q(1,3).").getFacts().get(0); - int p1Id = atomStore.get(p1); - int r2Id = atomStore.get(r2); - int s12Id = atomStore.get(s12); - int q11Id = atomStore.get(q11); - int q12Id = atomStore.get(q12); - int q13Id = atomStore.get(q13); - assignment.growForMaxAtomId(); - assignment.assign(p1Id, ThriceTruth.MBT); - assignment.assign(r2Id, ThriceTruth.TRUE); - assignment.assign(s12Id, ThriceTruth.TRUE); - assignment.assign(q11Id, ThriceTruth.TRUE); - assignment.assign(q12Id, ThriceTruth.TRUE); - assignment.assign(q13Id, ThriceTruth.FALSE); - - Set reasons = grounder.justifyAtom(p1Id, assignment); - assertFalse(reasons.isEmpty()); - } - - @Test - public void justifyMultipleReasons() { - String program = "n(a). n(b). n(c). n(d). n(e)." + - "s(a,b). s(b,c). s(c,d). s(d,e)." + - "{ q(X) } :- n(X)." + - "p(X) :- q(X)." + - "p(X) :- p(Y), s(Y,X)." + - ":- not p(c)."; - CompiledProgram internalProgram = parseAndPreprocess.apply(program); - AtomStore atomStore = new AtomStoreImpl(); - NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true); - grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); - Atom qa = parser.parse("q(a).").getFacts().get(0); - Atom qb = parser.parse("q(b).").getFacts().get(0); - Atom qc = parser.parse("q(c).").getFacts().get(0); - Atom qd = parser.parse("q(d).").getFacts().get(0); - Atom qe = parser.parse("q(e).").getFacts().get(0); - int qaId = atomStore.get(qa); - int qbId = atomStore.get(qb); - int qcId = atomStore.get(qc); - int qdId = atomStore.get(qd); - int qeId = atomStore.get(qe); - - assignment.growForMaxAtomId(); - assignment.assign(qaId, ThriceTruth.FALSE); - assignment.assign(qbId, ThriceTruth.FALSE); - assignment.assign(qcId, ThriceTruth.FALSE); - assignment.assign(qdId, ThriceTruth.FALSE); - assignment.assign(qeId, ThriceTruth.FALSE); - - Predicate nq = Predicates.getPredicate("_nq", 2, true); - Atom nqa = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("a"))); - Atom nqb = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("b"))); - Atom nqc = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("c"))); - Atom nqd = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("d"))); - Atom nqe = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("e"))); - int nqaId = atomStore.get(nqa); - int nqbId = atomStore.get(nqb); - int nqcId = atomStore.get(nqc); - int nqdId = atomStore.get(nqd); - int nqeId = atomStore.get(nqe); - - assignment.growForMaxAtomId(); - assignment.assign(nqaId, ThriceTruth.TRUE); - assignment.assign(nqbId, ThriceTruth.TRUE); - assignment.assign(nqcId, ThriceTruth.TRUE); - assignment.assign(nqdId, ThriceTruth.TRUE); - assignment.assign(nqeId, ThriceTruth.TRUE); - - Atom pc = parser.parse("p(c).").getFacts().get(0); - Set reasons = grounder.justifyAtom(atomStore.get(pc), assignment); - assertFalse(reasons.isEmpty()); - } - - @Test - public void justifyNegatedFactsRemovedFromReasons() { - String program = "forbidden(2,9). forbidden(1,9)." + - "p(X) :- q(X)." + - "q(X) :- p(X)." + - "q(5) :- r." + - "r :- not nr, not forbidden(2,9), not forbidden(1,9)." + - "nr :- not r." + - ":- not p(5)."; - CompiledProgram internalProgram = parseAndPreprocess.apply(program); - AtomStore atomStore = new AtomStoreImpl(); - NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true); - grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); - int rId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("r", 0))); - int nrId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("nr", 0))); - assignment.growForMaxAtomId(); - assignment.assign(rId, ThriceTruth.FALSE); - assignment.assign(nrId, ThriceTruth.TRUE); - BasicAtom p5 = Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Collections.singletonList(Terms.newConstant(5))); - assignment.assign(atomStore.get(p5), ThriceTruth.MBT); - Set reasons = grounder.justifyAtom(atomStore.get(p5), assignment); - assertFalse(reasons.isEmpty()); - for (Literal literal : reasons) { - // Check that facts are not present in justification. - assertNotEquals(literal.getPredicate(), Predicates.getPredicate("forbidden", 2)); - } - } -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ProgramTransformationTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ProgramTransformationTest.java index f11692dcf..cbc92ed2c 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ProgramTransformationTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ProgramTransformationTest.java @@ -15,10 +15,11 @@ import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; import at.ac.tuwien.kr.alpha.api.programs.Program; import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; -import at.ac.tuwien.kr.alpha.core.externals.Externals; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.programs.NormalProgramImpl; +// TODO This is a functional test and should not be run with standard unit tests public class ProgramTransformationTest { private static final Logger LOGGER = LoggerFactory.getLogger(ProgramTransformationTest.class); @@ -87,4 +88,4 @@ public static boolean sayTrue(int val) { return true; } -} \ No newline at end of file +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationRegressionTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationRegressionTest.java index b2450e02f..3c492d095 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationRegressionTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationRegressionTest.java @@ -34,6 +34,7 @@ import at.ac.tuwien.kr.alpha.core.solver.SolverFactory; import at.ac.tuwien.kr.alpha.core.test.util.TestUtils; +// TODO This is a functional test and should not be run with standard unit tests public class StratifiedEvaluationRegressionTest { private static final Logger LOGGER = LoggerFactory.getLogger(StratifiedEvaluationRegressionTest.class); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationTest.java index 939bded78..ac7c30ec4 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluationTest.java @@ -50,11 +50,11 @@ import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; import at.ac.tuwien.kr.alpha.commons.substitutions.Instance; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.externals.Externals; import at.ac.tuwien.kr.alpha.core.grounder.Grounder; import at.ac.tuwien.kr.alpha.core.grounder.GrounderFactory; import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; @@ -65,6 +65,7 @@ import at.ac.tuwien.kr.alpha.core.solver.SolverFactory; import at.ac.tuwien.kr.alpha.core.test.util.TestUtils; +// TODO This is a functional test and should not be run with standard unit tests public class StratifiedEvaluationTest { private final ProgramParser parser = new ProgramParserImpl(); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingRuleAnalysisTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingRuleAnalysisTest.java deleted file mode 100644 index a37c217d3..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingRuleAnalysisTest.java +++ /dev/null @@ -1,207 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates; - -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertFalse; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import org.junit.jupiter.api.Test; - -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.literals.AggregateLiteral; -import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; -import at.ac.tuwien.kr.alpha.api.terms.ArithmeticOperator; -import at.ac.tuwien.kr.alpha.api.terms.Term; -import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; -import at.ac.tuwien.kr.alpha.commons.Predicates; -import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; -import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; -import at.ac.tuwien.kr.alpha.commons.literals.Literals; -import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.test.util.RuleParser; - -public class AggregateRewritingRuleAnalysisTest { - - //@formatter:off - private static final String BINDING_AGGREGATE_NO_GLOBALS = - "p(X) :- X = #max{N : q(N)}, X < 10, p(X, Y)."; - private static final String NONBINDING_AGGREGATE_NO_GLOBALS_1 = - "p(X) :- X < #max{N : q(N)}, X < 10, p(X, Y)."; - private static final String NONBINDING_AGGREGATE_NO_GLOBALS_2 = - "p(X) :- X < #max{N : q(N)}, X < 10, X = 3 + Y, Y = Z + 4, r(S, Z)."; - private static final String BINDING_AGGREGATES_NO_GLOBALS_INCLUDED = - "p :- not p(X), 3 < #max { Y : q(Y) }, X = #count { Y : q(Y) }."; - private static final String BINDING_AGGREGATE_WITH_GLOBALS_1 = - "graph_vertex_degree(G, V, D) :-" - + " graph(G)," - + " graph_vertex(G, V)," - + " D = #count{ VN : graph_edge(G, e(V, VN)); VN : graph_edge(G, e(VN, V)) }."; - private static final String BINDING_AGGREGATE_WITH_GLOBALS_2 = - "graph_max_degree_vertices(G, DMAX, N) :-" - + " graph(G)," - + " DMAX = #max{ DV : graph_vertex_degree(G, V, DV)}," - + " N = #count{ V : graph_vertex_degree(G, V, DMAX)}."; - //@formatter:on - - private static final AggregateRewritingRuleAnalysis analyze(String rule) { - return AggregateRewritingRuleAnalysis.analyzeRuleDependencies(RuleParser.parse(rule)); - } - - @Test - public void bindingAggregateNoGlobals() { - AggregateRewritingRuleAnalysis analysis = analyze(BINDING_AGGREGATE_NO_GLOBALS); - assertEquals(1, analysis.globalVariablesPerAggregate.size()); - assertEquals(1, analysis.dependenciesPerAggregate.size()); - - AggregateLiteral aggregate = new ArrayList<>(analysis.globalVariablesPerAggregate.keySet()).get(0); - assertTrue(analysis.globalVariablesPerAggregate.get(aggregate).isEmpty()); - assertEquals(0, analysis.dependenciesPerAggregate.get(aggregate).size()); - } - - @Test - public void nonBindingAggregateNoGlobals1() { - AggregateRewritingRuleAnalysis analysis = analyze(NONBINDING_AGGREGATE_NO_GLOBALS_1); - assertEquals(1, analysis.globalVariablesPerAggregate.size()); - assertEquals(1, analysis.dependenciesPerAggregate.size()); - - AggregateLiteral aggregate = new ArrayList<>(analysis.globalVariablesPerAggregate.keySet()).get(0); - assertTrue(analysis.globalVariablesPerAggregate.get(aggregate).isEmpty()); - assertFalse(analysis.dependenciesPerAggregate.get(aggregate).isEmpty()); - - Set dependencies = analysis.dependenciesPerAggregate.get(aggregate); - assertEquals(1, dependencies.size()); - - Literal pXY = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("p", 2), Terms.newVariable("X"), Terms.newVariable("Y")), true); - assertTrue(dependencies.contains(pXY)); - } - - @Test - public void nonBindingAggregateNoGlobals2() { - AggregateRewritingRuleAnalysis analysis = analyze(NONBINDING_AGGREGATE_NO_GLOBALS_2); - assertEquals(1, analysis.globalVariablesPerAggregate.size()); - assertEquals(1, analysis.dependenciesPerAggregate.size()); - - AggregateLiteral aggregate = new ArrayList<>(analysis.globalVariablesPerAggregate.keySet()).get(0); - assertTrue(analysis.globalVariablesPerAggregate.get(aggregate).isEmpty()); - assertFalse(analysis.dependenciesPerAggregate.get(aggregate).isEmpty()); - - Set dependencies = analysis.dependenciesPerAggregate.get(aggregate); - assertEquals(3, dependencies.size()); - - Literal threePlusY = Literals.fromAtom( - Atoms.newComparisonAtom(Terms.newVariable("X"), - Terms.newArithmeticTerm(Terms.newConstant(3), ArithmeticOperator.PLUS, Terms.newVariable("Y")), - ComparisonOperators.EQ), - true); - assertTrue(dependencies.contains(threePlusY)); - - Literal zPlusFour = Literals.fromAtom( - Atoms.newComparisonAtom(Terms.newVariable("Y"), - Terms.newArithmeticTerm(Terms.newVariable("Z"), ArithmeticOperator.PLUS, Terms.newConstant(4)), - ComparisonOperators.EQ), - true); - assertTrue(dependencies.contains(zPlusFour)); - - Literal rSZ = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("r", 2), Terms.newVariable("S"), Terms.newVariable("Z")), true); - assertTrue(dependencies.contains(rSZ)); - } - - @Test - public void bindingAggregateWithGlobals1() { - AggregateRewritingRuleAnalysis analysis = analyze(BINDING_AGGREGATE_WITH_GLOBALS_1); - assertEquals(1, analysis.globalVariablesPerAggregate.size()); - assertEquals(1, analysis.dependenciesPerAggregate.size()); - - AggregateLiteral aggregate = new ArrayList<>(analysis.globalVariablesPerAggregate.keySet()).get(0); - assertFalse(analysis.globalVariablesPerAggregate.get(aggregate).isEmpty()); - assertFalse(analysis.dependenciesPerAggregate.get(aggregate).isEmpty()); - - Set globalVars = analysis.globalVariablesPerAggregate.get(aggregate); - assertTrue(globalVars.contains(Terms.newVariable("G"))); - assertTrue(globalVars.contains(Terms.newVariable("V"))); - - Set dependencies = analysis.dependenciesPerAggregate.get(aggregate); - assertEquals(2, dependencies.size()); - - Literal graph = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("graph", 1), Terms.newVariable("G")), true); - assertTrue(dependencies.contains(graph)); - - Literal graphVertex = Literals.fromAtom( - Atoms.newBasicAtom(Predicates.getPredicate("graph_vertex", 2), Terms.newVariable("G"), Terms.newVariable("V")), true); - assertTrue(dependencies.contains(graphVertex)); - } - - @Test - public void bindingAggregateWithGlobals2() { - AggregateRewritingRuleAnalysis analysis = analyze(BINDING_AGGREGATE_WITH_GLOBALS_2); - assertEquals(2, analysis.globalVariablesPerAggregate.size()); - assertEquals(2, analysis.dependenciesPerAggregate.size()); - - // Verify correct analysis of max aggregate - List vertexDegreeTerms = Collections.singletonList(Terms.newVariable("DV")); - Literal vertexDegreeLiteral = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("graph_vertex_degree", 3), Terms.newVariable("G"), - Terms.newVariable("V"), Terms.newVariable("DV")), true); - List vertexDegreeLiterals = Collections.singletonList(vertexDegreeLiteral); - AggregateElement vertexDegree = Atoms.newAggregateElement(vertexDegreeTerms, vertexDegreeLiterals); - AggregateLiteral maxAggregate = Literals.fromAtom( - Atoms.newAggregateAtom(ComparisonOperators.EQ, Terms.newVariable("DMAX"), AggregateFunctionSymbol.MAX, - Collections.singletonList(vertexDegree)), - true); - assertTrue(analysis.globalVariablesPerAggregate.containsKey(maxAggregate)); - - Set maxAggrGlobalVars = analysis.globalVariablesPerAggregate.get(maxAggregate); - assertEquals(1, maxAggrGlobalVars.size()); - assertTrue(maxAggrGlobalVars.contains(Terms.newVariable("G"))); - - assertTrue(analysis.dependenciesPerAggregate.containsKey(maxAggregate)); - Set maxAggrDependencies = analysis.dependenciesPerAggregate.get(maxAggregate); - assertEquals(1, maxAggrDependencies.size()); - Literal graph = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("graph", 1), Terms.newVariable("G")), true); - assertTrue(maxAggrDependencies.contains(graph)); - - // Verify correct analysis of count aggregate - List maxVertexDegreeTerms = Collections.singletonList(Terms.newVariable("V")); - Literal maxVertexDegreeLiteral = Literals.fromAtom(Atoms.newBasicAtom(Predicates.getPredicate("graph_vertex_degree", 3), Terms.newVariable("G"), - Terms.newVariable("V"), Terms.newVariable("DMAX")), true); - List maxVertexDegreeLiterals = Collections.singletonList(maxVertexDegreeLiteral); - AggregateElement maxVertexDegree = Atoms.newAggregateElement(maxVertexDegreeTerms, maxVertexDegreeLiterals); - AggregateLiteral countAggregate = Literals.fromAtom( - Atoms.newAggregateAtom(ComparisonOperators.EQ, Terms.newVariable("N"), AggregateFunctionSymbol.COUNT, - Collections.singletonList(maxVertexDegree)), - true); - assertTrue(analysis.globalVariablesPerAggregate.containsKey(countAggregate)); - Set cntAggrGlobalVars = analysis.globalVariablesPerAggregate.get(countAggregate); - assertEquals(2, cntAggrGlobalVars.size()); - assertTrue(cntAggrGlobalVars.contains(Terms.newVariable("G"))); - assertTrue(cntAggrGlobalVars.contains(Terms.newVariable("DMAX"))); - - assertTrue(analysis.dependenciesPerAggregate.containsKey(countAggregate)); - Set cntAggrDependencies = analysis.dependenciesPerAggregate.get(countAggregate); - assertEquals(2, cntAggrDependencies.size()); - assertTrue(cntAggrDependencies.contains(graph)); - assertTrue(cntAggrDependencies.contains(maxAggregate)); - } - - @Test - public void bindingAggregateGlobalsNotIncluded() { - AggregateRewritingRuleAnalysis analysis = analyze(BINDING_AGGREGATES_NO_GLOBALS_INCLUDED); - assertEquals(2, analysis.globalVariablesPerAggregate.size()); - assertEquals(2, analysis.dependenciesPerAggregate.size()); - - // Check that the #max aggregate does not include "not p(X)" as its dependency. - for (Map.Entry> aggregateDependencies : analysis.dependenciesPerAggregate.entrySet()) { - if (aggregateDependencies.getKey().getAtom().getAggregateFunction() == AggregateFunctionSymbol.MAX) { - for (Literal dependency : aggregateDependencies.getValue()) { - assertFalse(dependency.isNegated()); - } - } - } - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingTest.java index d514d90bd..e7dc1543f 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingTest.java @@ -29,6 +29,7 @@ import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; import at.ac.tuwien.kr.alpha.core.solver.SolverFactory; +// TODO This is a functional test and should not be run with standard unit tests public class AggregateRewritingTest { private static final ProgramParser PARSER = new ProgramParserImpl(); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AggregatesTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AggregatesTest.java index 62542ba2d..d81c3e435 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AggregatesTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AggregatesTest.java @@ -34,6 +34,7 @@ /** * Tests if correct answer sets for programs containing aggregates are computed. */ +// TODO This is a functional test and should not be run with standard unit tests public class AggregatesTest { private static final String LS = System.lineSeparator(); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AntecedentTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AntecedentTest.java deleted file mode 100644 index a2cb52826..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AntecedentTest.java +++ /dev/null @@ -1,32 +0,0 @@ -package at.ac.tuwien.kr.alpha.core.solver; - -import java.util.HashSet; - -public class AntecedentTest { - - /** - * Tests whether two Antecedent objects have the same reason literals (irrespective of their order). - * Note that both Antecedents are assumed to contain no duplicate literals. - * @param l left Antecedent. - * @param r right Antecedent - * @return true iff both Antecedents contain the same literals. - */ - public static boolean antecedentsEquals(Antecedent l, Antecedent r) { - if (l == r) { - return true; - } - if (l != null && r != null && l.getReasonLiterals().length == r.getReasonLiterals().length) { - HashSet lSet = new HashSet<>(); - for (int literal : l.getReasonLiterals()) { - lSet.add(literal); - } - for (int literal : r.getReasonLiterals()) { - if (!lSet.contains(literal)) { - return false; - } - } - return true; - } - return false; - } -} \ No newline at end of file diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ArithmeticTermsTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ArithmeticTermsTest.java index b232ba659..4d2aab5af 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ArithmeticTermsTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ArithmeticTermsTest.java @@ -8,6 +8,7 @@ * * Copyright (c) 2020, the Alpha Team. */ +// TODO This is a functional test and should not be run with standard unit tests public class ArithmeticTermsTest { @RegressionTest diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounterTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounterTests.java index 7e2adb491..f43a858e8 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounterTests.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounterTests.java @@ -52,6 +52,7 @@ import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; import at.ac.tuwien.kr.alpha.core.rules.InternalRule; +// TODO should this be part of an AtomStoreTest?? public class AtomCounterTests { private AtomStore atomStore; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManagerTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManagerTests.java index 0df75abb2..692e6840a 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManagerTests.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManagerTests.java @@ -29,22 +29,23 @@ import static org.junit.jupiter.api.Assertions.assertTrue; import java.util.Collection; +import java.util.Collections; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; import at.ac.tuwien.kr.alpha.core.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.core.common.NoGood; import at.ac.tuwien.kr.alpha.core.grounder.Grounder; import at.ac.tuwien.kr.alpha.core.grounder.NaiveGrounder; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; +import at.ac.tuwien.kr.alpha.core.rules.InternalRule; public class ChoiceManagerTests { private Grounder grounder; @@ -53,11 +54,19 @@ public class ChoiceManagerTests { @BeforeEach public void setUp() { - String testProgram = "h :- b1, b2, not b3, not b4."; - ASPCore2Program parsedProgram = new ProgramParserImpl().parse(testProgram); - CompiledProgram internalProgram = InternalProgram.fromNormalProgram(new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG).apply(parsedProgram)); + /* + * program := + * h :- b1, b2, not b3, not b4. + */ + CompiledProgram program = new InternalProgram(Collections.singletonList( + new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("h", 0))), + Atoms.newBasicAtom(Predicates.getPredicate("b1", 0)).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("b2", 0)).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("b3", 0)).toLiteral(false), + Atoms.newBasicAtom(Predicates.getPredicate("b4", 0)).toLiteral(false)) + ), Collections.emptyList()); atomStore = new AtomStoreImpl(); - grounder = new NaiveGrounder(internalProgram, atomStore, true); + grounder = new NaiveGrounder(program, atomStore, true); WritableAssignment assignment = new TrailAssignment(atomStore); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment); choiceManager = new ChoiceManager(assignment, store); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/HanoiTowerTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/HanoiTowerTest.java index 9083e3e6c..18afe56dc 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/HanoiTowerTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/HanoiTowerTest.java @@ -53,6 +53,7 @@ * Tests {@link AbstractSolver} using some hanoi tower test cases (see https://en.wikipedia.org/wiki/Tower_of_Hanoi). * */ +// TODO This is a functional test and should not be run with standard unit tests public class HanoiTowerTest { @SuppressWarnings("unused") diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStoreTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStoreTest.java index b7f29a6ef..135cda060 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStoreTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStoreTest.java @@ -3,7 +3,6 @@ import static at.ac.tuwien.kr.alpha.core.common.NoGood.fact; import static at.ac.tuwien.kr.alpha.core.common.NoGood.headFirst; import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals; -import static at.ac.tuwien.kr.alpha.core.solver.AntecedentTest.antecedentsEquals; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.FALSE; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE; @@ -350,7 +349,7 @@ public void conflictingFact() { assignment.assign(1, FALSE); ConflictCause conflictCause = store.add(1, noGood); assertNotNull(conflictCause); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -360,7 +359,7 @@ public void conflictingBinary() { assignment.assign(1, TRUE); assignment.assign(2, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -371,7 +370,7 @@ public void conflictingNary() { assignment.assign(2, TRUE); assignment.assign(3, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -384,7 +383,7 @@ public void propagateViolatedConstraint() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -407,7 +406,7 @@ public void propagateViolatedConstraintHeadless() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -420,7 +419,7 @@ public void propagateViolatedConstraintHeadlessMbt() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoamingTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoamingTest.java index 7c86b69bf..3cca5a1af 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoamingTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoamingTest.java @@ -3,7 +3,6 @@ import static at.ac.tuwien.kr.alpha.core.common.NoGood.fact; import static at.ac.tuwien.kr.alpha.core.common.NoGood.headFirst; import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals; -import static at.ac.tuwien.kr.alpha.core.solver.AntecedentTest.antecedentsEquals; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.FALSE; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE; @@ -348,7 +347,7 @@ public void conflictingFact() { assignment.assign(1, FALSE); ConflictCause conflictCause = store.add(1, noGood); assertNotNull(conflictCause); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -357,7 +356,7 @@ public void conflictingBinary() { assignment.assign(1, TRUE); assignment.assign(2, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -367,7 +366,7 @@ public void conflictingNary() { assignment.assign(2, TRUE); assignment.assign(3, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -380,7 +379,7 @@ public void propagateViolatedConstraint() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -402,7 +401,7 @@ public void propagateViolatedConstraintHeadless() { ConflictCause conflictCause = store.propagate(); assertFalse(store.didPropagate()); assertNotNull(conflictCause); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -415,7 +414,7 @@ public void propagateViolatedConstraintHeadlessMbt() { ConflictCause conflictCause = store.propagate(); assertFalse(store.didPropagate()); assertNotNull(conflictCause); - assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); + assertTrue(TestUtils.antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/OmigaBenchmarksTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/OmigaBenchmarksTest.java index 4962ddc4c..2d5713e14 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/OmigaBenchmarksTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/OmigaBenchmarksTest.java @@ -42,6 +42,7 @@ * Tests {@link AbstractSolver} using Omiga benchmark problems. * */ +// TODO This is a functional test and should not be run with standard unit tests public class OmigaBenchmarksTest { @SuppressWarnings("unused") diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PartSubpartConfigurationTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PartSubpartConfigurationTest.java index f39a9434a..670195ea1 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PartSubpartConfigurationTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PartSubpartConfigurationTest.java @@ -40,6 +40,7 @@ * Tests {@link AbstractSolver} using some configuration test cases in which subparts are assigned to parts. * */ +// TODO This is a functional test and should not be run with standard unit tests public class PartSubpartConfigurationTest { private static final int DEBUG_TIMEOUT_FACTOR = 5; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PigeonHoleTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PigeonHoleTest.java index d444d5a7e..318452c64 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PigeonHoleTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/PigeonHoleTest.java @@ -42,6 +42,7 @@ /** * Tests {@link AbstractSolver} using some pigeon-hole test cases (see https://en.wikipedia.org/wiki/Pigeonhole_principle). */ +// TODO This is a functional test and should not be run with standard unit tests public class PigeonHoleTest { private static final long DEBUG_TIMEOUT_FACTOR = 5; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RacksTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RacksTest.java index 1ea2b88ca..4c9150ca0 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RacksTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RacksTest.java @@ -44,6 +44,7 @@ * Tests {@link AbstractSolver} using a racks configuration problem. * */ +// TODO This is a functional test and should not be run with standard unit tests @Disabled("disabled to save resources during CI") public class RacksTest { diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java index 1afed713b..c091c53e9 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java @@ -38,8 +38,9 @@ import at.ac.tuwien.kr.alpha.api.StatisticsReportingSolver; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.grounder.DummyGrounder; +import at.ac.tuwien.kr.alpha.core.grounder.GrounderMockWithBasicProgram; +// TODO This is a functional test and should not be run with standard unit tests public class SolverStatisticsTests { private AtomStore atomStore; @@ -65,14 +66,14 @@ public void checkStatsStringOneChoice(RegressionTestConfig cfg) { @RegressionTest public void checkNoGoodCounterStatsByTypeUsingDummyGrounder(RegressionTestConfig cfg) { - Solver solver = buildSolverForRegressionTest(atomStore, new DummyGrounder(atomStore), cfg); + Solver solver = buildSolverForRegressionTest(atomStore, new GrounderMockWithBasicProgram(atomStore), cfg); assumeTrue(solver instanceof StatisticsReportingSolver); collectAnswerSetsAndCheckNoGoodCounterStatsByType(solver, 4, 0, 0, 0); } @RegressionTest public void checkNoGoodCounterStatsByCardinalityUsingDummyGrounder(RegressionTestConfig cfg) { - Solver solver = buildSolverForRegressionTest(atomStore, new DummyGrounder(atomStore), cfg); + Solver solver = buildSolverForRegressionTest(atomStore, new GrounderMockWithBasicProgram(atomStore), cfg); assumeTrue(solver instanceof StatisticsReportingSolver); collectAnswerSetsAndCheckNoGoodCounterStatsByCardinality(solver, 2, 1, 1); } diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java index 911a2dd32..d7cf1ad99 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java @@ -53,12 +53,13 @@ import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.grounder.ChoiceGrounder; -import at.ac.tuwien.kr.alpha.core.grounder.DummyGrounder; +import at.ac.tuwien.kr.alpha.core.grounder.GrounderMockWithChoice; +import at.ac.tuwien.kr.alpha.core.grounder.GrounderMockWithBasicProgram; import at.ac.tuwien.kr.alpha.core.parser.InlineDirectivesImpl; import at.ac.tuwien.kr.alpha.core.programs.InputProgram; import at.ac.tuwien.kr.alpha.core.test.util.AnswerSetsParser; +// // TODO This is a functional test and should not be run with standard unit tests public class SolverTests { private static class Thingy implements Comparable { @@ -807,13 +808,13 @@ public void smallCardinalityAggregate(RegressionTestConfig cfg) { @RegressionTest public void dummyGrounder(RegressionTestConfig cfg) { AtomStore atomStore = new AtomStoreImpl(); - assertEquals(DummyGrounder.EXPECTED, buildSolverForRegressionTest(atomStore, new DummyGrounder(atomStore), cfg).collectSet()); + assertEquals(GrounderMockWithBasicProgram.EXPECTED, buildSolverForRegressionTest(atomStore, new GrounderMockWithBasicProgram(atomStore), cfg).collectSet()); } @RegressionTest public void choiceGrounder(RegressionTestConfig cfg) { AtomStore atomStore = new AtomStoreImpl(); - assertEquals(ChoiceGrounder.EXPECTED, buildSolverForRegressionTest(atomStore, new ChoiceGrounder(atomStore), cfg).collectSet()); + assertEquals(GrounderMockWithChoice.EXPECTED, buildSolverForRegressionTest(atomStore, new GrounderMockWithChoice(atomStore), cfg).collectSet()); } } diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TestableChoiceManager.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TestableChoiceManager.java deleted file mode 100644 index 50eaa2443..000000000 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TestableChoiceManager.java +++ /dev/null @@ -1,50 +0,0 @@ -/** - * Copyright (c) 2017-2018 Siemens AG - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * 1) Redistributions of source code must retain the above copyright notice, this - * list of conditions and the following disclaimer. - * - * 2) Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE - * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR - * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER - * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, - * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ -package at.ac.tuwien.kr.alpha.core.solver; - -import org.apache.commons.lang3.tuple.Pair; - -import java.util.Map; -import java.util.Set; - -/** - * This class is only here to make {@link ChoiceManager#addChoiceInformation(Pair)} public so that unit tests can access it. - * - * Copyright (c) 2017 Siemens AG - * - */ -public class TestableChoiceManager extends ChoiceManager { - - public TestableChoiceManager(WritableAssignment assignment, NoGoodStore store) { - super(assignment, store); - } - - @Override - public void addChoiceInformation(Pair, Map> choiceAtoms, Map> headsToBodies) { - super.addChoiceInformation(choiceAtoms, headsToBodies); - } - -} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringRandomGraphTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringRandomGraphTest.java index 2108b65db..424ce245d 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringRandomGraphTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringRandomGraphTest.java @@ -45,6 +45,7 @@ import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.programs.InputProgram; +// TODO This is a functional test and should not be run with standard unit tests public class ThreeColouringRandomGraphTest { private static final long DEBUG_TIMEOUT_FACTOR = 5; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringTestWithRandom.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringTestWithRandom.java index d53a0b82d..821499ce4 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringTestWithRandom.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringTestWithRandom.java @@ -55,6 +55,7 @@ * In Theory and Practice of Logic Programming, pp. 1-45. DOI: * 10.1017/S1471068416000569 */ +// TODO This is a functional test and should not be run with standard unit tests public class ThreeColouringTestWithRandom { private static final long DEBUG_TIMEOUT_FACTOR = 5; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringWheelTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringWheelTest.java index 48603e2e8..989f241f3 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringWheelTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/ThreeColouringWheelTest.java @@ -53,6 +53,7 @@ * In Theory and Practice of Logic Programming, pp. 1-45. * DOI: 10.1017/S1471068416000569 */ +// TODO This is a functional test and should not be run with standard unit tests public class ThreeColouringWheelTest { private static final long DEBUG_TIMEOUT_FACTOR = 5; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignmentTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignmentTest.java index 72100a72b..1c9265d3d 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignmentTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignmentTest.java @@ -27,18 +27,6 @@ */ package at.ac.tuwien.kr.alpha.core.solver; -import at.ac.tuwien.kr.alpha.core.common.Assignment; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.core.common.IntIterator; -import at.ac.tuwien.kr.alpha.core.test.util.TestUtils; -import org.junit.jupiter.api.BeforeEach; -import org.junit.jupiter.api.Test; - -import java.util.Arrays; -import java.util.Collections; -import java.util.HashSet; - import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.FALSE; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE; @@ -48,6 +36,19 @@ import static org.junit.jupiter.api.Assertions.assertNull; import static org.junit.jupiter.api.Assertions.assertThrows; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashSet; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import at.ac.tuwien.kr.alpha.core.common.Assignment; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; +import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.core.common.IntIterator; +import at.ac.tuwien.kr.alpha.core.test.util.TestUtils; + /** * Copyright (c) 2018-2020, the Alpha Team. */ diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeuristicTestAssumptions.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeuristicTestAssumptions.java index b5c7516e0..6102ee79f 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeuristicTestAssumptions.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeuristicTestAssumptions.java @@ -29,27 +29,30 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertTrue; +import java.util.Arrays; import java.util.Collection; -import java.util.function.Function; +import java.util.List; import java.util.function.Predicate; import java.util.stream.Collectors; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; -import at.ac.tuwien.kr.alpha.api.config.SystemConfig; -import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; +import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.core.common.NoGood; import at.ac.tuwien.kr.alpha.core.grounder.Grounder; import at.ac.tuwien.kr.alpha.core.grounder.NaiveGrounder; -import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; -import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; +import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; +import at.ac.tuwien.kr.alpha.core.rules.InternalRule; +import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.core.solver.NaiveNoGoodStore; -import at.ac.tuwien.kr.alpha.core.solver.TestableChoiceManager; import at.ac.tuwien.kr.alpha.core.solver.TrailAssignment; import at.ac.tuwien.kr.alpha.core.solver.WritableAssignment; @@ -63,30 +66,39 @@ */ public class AlphaHeuristicTestAssumptions { - private final ProgramParser parser = new ProgramParserImpl(); - private final NormalizeProgramTransformation normalizer = new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG); - private final Function parseAndPreprocess = (str) -> { - return InternalProgram.fromNormalProgram(normalizer.apply(parser.parse(str))); - }; - private Grounder grounder; private WritableAssignment assignment; - private TestableChoiceManager choiceManager; + private ChoiceManager choiceManager; private AtomStore atomStore; @BeforeEach public void setUp() { - String testProgram = "" - + "b1." - + "b2." - + "{b3}." - + "{b4}." - + "h :- b1, b2, not b3, not b4."; - CompiledProgram internalProgram = parseAndPreprocess.apply(testProgram); + /* program := + * b1. b2. + * b3 :- not nb3. + * nb3 :- not b3. + * b4 :- not nb4. + * nb4 :- not b4. + * h :- b1, b2, not b3, not b4. + */ + List facts = Arrays.asList(Atoms.newBasicAtom(Predicates.getPredicate("b1", 0)), Atoms.newBasicAtom(Predicates.getPredicate("b2", 0))); + List rules = Arrays.asList( + new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("b3", 0))), Atoms.newBasicAtom(Predicates.getPredicate("nb3", 0)).toLiteral(false)), + new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("nb3", 0))), Atoms.newBasicAtom(Predicates.getPredicate("b3", 0)).toLiteral(false)), + new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("b4", 0))), Atoms.newBasicAtom(Predicates.getPredicate("nb4", 0)).toLiteral(false)), + new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("nb4", 0))), Atoms.newBasicAtom(Predicates.getPredicate("b4", 0)).toLiteral(false)), + new InternalRule(Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("h", 0))), + Atoms.newBasicAtom(Predicates.getPredicate("b1", 0)).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("b2", 0)).toLiteral(), + Atoms.newBasicAtom(Predicates.getPredicate("b3", 0)).toLiteral(false), + Atoms.newBasicAtom(Predicates.getPredicate("b4", 0)).toLiteral(false)) + ); + CompiledProgram program = new InternalProgram(rules, facts); + atomStore = new AtomStoreImpl(); - grounder = new NaiveGrounder(internalProgram, atomStore, true); + grounder = new NaiveGrounder(program, atomStore, true); assignment = new TrailAssignment(atomStore); - choiceManager = new TestableChoiceManager(assignment, new NaiveNoGoodStore(assignment)); + choiceManager = new ChoiceManager(assignment, new NaiveNoGoodStore(assignment)); } @Test diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/learning/GroundConflictNoGoodLearnerTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/learning/GroundConflictNoGoodLearnerTest.java index b7ea7ef40..229f78755 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/learning/GroundConflictNoGoodLearnerTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/learning/GroundConflictNoGoodLearnerTest.java @@ -1,7 +1,6 @@ package at.ac.tuwien.kr.alpha.core.solver.learning; import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals; -import static at.ac.tuwien.kr.alpha.core.solver.AntecedentTest.antecedentsEquals; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertFalse; import static org.junit.jupiter.api.Assertions.assertNotNull; @@ -71,7 +70,7 @@ public void smallConflictNonTrivial1UIP() { assertNotNull(conflictCause); Antecedent violatedNoGood = conflictCause.getAntecedent(); assertNotNull(violatedNoGood); - assertTrue(antecedentsEquals(violatedNoGood, n5.asAntecedent()) || antecedentsEquals(violatedNoGood, n7.asAntecedent())); + assertTrue(TestUtils.antecedentsEquals(violatedNoGood, n5.asAntecedent()) || TestUtils.antecedentsEquals(violatedNoGood, n7.asAntecedent())); GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); NoGood learnedNoGood = analysisResult.learnedNoGood; assertEquals(new NoGood(fromOldLiterals(1, -8)), learnedNoGood); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java index 75cbc20df..d8d100065 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java @@ -9,13 +9,13 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; +import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; import java.util.Set; import java.util.StringJoiner; import java.util.stream.Collectors; -import org.apache.commons.lang3.StringUtils; import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.function.Executable; @@ -43,6 +43,7 @@ import at.ac.tuwien.kr.alpha.core.programs.InternalProgram; import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; import at.ac.tuwien.kr.alpha.core.programs.transformation.StratifiedEvaluation; +import at.ac.tuwien.kr.alpha.core.solver.Antecedent; import at.ac.tuwien.kr.alpha.core.solver.RegressionTestConfig; import at.ac.tuwien.kr.alpha.core.solver.SolverFactory; @@ -55,25 +56,30 @@ public static void fillAtomStore(AtomStore atomStore, int numberOfAtomsToFill) { } } - public static Atom atom(String predicateName, String... termStrings) { - Term[] terms = new Term[termStrings.length]; - for (int i = 0; i < termStrings.length; i++) { - String termString = termStrings[i]; - if (StringUtils.isAllUpperCase(termString.substring(0, 1))) { - terms[i] = Terms.newVariable(termString); - } else { - terms[i] = Terms.newConstant(termString); - } + /** + * Tests whether two Antecedent objects have the same reason literals (irrespective of their order). + * Note that both Antecedents are assumed to contain no duplicate literals. + * @param l left Antecedent. + * @param r right Antecedent + * @return true iff both Antecedents contain the same literals. + */ + public static boolean antecedentsEquals(Antecedent l, Antecedent r) { + if (l == r) { + return true; } - return Atoms.newBasicAtom(Predicates.getPredicate(predicateName, terms.length), terms); - } - - public static Atom atom(String predicateName, int... termInts) { - Term[] terms = new Term[termInts.length]; - for (int i = 0; i < termInts.length; i++) { - terms[i] = Terms.newConstant(termInts[i]); + if (l != null && r != null && l.getReasonLiterals().length == r.getReasonLiterals().length) { + HashSet lSet = new HashSet<>(); + for (int literal : l.getReasonLiterals()) { + lSet.add(literal); + } + for (int literal : r.getReasonLiterals()) { + if (!lSet.contains(literal)) { + return false; + } + } + return true; } - return Atoms.newBasicAtom(Predicates.getPredicate(predicateName, terms.length), terms); + return false; } public static void printNoGoods(AtomStore atomStore, Collection noGoods) { diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateLiteralSplittingTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateLiteralSplittingTest.java similarity index 95% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateLiteralSplittingTest.java rename to alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateLiteralSplittingTest.java index 4670282dd..f674121de 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateLiteralSplittingTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateLiteralSplittingTest.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates; +package at.ac.tuwien.kr.alpha.api.impl; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -9,8 +9,9 @@ import at.ac.tuwien.kr.alpha.api.rules.Rule; import at.ac.tuwien.kr.alpha.api.rules.heads.Head; -import at.ac.tuwien.kr.alpha.core.test.util.RuleParser; +import at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates.AggregateLiteralSplitting; +// TODO This is a functional test and should not be run with standard unit tests public class AggregateLiteralSplittingTest { //@formatter:off diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalizationTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateOperatorNormalizationTest.java similarity index 95% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalizationTest.java rename to alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateOperatorNormalizationTest.java index 0461e9eea..5813bd930 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalizationTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateOperatorNormalizationTest.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates; +package at.ac.tuwien.kr.alpha.api.impl; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNotNull; @@ -17,8 +17,9 @@ import at.ac.tuwien.kr.alpha.api.terms.Term; import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.test.util.RuleParser; +import at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates.AggregateOperatorNormalization; +// TODO This is a functional test and should not be run with standard unit tests public class AggregateOperatorNormalizationTest { //@formatter:off @@ -38,6 +39,7 @@ public class AggregateOperatorNormalizationTest { "bla :- dom(X), not X > #count{N : thing(N)}."; public static final String OPERATOR_NORMALIZATION_GE_NEG_ASP = "bla :- dom(X), not X >= #count{N : thing(N)}."; + /** * Operator normalization must also make sure that literals with only a right-hand term * are normalized to left-hand term only (and then operator-normalized if necessary) @@ -175,9 +177,7 @@ private static void assertAggregateBoundIncremented(Rule sourceRule, Rule< ArithmeticTerm incrementTerm = (ArithmeticTerm) comparisonRightHandTerm; assertEquals(ArithmeticOperator.PLUS, incrementTerm.getOperator()); assertEquals(Terms.newConstant(1), incrementTerm.getRightOperand()); - Term sourceBound = sourceAggregate.getAtom().getLowerBoundTerm() != null ? sourceAggregate.getAtom().getLowerBoundTerm() - : sourceAggregate.getAtom().getUpperBoundTerm(); - assertEquals(sourceBound, incrementTerm.getLeftOperand()); + assertEquals(sourceAggregate.getAtom().getLowerBoundTerm(), incrementTerm.getLeftOperand()); } } diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingContextTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateRewritingContextTest.java similarity index 96% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingContextTest.java rename to alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateRewritingContextTest.java index b5603a9cf..92b41c9d8 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateRewritingContextTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AggregateRewritingContextTest.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates; +package at.ac.tuwien.kr.alpha.api.impl; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -19,8 +19,10 @@ import at.ac.tuwien.kr.alpha.commons.comparisons.ComparisonOperators; import at.ac.tuwien.kr.alpha.commons.terms.Terms; import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; +import at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates.AggregateRewritingContext; import at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates.AggregateRewritingContext.AggregateInfo; +// TODO This is a functional test and should not be run with standard unit tests public class AggregateRewritingContextTest { //@formatter:off diff --git a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java index 176862d40..9eba7a24f 100644 --- a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java @@ -68,18 +68,19 @@ import at.ac.tuwien.kr.alpha.commons.AnswerSetBuilder; import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.externals.AspStandardLibrary; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; +import at.ac.tuwien.kr.alpha.commons.externals.MethodPredicateInterpretation; import at.ac.tuwien.kr.alpha.commons.literals.Literals; import at.ac.tuwien.kr.alpha.commons.rules.heads.Heads; import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.MethodPredicateInterpretation; -import at.ac.tuwien.kr.alpha.core.externals.AspStandardLibrary; -import at.ac.tuwien.kr.alpha.core.externals.Externals; import at.ac.tuwien.kr.alpha.core.parser.InlineDirectivesImpl; import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; import at.ac.tuwien.kr.alpha.core.programs.InputProgram; import at.ac.tuwien.kr.alpha.core.rules.BasicRule; +// TODO This is a functional test and should not be run with standard unit tests public class AlphaImplTest { private static final Logger LOGGER = LoggerFactory.getLogger(AspStandardLibrary.class); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewritingTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/ArithmeticTermsRewritingTest.java similarity index 93% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewritingTest.java rename to alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/ArithmeticTermsRewritingTest.java index 17ade9d66..8bc8d06b3 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewritingTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/ArithmeticTermsRewritingTest.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.programs.transformation; +package at.ac.tuwien.kr.alpha.api.impl; import static java.util.stream.Collectors.toList; import static org.junit.jupiter.api.Assertions.assertEquals; @@ -21,14 +21,16 @@ import at.ac.tuwien.kr.alpha.api.rules.NormalRule; import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.api.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.externals.Externals; import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl; import at.ac.tuwien.kr.alpha.core.programs.NormalProgramImpl; +import at.ac.tuwien.kr.alpha.core.programs.transformation.ArithmeticTermsRewriting; /** * Copyright (c) 2021, the Alpha Team. */ +// TODO This is a functional test and should not be run with standard unit tests public class ArithmeticTermsRewritingTest { private final Map externalsOfThisClass = Externals.scan(ArithmeticTermsRewritingTest.class); diff --git a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/FixedInterpretationLiteralsTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/FixedInterpretationLiteralsTest.java index 6d236e447..ef0a1a625 100644 --- a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/FixedInterpretationLiteralsTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/FixedInterpretationLiteralsTest.java @@ -22,10 +22,11 @@ import at.ac.tuwien.kr.alpha.api.terms.ConstantTerm; import at.ac.tuwien.kr.alpha.commons.Predicates; import at.ac.tuwien.kr.alpha.commons.atoms.Atoms; +import at.ac.tuwien.kr.alpha.commons.externals.AspStandardLibrary; +import at.ac.tuwien.kr.alpha.commons.externals.Externals; import at.ac.tuwien.kr.alpha.commons.terms.Terms; -import at.ac.tuwien.kr.alpha.core.externals.AspStandardLibrary; -import at.ac.tuwien.kr.alpha.core.externals.Externals; +// // TODO This is a functional test and should not be run with standard unit tests public class FixedInterpretationLiteralsTest { @at.ac.tuwien.kr.alpha.api.externals.Predicate diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/RuleParser.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/RuleParser.java similarity index 93% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/RuleParser.java rename to alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/RuleParser.java index 38da4d36d..0033015e6 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/RuleParser.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/RuleParser.java @@ -1,4 +1,4 @@ -package at.ac.tuwien.kr.alpha.core.test.util; +package at.ac.tuwien.kr.alpha.api.impl; import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; import at.ac.tuwien.kr.alpha.api.programs.ProgramParser; diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleToStringTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/RuleToStringTest.java similarity index 98% rename from alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleToStringTest.java rename to alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/RuleToStringTest.java index 38f8db22a..9cf689a0b 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/RuleToStringTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/RuleToStringTest.java @@ -23,7 +23,7 @@ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -package at.ac.tuwien.kr.alpha.core.grounder; +package at.ac.tuwien.kr.alpha.api.impl; import static org.junit.jupiter.api.Assertions.assertEquals;