Extend model construction with assignment exclusion set (#3377)

This extends the core model building algorithm in CVC4 with "assignment exclusion sets".  This functionality is useful for assigning values to terms of finite type that have specific restrictions on what their value cannot be.

In detail, previously, all unassigned terms of finite type were always assigned the first term in the type enumeration.  This is done since it is assumed that theories (e.g. datatypes) always do enough work to ensure that *arbitrary* values can be assigned to terms of finite type, and *fresh* values can be assigned to terms of infinite type. However, there are compelling cases (sets+cardinality for finite element types) where one may want to impose restrictions on what values can be assigned to terms of finite types.  Thus, we now provide `setAssignmentExclusionSet` as a way of communicating these restrictions. 

This commit also refactors a few parts of `TheoryEngineModelBuilder::buildModel` to be clearer, in particular by adding a few helper functions, and by caching certain information early in the function instead of recomputing it.

This is work towards #1123.

1 files changed, 330 insertions, 55 deletions

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 6df412ae3..11758f1e9 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -27,10 +27,100 @@ using namespace CVC4::context;
 namespace CVC4 {
 namespace theory {
 
+void TheoryEngineModelBuilder::Assigner::initialize(
+    TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
+{
+  d_te.reset(new TypeEnumerator(tn, tep));
+  d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end());
+}
+
+Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
+{
+  Assert(d_te != nullptr);
+  Node n;
+  bool success = false;
+  TypeEnumerator& te = *d_te;
+  // Check if we have run out of elements. This should never happen; if it
+  // does we assert false and return null.
+  if (te.isFinished())
+  {
+    Assert(false);
+    return Node::null();
+  }
+  // must increment until we find one that is not in the assignment
+  // exclusion set
+  do
+  {
+    n = *te;
+    success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n)
+              == d_assignExcSet.end();
+    // increment regardless of fail or succeed, to set up the next value
+    ++te;
+  } while (!success);
+  return n;
+}
+
 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
 {
 }
 
+Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
+{
+  eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
+  for (; !eqc_i.isFinished(); ++eqc_i)
+  {
+    Node n = *eqc_i;
+    Trace("model-builder-debug") << "Look at term : " << n << std::endl;
+    if (!isAssignable(n))
+    {
+      Trace("model-builder-debug") << "...try to normalize" << std::endl;
+      Node normalized = normalize(m, n, true);
+      if (normalized.isConst())
+      {
+        return normalized;
+      }
+    }
+  }
+  return Node::null();
+}
+
+bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
+{
+  if (a.d_isActive)
+  {
+    return true;
+  }
+  std::vector<Node>& eset = a.d_assignExcSet;
+  std::map<Node, Node>::iterator it;
+  for (unsigned i = 0, size = eset.size(); i < size; i++)
+  {
+    // Members of exclusion set must have values, otherwise we are not yet
+    // assignable.
+    Node er = eset[i];
+    if (er.isConst())
+    {
+      // already processed
+      continue;
+    }
+    // Assignable members of assignment exclusion set should be representatives
+    // of their equivalence classes. This ensures we look up the constant
+    // representatives for assignable members of assignment exclusion sets.
+    Assert(er == tm->getRepresentative(er));
+    it = d_constantReps.find(er);
+    if (it == d_constantReps.end())
+    {
+      Trace("model-build-aes")
+          << "isAssignerActive: not active due to " << er << std::endl;
+      return false;
+    }
+    // update
+    eset[i] = it->second;
+  }
+  Trace("model-build-aes") << "isAssignerActive: active!" << std::endl;
+  a.d_isActive = true;
+  return true;
+}
+
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
   if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
@@ -286,6 +376,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
 {
   Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
   TheoryModel* tm = (TheoryModel*)m;
+  eq::EqualityEngine* ee = tm->d_equalityEngine;
 
   // buildModel should only be called once per check
   Assert(!tm->isBuilt());
@@ -324,13 +415,12 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   // equality engine
   // Also, record #eqc per type (for finite model finding)
   std::map<TypeNode, unsigned> eqc_usort_count;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
   {
     NodeSet cache;
     for (; !eqcs_i.isFinished(); ++eqcs_i)
     {
-      eq::EqClassIterator eqc_i =
-          eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine);
+      eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), ee);
       for (; !eqc_i.isFinished(); ++eqc_i)
       {
         addAssignableSubterms(*eqc_i, tm, cache);
@@ -356,6 +446,13 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   d_constantReps.clear();
   std::map<Node, Node> assertedReps;
   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+  // Compute type enumerator properties. This code ensures we do not
+  // enumerate terms that have uninterpreted constants that violate the
+  // bounds imposed by finite model finding. For example, if finite
+  // model finding insists that there are only 2 values { U1, U2 } of type U,
+  // then the type enumerator for list of U should enumerate:
+  //   nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
+  // instead of enumerating (cons U3 nil).
   TypeEnumeratorProperties tep;
   if (options::finiteModelFind())
   {
@@ -370,6 +467,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     }
     typeConstSet.setTypeEnumeratorProperties(&tep);
   }
+
   // AJR: build ordered list of types that ensures that base types are
   // enumerated first.
   // (I think) this is only strictly necessary for finite model finding +
@@ -446,6 +544,20 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     }
   }
 
+  Trace("model-builder") << "Compute assignable information..." << std::endl;
+  // The set of equivalence classes that are "assignable"
+  std::unordered_set<Node, NodeHashFunction> assignableEqc;
+  // The set of equivalence classes that are "evaluable"
+  std::unordered_set<Node, NodeHashFunction> evaluableEqc;
+  // Assigner objects for relevant equivalence classes
+  std::map<Node, Assigner> eqcToAssigner;
+  // Maps equivalence classes to the equivalence class that maps to its assigner
+  // object in the above map.
+  std::map<Node, Node> eqcToAssignerMaster;
+  // Compute the above information
+  computeAssignableInfo(
+      tm, tep, assignableEqc, evaluableEqc, eqcToAssigner, eqcToAssignerMaster);
+
   // Need to ensure that each EC has a constant representative.
 
   Trace("model-builder") << "Processing EC's..." << std::endl;
@@ -484,56 +596,40 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
         {
           Trace("model-builder") << "  Eval phase, working on type: " << t
                                  << endl;
-          bool assignable, evaluable, evaluated;
+          bool evaluable;
           d_normalizedCache.clear();
           for (i = noRepSet->begin(); i != noRepSet->end();)
           {
             i2 = i;
             ++i;
-            assignable = false;
-            evaluable = false;
-            evaluated = false;
             Trace("model-builder-debug") << "Look at eqc : " << (*i2)
                                          << std::endl;
-            eq::EqClassIterator eqc_i =
-                eq::EqClassIterator(*i2, tm->d_equalityEngine);
-            for (; !eqc_i.isFinished(); ++eqc_i)
+            Node normalized;
+            // only possible to normalize if we are evaluable
+            evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
+            if (evaluable)
             {
-              Node n = *eqc_i;
-              Trace("model-builder-debug") << "Look at term : " << n
-                                           << std::endl;
-              if (isAssignable(n))
-              {
-                assignable = true;
-                Trace("model-builder-debug") << "...assignable" << std::endl;
-              }
-              else
-              {
-                evaluable = true;
-                Trace("model-builder-debug") << "...try to normalize"
-                                             << std::endl;
-                Node normalized = normalize(tm, n, true);
-                if (normalized.isConst())
-                {
-                  typeConstSet.add(tb, normalized);
-                  assignConstantRep(tm, *i2, normalized);
-                  Trace("model-builder") << "    Eval: Setting constant rep of "
-                                         << (*i2) << " to " << normalized
-                                         << endl;
-                  changed = true;
-                  evaluated = true;
-                  noRepSet->erase(i2);
-                  break;
-                }
-              }
+              normalized = evaluateEqc(tm, *i2);
             }
-            if (!evaluated)
+            if (!normalized.isNull())
+            {
+              Assert(normalized.isConst());
+              typeConstSet.add(tb, normalized);
+              assignConstantRep(tm, *i2, normalized);
+              Trace("model-builder") << "    Eval: Setting constant rep of "
+                                     << (*i2) << " to " << normalized << endl;
+              changed = true;
+              noRepSet->erase(i2);
+            }
+            else
             {
               if (evaluable)
               {
                 evaluableSet.insert(tb);
               }
-              if (assignable)
+              // If assignable, remember there is an equivalence class that is
+              // not assigned and assignable.
+              if (assignableEqc.find(*i2) != assignableEqc.end())
               {
                 unassignedAssignable = true;
               }
@@ -657,26 +753,34 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
       Trace("model-builder") << "  Assign phase, working on type: " << t
                              << endl;
       bool assignable, evaluable CVC4_UNUSED;
+      std::map<Node, Assigner>::iterator itAssigner;
+      std::map<Node, Node>::iterator itAssignerM;
       for (i = noRepSet.begin(); i != noRepSet.end();)
       {
         i2 = i;
         ++i;
-        eq::EqClassIterator eqc_i =
-            eq::EqClassIterator(*i2, tm->d_equalityEngine);
-        assignable = false;
-        evaluable = false;
-        for (; !eqc_i.isFinished(); ++eqc_i)
+        // check whether it has an assigner object
+        itAssignerM = eqcToAssignerMaster.find(*i2);
+        if (itAssignerM != eqcToAssignerMaster.end())
         {
-          Node n = *eqc_i;
-          if (isAssignable(n))
-          {
-            assignable = true;
-          }
-          else
-          {
-            evaluable = true;
-          }
+          // Take the master's assigner. Notice we don't care which order
+          // equivalence classes are assigned. For instance, the master can
+          // be assigned after one of its slaves.
+          itAssigner = eqcToAssigner.find(itAssignerM->second);
+        }
+        else
+        {
+          itAssigner = eqcToAssigner.find(*i2);
         }
+        if (itAssigner != eqcToAssigner.end())
+        {
+          assignable = isAssignerActive(tm, itAssigner->second);
+        }
+        else
+        {
+          assignable = assignableEqc.find(*i2) != assignableEqc.end();
+        }
+        evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
         Trace("model-builder-debug")
             << "    eqc " << *i2 << " is assignable=" << assignable
             << ", evaluable=" << evaluable << std::endl;
@@ -692,8 +796,18 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
           Assert(!t.isBoolean() || (*i2).isVar()
                  || (*i2).getKind() == kind::APPLY_UF);
           Node n;
-          if (!t.isFinite())
+          if (itAssigner != eqcToAssigner.end())
+          {
+            Trace("model-builder-debug")
+                << "Get value from assigner for finite type..." << std::endl;
+            // if it has an assigner, get the value from the assigner.
+            n = itAssigner->second.getNextAssignment();
+            Assert(!n.isNull());
+          }
+          else if (!t.isFinite())
           {
+            // if its infinite, we get a fresh value that does not occur in
+            // the model.
             bool success;
             do
             {
@@ -743,13 +857,17 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
               }
               //---
             } while (!success);
+            Assert(!n.isNull());
           }
           else
           {
+            Trace("model-builder-debug")
+                << "Get first value from finite type..." << std::endl;
+            // Otherwise, we get the first value from the type enumerator.
             TypeEnumerator te(t);
             n = *te;
           }
-          Assert(!n.isNull());
+          Trace("model-builder-debug") << "...got " << n << std::endl;
           assignConstantRep(tm, *i2, n);
           changed = true;
           noRepSet.erase(i2);
@@ -830,6 +948,163 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   tm->d_modelBuiltSuccess = true;
   return true;
 }
+void TheoryEngineModelBuilder::computeAssignableInfo(
+    TheoryModel* tm,
+    TypeEnumeratorProperties& tep,
+    std::unordered_set<Node, NodeHashFunction>& assignableEqc,
+    std::unordered_set<Node, NodeHashFunction>& evaluableEqc,
+    std::map<Node, Assigner>& eqcToAssigner,
+    std::map<Node, Node>& eqcToAssignerMaster)
+{
+  eq::EqualityEngine* ee = tm->d_equalityEngine;
+  bool computeAssigners = tm->hasAssignmentExclusionSets();
+  std::unordered_set<Node, NodeHashFunction> processed;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+  // A flag set to true if the current equivalence class is assignable (see
+  // assignableEqc).
+  bool assignable = false;
+  // Set to true if the current equivalence class is evaluatable (see
+  // evaluableEqc).
+  bool evaluable = false;
+  // Set to true if a term in the current equivalence class has been given an
+  // assignment exclusion set.
+  bool hasESet = false;
+  // Set to true if we found that a term in the current equivalence class has
+  // been given an assignment exclusion set, and we have not seen this term
+  // as part of a previous assignment exclusion group. In other words, when
+  // this flag is true we construct a new assigner object with the current
+  // equivalence class as its master.
+  bool foundESet = false;
+  // Look at all equivalence classes in the model
+  for (; !eqcs_i.isFinished(); ++eqcs_i)
+  {
+    Node eqc = *eqcs_i;
+    if (d_constantReps.find(eqc) != d_constantReps.end())
+    {
+      // already assigned above, skip
+      continue;
+    }
+    // reset information for the current equivalence classe
+    assignable = false;
+    evaluable = false;
+    hasESet = false;
+    foundESet = false;
+    // the assignment exclusion set for the current equivalence class
+    std::vector<Node> eset;
+    // the group to which this equivalence class belongs when exclusion sets
+    // were assigned (see the argument group of
+    // TheoryModel::getAssignmentExclusionSet).
+    std::vector<Node> group;
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+    // For each term in the current equivalence class, we update the above
+    // information. We may terminate this loop before looking at all terms if we
+    // have inferred the value of all of the information above.
+    for (; !eqc_i.isFinished(); ++eqc_i)
+    {
+      Node n = *eqc_i;
+      if (!isAssignable(n))
+      {
+        evaluable = true;
+        if (!computeAssigners)
+        {
+          if (assignable)
+          {
+            // both flags set, we are done
+            break;
+          }
+        }
+        // expressions that are not assignable should not be given assignment
+        // exclusion sets
+        Assert(!tm->getAssignmentExclusionSet(n, group, eset));
+        continue;
+      }
+      else
+      {
+        assignable = true;
+        if (!computeAssigners)
+        {
+          if (evaluable)
+          {
+            // both flags set, we are done
+            break;
+          }
+          // we don't compute assigners, skip
+          continue;
+        }
+      }
+      // process the assignment exclusion set for term n
+      // was it processed as a slave of a group?
+      if (processed.find(n) != processed.end())
+      {
+        // Should not have two assignment exclusion sets for the same
+        // equivalence class
+        Assert(!hasESet);
+        Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end());
+        // already processed as a slave term
+        hasESet = true;
+        continue;
+      }
+      // was it assigned one?
+      if (tm->getAssignmentExclusionSet(n, group, eset))
+      {
+        // Should not have two assignment exclusion sets for the same
+        // equivalence class
+        Assert(!hasESet);
+        foundESet = true;
+        hasESet = true;
+      }
+    }
+    if (assignable)
+    {
+      assignableEqc.insert(eqc);
+    }
+    if (evaluable)
+    {
+      evaluableEqc.insert(eqc);
+    }
+    // If we found an assignment exclusion set, we construct a new assigner
+    // object.
+    if (foundESet)
+    {
+      // we don't accept assignment exclusion sets for evaluable eqc
+      Assert(!evaluable);
+      // construct the assigner
+      Assigner& a = eqcToAssigner[eqc];
+      // Take the representatives of each term in the assignment exclusion
+      // set, which ensures we can look up their value in d_constReps later.
+      std::vector<Node> aes;
+      for (const Node& e : eset)
+      {
+        // Should only supply terms that occur in the model or constants
+        // in assignment exclusion sets.
+        Assert(tm->hasTerm(e) || e.isConst());
+        Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e;
+        aes.push_back(er);
+      }
+      // initialize
+      a.initialize(eqc.getType(), &tep, aes);
+      // all others in the group are slaves of this
+      for (const Node& g : group)
+      {
+        Assert(isAssignable(g));
+        if (!tm->hasTerm(g))
+        {
+          // Ignore those that aren't in the model, in the case the user
+          // has supplied an assignment exclusion set to a variable not in
+          // the model.
+          continue;
+        }
+        Node gr = tm->getRepresentative(g);
+        if (gr != eqc)
+        {
+          eqcToAssignerMaster[gr] = eqc;
+          // remember that this term has been processed
+          processed.insert(g);
+        }
+      }
+    }
+  }
+}
 
 void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
 {