Changeset d3b2c32a for src/ResolvExpr/ResolveAssertions.cc

Timestamp:

Jun 6, 2019, 3:39:10 PM (5 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

b7d92b96

Parents:

3cd5fdd

Message:

Add limit to number of recursive assertions tried at once

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 = /* 10 */ 4;
+        static const int recursionLimit = 4;
+        /// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
+        static const int deferLimit = 10;
 
         void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out, std::list<std::string>& errors ) {
@@ -369 +371 @@
                                                 ss << tabs << "Unsatisfiable alternative:\n";
                                                 resn.alt.print( ss, ++tabs );
-                                                ss << --tabs << "Could not satisfy assertion:\n";
-                                                assn.decl->print( ss, ++tabs );
+                                                ss << (tabs-1) << "Could not satisfy assertion:\n";
+                                                assn.decl->print( ss, tabs );
                                                 
                                                 errors.emplace_back( ss.str() );
@@ -384 +386 @@
                                                 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
@@ -395 +411 @@
                                                 ss << tabs << "Unsatisfiable alternative:\n";
                                                 resn.alt.print( ss, ++tabs );
-                                                ss << --tabs << "No mutually-compatible satisfaction for assertions:\n";
-                                                ++tabs;
+                                                ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
                                                 for ( const auto& d : resn.deferred ) {
                                                         d.decl->print( ss, tabs );