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().

1 files changed, 9 insertions, 10 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index a6751e1ec..c777f164f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -424,22 +424,21 @@ public:
   virtual void finishInit() { }
 
   /**
-   * Some theories have kinds that are effectively definitions and
-   * should be expanded before they are handled.  Definitions allow
-   * a much wider range of actions than the normal forms given by the
-   * rewriter; they can enable other theories and create new terms.
-   * However no assumptions can be made about subterms having been
-   * expanded or rewritten.  Where possible rewrite rules should be
-   * used, definitions should only be used when rewrites are not
-   * possible, for example in handling under-specified operations
-   * using partially defined functions.
+   * Some theories have kinds that are effectively definitions and should be
+   * expanded before they are handled.  Definitions allow a much wider range of
+   * actions than the normal forms given by the rewriter. However no
+   * assumptions can be made about subterms having been expanded or rewritten.
+   * Where possible rewrite rules should be used, definitions should only be
+   * used when rewrites are not possible, for example in handling
+   * under-specified operations using partially defined functions.
    *
    * Some theories like sets use expandDefinition as a "context
    * independent preRegisterTerm".  This is required for cases where
    * a theory wants to be notified about a term before preprocessing
    * and simplification but doesn't necessarily want to rewrite it.
    */
-  virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
+  virtual Node expandDefinition(Node node)
+  {
     // by default, do nothing
     return node;
   }