From b61070cf03c30abe3ba5956596b88464053ff358 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 3 Jun 2021 07:39:55 -0700 Subject: [PATCH] Renaming pow2 to p2 in regression tests (#6675) We plan to add a unary pow2 operator to cvc5, that is obtained from the binary operator pow by fixing the first argument to 2. An initial working branch is here: https://github.com/yoni206/cvc5/tree/pow2 This PR does the first step, which is to rename some uninterpreted symbols in regression tests from pow2 to p2, to avoid clashing with the new operator. --- test/regress/regress1/fmf/pow2-bool.smt2 | 6 ++-- .../sygus-inst-ufnia-sat-t3_rw1505.smt2 | 30 +++++++++---------- .../regress2/nl/ufnia-factor-open-proof.smt2 | 12 ++++---- 3 files changed, 24 insertions(+), 24 deletions(-) diff --git a/test/regress/regress1/fmf/pow2-bool.smt2 b/test/regress/regress1/fmf/pow2-bool.smt2 index 93814578d..b92aec228 100644 --- a/test/regress/regress1/fmf/pow2-bool.smt2 +++ b/test/regress/regress1/fmf/pow2-bool.smt2 @@ -2,16 +2,16 @@ ; EXPECT: sat (set-logic ALL) -(define-fun-rec pow2 ((n Int) (p Int)) Bool ( +(define-fun-rec p2 ((n Int) (p Int)) Bool ( or (and (= n 0) (= p 1)) - (and (> n 0) (> p 1) (= 0 (mod p 2)) (pow2 (- n 1) (div p 2))) + (and (> n 0) (> p 1) (= 0 (mod p 2)) (p2 (- n 1) (div p 2))) )) (declare-const n Int) (declare-const p Int) (assert (= n 10)) -(assert (pow2 n p)) +(assert (p2 n p)) (check-sat) diff --git a/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 b/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 index 1dae93eb5..39790c38d 100644 --- a/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 +++ b/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 @@ -11,36 +11,36 @@ Publications: "Towards Bit-Width-Independent Proofs in SMT Solvers " by A. Nieme (set-info :license "https://creativecommons.org/licenses/by/4.0/") (set-info :category "crafted") (set-info :status sat) -(declare-fun pow2 (Int) Int) +(declare-fun p2 (Int) Int) (declare-fun intand (Int Int Int) Int) (declare-fun intor (Int Int Int) Int) (declare-fun intxor (Int Int Int) Int) -(define-fun bitof ((k Int) (l Int) (a Int)) Int (mod (div a (pow2 l)) 2)) -(define-fun int_all_but_msb ((k Int) (a Int)) Int (mod a (pow2 (- k 1)))) -(define-fun intmax ((k Int)) Int (- (pow2 k) 1)) +(define-fun bitof ((k Int) (l Int) (a Int)) Int (mod (div a (p2 l)) 2)) +(define-fun int_all_but_msb ((k Int) (a Int)) Int (mod a (p2 (- k 1)))) +(define-fun intmax ((k Int)) Int (- (p2 k) 1)) (define-fun intmin ((k Int)) Int 0) (define-fun in_range ((k Int) (x Int)) Bool (and (>= x 0) (<= x (intmax k)))) -(define-fun intudivtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) (- (pow2 k) 1) (div a b) )) +(define-fun intudivtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) (- (p2 k) 1) (div a b) )) (define-fun intmodtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b))) -(define-fun intneg ((k Int) (a Int)) Int (intmodtotal k (- (pow2 k) a) (pow2 k))) +(define-fun intneg ((k Int) (a Int)) Int (intmodtotal k (- (p2 k) a) (p2 k))) (define-fun intnot ((k Int) (a Int)) Int (- (intmax k) a)) -(define-fun intmins ((k Int)) Int (pow2 (- k 1))) +(define-fun intmins ((k Int)) Int (p2 (- k 1))) (define-fun intmaxs ((k Int)) Int (intnot k (intmins k))) -(define-fun intshl ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a (pow2 b)) (pow2 k))) -(define-fun intlshr ((k Int) (a Int) (b Int)) Int (intmodtotal k (intudivtotal k a (pow2 b)) (pow2 k))) +(define-fun intshl ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a (p2 b)) (p2 k))) +(define-fun intlshr ((k Int) (a Int) (b Int)) Int (intmodtotal k (intudivtotal k a (p2 b)) (p2 k))) (define-fun intashr ((k Int) (a Int) (b Int) ) Int (ite (= (bitof k (- k 1) a) 0) (intlshr k a b) (intnot k (intlshr k (intnot k a) b)))) -(define-fun intconcat ((k Int) (m Int) (a Int) (b Int)) Int (+ (* a (pow2 m)) b)) -(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (pow2 k))) -(define-fun intmul ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a b) (pow2 k))) +(define-fun intconcat ((k Int) (m Int) (a Int) (b Int)) Int (+ (* a (p2 m)) b)) +(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (p2 k))) +(define-fun intmul ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a b) (p2 k))) (define-fun intsub ((k Int) (a Int) (b Int)) Int (intadd k a (intneg k b))) (define-fun unsigned_to_signed ((k Int) (x Int)) Int (- (* 2 (int_all_but_msb k x)) x)) (define-fun intslt ((k Int) (a Int) (b Int)) Bool (< (unsigned_to_signed k a) (unsigned_to_signed k b)) ) (define-fun intsgt ((k Int) (a Int) (b Int)) Bool (> (unsigned_to_signed k a) (unsigned_to_signed k b)) ) (define-fun intsle ((k Int) (a Int) (b Int)) Bool (<= (unsigned_to_signed k a) (unsigned_to_signed k b)) ) (define-fun intsge ((k Int) (a Int) (b Int)) Bool (>= (unsigned_to_signed k a) (unsigned_to_signed k b)) ) -(define-fun pow2_base_cases () Bool (and (= (pow2 0) 1) (= (pow2 1) 2) (= (pow2 2) 4) (= (pow2 3) 8) ) ) +(define-fun p2_base_cases () Bool (and (= (p2 0) 1) (= (p2 1) 2) (= (p2 2) 4) (= (p2 3) 8) ) ) ;qf axioms -(define-fun pow2_ax () Bool pow2_base_cases) +(define-fun p2_ax () Bool p2_base_cases) (define-fun and_ax ((k Int)) Bool true) (define-fun or_ax ((k Int)) Bool true) (define-fun xor_ax ((k Int)) Bool true) @@ -59,7 +59,7 @@ Publications: "Towards Bit-Width-Independent Proofs in SMT Solvers " by A. Nieme ; problem start -(assert pow2_ax) +(assert p2_ax) (assert (not (forall ((s Int) (t Int) (k Int)) (=> (and (is_bv_var k s) (is_bv_var k t) (is_bv_width k)) diff --git a/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 index 6d910b464..dc61155e8 100644 --- a/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 +++ b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 @@ -1,15 +1,15 @@ ; COMMAND-LINE: --no-check-unsat-cores (set-logic QF_UFNIA) (set-info :status unsat) -(declare-fun pow2 (Int) Int) -(define-fun intmax ((k Int)) Int (- (pow2 k) 1)) -(define-fun intmodtotal ((pow2 Int) (a Int) (b Int)) Int (mod a b)) +(declare-fun p2 (Int) Int) +(define-fun intmax ((k Int)) Int (- (p2 k) 1)) +(define-fun intmodtotal ((p2 Int) (a Int) (b Int)) Int (mod a b)) (define-fun intneg ((k Int) (a Int)) Int 1) -(define-fun intmul ((k Int) (a Int) (b Int)) Int (mod (* a b) (pow2 k))) +(define-fun intmul ((k Int) (a Int) (b Int)) Int (mod (* a b) (p2 k))) (declare-fun k () Int) (assert (> k 0)) -(assert (= 1 (pow2 1))) +(assert (= 1 (p2 1))) (declare-fun %x () Int) (assert (> %x 0)) -(assert (not (= (intmul k %x (intmax k)) (mod (- (pow2 k) %x) (pow2 k))))) +(assert (not (= (intmul k %x (intmax k)) (mod (- (p2 k) %x) (p2 k))))) (check-sat) -- 2.30.2