Limit duplicate propagating instances to avoid exponential behavior in QuantConflictFind.

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 93cd4be91c6cf620adcc1ca07824b20738e058e3..ec93b96fc3a620009168a4ee180347d21027ece7 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2069,7 +2069,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       }
                     }else{
                       Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
-                      //Assert( false );
+                      //this should only happen if the algorithm generates the same propagating instance twice this round
+                      //in this case, break to avoid exponential behavior
+                      break;
                     }
                   }
                   //clean up assigned
@@ -2082,6 +2084,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                 Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
               }
             }
+            Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
             if( d_conflict ){
               break;
             }

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index c10ba944b21af874d817e3da872bed9c98b1cce4..b0340d630899b4750248770f95f4809b1952faf7 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -305,6 +305,10 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
       }
       childrenChanged = childrenChanged || c!=body[i];
     }
+    //if( body.getKind()==ITE && isLiteral( body[0] ) ){
+    //  ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), 
+    //                                               NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) );
+    //}
     if( childrenChanged ){
       return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
     }else{

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index e8000eff14d3893a797efcc54b5a7210c841a13b..f0c9b5a33acd155a9b7488bbaa2733e03b345202 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -75,7 +75,8 @@ TESTS =       \
        subtype-param-unk.smt2 \
        subtype-param.smt2 \
        anti-sk-simp.smt2 \
-       pure_dt_cbqi.smt2
+       pure_dt_cbqi.smt2 \
+       florian-case-ax.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine

diff --git a/test/regress/regress0/quantifiers/florian-case-ax.smt2 b/test/regress/regress0/quantifiers/florian-case-ax.smt2
new file mode 100644 (file)
index 0000000..35ebb28
--- /dev/null
+++ b/test/regress/regress0/quantifiers/florian-case-ax.smt2
@@ -0,0 +1,168 @@
+(set-logic AUFLIA)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun A (U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U U U
+  U U
+  U) (Array Int U))
+
+(assert
+  (forall ((v_184 U) (v_185 U)
+  (v_186 U) (v_187 U)
+  (v_188 U) (v_189 U)
+  (v_190 U) (v_191 U)
+  (v_192 U) (v_193 U)
+  (v_194 U) (v_195 U)
+  (v_196 U) (v_197 U)
+  (v_198 U) (v_199 U)
+  (v_200 U) (v_201 U)
+  (v_202 U) (v_203 U)
+  (v_204 U) (v_205 U)
+  (v_206 U) (v_207 U)
+  (v_208 U) (v_209 U)
+  (v_210 U) (v_211 U)
+  (v_212 U) (v_213 U)
+  (v_214 U) (v_215 U)
+  (v_216 U) (v_217 U)
+  (v_218 U) (v_219 U)
+  (v_220 U) (v_221 U)
+  (v_222 U) (v_223 U)
+  (v_224 U) (v_225 U)
+  (v_226 U) (v_227 U)
+  (v_228 U) (v_229 U)
+  (v_230 U) (v_231 U)
+  (v_232 U) (v_233 U)
+  (v_234 U) (v_235 U)
+  (v_236 U) (v_237 U)
+  (v_238 U) (v_239 U)
+  (v_240 U) (v_241 U) (v_242 Int))
+  (let ((v_183 (A v_184 v_185 v_186 v_187
+                    v_188 v_189 v_190 v_191 v_192
+                    v_193 v_194 v_195 v_196 v_197
+                    v_198 v_199 v_200 v_201 v_202
+                    v_203 v_204 v_205 v_206 v_207
+                    v_208 v_209 v_210 v_211 v_212
+                    v_213 v_214 v_215 v_216 v_217
+                    v_218 v_219 v_220 v_221 v_222
+                    v_223 v_224 v_225 v_226 v_227
+                    v_228 v_229 v_230 v_231 v_232
+                    v_233 v_234 v_235 v_236 v_237
+                    v_238 v_239 v_240 v_241)))
+  (ite (= v_242 59) (= (select v_183 v_242) v_240)
+  (ite (= v_242 58) (= (select v_183 v_242) v_239)
+  (ite (= v_242 57) (= (select v_183 v_242) v_238)
+  (ite (= v_242 56) (= (select v_183 v_242) v_237)
+  (ite (= v_242 55) (= (select v_183 v_242) v_236)
+  (ite (= v_242 54) (= (select v_183 v_242) v_235)
+  (ite (= v_242 53) (= (select v_183 v_242) v_234)
+  (ite (= v_242 52) (= (select v_183 v_242) v_233)
+  (ite (= v_242 51) (= (select v_183 v_242) v_232)
+  (ite (= v_242 50) (= (select v_183 v_242) v_231)
+  (ite (= v_242 49) (= (select v_183 v_242) v_230)
+  (ite (= v_242 48) (= (select v_183 v_242) v_229)
+  (ite (= v_242 47) (= (select v_183 v_242) v_228)
+  (ite (= v_242 46) (= (select v_183 v_242) v_227)
+  (ite (= v_242 45) (= (select v_183 v_242) v_226)
+  (ite (= v_242 44) (= (select v_183 v_242) v_225)
+  (ite (= v_242 43) (= (select v_183 v_242) v_224)
+  (ite (= v_242 41) (= (select v_183 v_242) v_223)
+  (ite (= v_242 40) (= (select v_183 v_242) v_222)
+  (ite (= v_242 39) (= (select v_183 v_242) v_221)
+  (ite (= v_242 37) (= (select v_183 v_242) v_220)
+  (ite (= v_242 36) (= (select v_183 v_242) v_219)
+  (ite (= v_242 34) (= (select v_183 v_242) v_218)
+  (ite (= v_242 33) (= (select v_183 v_242) v_217)
+  (ite (= v_242 32) (= (select v_183 v_242) v_216)
+  (ite (= v_242 31) (= (select v_183 v_242) v_215)
+  (ite (= v_242 30) (= (select v_183 v_242) v_214)
+  (ite (= v_242 29) (= (select v_183 v_242) v_213)
+  (ite (= v_242 28) (= (select v_183 v_242) v_212)
+  (ite (= v_242 27) (= (select v_183 v_242) v_211)
+  (ite (= v_242 26) (= (select v_183 v_242) v_210)
+  (ite (= v_242 25) (= (select v_183 v_242) v_209)
+  (ite (= v_242 24) (= (select v_183 v_242) v_208)
+  (ite (= v_242 23) (= (select v_183 v_242) v_207)
+  (ite (= v_242 22) (= (select v_183 v_242) v_206)
+  (ite (= v_242 21) (= (select v_183 v_242) v_205)
+  (ite (= v_242 20) (= (select v_183 v_242) v_204)
+  (ite (= v_242 19) (= (select v_183 v_242) v_203)
+  (ite (= v_242 18) (= (select v_183 v_242) v_202)
+  (ite (= v_242 17) (= (select v_183 v_242) v_201)
+  (ite (= v_242 16) (= (select v_183 v_242) v_200)
+  (ite (= v_242 15) (= (select v_183 v_242) v_199)
+  (ite (= v_242 14) (= (select v_183 v_242) v_198)
+  (ite (= v_242 13) (= (select v_183 v_242) v_197)
+  (ite (= v_242 12) (= (select v_183 v_242) v_196)
+  (ite (= v_242 11) (= (select v_183 v_242) v_195)
+  (ite (= v_242 10) (= (select v_183 v_242) v_194)
+  (ite (= v_242 9) (= (select v_183 v_242) v_193)
+  (ite (= v_242 8) (= (select v_183 v_242) v_192)
+  (ite (= v_242 7) (= (select v_183 v_242) v_191)
+  (ite (= v_242 6) (= (select v_183 v_242) v_190)
+  (ite (= v_242 5) (= (select v_183 v_242) v_189)
+  (ite (= v_242 4) (= (select v_183 v_242) v_188)
+  (ite (= v_242 3) (= (select v_183 v_242) v_187)
+  (ite (= v_242 2) (= (select v_183 v_242) v_186)
+  (ite (= v_242 1) (= (select v_183 v_242) v_185)
+  (ite (= v_242 0) (= (select v_183 v_242) v_184)
+  (= (select v_183 v_242) v_241)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+  
+(declare-const c_184 U) (declare-const c_185 U)
+(declare-const c_186 U) (declare-const c_187 U)
+(declare-const c_188 U) (declare-const c_189 U)
+(declare-const c_190 U) (declare-const c_191 U)
+(declare-const c_192 U) (declare-const c_193 U)
+(declare-const c_194 U) (declare-const c_195 U)
+(declare-const c_196 U) (declare-const c_197 U)
+(declare-const c_198 U) (declare-const c_199 U)
+(declare-const c_200 U) (declare-const c_201 U)
+(declare-const c_202 U) (declare-const c_203 U)
+(declare-const c_204 U) (declare-const c_205 U)
+(declare-const c_206 U) (declare-const c_207 U)
+(declare-const c_208 U) (declare-const c_209 U)
+(declare-const c_210 U) (declare-const c_211 U)
+(declare-const c_212 U) (declare-const c_213 U)
+(declare-const c_214 U) (declare-const c_215 U)
+(declare-const c_216 U) (declare-const c_217 U)
+(declare-const c_218 U) (declare-const c_219 U)
+(declare-const c_220 U) (declare-const c_221 U)
+(declare-const c_222 U) (declare-const c_223 U)
+(declare-const c_224 U) (declare-const c_225 U)
+(declare-const c_226 U) (declare-const c_227 U)
+(declare-const c_228 U) (declare-const c_229 U)
+(declare-const c_230 U) (declare-const c_231 U)
+(declare-const c_232 U) (declare-const c_233 U)
+(declare-const c_234 U) (declare-const c_235 U)
+(declare-const c_236 U) (declare-const c_237 U)
+(declare-const c_238 U) (declare-const c_239 U)
+(declare-const c_240 U) (declare-const c_241 U)
+  
+(declare-fun b () Int)
+(declare-fun c () U)
+(assert (not (= (select (A c_184 c_185 c_186 c_187
+                          c_188 c_189 c_190 c_191 c_192
+                          c_193 c_194 c_195 c_196 c_197
+                          c_198 c_199 c_200 c_201 c_202
+                          c_203 c_204 c_205 c_206 c_207
+                          c_208 c_209 c_210 c_211 c_212
+                          c_213 c_214 c_215 c_216 c_217
+                          c_218 c_219 c_220 c_221 c_222
+                          c_223 c_224 c_225 c_226 c_227
+                          c_228 c_229 c_230 c_231 c_232
+                          c_233 c_234 c_235 c_236 c_237
+                          c_238 c_239 c_240 c_241) b) c)))
+(assert (and (= b 28) (= c c_212)))
+
+(check-sat)