Fix bool lets

Kernel/Signature.hpp

@@ -693,18 +693,18 @@ class Signature
   /** Return the function symbol by its number */
   inline Symbol* getFunction(unsigned n)
   {
-    ASS_REP(n < _funs.length(),n);
+    ASS_L(n, _funs.length());
     return _funs[n];
   } // getFunction
   /** Return the predicate symbol by its number */
   inline Symbol* getPredicate(unsigned n)
   {
-    ASS(n < _preds.length());
+    ASS_L(n, _preds.length());
     return _preds[n];
   } // getPredicate
   inline Symbol* getTypeCon(unsigned n)
   {
-    ASS(n < _typeCons.length());
+    ASS_L(n, _typeCons.length());
     return _typeCons[n];
   }
 

Kernel/Theory.cpp

@@ -1053,7 +1053,8 @@ unsigned Theory::Tuples::getConstructor(unsigned arity)
 
 bool Theory::Tuples::isConstructor(Term* t)
 {
-  return !t->isSpecial() && !t->isSort() && getConstructor(t->numTypeArguments()) == t->functor();
+  return !t->isSpecial() && !t->isSort() && SortHelper::getResultSort(t).isTupleSort()
+    && getConstructor(t->numTypeArguments()) == t->functor();
 }
 
 unsigned Theory::Tuples::getProjectionFunctor(unsigned arity, unsigned proj)

Parse/SMTLIB2.cpp

@@ -1499,8 +1499,20 @@ void SMTLIB2::parseLetEnd(LExpr* exp)
     }
 
     auto varList = vars.list();
-    auto args = TermStack::fromIterator(iterTraits(varList->iter()).map(unsignedToVarFn));
-    auto binder = Formula::createDefinition(Term::create(exprT->functor(), args), SubstHelper::apply(boundExpr,subst), varList);
+    TermStack args;
+    if (varList) {
+      args.loadFromIterator(iterTraits(varList->iter()).map(unsignedToVarFn));
+    }
+    Term* lhs;
+    if (exprSort == AtomicSort::boolSort()) {
+      // This solution is ugly, but either := has to be special or we have
+      // to wrap this as a formula to preserve the term-formula boundary.
+      lhs = Term::createFormula(new AtomicFormula(Literal::create(exprT->functor(), args.size(), true, args.begin())));
+    } else {
+      lhs = Term::create(exprT->functor(), args);
+    }
+
+    auto binder = Formula::createDefinition(lhs, SubstHelper::apply(boundExpr,subst), varList);
     let = TermList(Term::createLet(binder, let, letSort));
   }
 

Shell/FOOLElimination.cpp

@@ -620,9 +620,17 @@ void FOOLElimination::process(Term* term, Context context, TermList& termResult,
         auto vars = VList::append(bodyFreeVars, argumentVars);
         collectSorts(vars, typeVars, termVars, allVars, termVarSorts);
 
+        // this is ugly, but otherwise := would have to be special
+        if (bindingLhs->isBoolean()) {
+          ASS(bindingLhs->isFormula());
+          auto inner = bindingLhs->getSpecialData()->getFormula();
+          ASS_EQ(inner->connective(), Connective::LITERAL);
+          bindingLhs = inner->literal();
+        }
+
         // take the defined function symbol and its result sort
         unsigned symbol = bindingLhs->functor();
-        TermList bindingSort = SortHelper::getResultSort(bindingLhs);
+        TermList bindingSort = bindingLhs->isLiteral() ? AtomicSort::boolSort() : SortHelper::getResultSort(bindingLhs);
 
         SortHelper::normaliseSort(typeVars, bindingSort);
 

Shell/NewCNF.cpp

@@ -763,18 +763,15 @@ TermList NewCNF::nameLetBinding(Term* bindingLhs, TermList bindingRhs, TermList
 
   bool isPredicate = bindingLhs->isBoolean();
   // the symbol that we name must be in the form of a literal
-  if (isPredicate && !bindingLhs->isLiteral()) {
+  if (isPredicate) {
     ASS(bindingLhs->isFormula());
     auto inner = bindingLhs->getSpecialData()->getFormula();
     ASS_EQ(inner->connective(), Connective::LITERAL);
     bindingLhs = inner->literal();
   }
 
   unsigned nameArity = VList::length(bindingBoundVars) + bindingFreeVars.size();
-  TermList nameSort;
-  if (!isPredicate) {
-    nameSort = SortHelper::getResultSort(bindingLhs);
-  }
+  TermList nameSort = isPredicate ? AtomicSort::boolSort() : SortHelper::getResultSort(bindingLhs);
 
   unsigned freshSymbol = bindingLhs->functor();
 

Shell/SymbolOccurrenceReplacement.cpp

@@ -78,8 +78,6 @@ Formula* SymbolOccurrenceReplacement::process(Formula* formula) {
     case LITERAL: {
       Literal* literal = formula->literal();
 
-      Literal* processedLiteral;
-
       if (_isPredicate && (literal->functor() == _oldApplication->functor())) {
         Substitution substitution;
         for (unsigned i = 0; i < literal->arity(); i++) {

Shell/SymbolOccurrenceReplacement.hpp

@@ -31,10 +31,11 @@ class SymbolOccurrenceReplacement {
      * freshApplication = g(A1, ..., Am, B1, ..., Bj,X1, ..., Xn, Y1, ..., Yk)
      */
     SymbolOccurrenceReplacement(Term* oldApplication, Term* freshApplication)
-      : _isPredicate(oldApplication->isBoolean()),
+      : _isPredicate(oldApplication->isLiteral()),
         _oldApplication(oldApplication),
         _freshApplication(freshApplication)
     {
+      ASS(!oldApplication->isSpecial());
         // The implementation of this class doesn't requite argVars to be
         // non-empty, however, its use case expects this constraint
         //ASS(argVars || !env.signature->getFunction(symbol)->introduced());