Commit 9cce6bfb authored by Tomáš Fiedor's avatar Tomáš Fiedor
Browse files

Fix issue with wrongly sorted join units

parent db340e04

ta/containers/Path.cpp

+43 −0
Original line number Diff line number Diff line
@@ -6,10 +6,53 @@ 
#include <algorithm>

#include <cstring>

#include <iostream>

#include <memory>

#include "Path.h"





namespace Termination {

    JoinPath::JoinPath(PathPtr &lhs, PathPtr &rhs, bool is_core) {

        this->_type = PathType::PATH_JOIN;



        if(!is_core) {

            // Collect all of the atoms/concats for lhs and rhs

            std::vector<PathPtr> worklist{lhs, rhs};

            std::vector<PathPtr> units;



            while(!worklist.empty()) {

                PathPtr item = worklist.back();

                worklist.pop_back();



                if(item->_type == PATH_JOIN) {

                    JoinPtr join_item = std::static_pointer_cast<JoinPath>(item);

                    worklist.push_back(join_item->left);

                    worklist.push_back(join_item->right);

                } else {

                    units.push_back(item);

                }

            }



            std::sort(units.begin(), units.end(), [](PathPtr llhs, PathPtr rrhs) {

                return llhs->ToString() < rrhs->ToString();

            });



            assert(units.size() >= 2);

            while(units.size() != 2) {

                PathPtr right = units.back();

                units.pop_back();

                PathPtr left = units.back();

                units.pop_back();

                JoinPtr joined = std::make_shared<JoinPath>(left, right, true);

                units.push_back(joined);

            }

            this->right = units.back();

            units.pop_back();

            this->left = units.back();

        } else {

            this->left = lhs;

            this->right = rhs;

        }

    }

    // <<< Static members >>>



    PathPtr Path::JoinPaths(PathPtr& lhs, PathPtr& rhs) {

ta/containers/Path.h

+3 −1
Original line number Diff line number Diff line
@@ -94,7 +94,7 @@ namespace Termination { 
        PathPtr left;

        PathPtr right;



        JoinPath(PathPtr& lhs, PathPtr& rhs) : Path(PATH_JOIN), left((lhs)), right((rhs)) {}

        JoinPath(PathPtr& lhs, PathPtr& rhs, bool is_core = false);

        std::string ToString() const;

        std::string ToVar() const;

        bool Contains(PathPtr&, PathType) const;
@@ -104,6 +104,8 @@ namespace Termination { 
        PathList GenerateJoinFree();

    };



    using JoinPtr = std::shared_ptr<JoinPath>;



    class EmptyPath : public Path {

    protected:

        bool _IsSubsumedCore(Path&);