Update ownership policy for dynamic quantifiers splitting (#3493)

3 files changed, 523 insertions, 13 deletions

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 54708f6cb..e425cd345 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -41,8 +41,8 @@ void QuantDSplit::checkOwnership(Node q)
   {
     return;
   }
-  int max_index = -1;
-  int max_score = -1;
+  bool takeOwnership = false;
+  bool doSplit = false;
   Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
@@ -51,9 +51,9 @@ void QuantDSplit::checkOwnership(Node q)
       if( dt.isRecursiveSingleton( tn.toType() ) ){
         Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
       }else{
-        int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0;
+          // split if it is a finite datatype
+          doSplit = dt.isInterpretedFinite(tn.toType());
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
           if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
             if (dt.isInterpretedFinite(tn.toType()))
@@ -61,29 +61,43 @@ void QuantDSplit::checkOwnership(Node q)
               // split if goes from being unhandled -> handled by finite
               // instantiation. An example is datatypes with uninterpreted sort
               // fields which are "interpreted finite" but not "finite".
-              score = 1;
+              doSplit = true;
+              // we additionally take ownership of this formula, in other words,
+              // we mark it reduced.
+              takeOwnership = true;
             }
             else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
             {
               // split if only one constructor
-              score = 1;
+              doSplit = true;
             }
           }
         }
-        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl;
-        if( score>max_score ){
-          max_index = i;
-          max_score = score;
+        if (doSplit)
+        {
+          // store the index to split
+          d_quant_to_reduce[q] = i;
+          Trace("quant-dsplit-debug")
+              << "Split at index " << i << " based on datatype " << dt.getName()
+              << std::endl;
+          break;
         }
+        Trace("quant-dsplit-debug")
+            << "Do not split based on datatype " << dt.getName() << std::endl;
       }
     }
   }
 
-  if( max_index!=-1 ){
-    Trace("quant-dsplit-debug") << "Will split at index " << max_index << "." << std::endl;
-    d_quant_to_reduce[q] = max_index;
+  if (takeOwnership)
+  {
+    Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
     d_quantEngine->setOwner( q, this );
   }
+  // Notice we may not take ownership in some cases, meaning that both the
+  // original quantified formula and the split one are generated. This may
+  // increase our ability to answer "unsat", since quantifier instantiation
+  // heuristics may be more effective for one or the other (see issues #993
+  // and 3481).
 }
 
 /* whether this module needs to check this round */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 946f54650..a098201b2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1404,6 +1404,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3250-syg-inf-q.smt2
   regress1/quantifiers/issue3316.smt2
   regress1/quantifiers/issue3317.smt2
+  regress1/quantifiers/issue3481.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2
new file mode 100644
index 000000000..47d2bcbe4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3481.smt2
@@ -0,0 +1,495 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
+
+;; produced by cvc4_16.drv ;;
+(set-info :smt-lib-version 2.6)
+(set-logic AUFBVFPDTNIRA)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+;;; SMT-LIB2: integer arithmetic
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-sort us_private 0)
+
+(declare-fun private__bool_eq (us_private us_private) Bool)
+
+(declare-const us_null_ext__ us_private)
+
+(declare-sort us_type_of_heap 0)
+
+(declare-datatypes ((us_type_of_heap__ref 0))
+(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
+(declare-sort us_image 0)
+
+(declare-datatypes ((int__ref 0))
+(((int__refqtmk (int__content Int)))))
+(declare-datatypes ((bool__ref 0))
+(((bool__refqtmk (bool__content Bool)))))
+(declare-datatypes ((us_fixed__ref 0))
+(((us_fixed__refqtmk (us_fixed__content Int)))))
+(declare-datatypes ((real__ref 0))
+(((real__refqtmk (real__content Real)))))
+(declare-datatypes ((us_private__ref 0))
+(((us_private__refqtmk (us_private__content us_private)))))
+(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
+
+(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
+                                                               a))
+
+(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
+
+(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
+
+(define-fun us_private__ref___projection ((a us_private__ref)) us_private 
+  (us_private__content a))
+
+(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
+
+(declare-sort integer 0)
+
+(declare-fun integerqtint (integer) Int)
+
+
+(declare-fun attr__ATTRIBUTE_IMAGE1 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Int)
+
+(declare-fun user_eq (integer integer) Bool)
+
+(declare-const dummy integer)
+
+(declare-datatypes ((integer__ref 0))
+(((integer__refqtmk (integer__content integer)))))
+(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer 
+  (integer__content a))
+
+(define-fun to_rep ((x integer)) Int (integerqtint x))
+
+(declare-fun of_rep (Int) integer)
+
+
+(declare-sort positive 0)
+
+(declare-fun positiveqtint (positive) Int)
+
+(declare-datatypes ((positive__ref 0))
+(((positive__refqtmk (positive__content positive)))))
+(define-fun positive__ref_positive__content__projection ((a positive__ref)) positive 
+  (positive__content a))
+
+(declare-datatypes ((us_split_fields 0))
+(((us_split_fieldsqtmk
+  (rec__test_route__point__x integer)(rec__test_route__point__y integer)))))
+(define-fun us_split_fields_rec__test_route__point__x__projection ((a us_split_fields)) integer 
+  (rec__test_route__point__x a))
+
+(define-fun us_split_fields_rec__test_route__point__y__projection ((a us_split_fields)) integer 
+  (rec__test_route__point__y a))
+
+(declare-datatypes ((us_split_fields__ref 0))
+(((us_split_fields__refqtmk (us_split_fields__content us_split_fields)))))
+(define-fun us_split_fields__ref___split_fields__content__projection ((a us_split_fields__ref)) us_split_fields 
+  (us_split_fields__content a))
+
+(declare-datatypes ((us_rep 0))
+(((us_repqtmk (us_split_fields1 us_split_fields)))))
+(define-fun us_rep___split_fields__projection ((a us_rep)) us_split_fields 
+  (us_split_fields1 a))
+
+
+(declare-const value__size Int)
+
+(declare-const object__size Int)
+
+(declare-const alignment Int)
+
+(declare-const test_route__point__x__first__bit Int)
+
+(declare-const test_route__point__x__last__bit Int)
+
+(declare-const test_route__point__x__position Int)
+
+(declare-const test_route__point__y__first__bit Int)
+
+(declare-const test_route__point__y__last__bit Int)
+
+(declare-const test_route__point__y__position Int)
+
+(declare-fun user_eq2 (us_rep us_rep) Bool)
+
+(declare-const dummy2 us_rep)
+
+(declare-datatypes ((point__ref 0))
+(((point__refqtmk (point__content us_rep)))))
+(define-fun point__ref_point__content__projection ((a point__ref)) us_rep 
+  (point__content a))
+
+(declare-datatypes ((us_rep1 0))
+(((us_repqtmk1
+  (rec__test_route__point_acc__is_null_pointer Bool)(rec__test_route__point_acc__pointer_address Int)(rec__test_route__point_acc__pointer_value us_rep)))))
+(define-fun us_rep_rec__test_route__point_acc__is_null_pointer__projection ((a us_rep1)) Bool 
+  (rec__test_route__point_acc__is_null_pointer a))
+
+(define-fun us_rep_rec__test_route__point_acc__pointer_address__projection ((a us_rep1)) Int 
+  (rec__test_route__point_acc__pointer_address a))
+
+(define-fun us_rep_rec__test_route__point_acc__pointer_value__projection ((a us_rep1)) us_rep 
+  (rec__test_route__point_acc__pointer_value a))
+
+(declare-datatypes ((us_rep__ref 0))
+(((us_rep__refqtmk (us_rep__content us_rep1)))))
+(define-fun us_rep__ref___rep__content__projection ((a us_rep__ref)) us_rep1 
+  (us_rep__content a))
+
+(define-fun rec__test_route__point_acc__pointer_value__pred ((a us_rep1)) Bool 
+  (not (= (rec__test_route__point_acc__is_null_pointer a) true)))
+
+(declare-const us_null_pointer us_rep1)
+
+;; __null_pointer__def_axiom
+  (assert
+  (= (rec__test_route__point_acc__is_null_pointer us_null_pointer) true))
+
+(declare-const dummy3 us_rep1)
+
+(declare-datatypes ((t1b__ref 0))
+(((t1b__refqtmk (t1b__content us_rep1)))))
+(define-fun t1b__ref_t1b__content__projection ((a t1b__ref)) us_rep1 
+  (t1b__content a))
+
+(declare-sort us_main_type 0)
+
+(declare-datatypes ((us_rep2 0))
+(((us_repqtmk2
+  (rec__test_route__route_acc__is_null_pointer Bool)(rec__test_route__route_acc__pointer_address Int)(rec__test_route__route_acc__pointer_value_abstr us_main_type)))))
+(define-fun us_rep_rec__test_route__route_acc__is_null_pointer__projection ((a us_rep2)) Bool 
+  (rec__test_route__route_acc__is_null_pointer a))
+
+(define-fun us_rep_rec__test_route__route_acc__pointer_address__projection ((a us_rep2)) Int 
+  (rec__test_route__route_acc__pointer_address a))
+
+(define-fun us_rep_rec__test_route__route_acc__pointer_value_abstr__projection ((a us_rep2)) us_main_type 
+  (rec__test_route__route_acc__pointer_value_abstr a))
+
+(declare-datatypes ((us_rep__ref1 0))
+(((us_rep__refqtmk1 (us_rep__content1 us_rep2)))))
+(define-fun us_rep__ref___rep__content__2__projection ((a us_rep__ref1)) us_rep2 
+  (us_rep__content1 a))
+
+
+(declare-const dummy4 us_rep2)
+
+(declare-datatypes ((t4b__ref 0))
+(((t4b__refqtmk (t4b__content us_rep2)))))
+(define-fun t4b__ref_t4b__content__projection ((a t4b__ref)) us_rep2 
+  (t4b__content a))
+
+(declare-fun length (us_rep2) Int)
+
+(declare-fun length__function_guard (Int us_rep2) Bool)
+
+(define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
+
+(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
+
+(declare-sort natural 0)
+
+(declare-fun naturalqtint (natural) Int)
+
+(define-fun in_range3 ((x Int)) Bool (and (<= 0 x) (<= x 2147483647)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int)
+
+(declare-fun user_eq3 (natural natural) Bool)
+
+(declare-const dummy5 natural)
+
+(declare-datatypes ((natural__ref 0))
+(((natural__refqtmk (natural__content natural)))))
+(define-fun natural__ref_natural__content__projection ((a natural__ref)) natural 
+  (natural__content a))
+
+(declare-const dummy6 us_rep1)
+
+(declare-datatypes ((point_acc__ref 0))
+(((point_acc__refqtmk (point_acc__content us_rep1)))))
+(define-fun point_acc__ref_point_acc__content__projection ((a point_acc__ref)) us_rep1 
+  (point_acc__content a))
+
+(declare-const dummy7 us_rep2)
+
+(declare-datatypes ((route_acc__ref 0))
+(((route_acc__refqtmk (route_acc__content us_rep2)))))
+(define-fun route_acc__ref_route_acc__content__projection ((a route_acc__ref)) us_rep2 
+  (route_acc__content a))
+
+(declare-datatypes ((us_split_fields2 0))
+(((us_split_fieldsqtmk1
+  (rec__test_route__route__current us_rep1)(rec__test_route__route__rest us_rep2)))))
+(define-fun us_split_fields_rec__test_route__route__current__projection ((a us_split_fields2)) us_rep1 
+  (rec__test_route__route__current a))
+
+(define-fun us_split_fields_rec__test_route__route__rest__projection ((a us_split_fields2)) us_rep2 
+  (rec__test_route__route__rest a))
+
+(declare-datatypes ((us_split_fields__ref1 0))
+(((us_split_fields__refqtmk1 (us_split_fields__content1 us_split_fields2)))))
+(define-fun us_split_fields__ref___split_fields__content__2__projection ((a us_split_fields__ref1)) us_split_fields2 
+  (us_split_fields__content1 a))
+
+(declare-datatypes ((us_rep3 0))
+(((us_repqtmk3 (us_split_fields3 us_split_fields2)))))
+(define-fun us_rep___split_fields__2__projection ((a us_rep3)) us_split_fields2 
+  (us_split_fields3 a))
+
+(declare-const value__size1 Int)
+
+(declare-const object__size1 Int)
+
+(declare-const alignment1 Int)
+
+(declare-const test_route__route__current__first__bit Int)
+
+(declare-const test_route__route__current__last__bit Int)
+
+(declare-const test_route__route__current__position Int)
+
+
+(declare-const test_route__route__rest__first__bit Int)
+
+(declare-const test_route__route__rest__last__bit Int)
+
+(declare-const test_route__route__rest__position Int)
+
+
+(declare-fun user_eq4 (us_rep3 us_rep3) Bool)
+
+(declare-const dummy8 us_rep3)
+
+(declare-datatypes ((route__ref 0))
+(((route__refqtmk (route__content us_rep3)))))
+(define-fun route__ref_route__content__projection ((a route__ref)) us_rep3 
+  (route__content a))
+
+(declare-fun us_open (us_main_type) us_rep3)
+
+(declare-fun us_close (us_rep3) us_main_type)
+
+(define-fun rec__test_route__route_acc__pointer_value ((a us_rep2)) us_rep3 
+  (us_open (rec__test_route__route_acc__pointer_value_abstr a)))
+
+(define-fun rec__test_route__route_acc__pointer_value__pred ((a us_rep2)) Bool 
+  (not (= (rec__test_route__route_acc__is_null_pointer a) true)))
+
+(declare-const us_null_pointer1 us_rep2)
+
+
+(declare-fun temp___dynamic_invariant_202 (us_rep2 Bool Bool Bool Bool) Bool)
+
+
+
+(declare-const dummy9 us_rep2)
+
+(declare-datatypes ((t5b__ref 0))
+(((t5b__refqtmk (t5b__content us_rep2)))))
+(define-fun t5b__ref_t5b__content__projection ((a t5b__ref)) us_rep2 
+  (t5b__content a))
+
+(declare-fun nth_x (us_rep2 Int) Int)
+
+(declare-fun nth_x__function_guard (Int us_rep2 Int) Bool)
+
+(declare-datatypes ((map__ref 0))
+(((map__refqtmk (map__content (Array Int integer))))))
+(declare-fun slide ((Array Int integer) Int Int) (Array Int integer))
+
+
+(declare-sort t 0)
+
+(declare-fun first (t) integer)
+
+(declare-fun last (t) integer)
+
+(declare-fun mk (Int Int) t)
+
+(declare-datatypes ((us_t 0))
+(((us_tqtmk (elts (Array Int integer))(rt t)))))
+
+(declare-const value__size2 Int)
+
+(declare-const object__size2 Int)
+
+(declare-const component__size Int)
+
+(declare-const alignment2 Int)
+
+
+(declare-fun user_eq5 (us_t us_t) Bool)
+
+(declare-const dummy10 us_t)
+
+(declare-datatypes ((int_array__ref 0))
+(((int_array__refqtmk (int_array__content us_t)))))
+(define-fun int_array__ref_int_array__content__projection ((a int_array__ref)) us_t 
+  (int_array__content a))
+
+(declare-const dummy11 us_rep2)
+
+(declare-datatypes ((t9b__ref 0))
+(((t9b__refqtmk (t9b__content us_rep2)))))
+(define-fun t9b__ref_t9b__content__projection ((a t9b__ref)) us_rep2 
+  (t9b__content a))
+
+
+(declare-const dummy12 us_rep2)
+
+(declare-datatypes ((t21b__ref 0))
+(((t21b__refqtmk (t21b__content us_rep2)))))
+(define-fun t21b__ref_t21b__content__projection ((a t21b__ref)) us_rep2 
+  (t21b__content a))
+
+(declare-const dummy13 us_rep1)
+
+(declare-datatypes ((t22b__ref 0))
+(((t22b__refqtmk (t22b__content us_rep1)))))
+(define-fun t22b__ref_t22b__content__projection ((a t22b__ref)) us_rep1 
+  (t22b__content a))
+
+(declare-fun nth_point (us_rep2 Int) us_rep1)
+
+(declare-fun nth_point__function_guard (us_rep1 us_rep2 Int) Bool)
+
+(declare-sort us_pledge_ty 0)
+
+(declare-datatypes ((us_pledge_ty__ref 0))
+(((us_pledge_ty__refqtmk (us_pledge_ty__content us_pledge_ty)))))
+(declare-fun us_pledge_get (us_pledge_ty us_rep2 us_rep1) Bool)
+
+(declare-fun test_route__nth_point__pledge (us_rep2 Int) us_pledge_ty)
+
+(declare-const r__pointer_address Int)
+
+(declare-const r__is_null_pointer Bool)
+
+(declare-const attr__ATTRIBUTE_ADDRESS Int)
+
+(declare-const n Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
+
+(declare-const s Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS2 Int)
+
+(declare-const l Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS3 Int)
+
+(declare-const dummy14 us_rep2)
+
+(declare-datatypes ((t29b__ref 0))
+(((t29b__refqtmk (t29b__content us_rep2)))))
+(define-fun t29b__ref_t29b__content__projection ((a t29b__ref)) us_rep2 
+  (t29b__content a))
+
+(declare-const dummy15 us_rep1)
+
+(declare-datatypes ((t34b__ref 0))
+(((t34b__refqtmk (t34b__content us_rep1)))))
+(define-fun t34b__ref_t34b__content__projection ((a t34b__ref)) us_rep1 
+  (t34b__content a))
+
+(declare-const attr__ATTRIBUTE_ADDRESS4 Int)
+
+(declare-sort us_pledge_ty1 0)
+
+(declare-datatypes ((us_pledge_ty__ref1 0))
+(((us_pledge_ty__refqtmk1 (us_pledge_ty__content1 us_pledge_ty1)))))
+(declare-fun us_pledge_get1 (us_pledge_ty1 us_rep2 us_rep1) Bool)
+
+
+(declare-const r__pointer_value us_split_fields2)
+
+
+(define-fun o () us_rep2 (us_repqtmk2 r__is_null_pointer r__pointer_address
+                         (us_close (us_repqtmk3 r__pointer_value))))
+
+(define-fun test_route__shift_nth_x__l__assume () Int (length o))
+
+
+(define-fun o1 () Int n)
+
+(define-fun o2 () us_rep2 (us_repqtmk2 r__is_null_pointer r__pointer_address
+                          (us_close (us_repqtmk3 r__pointer_value))))
+
+(define-fun test_route__shift_nth_x__p__assume () us_rep1 (nth_point o2 o1))
+
+
+
+(declare-const usf us_pledge_ty1)
+
+
+(declare-const test_route__shift_nth_x__p__pledge us_pledge_ty1)
+
+
+(declare-const p__pointer_value us_split_fields)
+
+
+(declare-const p__pointer_address Int)
+
+
+(declare-const p__is_null_pointer Bool)
+
+
+(declare-const temp___borrowed_250 us_rep2)
+
+(declare-const temp___brower_249 us_rep1)
+
+;; H
+  (assert
+
+  (forall ((temp___borrowed_236 us_rep2))
+  (forall ((temp___brower_235 us_rep1))
+   (=>
+     (and
+     (and
+     (= (us_pledge_get (test_route__nth_point__pledge o2 n) temp___borrowed_236
+        temp___brower_235) true)
+     (not
+     (= (rec__test_route__point_acc__is_null_pointer temp___brower_235) true)))
+     (and
+     (= r__is_null_pointer (rec__test_route__route_acc__is_null_pointer
+                           temp___borrowed_236))
+     (= (rec__test_route__point_acc__is_null_pointer
+        test_route__shift_nth_x__p__assume) (rec__test_route__point_acc__is_null_pointer
+                                            temp___brower_235))))
+     (= (length temp___borrowed_236) (length o2))))))
+							     
+(assert (not (=>
+     (and
+     (and
+     (= (us_pledge_get (test_route__nth_point__pledge o2 n) temp___borrowed_250
+        temp___brower_249) true)
+     (not
+     (= (rec__test_route__point_acc__is_null_pointer temp___brower_249) true)))
+     (and
+     (= r__is_null_pointer (rec__test_route__route_acc__is_null_pointer
+                           temp___borrowed_250))
+     (= (rec__test_route__point_acc__is_null_pointer
+        test_route__shift_nth_x__p__assume) (rec__test_route__point_acc__is_null_pointer
+                                            temp___brower_249))))
+     (= (length temp___borrowed_250) (length o2)))))
+
+(check-sat)