Changes in src/ResolvExpr/ResolveAssertions.cc [d3b2c32a:99d4584]

File:

• src/ResolvExpr/ResolveAssertions.cc (modified) (4 diffs)

src/ResolvExpr/ResolveAssertions.cc

@@ -342 +342 @@
 
         /// Limit to depth of recursion of assertion satisfaction
-        static const int recursionLimit = 4;
-        /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
-        static const int deferLimit = 10;
+        static const int recursionLimit = /* 10 */ 4;
 
         void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out, std::list<std::string>& errors ) {
@@ -371 +369 @@
                                                 ss << tabs << "Unsatisfiable alternative:\n";
                                                 resn.alt.print( ss, ++tabs );
-                                                ss << (tabs-1) << "Could not satisfy assertion:\n";
-                                                assn.decl->print( ss, tabs );
+                                                ss << --tabs << "Could not satisfy assertion:\n";
+                                                assn.decl->print( ss, ++tabs );
                                                 
                                                 errors.emplace_back( ss.str() );
@@ -386 +384 @@
                                                 new_resns.emplace_back( std::move(resn), IterateState );
                                         }
-                                } else if ( resn.deferred.size() > deferLimit ) {
-                                        // too many deferred assertions to attempt mutual compatibility
-                                        Indenter tabs{ 3 };
-                                        std::ostringstream ss;
-                                        ss << tabs << "Unsatisfiable alternative:\n";
-                                        resn.alt.print( ss, ++tabs );
-                                        ss << (tabs-1) << "Too many non-unique satisfying assignments for "
-                                                "assertions:\n";
-                                        for ( const auto& d : resn.deferred ) {
-                                                d.decl->print( ss, tabs );
-                                        }
-
-                                        errors.emplace_back( ss.str() );
-                                        goto nextResn;
                                 } else {
                                         // resolve deferred assertions by mutual compatibility
@@ -411 +395 @@
                                                 ss << tabs << "Unsatisfiable alternative:\n";
                                                 resn.alt.print( ss, ++tabs );
-                                                ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
+                                                ss << --tabs << "No mutually-compatible satisfaction for assertions:\n";
+                                                ++tabs;
                                                 for ( const auto& d : resn.deferred ) {
                                                         d.decl->print( ss, tabs );