CBQI BV choice expressions (#1296)

* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.

* Minor

* Make unique bound variables for choice functions in BvInstantor, clean up.

* Incorporate missing optimizations

* Clang format

* Unused field.

* Minor

* Fix, add regression.

* Fix regression.

* Fix bug that led to incorrect cleanup of instantiations.

* Add missing regression

* Improve handling of choice rewriting.

* Fix

* Clang format

* Use canonical variables for choice functions in cbqi bv.

* Add regression

* Clang format.

* Address review.

* Clang format

1 files changed, 53 insertions, 14 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 57bfb2d14..e7749cd92 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -46,24 +46,35 @@ CegInstantiator::~CegInstantiator() {
 void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
-    if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){
-      d_prog_var[n][n] = true;
+    if (n.getKind() == kind::CHOICE)
+    {
+      Assert(d_prog_var.find(n[0][0]) == d_prog_var.end());
+      d_prog_var[n[0][0]].clear();
+    }
+    if (d_vars_set.find(n) != d_vars_set.end())
+    {
+      d_prog_var[n].insert(n);
     }else if( !d_out->isEligibleForInstantiation( n ) ){
-      d_inelig[n] = true;
+      d_inelig.insert(n);
       return;
     }
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       computeProgVars( n[i] );
       if( d_inelig.find( n[i] )!=d_inelig.end() ){
-        d_inelig[n] = true;
-      }
-      for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
-        d_prog_var[n][it->first] = true;
-      }
-      //selectors applied to program variables are also variables
-      if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){
-        d_prog_var[n][n] = true;
+        d_inelig.insert(n);
       }
+      // all variables in child are contained in this
+      d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
+    }
+    // selectors applied to program variables are also variables
+    if (n.getKind() == APPLY_SELECTOR_TOTAL
+        && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
+    {
+      d_prog_var[n].insert(n);
+    }
+    if (n.getKind() == kind::CHOICE)
+    {
+      d_prog_var.erase(n[0][0]);
     }
   }
 }
@@ -113,7 +124,8 @@ void CegInstantiator::unregisterInstantiationVariable( Node v ) {
 bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){
   if( i==d_vars.size() ){
     //solved for all variables, now construct instantiation
-    bool needsPostprocess = false;
+    bool needsPostprocess =
+        sf.d_vars.size() > d_vars.size() || !d_var_order_index.empty();
     std::vector< Instantiator * > pp_inst;
     std::map< Instantiator *, Node > pp_inst_to_var;
     std::vector< Node > lemmas;
@@ -522,8 +534,13 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
 bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   if( !non_basic.empty() ){
-    for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){
-      if( std::find( non_basic.begin(), non_basic.end(), it->first )!=non_basic.end() ){
+    for (std::unordered_set<Node, NodeHashFunction>::iterator it =
+             d_prog_var[n].begin();
+         it != d_prog_var[n].end();
+         ++it)
+    {
+      if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end())
+      {
         return false;
       }
     }
@@ -699,6 +716,7 @@ bool CegInstantiator::check() {
   for( unsigned r=0; r<2; r++ ){
     SolvedForm sf;
     d_stack_vars.clear();
+    d_bound_var_index.clear();
     //try to add an instantiation
     if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){
       return true;
@@ -979,6 +997,26 @@ Node CegInstantiator::getModelValue( Node n ) {
   return d_qe->getModel()->getValue( n );
 }
 
+Node CegInstantiator::getBoundVariable(TypeNode tn)
+{
+  unsigned index = 0;
+  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb =
+      d_bound_var_index.find(tn);
+  if (itb != d_bound_var_index.end())
+  {
+    index = itb->second;
+  }
+  d_bound_var_index[tn] = index + 1;
+  while (index >= d_bound_var[tn].size())
+  {
+    std::stringstream ss;
+    ss << "x" << index;
+    Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn);
+    d_bound_var[tn].push_back(x);
+  }
+  return d_bound_var[tn][index];
+}
+
 void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
   if( n.getKind()==FORALL ){
     d_is_nested_quant = true;
@@ -1010,6 +1048,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   //Assert( d_vars.empty() );
   d_vars.clear();
   d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+  d_vars_set.insert(ce_vars.begin(), ce_vars.end());
 
   //determine variable order: must do Reals before Ints
   if( !d_vars.empty() ){