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.

diff --git a/test/regress/regress1/fmf/pow2-bool.smt2 b/test/regress/regress1/fmf/pow2-bool.smt2
index 93814578dae54415ab0a06f6dd0f35f2a1bb0eae..b92aec2285dc8a77bdbfddb229fec78a9df8ebce 100644 (file)
--- 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 1dae93eb5b22df4f103ae3c7dbdc6655f6973bb5..39790c38dff42503846344e1aa2df056dc52165b 100644 (file)
--- 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 6d910b4646f83d9ae86b65cac351fb52e22c6a1c..dc61155e8c30fe3ea21f33fc67dc509bd167f269 100644 (file)
--- 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)