From db83224b35a218a0bb449850530f0d2bea484eae Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 19 Mar 2018 23:16:45 -0500
Subject: [PATCH] Enable CEGQI for non-linear (#1674)

---
 .../quantifiers/cegqi/ceg_instantiator.cpp      | 17 +++++++++++++++++
 src/theory/quantifiers/cegqi/ceg_instantiator.h |  8 ++++++++
 .../quantifiers/cegqi/ceg_t_instantiator.cpp    | 11 +++++------
 .../quantifiers/cegqi/inst_strategy_cbqi.cpp    | 11 +++++------
 src/theory/quantifiers/ematching/trigger.cpp    | 10 ----------
 src/theory/quantifiers/ematching/trigger.h      |  7 -------
 test/regress/regress0/quantifiers/Makefile.am   |  4 +++-
 .../regress0/quantifiers/cegqi-nl-simp.cvc      |  2 ++
 .../regress0/quantifiers/cegqi-nl-sq.smt2       |  5 +++++
 9 files changed, 45 insertions(+), 30 deletions(-)
 create mode 100644 test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
 create mode 100644 test/regress/regress0/quantifiers/cegqi-nl-sq.smt2

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index d7d46bb4b..358efede7 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -127,6 +127,23 @@ bool CegInstantiator::isEligible( Node n ) {
   return d_inelig.find( n )==d_inelig.end();
 }
 
+bool CegInstantiator::isCbqiKind(Kind k)
+{
+  if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ
+      || k == EQUAL
+      || k == MULT
+      || k == NONLINEAR_MULT)
+  {
+    return true;
+  }
+  else
+  {
+    // CBQI typically works for satisfaction-complete theories
+    TheoryId t = kindToTheoryId(k);
+    return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL;
+  }
+}
+
 bool CegInstantiator::hasVariable( Node n, Node pv ) {
   computeProgVars( n );
   return d_prog_var[n].find( pv )!=d_prog_var[n].end();
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index c12890b83..6cbc7418c 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -297,6 +297,14 @@ class CegInstantiator {
   bool useVtsInfinity() { return d_use_vts_inf; }
   /** are we processing a nested quantified formula? */
   bool hasNestedQuantification() { return d_is_nested_quant; }
+  /** Is k a kind for which counterexample-guided instantiation is possible?
+   *
+  * This typically corresponds to kinds that correspond to operators that
+  * have total interpretations and are a part of the signature of
+  * satisfaction complete theories (see Reynolds et al., CAV 2015).
+  */
+  static bool isCbqiKind(Kind k);
+
  private:
   /** quantified formula associated with this instantiator */
   QuantifiersEngine* d_qe;
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index bb210edcc..b526fb1ee 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -155,12 +155,11 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
         }
         Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
       }
-      if( options::cbqiAll() ){
-        // when not pure LIA/LRA, we must check whether the lhs contains pv
-        if( TermUtil::containsTerm( val, pv ) ){
-          Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
-          return 0;
-        }
+      // when not pure LIA/LRA, we must check whether the lhs contains pv
+      if (TermUtil::containsTerm(val, pv))
+      {
+        Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
+        return 0;
       }
       if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
         //redo, split integer/non-integer parts
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 8de3dbfcb..c07ddcd8f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -484,13 +483,13 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
     if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){
-      if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
+      if (!CegInstantiator::isCbqiKind(n.getKind()))
+      {
         Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
         return true;
-      }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
-        Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
-        return true;
-      }else if( n.getKind()==FORALL ){
+      }
+      else if (n.getKind() == FORALL || n.getKind() == CHOICE)
+      {
         return hasNonCbqiOperator( n[1], visited );
       }else{
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index b73c3368d..430d261a1 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -393,16 +393,6 @@ bool Trigger::isRelationalTrigger( Node n ) {
 bool Trigger::isRelationalTriggerKind( Kind k ) {
   return k==EQUAL || k==GEQ;
 }
-  
-bool Trigger::isCbqiKind( Kind k ) {
-  if( quantifiers::TermUtil::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
-    return true;
-  }else{
-    //CBQI typically works for satisfaction-complete theories
-    TheoryId t = kindToTheoryId( k );
-    return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL;
-  }
-}
 
 bool Trigger::isSimpleTrigger( Node n ){
   Node t = n.getKind()==NOT ? n[0] : n;
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index e91a87e58..cd10e4f8a 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -313,13 +313,6 @@ class Trigger {
   static bool isRelationalTrigger( Node n );
   /** Is k a relational trigger kind? */
   static bool isRelationalTriggerKind( Kind k );
-  /** Is k a kind for which counterexample-guided instantiation is possible?
-   *
-  * This typically corresponds to kinds that correspond to operators that
-  * have total interpretations and are a part of the signature of
-  * satisfaction complete theories (see Reynolds et al., CAV 2015).
-  */
-  static bool isCbqiKind( Kind k );
   /** is n a simple trigger (see inst_match_generator.h)? */
   static bool isSimpleTrigger( Node n );
   /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 1711c301e..809297863 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -71,7 +71,9 @@ TESTS =	\
 	qbv-test-invert-concat-1.smt2 \
 	qbv-test-invert-sign-extend.smt2 \
 	clock-10.smt2 \
-	lra-triv-gn.smt2
+	lra-triv-gn.smt2 \
+	cegqi-nl-simp.cvc \
+	cegqi-nl-sq.smt2
 
 EXTRA_DIST = $(TESTS) \
 	bug291.smt2.expect
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
new file mode 100644
index 000000000..63cf52fd6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
@@ -0,0 +1,2 @@
+% EXPECT: valid
+QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 b/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2
new file mode 100644
index 000000000..703f816d5
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2
@@ -0,0 +1,5 @@
+(set-logic NIA)
+(set-info :status unsat)
+(assert (not (exists ((?X Int)) (= (* ?X ?X) ?X))))
+(check-sat)
+(exit)
-- 
2.30.2