From dc99f1c45f616a93ee84b2a6ba877518206bdbaf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 2 Dec 2019 13:02:01 -0600 Subject: [PATCH] Update ownership policy for dynamic quantifiers splitting (#3493) --- src/theory/quantifiers/quant_split.cpp | 40 +- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/issue3481.smt2 | 495 ++++++++++++++++++ 3 files changed, 523 insertions(+), 13 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue3481.smt2 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; iisFiniteBound( 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) -- 2.30.2