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, 66 insertions, 0 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index da66a2ef2..c6055ede9 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -74,6 +74,9 @@ void TheoryModel::reset(){
   d_approximations.clear();
   d_approx_list.clear();
   d_reps.clear();
+  d_assignExcSet.clear();
+  d_aesMaster.clear();
+  d_aesSlaves.clear();
   d_rep_set.clear();
   d_uf_terms.clear();
   d_ho_uf_terms.clear();
@@ -520,6 +523,69 @@ void TheoryModel::assertSkeleton(TNode n)
   d_reps[ n ] = n;
 }
 
+void TheoryModel::setAssignmentExclusionSet(TNode n,
+                                            const std::vector<Node>& eset)
+{
+  // should not be assigned yet
+  Assert(d_assignExcSet.find(n) == d_assignExcSet.end());
+  Trace("model-builder-debug")
+      << "Exclude values of " << n << " : " << eset << std::endl;
+  std::vector<Node>& aes = d_assignExcSet[n];
+  aes.insert(aes.end(), eset.begin(), eset.end());
+}
+
+void TheoryModel::setAssignmentExclusionSetGroup(
+    const std::vector<TNode>& group, const std::vector<Node>& eset)
+{
+  if (group.empty())
+  {
+    return;
+  }
+  // for efficiency, we store a single copy of eset and set a slave/master
+  // relationship
+  setAssignmentExclusionSet(group[0], eset);
+  std::vector<Node>& gslaves = d_aesSlaves[group[0]];
+  for (unsigned i = 1, gsize = group.size(); i < gsize; ++i)
+  {
+    Node gs = group[i];
+    // set master
+    d_aesMaster[gs] = group[0];
+    // add to slaves
+    gslaves.push_back(gs);
+  }
+}
+
+bool TheoryModel::getAssignmentExclusionSet(TNode n,
+                                            std::vector<Node>& group,
+                                            std::vector<Node>& eset)
+{
+  // does it have a master?
+  std::map<Node, Node>::iterator itm = d_aesMaster.find(n);
+  if (itm != d_aesMaster.end())
+  {
+    return getAssignmentExclusionSet(itm->second, group, eset);
+  }
+  std::map<Node, std::vector<Node> >::iterator ita = d_assignExcSet.find(n);
+  if (ita == d_assignExcSet.end())
+  {
+    return false;
+  }
+  eset.insert(eset.end(), ita->second.begin(), ita->second.end());
+  group.push_back(n);
+  // does it have slaves?
+  ita = d_aesSlaves.find(n);
+  if (ita != d_aesSlaves.end())
+  {
+    group.insert(group.end(), ita->second.begin(), ita->second.end());
+  }
+  return true;
+}
+
+bool TheoryModel::hasAssignmentExclusionSets() const
+{
+  return !d_assignExcSet.empty();
+}
+
 void TheoryModel::recordApproximation(TNode n, TNode pred)
 {
   Trace("model-builder-debug")