@@ -774,9 +774,6 @@ void ClauseTranslator::indexAggregatorBody(const ast::Aggregator& agg) {
774774}
775775
776776void ClauseTranslator::indexAggregators (const ast::Clause& clause) {
777- // Add each aggregator as an internal generator
778- visit (clause, [&](const ast::Aggregator& agg) { indexGenerator (agg); });
779-
780777 // Index aggregator bodies
781778 visit (clause, [&](const ast::Aggregator& agg) { indexAggregatorBody (agg); });
782779
@@ -791,13 +788,6 @@ void ClauseTranslator::indexAggregators(const ast::Clause& clause) {
791788}
792789
793790void ClauseTranslator::indexMultiResultFunctors (const ast::Clause& clause) {
794- // Add each multi-result functor as an internal generator
795- visit (clause, [&](const ast::IntrinsicFunctor& func) {
796- if (ast::analysis::FunctorAnalysis::isMultiResult (func)) {
797- indexGenerator (func);
798- }
799- });
800-
801791 // Add multi-result functor value introductions
802792 visit (clause, [&](const ast::BinaryConstraint& bc) {
803793 if (!isEqConstraint (bc.getBaseOperator ())) return ;
@@ -809,8 +799,94 @@ void ClauseTranslator::indexMultiResultFunctors(const ast::Clause& clause) {
809799 });
810800}
811801
802+ void ClauseTranslator::indexGenerators (const ast::Clause& clause) {
803+ // generators must be indexed in topological order according to
804+ // dependencies between them.
805+ // see issue #2416
806+
807+ std::map<std::string, const ast::Argument*> varGenerator;
808+
809+ visit (clause, [&](const ast::BinaryConstraint& bc) {
810+ if (!isEqConstraint (bc.getBaseOperator ())) return ;
811+ const auto * lhs = as<ast::Variable>(bc.getLHS ());
812+ const ast::Argument* rhs = as<ast::IntrinsicFunctor>(bc.getRHS ());
813+ if (rhs == nullptr ) {
814+ rhs = as<ast::Aggregator>(bc.getRHS ());
815+ } else {
816+ if (!ast::analysis::FunctorAnalysis::isMultiResult (*as<ast::IntrinsicFunctor>(rhs))) return ;
817+ }
818+ if (lhs == nullptr || rhs == nullptr ) return ;
819+ varGenerator[lhs->getName ()] = rhs;
820+ });
821+
822+ // all the generators in the clause
823+ std::vector<const ast::Argument*> generators;
824+
825+ // 'predecessor' mapping from a generator to the generators that must
826+ // evaluate before.
827+ std::multimap<const ast::Argument*, const ast::Argument*> dependencies;
828+
829+ // harvest generators and dependencies
830+ visit (clause, [&](const ast::Argument& arg) {
831+ if (const ast::IntrinsicFunctor* func = as<ast::IntrinsicFunctor>(arg)) {
832+ if (ast::analysis::FunctorAnalysis::isMultiResult (*func)) {
833+ generators.emplace_back (func);
834+ visit (func, [&](const ast::Variable& use) {
835+ if (varGenerator.count (use.getName ()) > 0 ) {
836+ dependencies.emplace (func, varGenerator.at (use.getName ()));
837+ }
838+ });
839+ }
840+ } else if (const ast::Aggregator* agg = as<ast::Aggregator>(arg)) {
841+ generators.emplace_back (agg);
842+ visit (agg, [&](const ast::Variable& use) {
843+ if (varGenerator.count (use.getName ()) > 0 ) {
844+ dependencies.emplace (agg, varGenerator.at (use.getName ()));
845+ }
846+ });
847+ }
848+ });
849+
850+ // the set of already indexed generators
851+ std::set<const ast::Argument*> indexed;
852+ // the recursion stack to detect a cycle in the depth-first traversal
853+ std::set<const ast::Argument*> recStack;
854+
855+ // recursive depth-first traversal, perform a post-order indexing of genertors.
856+ const std::function<void (const ast::Argument*)> dfs = [&](const ast::Argument* reached) {
857+ if (indexed.count (reached)) {
858+ return ;
859+ }
860+
861+ if (!recStack.emplace (reached).second ) {
862+ // cycle detected
863+ fatal (" cyclic dependency" );
864+ }
865+
866+ auto range = dependencies.equal_range (reached);
867+ for (auto it = range.first ; it != range.second ; ++it) {
868+ if (it->second == reached) {
869+ continue ; // ignore self-dependency
870+ }
871+ dfs (it->second );
872+ }
873+
874+ // index this generator
875+ indexGenerator (*reached);
876+
877+ indexed.insert (reached);
878+ recStack.erase (reached);
879+ };
880+
881+ // topological sorting by depth-first search
882+ for (const ast::Argument* root : generators) {
883+ dfs (root);
884+ }
885+ }
886+
812887void ClauseTranslator::indexClause (const ast::Clause& clause) {
813888 indexAtoms (clause);
889+ indexGenerators (clause);
814890 indexAggregators (clause);
815891 indexMultiResultFunctors (clause);
816892}
0 commit comments