Enable CEGQI for non-linear (#1674)

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index d7d46bb4bc99b15d8e6220ef995fc2bef2144de3..358efede7bf920795b1b143117f55cd059186335 100644 (file)
--- 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 c12890b832e190b0b130f7ad5f4165a937e63f17..6cbc7418c43b81f313023d94e5714dcb0ece594c 100644 (file)
--- 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 bb210edcce835103952d87d3433470ac2177c757..b526fb1ee99b3b09acdf8b58b002379174178575 100644 (file)
--- 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 8de3dbfcb6343dfed5e0c9701783e91e129e1780..c07ddcd8fc03a8591d35248d817aa55c07afb9f7 100644 (file)
--- 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 b73c3368dc3a0d6c99f5172d713a7fcd5ff13664..430d261a121e005005d39f257ebf32c308edec25 100644 (file)
--- 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 e91a87e58b5a0ce5f5911d2af28f47eeb72d47ec..cd10e4f8a51fd5f6e9635de566de09da20a256ae 100644 (file)
--- 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 1711c301e19f2fb5c4e8624894b304ed03137682..8092978633c2ef7b539afb6eef486ce08629be47 100644 (file)
--- 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 (file)
index 0000000..63cf52f
--- /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 (file)
index 0000000..703f816
--- /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)