Fixes for cbqi (#1453)

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 877db6797619abca4b432f9dd3d8f40145190282..78cd77c6ecea8f660b1ace428fce5fe882db5ca4 100644 (file)
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -1160,15 +1160,6 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited )
   }
 }
 
-struct sortCegVarOrder {
-  bool operator() (Node i, Node j) {
-    TypeNode it = i.getType();
-    TypeNode jt = j.getType();
-    return ( it!=jt && jt.isSubtypeOf( it ) ) || ( it==jt && i<j );
-  }
-};
-
-
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
   Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
   d_input_vars.clear();
@@ -1245,29 +1236,40 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   Trace("cbqi-debug") << "Determine variable order..." << std::endl;
   if (!d_vars.empty())
   {
-    TypeNode tn0 = d_vars[0].getType();
-    bool doSort = false;
     std::map<Node, unsigned> voo;
-    for (unsigned i = 0; i < d_vars.size(); i++)
+    bool doSort = false;
+    std::vector<Node> vars;
+    std::map<TypeNode, std::vector<Node> > tvars;
+    for (unsigned i = 0, size = d_vars.size(); i < size; i++)
     {
       voo[d_vars[i]] = i;
       d_var_order_index.push_back(0);
-      if (d_vars[i].getType() != tn0)
+      TypeNode tn = d_vars[i].getType();
+      if (tn.isInteger())
       {
         doSort = true;
+        tvars[tn].push_back(d_vars[i]);
+      }
+      else
+      {
+        vars.push_back(d_vars[i]);
       }
     }
     if (doSort)
     {
       Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
-      sortCegVarOrder scvo;
-      std::sort(d_vars.begin(), d_vars.end(), scvo);
+      for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars)
+      {
+        vars.insert(vars.end(), vs.second.begin(), vs.second.end());
+      }
+
       Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
-      for (unsigned i = 0; i < d_vars.size(); i++)
+      for (unsigned i = 0; i < vars.size(); i++)
       {
-        d_var_order_index[voo[d_vars[i]]] = i;
-        Trace("cbqi-debug") << "  " << d_vars[i] << " : " << d_vars[i].getType()
-                            << ", index was : " << voo[d_vars[i]] << std::endl;
+        d_var_order_index[voo[vars[i]]] = i;
+        Trace("cbqi-debug") << "  " << vars[i] << " : " << vars[i].getType()
+                            << ", index was : " << voo[vars[i]] << std::endl;
+        d_vars[i] = vars[i];
       }
       Trace("cbqi-debug") << std::endl;
     }

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 2d97bd160af923217848b6a8a1712e3a469f7e6e..609b6e461e53e759a0203ca781ad9bf84b567fd2 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -400,7 +400,7 @@ bool Trigger::isCbqiKind( Kind k ) {
   }else{
     //CBQI typically works for satisfaction-complete theories
     TheoryId t = kindToTheoryId( k );
-    return t==THEORY_BV || t==THEORY_DATATYPES;
+    return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL;
   }
 }