From 558ceb2f64877fa2cc5f1cd448147e529b5c1c02 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 12 Aug 2020 15:17:18 +0200
Subject: [PATCH] Fix infinite loop in arith_ite_simp (#4805)

We have an open issue with an infinite loop with --ite-simp for a long time in #789 , for example on

(declare-fun a () Int)
(declare-fun b () Int)
(assert
    (and
        (= 1 (+ a b))
        (or (= 0 a) (= 0 b))
        (or (= 0 b) (>= b 8))
        (or (= 0 a) (not (>= b 8)))
    )
)
(check-sat)
The problem goes back to arith_ite_utils.cpp and roughly is as follows:
The method solveBinOr looks for patterns like (or (= b 0) (= b 1)). It introduces a new Boolean variable deor_1 and substitutes b -> (ite deor_1 1 0).
The method also stores another mapping in d_skolems: deor_1 -> (>= b 8) here which is also used in selectForCmp. However, these skolems are also used to add even more substitutions here after applying the already added substitutions to it. Eventually, we have a substitution deor_1 -> (>= (ite deor_1 1 0) 8) which inevitably leads to an infinite loop.
I have found no reason for the second mapping (deor_1 -> (>= b 8)) to be added as a substitution, and thus this PR removes it.

Benchmarks are running to check whether there are further issues with this, and whether this simplification is beneficial.

Fixes #789.
---
 src/theory/arith/arith_ite_utils.cpp | 11 -----------
 src/theory/arith/arith_ite_utils.h   |  2 --
 2 files changed, 13 deletions(-)

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 4892389f2..15fd7af6c 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -151,7 +151,6 @@ ArithIteUtils::ArithIteUtils(
       d_subcount(uc, 0),
       d_skolems(uc),
       d_implies(),
-      d_skolemsAdded(),
       d_orBinEqs()
 {
   d_subs = new SubstitutionMap(uc);
@@ -313,16 +312,7 @@ void ArithIteUtils::learnSubstitutions(const std::vector<Node>& assertions){
     d_orBinEqs.resize(writePos);
   }while(solvedSomething);
 
-  for(size_t i = 0, N=d_skolemsAdded.size(); i<N; ++i){
-    Node sk = d_skolemsAdded[i];
-    Node to = d_skolems[sk];
-    if(!to.isNull()){
-      Node fp = applySubstitutions(to);
-      addSubstitution(sk, fp);
-    }
-  }
   d_implies.clear();
-  d_skolemsAdded.clear();
   d_orBinEqs.clear();
 }
 
@@ -457,7 +447,6 @@ bool ArithIteUtils::solveBinOr(TNode binor){
         Node sk = nm->mkSkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);
         d_skolems.insert(sk, cnd);
-        d_skolemsAdded.push_back(sk);
         addSubstitution(sel, ite);
         return true;
       }
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index f86328d5d..d03b0795f 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -69,8 +69,6 @@ class ArithIteUtils {
   typedef std::map<Node, std::set<Node> > ImpMap;
   ImpMap d_implies;
 
-  std::vector<Node> d_skolemsAdded;
-
   std::vector<Node> d_orBinEqs;
 
 public:
-- 
2.30.2