alpha-asp / Alpha

A lazy-grounding Answer-Set Programming system
BSD 2-Clause "Simplified" License
58 stars 10 forks source link

Cannot reconstruct substitution with function terms correctly from body-representing atoms #352

Closed AntoniusW closed 1 year ago

AntoniusW commented 1 year ago

Body-representing atoms, i.e., RuleAtom-s, currently use strings to represent the substitution with which the non-ground rule was grounded with. The String-representation has always been ugly and in addition leads to a bug when the original Substitution is reconstructed and if the substitution contained function terms. The following test causes the bug on the master branch.

    @Test
    public void substitutionWithFunctionTermsObtainableFromRuleAtom() {
        Rule<Head> rule = PARSER.parse("q(X) :- p(X,Y).").getRules().get(0);
        CompiledRule nonGroundRule = InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(rule));
        // Build substitution X -> b(a,a), Y -> b(b(a,a),b(a,a)).
        BasicAtom atomForSpecialize = Atoms.newBasicAtom(Predicates.getPredicate("p", 2), X, Y);
        ConstantTerm<String> aTerm = Terms.newSymbolicConstant("a");
        Instance instanceForSpecialize = new Instance(Terms.newFunctionTerm("b", aTerm, aTerm),
            Terms.newFunctionTerm("b",
                Terms.newFunctionTerm("b", aTerm, aTerm),
                Terms.newFunctionTerm("b", aTerm, aTerm)));
        Substitution substitution = BasicSubstitution.specializeSubstitution(
            atomForSpecialize, instanceForSpecialize, BasicSubstitution.EMPTY_SUBSTITUTION);

        RuleAtom ruleAtom = new RuleAtom(nonGroundRule, substitution);
        String substitutionString = (String) ((ConstantTerm<?>) ruleAtom.getTerms().get(1)).getObject();
        Substitution fromString = Substitutions.fromString(substitutionString);
        assertEquals(substitution, fromString);
    }

Although the buggy code is in Substitutions.fromString(..) and could be fixed using a better parser, an even better solution seems to be getting rid of the String-representation itself and using instead of the String, a ConstantTerm<..> that directly refers to the Substitution object.