Simplify auxiliary variable handling in CEGQI (#4141)

Fixes #3849 and fixes #4062.

Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables.

In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be:
(1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 )
(2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2).
Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities).

This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above.

Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given.

1 files changed, 9 insertions, 7 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 2e5a834b1..27d77dfbb 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -564,13 +564,15 @@ Node CegSingleInv::reconstructToSyntax(Node s,
     }
   }
 
-
-  if( Trace.isOn("csi-sol") ){
-    //debug solution
-    if (!d_sol->debugSolution(d_solution))
-    {
-      Trace("csi-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl;
-    }
+  // debug solution
+  if (!d_sol->debugSolution(d_solution))
+  {
+    // This can happen if we encountered free variables in either the
+    // instantiation terms, or in the instantiation lemmas after postprocessing.
+    // In this case, we fail, since the solution is not valid.
+    Trace("csi-sol") << "FAIL : solution " << d_solution
+                     << " contains free constants." << std::endl;
+    reconstructed = -1;
   }
   if( Trace.isOn("cegqi-stats") ){
     int tsize, itesize;