<commit_before>package fape.core.planning.search.flaws.flaws;

import fape.core.planning.planner.APlanner;
import fape.core.planning.preprocessing.ActionSupporterFinder;
import fape.core.planning.preprocessing.TaskDecompositions;
import fape.core.planning.search.flaws.resolvers.Resolver;
import fape.core.planning.search.flaws.resolvers.SupportingAction;
import fape.core.planning.search.flaws.resolvers.SupportingTaskDecomposition;
import fape.core.planning.search.flaws.resolvers.SupportingTimeline;
import fape.core.planning.states.State;
import fape.core.planning.timelines.ChainComponent;
import fape.core.planning.timelines.Timeline;
import planstack.anml.model.LVarRef;
import planstack.anml.model.ParameterizedStateVariable;
import planstack.anml.model.abs.AbstractAction;
import planstack.anml.model.abs.statements.AbstractAssignment;
import planstack.anml.model.abs.statements.AbstractLogStatement;
import planstack.anml.model.abs.statements.AbstractTransition;
import planstack.anml.model.concrete.TPRef;
import planstack.anml.model.concrete.Task;
import planstack.anml.model.concrete.statements.LogStatement;

import java.util.*;

public class UnsupportedTimeline extends Flaw {

    public final Timeline consumer;

    public UnsupportedTimeline(Timeline tdb) {
        this.consumer = tdb;
    }

    @Override
    public String toString() {
        return "Unsupported: " + consumer;
    }

    /**
     * Returns true if the first time-point *must* occur *exactly* one time unit before the second one.
     */
    private boolean areNecessarilyGlued(State st, TPRef first, TPRef second) {
        return !st.csp.stn().isConstraintPossible(first, second, 0)
                && !st.csp.stn().isConstraintPossible(second, first, -2);
    }

    /**
     * Returns true if the two state variables are necessarily identical.
     * This is true if they are on the same state variable and all their arguments are equals.
     */
    private boolean areNecessarilyIdentical(State st, ParameterizedStateVariable sv1, ParameterizedStateVariable sv2) {
        if(sv1.func() != sv2.func())
            return false;
        for(int i=0 ; i<sv1.args().length ; i++) {
            if(st.separable(sv1.arg(i), sv2.arg(i)))
                return false;
        }
        return true;
    }

    /** Returns true if the nth change in potentialSupporter (n = changeNumber) can support the consumer timeline */
    public static boolean isSupporting(Timeline potentialSupporter, int changeNumber, Timeline consumer, State st) {
        if(consumer == potentialSupporter)
            return false; //TODO: this should not be necessary to avoid the assertion since they should be temporally distinct

        if(!st.unifiable(potentialSupporter, consumer))
            return false;

        // if the consumer contains changes, the only possible support is the last change of the supporter
        if(!consumer.hasSinglePersistence() && changeNumber != potentialSupporter.numChanges()-1)
            return false;

        final ChainComponent supportingCC = potentialSupporter.getChangeNumber(changeNumber);
        if(!st.unifiable(supportingCC.getSupportValue(), consumer.getGlobalConsumeValue()))
            return false;

        if(!st.canAllBeBefore(supportingCC.getSupportTimePoint(), consumer.getFirstTimePoints()))
            return false;

        // if the supporter is not the last change, check that we can fit the consuming db before the next change
        if(changeNumber < potentialSupporter.numChanges()-1) {
            final ChainComponent afterCC = potentialSupporter.getChangeNumber(changeNumber+1);
            if(!st.canAllBeBefore(consumer.getLastTimePoints(), afterCC.getConsumeTimePoint()))
                return false;
        }

        assert potentialSupporter != consumer;

        return true;
    }

    @Override
    public List<Resolver> getResolvers(State st, APlanner planner) {
        if(resolvers != null)
            return resolvers;

        resolvers = new LinkedList<>();

        //here we need to find several types of supporters
        //1) chain parts that provide the value we need
        //2) actions that provide the value we need and can be added
        //3) tasks that can decompose into an action we need

        resolvers.addAll(st.getTimelineSupportersFor(consumer));

        // checks all the given resolvers to check if one must be applied.
        // this is true iff the supporter is non separable from the consumer:
        //    they are necessarily on the same state variable and they cannot be temporally separated.
        // If such a resolver if found, it means that no other resolver is applicable and only this one is returned.
        for(Resolver res : resolvers) {
            SupportingTimeline sdb = (SupportingTimeline) res;
            ChainComponent supportingCC = st.getTimeline(sdb.supporterID).getChangeNumber(sdb.supportingComponent);
            ChainComponent consumingCC = st.getTimeline(sdb.consumerID).getChainComponent(0);

            for(LogStatement sup : supportingCC.statements) {
                for(LogStatement cons : consumingCC.statements) {
                    if(areNecessarilyGlued(st, sup.end(), cons.start()) && areNecessarilyIdentical(st, sup.sv(), cons.sv())) {
                        resolvers.clear();
                        resolvers.add(res);
                        return resolvers;
                    }
                }
            }
        }

        if(planner.options.checkUnsolvableThreatsForOpenGoalsResolvers) {
            // here we check to see if some resolvers are not valid because resulting in unsolvable threats
            List<Resolver> toRemove = new LinkedList<>();
            for (Resolver res : resolvers) {
                Timeline supporter = st.getTimeline(((SupportingTimeline) res).supporterID);
                for (Timeline other : st.getTimelines()) {
                    if (other != consumer && other != supporter)
                        if (!other.hasSinglePersistence() && (st.unified(other, supporter) || st.unified(other, consumer))) {
                            // other is on the same state variable and chages the value of the state variable
                            // if it must be between the two, it will result in an unsolvable threat
                            // hence it must can be after the end of the consumer or before the start of the
                            if (!st.canAllBeBefore(consumer.getLastTimePoints(), other.getFirstChangeTimePoint())
                                    && !st.canAllBeBefore(other.getSupportTimePoint(), supporter.getFirstTimePoints())) {
                                // will result in unsolvable threat
                                toRemove.add(res);
                            }
                        }
                }
            }
            resolvers.removeAll(toRemove);
        }

        // adding actions
        // ... the idea is to decompose actions as long as they provide some support that I need, if they cant, I start adding actions
        //find actions that help me with achieving my value through some decomposition in the task netAbstractActionwork
        //they are those that I can find in the virtual decomposition tree
        //first get the action names from the abstract dtgs
        ActionSupporterFinder supporters = planner.getActionSupporterFinder();
        TaskDecompositions decompositions = new TaskDecompositions(st.pb);

        // a list of (abstract-action, decompositionID) of supporters
        Collection<fape.core.planning.preprocessing.SupportingAction> potentialSupporters = supporters.getActionsSupporting(st, consumer);

        // all actions that have an effect on the state variable
        Set<AbstractAction> potentiallySupportingAction = new HashSet<>();
        for(fape.core.planning.preprocessing.SupportingAction sa : potentialSupporters)
            potentiallySupportingAction.add(sa.absAct);

        // look for task decomposition that might produce a desired action in the future
        if(planner.isTopDownOnly()) {
            for (Task t : st.getOpenTasks()) {
                Collection<AbstractAction> decs = decompositions.possibleMethodsToDeriveTargetActions(t, potentiallySupportingAction);
                for (AbstractAction dec : decs) {
                    resolvers.add(new SupportingTaskDecomposition(t, dec, consumer));
                }
            }
        }

        //now we can look for adding the actions ad-hoc ...
        if (APlanner.actionResolvers) {
            for (fape.core.planning.preprocessing.SupportingAction aa : potentialSupporters) {
                if (planner.isTopDownOnly() && aa.absAct.mustBeMotivated())
                    continue;
                if(!st.isAddable(aa.absAct))
                    continue;

                // if the supporting variable is defined already (typically a constant) check if it is unifiable with our consumer
                AbstractLogStatement supporter = aa.absAct.getLogStatement(aa.statementRef);
                assert supporter.id().equals(aa.statementRef);
                LVarRef supportingCar = supporter.effectValue();
                if(aa.absAct.context().hasGlobalVar(supportingCar) &&
                        !st.unifiable(aa.absAct.context().getGlobalVar(supportingCar), consumer.getGlobalConsumeValue()))
                    continue;

                resolvers.add(new SupportingAction(aa.absAct, aa.statementRef, consumer));
            }
        }

        // make sure all resolvers validate the constraints built by previous resolvers.
        if(planner.isTopDownOnly()) {<commit_msg>[planning] add a more involved check to see if state variables are unifiable when looking for an action supporter<commit_after>package fape.core.planning.search.flaws.flaws;

import fape.core.planning.planner.APlanner;
import fape.core.planning.preprocessing.ActionSupporterFinder;
import fape.core.planning.preprocessing.TaskDecompositions;
import fape.core.planning.search.flaws.resolvers.Resolver;
import fape.core.planning.search.flaws.resolvers.SupportingAction;
import fape.core.planning.search.flaws.resolvers.SupportingTaskDecomposition;
import fape.core.planning.search.flaws.resolvers.SupportingTimeline;
import fape.core.planning.states.Printer;
import fape.core.planning.states.State;
import fape.core.planning.timelines.ChainComponent;
import fape.core.planning.timelines.Timeline;
import planstack.anml.model.LVarRef;
import planstack.anml.model.ParameterizedStateVariable;
import planstack.anml.model.abs.AbstractAction;
import planstack.anml.model.abs.statements.AbstractAssignment;
import planstack.anml.model.abs.statements.AbstractLogStatement;
import planstack.anml.model.abs.statements.AbstractTransition;
import planstack.anml.model.concrete.TPRef;
import planstack.anml.model.concrete.Task;
import planstack.anml.model.concrete.statements.LogStatement;

import java.util.*;

public class UnsupportedTimeline extends Flaw {

    public final Timeline consumer;

    public UnsupportedTimeline(Timeline tdb) {
        this.consumer = tdb;
    }

    @Override
    public String toString() {
        return "Unsupported: " + consumer;
    }

    /**
     * Returns true if the first time-point *must* occur *exactly* one time unit before the second one.
     */
    private boolean areNecessarilyGlued(State st, TPRef first, TPRef second) {
        return !st.csp.stn().isConstraintPossible(first, second, 0)
                && !st.csp.stn().isConstraintPossible(second, first, -2);
    }

    /**
     * Returns true if the two state variables are necessarily identical.
     * This is true if they are on the same state variable and all their arguments are equals.
     */
    private boolean areNecessarilyIdentical(State st, ParameterizedStateVariable sv1, ParameterizedStateVariable sv2) {
        if(sv1.func() != sv2.func())
            return false;
        for(int i=0 ; i<sv1.args().length ; i++) {
            if(st.separable(sv1.arg(i), sv2.arg(i)))
                return false;
        }
        return true;
    }

    /** Returns true if the nth change in potentialSupporter (n = changeNumber) can support the consumer timeline */
    public static boolean isSupporting(Timeline potentialSupporter, int changeNumber, Timeline consumer, State st) {
        if(consumer == potentialSupporter)
            return false; //TODO: this should not be necessary to avoid the assertion since they should be temporally distinct

        if(!st.unifiable(potentialSupporter, consumer))
            return false;

        // if the consumer contains changes, the only possible support is the last change of the supporter
        if(!consumer.hasSinglePersistence() && changeNumber != potentialSupporter.numChanges()-1)
            return false;

        final ChainComponent supportingCC = potentialSupporter.getChangeNumber(changeNumber);
        if(!st.unifiable(supportingCC.getSupportValue(), consumer.getGlobalConsumeValue()))
            return false;

        if(!st.canAllBeBefore(supportingCC.getSupportTimePoint(), consumer.getFirstTimePoints()))
            return false;

        // if the supporter is not the last change, check that we can fit the consuming db before the next change
        if(changeNumber < potentialSupporter.numChanges()-1) {
            final ChainComponent afterCC = potentialSupporter.getChangeNumber(changeNumber+1);
            if(!st.canAllBeBefore(consumer.getLastTimePoints(), afterCC.getConsumeTimePoint()))
                return false;
        }

        assert potentialSupporter != consumer;

        return true;
    }

    @Override
    public List<Resolver> getResolvers(State st, APlanner planner) {
        if(resolvers != null)
            return resolvers;

        resolvers = new LinkedList<>();

        //here we need to find several types of supporters
        //1) chain parts that provide the value we need
        //2) actions that provide the value we need and can be added
        //3) tasks that can decompose into an action we need

        resolvers.addAll(st.getTimelineSupportersFor(consumer));

        // checks all the given resolvers to check if one must be applied.
        // this is true iff the supporter is non separable from the consumer:
        //    they are necessarily on the same state variable and they cannot be temporally separated.
        // If such a resolver if found, it means that no other resolver is applicable and only this one is returned.
        for(Resolver res : resolvers) {
            SupportingTimeline sdb = (SupportingTimeline) res;
            ChainComponent supportingCC = st.getTimeline(sdb.supporterID).getChangeNumber(sdb.supportingComponent);
            ChainComponent consumingCC = st.getTimeline(sdb.consumerID).getChainComponent(0);

            for(LogStatement sup : supportingCC.statements) {
                for(LogStatement cons : consumingCC.statements) {
                    if(areNecessarilyGlued(st, sup.end(), cons.start()) && areNecessarilyIdentical(st, sup.sv(), cons.sv())) {
                        resolvers.clear();
                        resolvers.add(res);
                        return resolvers;
                    }
                }
            }
        }

        if(planner.options.checkUnsolvableThreatsForOpenGoalsResolvers) {
            // here we check to see if some resolvers are not valid because resulting in unsolvable threats
            List<Resolver> toRemove = new LinkedList<>();
            for (Resolver res : resolvers) {
                Timeline supporter = st.getTimeline(((SupportingTimeline) res).supporterID);
                for (Timeline other : st.getTimelines()) {
                    if (other != consumer && other != supporter)
                        if (!other.hasSinglePersistence() && (st.unified(other, supporter) || st.unified(other, consumer))) {
                            // other is on the same state variable and chages the value of the state variable
                            // if it must be between the two, it will result in an unsolvable threat
                            // hence it must can be after the end of the consumer or before the start of the
                            if (!st.canAllBeBefore(consumer.getLastTimePoints(), other.getFirstChangeTimePoint())
                                    && !st.canAllBeBefore(other.getSupportTimePoint(), supporter.getFirstTimePoints())) {
                                // will result in unsolvable threat
                                toRemove.add(res);
                            }
                        }
                }
            }
            resolvers.removeAll(toRemove);
        }

        // adding actions
        // ... the idea is to decompose actions as long as they provide some support that I need, if they cant, I start adding actions
        //find actions that help me with achieving my value through some decomposition in the task netAbstractActionwork
        //they are those that I can find in the virtual decomposition tree
        //first get the action names from the abstract dtgs
        ActionSupporterFinder supporters = planner.getActionSupporterFinder();
        TaskDecompositions decompositions = new TaskDecompositions(st.pb);

        // a list of (abstract-action, decompositionID) of supporters
        Collection<fape.core.planning.preprocessing.SupportingAction> potentialSupporters = supporters.getActionsSupporting(st, consumer);

        // all actions that have an effect on the state variable
        Set<AbstractAction> potentiallySupportingAction = new HashSet<>();
        for(fape.core.planning.preprocessing.SupportingAction sa : potentialSupporters)
            potentiallySupportingAction.add(sa.absAct);

        // look for task decomposition that might produce a desired action in the future
        if(planner.isTopDownOnly()) {
            for (Task t : st.getOpenTasks()) {
                Collection<AbstractAction> decs = decompositions.possibleMethodsToDeriveTargetActions(t, potentiallySupportingAction);
                for (AbstractAction dec : decs) {
                    resolvers.add(new SupportingTaskDecomposition(t, dec, consumer));
                }
            }
        }

        //now we can look for adding the actions ad-hoc ...
        if (APlanner.actionResolvers) {
            for (fape.core.planning.preprocessing.SupportingAction aa : potentialSupporters) {
                if (planner.isTopDownOnly() && aa.absAct.mustBeMotivated())
                    continue;
                if(!st.isAddable(aa.absAct))
                    continue;

                // if the supporting variable is defined already (typically a constant) check if it is unifiable with our consumer
                AbstractLogStatement supporter = aa.absAct.getLogStatement(aa.statementRef);
                assert supporter.id().equals(aa.statementRef);
                LVarRef supportingCar = supporter.effectValue();
                if(aa.absAct.context().hasGlobalVar(supportingCar) &&
                        !st.unifiable(aa.absAct.context().getGlobalVar(supportingCar), consumer.getGlobalConsumeValue()))
                    continue;

                boolean areStateVariablesUnifiable = true;
                for(int i=0 ; i<supporter.sv().args().size() ; i++) {
                    if(aa.absAct.context().hasGlobalVar(supporter.sv().jArgs().get(i)) &&
                            !st.unifiable(
                                    aa.absAct.context().getGlobalVar(supporter.sv().jArgs().get(i)),
                                    consumer.stateVariable.arg(i)))
                        areStateVariablesUnifiable = false;
                }

                if(areStateVariablesUnifiable)
                    resolvers.add(new SupportingAction(aa.absAct, aa.statementRef, consumer));
            }
        }

        // make sure all resolvers validate the constraints built by previous resolvers.
        if(planner.isTopDownOnly()) {
{'fraction_non_alphanumeric': 0.08380278179370856, 'fraction_numerical': 0.0017448526845804876, 'mean_word_length': 2.4284737651683472, 'pattern_counts': {'":': 0, '<': 24, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5940050', 'n_tokens_mistral': 5250, 'n_tokens_neox': 4967, 'n_words': 1436}