From 7f98701cfb481786a96835d7770f8b1aa4f94882 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Mar 2020 14:45:13 -0500
Subject: [PATCH] Guard cases of sort inference in quantifier free logics in uf
 cardinality (#4074)

Fixes #4068 and fixes #4085 and fixes #4063.
---
 src/theory/uf/cardinality_extension.cpp       | 40 ++++++++++++++-----
 test/regress/CMakeLists.txt                   |  1 +
 .../regress/regress1/fmf/issue4068-si-qf.smt2 |  8 ++++
 3 files changed, 38 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress1/fmf/issue4068-si-qf.smt2

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 34952084b..908e788f8 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -737,13 +737,15 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
                                  << std::endl;
             Trace("uf-ss-si")  << "Must combine region" << std::endl;
             bool recheck = false;
-            if( options::sortInference()){
+            SortInference* si = d_thss->getSortInference();
+            if (si != nullptr)
+            {
               //If sort inference is enabled, search for regions with same sort.
               std::map< int, int > sortsFound;
               for( int i=0; i<(int)d_regions_index; i++ ){
                 if( d_regions[i]->valid() ){
                   Node op = d_regions[i]->frontKey();
-                  int sort_id = d_thss->getSortInference()->getSortId(op);
+                  int sort_id = si->getSortId(op);
                   if( sortsFound.find( sort_id )!=sortsFound.end() ){
                     Debug("fmf-full-check") << "Combined regions " << i << " " << sortsFound[sort_id] << std::endl;
                     combineRegions( sortsFound[sort_id], i );
@@ -1015,10 +1017,12 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
         AlwaysAssert(false);
       }
     }
-    if( options::sortInference()) {
+    SortInference* si = d_thss->getSortInference();
+    if (si != nullptr)
+    {
       for( int i=0; i<2; i++ ){
-        int si = d_thss->getSortInference()->getSortId( ss[i] );
-        Trace("uf-ss-split-si") << si << " ";
+        int sid = si->getSortId(ss[i]);
+        Trace("uf-ss-split-si") << sid << " ";
       }
       Trace("uf-ss-split-si")  << std::endl;
     }
@@ -1068,11 +1072,14 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out
 void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
   if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
     if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){
+      NodeManager* nm = NodeManager::currentNM();
       d_totality_lems[n].push_back( cardinality );
       Node cardLit = d_cardinality_literal[ cardinality ];
       int sort_id = 0;
-      if( options::sortInference() ){
-        sort_id = d_thss->getSortInference()->getSortId(n);
+      SortInference* si = d_thss->getSortInference();
+      if (si != nullptr)
+      {
+        sort_id = si->getSortId(n);
       }
       Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl;
       int use_cardinality = cardinality;
@@ -1106,7 +1113,7 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
       for( int i=0; i<use_cardinality; i++ ){
         eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
       }
-      Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
+      Node ax = eqs.size() == 1 ? eqs[0] : nm->mkNode(OR, eqs);
       Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
       Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
       //send as lemma to the output channel
@@ -1334,7 +1341,16 @@ CardinalityExtension::~CardinalityExtension()
 
 SortInference* CardinalityExtension::getSortInference()
 {
-  return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
+  if (!options::sortInference())
+  {
+    return nullptr;
+  }
+  QuantifiersEngine* qe = d_th->getQuantifiersEngine();
+  if (qe != nullptr)
+  {
+    return qe->getTheoryEngine()->getSortInference();
+  }
+  return nullptr;
 }
 
 /** get default sat context */
@@ -1467,8 +1483,10 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
             std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
             if( it==d_tn_mono_slave.end() ){
               bool isMonotonic;
-              if( d_th->getQuantifiersEngine() ){
-                isMonotonic = getSortInference()->isMonotonic( tn );
+              SortInference* si = getSortInference();
+              if (si != nullptr)
+              {
+                isMonotonic = si->isMonotonic(tn);
               }else{
                 //if ground, everything is monotonic
                 isMonotonic = true;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index be96ca70d..50ef63780 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1282,6 +1282,7 @@ set(regress_1_tests
   regress1/fmf/issue3615.smt2
   regress1/fmf/issue3626.smt2
   regress1/fmf/issue3689.smt2
+  regress1/fmf/issue4068-si-qf.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc
diff --git a/test/regress/regress1/fmf/issue4068-si-qf.smt2 b/test/regress/regress1/fmf/issue4068-si-qf.smt2
new file mode 100644
index 000000000..792977260
--- /dev/null
+++ b/test/regress/regress1/fmf/issue4068-si-qf.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --uf-ss-totality --fmf-fun --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic QF_UFNIA)
+(set-info :status sat)
+(declare-const i15 Int)
+(assert (= true true true (not (= i15 0))))
+(check-sat)
+(exit)
-- 
2.30.2