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.

5 files changed, 26 insertions, 152 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0dc8f262e..f81b0e160 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -543,20 +543,11 @@ void CegInstantiator::registerTheoryId(TheoryId tid)
   }
 }
 
-void CegInstantiator::registerVariable(Node v, bool is_aux)
+void CegInstantiator::registerVariable(Node v)
 {
   Assert(std::find(d_vars.begin(), d_vars.end(), v) == d_vars.end());
-  Assert(std::find(d_aux_vars.begin(), d_aux_vars.end(), v)
-         == d_aux_vars.end());
-  if (!is_aux)
-  {
-    d_vars.push_back(v);
-    d_vars_set.insert(v);
-  }
-  else
-  {
-    d_aux_vars.push_back(v);
-  }
+  d_vars.push_back(v);
+  d_vars_set.insert(v);
   TypeNode vtn = v.getType();
   Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
                            << v << std::endl;
@@ -1410,15 +1401,14 @@ void CegInstantiator::presolve( Node q ) {
 }
 
 void CegInstantiator::processAssertions() {
-  Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
+  Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size()
+                     << std::endl;
   d_curr_asserts.clear();
   d_curr_eqc.clear();
   d_curr_type_eqc.clear();
 
   // must use master equality engine to avoid value instantiations
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
-  //to eliminate identified illegal terms
-  std::map< Node, Node > aux_subs;
 
   //for each variable
   for( unsigned i=0; i<d_vars.size(); i++ ){
@@ -1455,21 +1445,6 @@ void CegInstantiator::processAssertions() {
         }else{
           Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
         }
-        if( lit.getKind()==EQUAL ){
-          std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
-          if( itae!=d_aux_eq.end() ){
-            for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){
-              aux_subs[ itae2->first ] = itae2->second;
-              Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
-            }
-          }
-        }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){
-          if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){
-            Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT );
-            aux_subs[ atom ] = val;
-            Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl;
-          }
-        }
       }
     }
   }
@@ -1501,43 +1476,6 @@ void CegInstantiator::processAssertions() {
     }
     ++eqcs_i;
   }
-  //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula)
-  std::vector< Node > subs_lhs;
-  std::vector< Node > subs_rhs;
-  for( unsigned i=0; i<d_aux_vars.size(); i++ ){
-    Node r = d_aux_vars[i];
-    std::map< Node, Node >::iterator it = aux_subs.find( r );
-    if( it!=aux_subs.end() ){
-      addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second );
-    }else{
-      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl;
-      Assert(false);
-    }
-  }
-
-  //apply substitutions to everything, if necessary
-  if( !subs_lhs.empty() ){
-    Trace("cbqi-proc") << "Applying substitution : " << std::endl;
-    for( unsigned i=0; i<subs_lhs.size(); i++ ){
-      Trace("cbqi-proc") << "  " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl;
-    }
-    for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Node lit = it->second[i];
-        lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-        lit = Rewriter::rewrite( lit );
-        it->second[i] = lit;
-      }
-    }
-    for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Node n = it->second[i];
-        n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-        n = Rewriter::rewrite( n  );
-        it->second[i] = n;
-      }
-    }
-  }
 
   //remove unecessary assertions
   for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
@@ -1574,23 +1512,6 @@ void CegInstantiator::processAssertions() {
   }
 }
 
-void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) {
-  r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-
-  std::vector< Node > cl;
-  cl.push_back( l );
-  std::vector< Node > cr;
-  cr.push_back( r );
-  for( unsigned i=0; i<subs_lhs.size(); i++ ){
-    Node nr = subs_rhs[i].substitute( cl.begin(), cl.end(), cr.begin(), cr.end() );
-    nr = Rewriter::rewrite( nr );
-    subs_rhs[i] = nr;
-  }
-
-  subs_lhs.push_back( l );
-  subs_rhs.push_back( r );
-}
-
 Node CegInstantiator::getModelValue( Node n ) {
   return d_qe->getModel()->getValue( n );
 }
@@ -1687,12 +1608,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   //remove ITEs
   IteSkolemMap iteSkolemMap;
   d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
-  //Assert( d_aux_vars.empty() );
-  d_aux_vars.clear();
-  d_aux_eq.clear();
   for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
     Trace("cbqi-reg") << "  register aux variable : " << i->first << std::endl;
-    registerVariable(i->first, true);
+    registerVariable(i->first);
   }
   for( unsigned i=0; i<lems.size(); i++ ){
     Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
@@ -1702,26 +1620,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     // collect below are identical to the atoms that we add to the CNF stream
     rlem = d_qe->getTheoryEngine()->preprocess(rlem);
     Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
-    //record the literals that imply auxiliary variables to be equal to terms
-    if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
-      if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
-        if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){
-          Node v = lems[i][1][0];
-          for( unsigned r=1; r<=2; r++ ){
-            d_aux_eq[rlem[r]][v] = lems[i][r][1];
-            Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
-          }
-        }
-      }
-    }
-    /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){
-      //Boolean terms
-      if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){
-        Node v = lems[i][0];
-        d_aux_eq[rlem][v] = lems[i][1];
-         Trace("cbqi-debug") << "  " << rlem << " implies " << v << " = " << lems[i][1] << std::endl;
-      }
-    }*/
     lems[i] = rlem;
   }
   // determine variable order: must do Reals before Ints
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 76e0869fa..b4aa38c07 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -396,15 +396,6 @@ class CegInstantiator {
    * such as the above data structures.
    */
   void processAssertions();
-  /** add to auxiliary variable substitution
-   * This adds the substitution l -> r to the auxiliary
-   * variable substitution subs_lhs -> subs_rhs, and serializes
-   * it (applies it to existing substitutions).
-   */
-  void addToAuxVarSubstitution(std::vector<Node>& subs_lhs,
-                               std::vector<Node>& subs_rhs,
-                               Node l,
-                               Node r);
   /** cache bound variables for type returned
    * by getBoundVariable(...).
    */
@@ -462,35 +453,8 @@ class CegInstantiator {
    * and sending on the output channel of this class.
    */
   std::vector<Node> d_input_vars;
-  /** literals to equalities for aux vars
-   * This stores entries of the form
-   *   L -> ( k -> t )
-   * where
-   *   k is a variable in d_aux_vars,
-   *   L is a literal that if asserted implies that our
-   *    instantiation should map { k -> t }.
-   * For example, if a term of the form
-   *   ite( C, t1, t2 )
-   * was replaced by k, we get this (top-level) assertion:
-   *   ite( C, k=t1, k=t2 )
-   * The vector d_aux_eq contains the exact form of
-   * the literals in the above constraint that they would
-   * appear in assertions, meaning d_aux_eq may contain:
-   *   t1=k -> ( k -> t1 )
-   *   t2=k -> ( k -> t2 )
-   * where t1=k and t2=k are the rewritten form of
-   * k=t1 and k=t2 respectively.
-   */
-  std::map<Node, std::map<Node, Node> > d_aux_eq;
-  /** auxiliary variables
-   * These variables include the result of removing ITE
-   * terms from the quantified formula we are processing.
-   * These variables must be eliminated from constraints
-   * as a preprocess step to check().
-   */
-  std::vector<Node> d_aux_vars;
   /** register variable */
-  void registerVariable(Node v, bool is_aux = false);
+  void registerVariable(Node v);
   //-------------------------------the variables
 
   //-------------------------------quantified formula info
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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cd83ef3d1..4cd3c70d2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1502,6 +1502,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3765.smt2
   regress1/quantifiers/issue3765-quant-dd.smt2
   regress1/quantifiers/issue4021-ind-opts.smt2
+  regress1/quantifiers/issue4062-cegqi-aux.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
diff --git a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
new file mode 100644
index 000000000..0296c978c
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models
+; EXPECT: sat
+(set-logic NIA)
+(set-option :arith-rewrite-equalities true)
+(set-option :global-negate true)
+(set-info :status sat)
+(declare-const i5 Int)
+(assert (= 562 (abs i5)))
+(check-sat)