From 1e7207dc661a1aa7d6509cc21d86fb757938efb1 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Apr 2015 11:37:24 +0200
Subject: [PATCH] Minor fixes for cegqi.

---
 .../quantifiers/ce_guided_single_inv.cpp      | 29 +++++++++++--------
 .../quantifiers/instantiation_engine.cpp      |  2 +-
 2 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 7d1c06b8e..b3c1e1eaa 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -218,16 +218,21 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       }
 
       //[3] directly look at assertions
-      TheoryId tid = Theory::theoryOf( pv );
-      Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
-      if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) {
-        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-        for (unsigned j = 0; it != it_end; ++ it, ++j) {
-          Node lit = (*it).assertion;
-          Node atom = lit.getKind()==NOT ? lit[0] : lit;
-          bool pol = lit.getKind()!=NOT;
-          if( tid==THEORY_ARITH ){
-            if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
+      unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+      for( unsigned r=0; r<rmax; r++ ){
+        TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
+        Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
+        Trace("cegqi-si-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl;
+        if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) {
+          Trace("cegqi-si-inst-debug2") << "Look at assertions of " << tid << std::endl;
+          context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+          for (unsigned j = 0; it != it_end; ++ it, ++j) {
+            Node lit = (*it).assertion;
+            Trace("cegqi-si-inst-debug2") << "  look at " << lit << std::endl;
+            Node atom = lit.getKind()==NOT ? lit[0] : lit;
+            bool pol = lit.getKind()!=NOT;
+            //arithmetic inequalities and disequalities
+            if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && ( atom[0].getType().isInteger() || atom[0].getType().isReal() ) ) ){
               Assert( atom.getKind()!=GEQ || atom[1].isConst() );
               Node atom_lhs;
               Node atom_rhs;
@@ -1165,9 +1170,9 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
     Assert( d_cinst!=NULL );
     d_curr_lemmas.clear();
     //check if there are delta lemmas
-    d_cinst->getDeltaLemmas( d_curr_lemmas );
+    d_cinst->getDeltaLemmas( lems );
     //if not, do ce-guided instantiation
-    if( d_curr_lemmas.empty() ){
+    if( lems.empty() ){
       //call check for instantiator
       d_cinst->check();
       //add lemmas
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index cb01fd373..ea3e18be1 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -328,7 +328,7 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){
 }
 
 bool InstantiationEngine::doCbqi( Node f ){
-  if( options::cbqi.wasSetByUser() ){
+  if( options::cbqi.wasSetByUser() || options::cbqi2.wasSetByUser() ){
     return options::cbqi();
   }else if( options::cbqi() ){
     //if quantifier has a non-arithmetic variable, then do not use cbqi
-- 
2.30.2