Using a single condition enumerator in sygus-unif (#2440)

This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).

In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:

- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.

A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.

There is also small improvements for trace messages.

1 files changed, 11 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 7319ba73e..204daa49a 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -166,7 +166,17 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     Trace("cegis") << "  Enumerators :\n";
     for (unsigned i = 0, size = enums.size(); i < size; ++i)
     {
-      Trace("cegis") << "    " << enums[i] << " -> ";
+      bool isUnit = false;
+      for (const Node& hd_unit : d_rl_eval_hds)
+      {
+        if (enums[i] == hd_unit[0])
+        {
+          isUnit = true;
+          break;
+        }
+      }
+      Trace("cegis") << "    " << enums[i]
+                     << (options::sygusUnif() && isUnit ? "*" : "") << " -> ";
       std::stringstream ss;
       Printer::getPrinter(options::outputLanguage())
           ->toStreamSygus(ss, enum_values[i]);