Fix term simplification based on entailment in quantifiers rewriter (#3746)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 74d8ac3a61aa5bf00400e96d3358330a79232880..e355952877b943a209a2cdc51a2389409d2672bb 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -416,23 +416,38 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
       }
     }
   }
+  else if (n.isConst())
+  {
+    return n.getConst<bool>() ? 1 : -1;
+  }
   return 0;
 }
 
 bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
+  if (n.isConst())
+  {
+    Trace("quantifiers-rewrite-term-debug")
+        << "constant cond : " << n << " -> " << pol << std::endl;
+    if (n.getConst<bool>() != pol)
+    {
+      conflict = true;
+    }
+    return false;
+  }
   std::map< Node, bool >::iterator it = currCond.find( n );
   if( it==currCond.end() ){
     Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl;
     new_cond.push_back( n );
     currCond[n] = pol;
     return true;
-  }else{
-    if( it->second!=pol ){
-      Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl;
-      conflict = true;
-    }
-    return false;
   }
+  else if (it->second != pol)
+  {
+    Trace("quantifiers-rewrite-term-debug")
+        << "CONFLICTING cond : " << n << " -> " << pol << std::endl;
+    conflict = true;
+  }
+  return false;
 }
 
 void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bac0b2615b15392aae40790b671c01473d587e4..aaabd2301387377866b9b1ffc07cbdc229304e34 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1450,6 +1450,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3537.smt2
   regress1/quantifiers/issue3628.smt2
   regress1/quantifiers/issue3664.smt2
+  regress1/quantifiers/issue3724-quant.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2

diff --git a/test/regress/regress1/quantifiers/issue3724-quant.smt2 b/test/regress/regress1/quantifiers/issue3724-quant.smt2
new file mode 100644 (file)
index 0000000..6dd874f
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3724-quant.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unknown
+(set-logic ALL)
+(assert
+(forall ((BOUND_VARIABLE_313 Bool) (BOUND_VARIABLE_314 (-> Int Bool)) (BOUND_VARIABLE_315 (-> Int Int)) (BOUND_VARIABLE_316 Int) (BOUND_VARIABLE_317 (-> Int Bool)) (BOUND_VARIABLE_318 Int)) (! (not (and (not (and (= (ite (and (not (= BOUND_VARIABLE_318 0)) (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))) (ite (BOUND_VARIABLE_317 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9))))))) BOUND_VARIABLE_316 0) 0) 0) (not (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))))) true)) :pattern (true)))
+)
+(check-sat)