Perform theory widening eagerly (#4044)

Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one
(check-sat) call to another. In the reported issue, we start with QF_NIA
but then switch to QF_UFNIA because there is a div term (which has a UF in
its expanded form). Dealing with this issue is challenging in general. As a
result, we have decided not to allow theory widening in
Theory::expandDefinitions() anymore but instead to do it eagerly in
SmtEngine::setDefaults().

2 files changed, 3 insertions, 4 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 94fc1e34c..32791415e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -194,7 +194,8 @@ void TheoryBV::finishInit()
   tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
 }
 
-Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
+Node TheoryBV::expandDefinition(Node node)
+{
   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 
   switch (node.getKind()) {
@@ -221,7 +222,6 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
     Node divByZero = getBVDivByZero(node.getKind(), width);
     Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
     node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
-    logicRequest.widenLogic(THEORY_UF);
     return node;
   }
     break;
@@ -234,7 +234,6 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
   Unreachable();
 }
 
-
 void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index bc54a09e7..7f88d8388 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -79,7 +79,7 @@ public:
 
   void finishInit() override;
 
-  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+  Node expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode n) override;