Fix handling of Boolean term variables (#4550)

Fixes #4446. This commit fixes two issues related to the handling of
Boolean term variables:

Removing Boolean subterms and replacing them with a Boolean term
variable introduces an equality of the form (= v t) where v is the
Boolean term variable and t is the term. It is important that these
equalities do not get removed. This commit changes
Theory::isLegalElimination() to take this into account.

The incorrect model reported in the issue was caused by some of the
Boolean term variables not being assigned values by the SAT solver
when we decided that the benchmark is satisfiable. Our justification
heuristic (correctly) decided that it is enough to satisfy one of the
disjuncts in the assertion to satisfy the whole assertion. However,
the assignments that we received from the SAT solver restricted us to
pick a specific value for one of the Boolean constants:

Literal | Value | Expr
---------------------------------------------------------
'7 ' 0 c
'0 ' 1 true
'1 ' 0 false
'2 ' 0 (a BOOLEAN_TERM_VARIABLE_274)
'5 ' _ b
'3 ' 1 (a BOOLEAN_TERM_VARIABLE_277)
'4 ' _ BOOLEAN_TERM_VARIABLE_274
'6 ' 0 BOOLEAN_TERM_VARIABLE_277
This meant that we had to pick true for BOOLEAN_TERM_VARIABLE_274
but we picked false since we simply treated it as an unassigned
variable. In general, the justification heuristic handles embedded
skolems introduced by term removal first and asks the SAT solver to
decide on Boolean term variables. However, for some logics, such as
QF_AUFLIA, we use the justification heuristic not for decisions but
only to decide when to stop, so those decisions were not done. This
commit introduces a conservative fix that adds a check after
satsifying all the assertions that makes sure that the equalities
introduced for Boolean terms are satisfied as well. Due to the eager
treatment of Boolean term variables when we use the justification
heuristic also for decisions, it is likely that we don't really have
the problem in that case but it doesn't hurt to enable the fix. It is
also possible that this fix is only required with models but it is
definitely safer to just always enable it (there could be tricky
corner cases involving the theory combination between UF and Boolean
terms). Additionally, this commit changes the ITE-specific naming in
the justification heuristic to reflect more accurately that we are in
general dealing with skolems introduced by term removals and not only
due to ITE removal.

2 files changed, 67 insertions, 47 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index ce79d6ca0..a3873c6da 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -40,10 +40,10 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
       d_giveup("decision::jh::giveup", 0),
       d_timestat("decision::jh::time"),
       d_assertions(uc),
-      d_iteAssertions(uc),
-      d_iteCache(uc),
+      d_skolemAssertions(uc),
+      d_skolemCache(uc),
       d_visited(),
-      d_visitedComputeITE(),
+      d_visitedComputeSkolems(),
       d_curDecision(),
       d_curThreshold(0),
       d_childCache(uc),
@@ -175,10 +175,26 @@ void JustificationHeuristic::addAssertions(
     << " assertionsEnd = " << assertionsEnd
     << std::endl;
 
-  // Save the 'real' assertions locally
-  for (size_t i = 0; i < assertionsEnd; i++)
+  // Save all assertions locally, including the assertions generated by term
+  // removal. We have to make sure that we assign a value to all the Boolean
+  // term variables. To illustrate why this is, consider the case where we have
+  // a single assertion
+  //
+  // (or (f a) (f b))
+  //
+  // where `f` is a function `Bool -> Bool`. Given an assignment:
+  //
+  // (f a) -> true
+  // (f b) -> false
+  // a -> false
+  //
+  // UF will not complain and the justification heuristic considers the
+  // assertion to be satisifed. However, we also have to make sure that we pick
+  // a value for `b` that is not in conflict with the other assignments (we can
+  // only choose `b` to be `true` otherwise the model is incorrect).
+  for (const Node& assertion : assertions)
   {
-    d_assertions.push_back(assertions[i]);
+    d_assertions.push_back(assertion);
   }
 
   // Save mapping between ite skolems and ite assertions
@@ -188,7 +204,7 @@ void JustificationHeuristic::addAssertions(
                                << assertions[(i.second)] << std::endl;
     Assert(i.second >= assertionsEnd && i.second < assertions.size());
 
-    d_iteAssertions[i.first] = assertions[i.second];
+    d_skolemAssertions[i.first] = assertions[i.second];
   }
 
   // Automatic weight computation
@@ -363,36 +379,39 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
   }//end of else
 }
 
-JustificationHeuristic::IteList
-JustificationHeuristic::getITEs(TNode n)
+JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n)
 {
-  IteCache::iterator it = d_iteCache.find(n);
-  if(it != d_iteCache.end()) {
+  SkolemCache::iterator it = d_skolemCache.find(n);
+  if (it != d_skolemCache.end())
+  {
     return (*it).second;
-  } else {
-    // Compute the list of ITEs
-    // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
-    d_visitedComputeITE.clear();
-    IteList ilist;
-    computeITEs(n, ilist);
-    d_iteCache.insert(n, ilist);
+  }
+  else
+  {
+    // Compute the list of Skolems
+    // TODO: optimize by avoiding multiple lookup for d_skolemCache[n]
+    d_visitedComputeSkolems.clear();
+    SkolemList ilist;
+    computeSkolems(n, ilist);
+    d_skolemCache.insert(n, ilist);
     return ilist;
   }
 }
 
-void JustificationHeuristic::computeITEs(TNode n, IteList &l)
+void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l)
 {
-  Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n";
-  d_visitedComputeITE.insert(n);
+  Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n";
+  d_visitedComputeSkolems.insert(n);
   for(unsigned i=0; i<n.getNumChildren(); ++i) {
-    SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
-    if(it2 != d_iteAssertions.end()) {
+    SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]);
+    if (it2 != d_skolemAssertions.end())
+    {
       l.push_back(make_pair(n[i], (*it2).second));
       Assert(n[i].getNumChildren() == 0);
     }
-    if(d_visitedComputeITE.find(n[i]) ==
-         d_visitedComputeITE.end()) {
-      computeITEs(n[i], l);
+    if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end())
+    {
+      computeSkolems(n[i], l);
     }
   }
 }
@@ -470,9 +489,8 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
    * If not in theory of booleans, check if this is something to split-on.
    */
   if(isAtom) {
-    // if node has embedded ites, resolve that first
-    if(handleEmbeddedITEs(node) == FOUND_SPLITTER)
-      return FOUND_SPLITTER;
+    // if node has embedded skolems due to term removal, resolve that first
+    if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER;
 
     if(litVal != SAT_VALUE_UNKNOWN) {
       Assert(litVal == desiredVal);
@@ -700,13 +718,15 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod
   }// else (...ifVal...)
 }
 
-JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(TNode node)
+JustificationHeuristic::SearchResult
+JustificationHeuristic::handleEmbeddedSkolems(TNode node)
 {
-  const IteList l = getITEs(node);
-  Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
+  const SkolemList l = getSkolems(node);
+  Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl;
 
   bool noSplitter = true;
-  for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
+  for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i)
+  {
     if(d_visited.find((*i).first) == d_visited.end()) {
       d_visited.insert((*i).first);
       SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE);
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index bb426ad1e..9e6765438 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -42,8 +42,8 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   //                   TRUE           FALSE         MEH
   enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
 
-  typedef std::vector<pair<TNode,TNode> > IteList;
-  typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache;
+  typedef std::vector<pair<TNode, TNode> > SkolemList;
+  typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache;
   typedef std::vector<TNode> ChildList;
   typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
@@ -63,18 +63,19 @@ class JustificationHeuristic : public ITEDecisionStrategy {
 
   /**
    * A copy of the assertions that need to be justified
-   * directly. Doesn't have ones introduced during during ITE-removal.
+   * directly. Doesn't have ones introduced during during term removal.
    */
   context::CDList<TNode> d_assertions;
   //TNode is fine since decisionEngine has them too
 
-  /** map from ite-rewrite skolem to a boolean-ite assertion */
-  SkolemMap d_iteAssertions;
+  /** map from skolems introduced in term removal to the corresponding assertion
+   */
+  SkolemMap d_skolemAssertions;
   // 'key' being TNode is fine since if a skolem didn't exist anywhere,
   // we won't look it up. as for 'value', same reason as d_assertions
 
-  /** Cache for ITE skolems present in a atomic formula */
-  IteCache d_iteCache;
+  /** Cache for skolems present in a atomic formula */
+  SkolemCache d_skolemCache;
 
   /**
    * This is used to prevent infinite loop when trying to find a
@@ -84,10 +85,10 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   std::unordered_set<TNode,TNodeHashFunction> d_visited;
 
   /**
-   * Set to track visited nodes in a dfs search done in computeITE
+   * Set to track visited nodes in a dfs search done in computeSkolems
    * function
    */
-  std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+  std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems;
 
   /** current decision for the recursive call */
   SatLiteral d_curDecision;
@@ -153,8 +154,7 @@ public:
   SatValue tryGetSatValue(Node n);
 
   /* Get list of all term-ITEs for the atomic formula v */
-  JustificationHeuristic::IteList getITEs(TNode n);
-
+  JustificationHeuristic::SkolemList getSkolems(TNode n);
 
   /**
    * For big and/or nodes, a cache to save starting index into children
@@ -165,8 +165,8 @@ public:
   int getStartIndex(TNode node);
   void saveStartIndex(TNode node, int val);
 
-  /* Compute all term-ITEs in a node recursively */
-  void computeITEs(TNode n, IteList &l);
+  /* Compute all term-removal skolems in a node recursively */
+  void computeSkolems(TNode n, SkolemList& l);
 
   SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
   SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
@@ -175,7 +175,7 @@ public:
   SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
                         TNode node2, SatValue desiredVal2);
   SearchResult handleITE(TNode node, SatValue desiredVal);
-  SearchResult handleEmbeddedITEs(TNode node);
+  SearchResult handleEmbeddedSkolems(TNode node);
 };/* class JustificationHeuristic */
 
 }/* namespace decision */