diff options
Diffstat (limited to 'test')
139 files changed, 1307 insertions, 845 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index d3ff709ca..5f96d2b9b 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -41,8 +41,3 @@ add_subdirectory(api EXCLUDE_FROM_ALL) if(ENABLE_UNIT_TESTING) add_subdirectory(unit EXCLUDE_FROM_ALL) endif() - -# add Python bindings tests if building with Python bindings -if (BUILD_BINDINGS_PYTHON) - add_subdirectory(python) -endif() diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt deleted file mode 100644 index 5b681ca36..000000000 --- a/test/python/CMakeLists.txt +++ /dev/null @@ -1,37 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Yoni Zohar, Aina Niemetz, Mathias Preiner -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -# -# The build system configuration. -## - -# Check if the pytest Python module is installed. -check_python_module("pytest") - -# Add Python bindings API tests. -macro(cvc5_add_python_api_test name filename) -# We create test target 'python/unit/api/myapitest' and run it with -# 'ctest -R "python/unit/api/myapitest"'. -add_test (NAME python/unit/api/${name} - COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} - # directory for importing the python bindings - WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) -endmacro() - -# add specific test files -cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py) -cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py) -cvc5_add_python_api_test(pytest_term unit/api/test_term.py) -cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py) -cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) -cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py) -cvc5_add_python_api_test(pytest_op unit/api/test_op.py) -cvc5_add_python_api_test(pytest_result unit/api/test_result.py) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b08b2f6f5..bffb3e8cb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -109,6 +109,7 @@ set(regress_0_tests regress0/arrays/issue3813-massign-assert.smt2 regress0/arrays/issue3814.smt2 regress0/arrays/issue4927-unsat-cores.smt2 + regress0/arrays/issue7596-define-array-uminus.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 regress0/arrays/x3.smtv1.smt2 @@ -659,11 +660,14 @@ set(regress_0_tests regress0/ho/issue6536.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 + regress0/ho/lazy-lambda-model.smt2 regress0/ho/match-middle.smt2 regress0/ho/modulo-func-equality.smt2 regress0/ho/qgu-fuzz-ho-1-dd.smt2 regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 regress0/ho/shadowing-defs.smt2 + regress0/ho/simple-conf-lazy-lambda-lift.smt2 + regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 regress0/ho/trans.smt2 @@ -1083,6 +1087,7 @@ set(regress_0_tests regress0/seq/issue5665-invalid-model.smt2 regress0/seq/issue6337-seq.smt2 regress0/seq/len_simplify.smt2 + regress0/seq/proj-issue340.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 @@ -1599,9 +1604,11 @@ set(regress_1_tests regress1/bags/fuzzy3.smt2 regress1/bags/fuzzy4.smt2 regress1/bags/fuzzy5.smt2 + regress1/bags/fuzzy6.smt2 regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 + regress1/bags/map-lazy-lam.smt2 regress1/bags/map1.smt2 regress1/bags/map2.smt2 regress1/bags/map3.smt2 @@ -1726,8 +1733,10 @@ set(regress_1_tests regress1/fmf/with-ind-104-core.smt2 regress1/gensys_brn001.smt2 regress1/ho/bug_freeVar_BDD_General_data_270.p + regress1/ho/bug_freevar_PHI004^4-delta.smt2 regress1/ho/bound_var_bug.p regress1/ho/fta0328.lfho.p + regress1/ho/ho-fun-sharing-dd.smt2 regress1/ho/issue3136-fconst-bool-bool.smt2 regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 @@ -2803,8 +2812,6 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # disabled temporarily until lazy lambda handling is merged - regress1/ho/bug_freevar_PHI004^4-delta.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers diff --git a/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 new file mode 100644 index 000000000..da21db28e --- /dev/null +++ b/test/regress/regress0/arrays/issue7596-define-array-uminus.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1))) +(assert (= (select foo 0) (- 1))) +(check-sat) diff --git a/test/regress/regress0/ho/lazy-lambda-model.smt2 b/test/regress/regress0/ho/lazy-lambda-model.smt2 new file mode 100644 index 000000000..71df017e9 --- /dev/null +++ b/test/regress/regress0/ho/lazy-lambda-model.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --uf-lazy-ll +; EXPECT: sat +(set-logic HO_ALL) +(declare-fun g (Int) Int) +(declare-fun h (Int) Int) +(define-fun f ((x Int)) Int (ite (> x 0) (* 2 x) x)) + +(declare-fun a () Int) +(declare-fun b () Int) + + +(assert (or (= f g) (= f h))) + +(assert (and (= (h a) 26) (= (g b) 26))) + +(check-sat) diff --git a/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 new file mode 100644 index 000000000..ab949c40c --- /dev/null +++ b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --uf-lazy-ll +; EXPECT: unsat +(set-logic HO_ALL) +(set-info :status unsat) +(define-fun f ((x Int)) Int (+ x 1)) +(declare-fun g (Int) Int) +(declare-fun h (Int) Int) + +(assert (or (= f g) (= f h))) + +(assert (= (g 4) 0)) +(assert (= (h 4) 8)) + +(check-sat) diff --git a/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 new file mode 100644 index 000000000..d11a4418b --- /dev/null +++ b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --uf-lazy-ll +; EXPECT: unsat +(set-logic HO_ALL) +(set-info :status unsat) +(define-fun f ((x Int)) Int (+ x 1)) +(define-fun g ((x Int)) Int (+ x 2)) +(define-fun h ((x Int)) Int 6) + +(assert (or (= f g) (= f h))) + +(check-sat) diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 index 70488b4eb..9bc85f268 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc.smt2 +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -33,7 +33,7 @@ (assert (set.member t_tup Target)) (assert (set.subset (rel.join (rel.join Book addr) Target) Name)) (assert (set.subset (rel.join Book names) Name)) -(assert (= (set.intersection Name Addr) (as set.empty (Set (Tuple Atom))))) +(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom))))) (assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup))))) diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2 index 1cdeffbff..75dc80d22 100644 --- a/test/regress/regress0/rels/iden_0.cvc.smt2 +++ b/test/regress/regress0/rels/iden_0.cvc.smt2 @@ -21,5 +21,5 @@ (assert (set.member v x)) (assert (set.member a x)) (assert (= id (rel.iden t))) -(assert (not (set.member (tuple 1 1) (set.intersection id x)))) +(assert (not (set.member (tuple 1 1) (set.inter id x)))) (check-sat) diff --git a/test/regress/regress0/seq/proj-issue340.smt2 b/test/regress/regress0/seq/proj-issue340.smt2 new file mode 100644 index 000000000..75a4fb3a6 --- /dev/null +++ b/test/regress/regress0/seq/proj-issue340.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(declare-const x0 Bool) +(declare-const x2 (Seq Bool)) +(declare-const i Int) +(assert (= i (str.to_int (str.from_code (seq.len x2))))) +(assert (not (seq.nth x2 i))) +(assert (>= i 0)) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2 index 20cfb36f8..2046b2fc9 100644 --- a/test/regress/regress0/sets/complement3.cvc.smt2 +++ b/test/regress/regress0/sets/complement3.cvc.smt2 @@ -8,7 +8,7 @@ (declare-fun C4 () (Set (Tuple Atom))) (declare-fun ATOM_UNIV () (Set (Tuple Atom))) (declare-fun V1 () Atom) -(assert (= C32 (set.intersection (set.complement C2) (set.complement C4)))) +(assert (= C32 (set.inter (set.complement C2) (set.complement C4)))) (assert (set.member (tuple V1) (set.complement C32))) (assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom))))) (assert (set.member (tuple V1) ATOM_UNIV)) diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2 index 9ee199b43..9c89df0c6 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc.smt2 +++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2 @@ -20,12 +20,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b))) -(assert (not (= c (set.intersection a b)))) +(assert (not (= c (set.inter a b)))) (assert (= c (set.minus a b))) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (push 1) (assert true) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index 0ecd32bf8..c93b18857 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -10,9 +10,9 @@ (declare-fun H () (Set Int) ) (declare-fun I () (Set Int) ) (declare-fun x () Int) -(assert (set.member x (set.intersection (set.union A B) C))) +(assert (set.member x (set.inter (set.union A B) C))) (assert (not (set.member x G))) (assert (= (set.union A B) D)) -(assert (= C (set.intersection E F))) +(assert (= C (set.inter E F))) (assert (and (= F H) (= G H) (= H I))) (check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index 7e2f627ae..76592a691 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index f6fd4bd53..b0172db39 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 index f70d59b16..1538a2e9f 100644 --- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -66,7 +66,7 @@ (assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_38$0 sk_?X_37$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_38$0 sk_?X_37$0)) :named precondition_of_rec_copy_loop_34_11_19)) (assert (! (= old_cp_2$0 cp$0) :named assign_41_4)) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index 6857e5147..66f843c9d 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -5,7 +5,7 @@ (declare-fun b () (Set Int)) (declare-fun x () Int) ;(assert (not (set.member x a))) -(assert (set.member x (set.intersection a b))) +(assert (set.member x (set.inter a b))) (assert (not (set.member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 4a49bef07..0020e5c55 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -8,7 +8,7 @@ (declare-fun x () Int) (assert (set.member x (set.union A B))) -(assert (not (set.member x (set.intersection A B)))) +(assert (not (set.member x (set.inter A B)))) (assert (not (set.member x (set.minus A B)))) ;(assert (not (set.member x (set.minus B A)))) ;(assert (set.member x B)) diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 index 20832c573..00546eee2 100644 --- a/test/regress/regress0/sets/sets-poly-int-real.smt2 +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -11,7 +11,7 @@ (assert (= t1 (set.union s (set.singleton 2.5)))) (assert (= t2 (set.union s (set.singleton 2.0)))) (assert (= t3 (set.union r3 (set.singleton 2.5)))) -(assert (= (set.intersection r1 r2) (set.intersection s (set.singleton 0.0)))) +(assert (= (set.inter r1 r2) (set.inter s (set.singleton 0.0)))) (assert (not (= r1 (as set.empty (Set Real))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 3dcafae08..4a11bcc78 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -15,12 +15,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b) )) -(assert (not (= c (set.intersection a b) ))) +(assert (not (= c (set.inter a b) ))) (assert (= c (set.minus a b) )) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (check-sat) (pop 1) diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2 index be746be1d..a591792cf 100644 --- a/test/regress/regress0/sets/sharing-simp.smt2 +++ b/test/regress/regress0/sets/sharing-simp.smt2 @@ -9,7 +9,7 @@ (assert (set.member x A)) (assert (set.member y B)) -(assert (or (= C (set.intersection A B)) (= D (set.intersection A B)))) +(assert (or (= C (set.inter A B)) (= D (set.inter A B)))) (check-sat) diff --git a/test/regress/regress1/bags/choose1.smt2 b/test/regress/regress1/bags/choose1.smt2 index b157bbc70..53cd7c771 100644 --- a/test/regress/regress1/bags/choose1.smt2 +++ b/test/regress/regress1/bags/choose1.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (= (bag.choose A) 10)) (assert (= a (bag.choose A))) (assert (exists ((x Int)) (and (= x (bag.choose A)) (= x a)))) diff --git a/test/regress/regress1/bags/choose3.smt2 b/test/regress/regress1/bags/choose3.smt2 index ffa9ae9a7..adf1a3e21 100644 --- a/test/regress/regress1/bags/choose3.smt2 +++ b/test/regress/regress1/bags/choose3.smt2 @@ -4,5 +4,5 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (assert (= (bag.choose A) 10)) -(assert (= A (as emptybag (Bag Int)))) +(assert (= A (as bag.empty (Bag Int)))) (check-sat) diff --git a/test/regress/regress1/bags/choose4.smt2 b/test/regress/regress1/bags/choose4.smt2 index a0290b90b..cdf4065d4 100644 --- a/test/regress/regress1/bags/choose4.smt2 +++ b/test/regress/regress1/bags/choose4.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (> (bag.count 10 A) 0)) (assert (= a (bag.choose A))) (check-sat) diff --git a/test/regress/regress1/bags/difference_remove1.smt2 b/test/regress/regress1/bags/difference_remove1.smt2 index f5a87c149..82f6ec53d 100644 --- a/test/regress/regress1/bags/difference_remove1.smt2 +++ b/test/regress/regress1/bags/difference_remove1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal1.smt2 b/test/regress/regress1/bags/duplicate_removal1.smt2 index 2b662c6e5..27ce2360b 100644 --- a/test/regress/regress1/bags/duplicate_removal1.smt2 +++ b/test/regress/regress1/bags/duplicate_removal1.smt2 @@ -3,6 +3,6 @@ (set-option :produce-models true) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal2.smt2 b/test/regress/regress1/bags/duplicate_removal2.smt2 index 7dacaae43..5382f773f 100644 --- a/test/regress/regress1/bags/duplicate_removal2.smt2 +++ b/test/regress/regress1/bags/duplicate_removal2.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) -(assert (= B (union_max A B))) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) +(assert (= B (bag.union_max A B))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/emptybag1.smt2 b/test/regress/regress1/bags/emptybag1.smt2 index f7f92599d..61b29f414 100644 --- a/test/regress/regress1/bags/emptybag1.smt2 +++ b/test/regress/regress1/bags/emptybag1.smt2 @@ -4,7 +4,7 @@ (declare-fun x () String) (declare-fun y () Int) (assert (= x "x")) -(assert (= A (as emptybag (Bag String)))) +(assert (= A (as bag.empty (Bag String)))) (assert (= (bag.count x A) y)) (assert(> y 1)) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2 index f9fee0ec4..79ccc4b82 100644 --- a/test/regress/regress1/bags/fuzzy1.smt2 +++ b/test/regress/regress1/bags/fuzzy1.smt2 @@ -5,6 +5,6 @@ (declare-fun c () Int) ; c here is zero (assert (and - (= b (difference_subtract b a)) ; b is empty + (= b (bag.difference_subtract b a)) ; b is empty (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|} (check-sat) diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2 index 31da47f53..c7968b274 100644 --- a/test/regress/regress1/bags/fuzzy2.smt2 +++ b/test/regress/regress1/bags/fuzzy2.smt2 @@ -8,8 +8,8 @@ (let ((D (bag d c))) ; when c = zero, then D is empty (and (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty - (= a (union_max a D)) - (= a (difference_subtract a (bag d 1))) - (= a (union_disjoint a D)) - (= a (intersection_min a D))))) + (= a (bag.union_max a D)) + (= a (bag.difference_subtract a (bag d 1))) + (= a (bag.union_disjoint a D)) + (= a (bag.inter_min a D))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy3.smt2 b/test/regress/regress1/bags/fuzzy3.smt2 index dd6dd02dc..a457bf9ae 100644 --- a/test/regress/regress1/bags/fuzzy3.smt2 +++ b/test/regress/regress1/bags/fuzzy3.smt2 @@ -8,6 +8,6 @@ (assert (not (= - (= A (difference_remove (bag d c) A)) + (= A (bag.difference_remove (bag d c) A)) (= A (bag (tuple c c) c))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2 index b733a4862..5b24b8d6e 100644 --- a/test/regress/regress1/bags/fuzzy4.smt2 +++ b/test/regress/regress1/bags/fuzzy4.smt2 @@ -7,8 +7,8 @@ (assert (not (= - (= A (bag d (+ c (bag.count d (union_disjoint A A))))) - (= A (difference_remove (bag d c) A))))) + (= A (bag d (+ c (bag.count d (bag.union_disjoint A A))))) + (= A (bag.difference_remove (bag d c) A))))) (assert (= A (bag (tuple 0 0) 5))) (assert (= c (- 5))) (assert (= d (tuple 0 0))) diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2 index 2dea236a5..0674fad9c 100644 --- a/test/regress/regress1/bags/fuzzy5.smt2 +++ b/test/regress/regress1/bags/fuzzy5.smt2 @@ -10,7 +10,7 @@ (and (not (= (= A (bag (tuple 0 c) (+ c c))) - (= A (difference_remove (bag d c) A)))) + (= A (bag.difference_remove (bag d c) A)))) (not (= (= A (bag (tuple 0 1) c_plus_1)) (= A (bag (tuple c 1) c_plus_1))))))) diff --git a/test/regress/regress1/bags/fuzzy6.smt2 b/test/regress/regress1/bags/fuzzy6.smt2 new file mode 100644 index 000000000..2bcc024dd --- /dev/null +++ b/test/regress/regress1/bags/fuzzy6.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert + (let ((double_c (+ c c))) + (let ((formula (= A (bag (tuple c double_c) c)))) + (and (not (= formula (= A (bag (tuple c c) c)))) + (not (= formula (= A (bag (tuple 0 c) double_c)))))))) + +(check-sat) diff --git a/test/regress/regress1/bags/intersection_min1.smt2 b/test/regress/regress1/bags/intersection_min1.smt2 index f5a515b9c..0ced4aa89 100644 --- a/test/regress/regress1/bags/intersection_min1.smt2 +++ b/test/regress/regress1/bags/intersection_min1.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (assert (distinct A B C)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/intersection_min2.smt2 b/test/regress/regress1/bags/intersection_min2.smt2 index 66afa2f3a..119f34665 100644 --- a/test/regress/regress1/bags/intersection_min2.smt2 +++ b/test/regress/regress1/bags/intersection_min2.smt2 @@ -3,7 +3,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (= C (union_disjoint A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (= C (bag.union_disjoint A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (check-sat) diff --git a/test/regress/regress1/bags/issue5759.smt2 b/test/regress/regress1/bags/issue5759.smt2 index ba3752e09..1c29afea6 100644 --- a/test/regress/regress1/bags/issue5759.smt2 +++ b/test/regress/regress1/bags/issue5759.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag Int)) (declare-fun B () (Bag Int)) (declare-fun x () Int) -(assert (not (= A (union_max (bag x 1) (bag 0 1))))) -(assert (= A (union_disjoint B (bag 0 1)))) +(assert (not (= A (bag.union_max (bag x 1) (bag 0 1))))) +(assert (= A (bag.union_disjoint B (bag 0 1)))) (assert (= x 1)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/map-lazy-lam.smt2 b/test/regress/regress1/bags/map-lazy-lam.smt2 new file mode 100644 index 000000000..c99bab7c9 --- /dev/null +++ b/test/regress/regress1/bags/map-lazy-lam.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --fmf-bound --uf-lazy-ll +; EXPECT: sat +(set-logic HO_ALL) +(define-fun f ((x String)) Int 1) +(define-fun cardinality ((A (Bag String))) Int + (bag.count 1 (bag.map f A))) +(declare-fun A () (Bag String)) +(assert (= (cardinality A) 20)) +(check-sat) diff --git a/test/regress/regress1/bags/map1.smt2 b/test/regress/regress1/bags/map1.smt2 index 54d671415..c7dc3d636 100644 --- a/test/regress/regress1/bags/map1.smt2 +++ b/test/regress/regress1/bags/map1.smt2 @@ -5,8 +5,8 @@ (declare-fun x () Int) (declare-fun y () Int) (declare-fun f (Int) Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) (assert (= B (bag.map f A))) (assert (distinct (f x) (f y) x y)) (check-sat) diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2 index 637815fa5..ae0184008 100644 --- a/test/regress/regress1/bags/map3.smt2 +++ b/test/regress/regress1/bags/map3.smt2 @@ -6,5 +6,5 @@ (define-fun f ((x Int)) Int (+ x 1)) (assert (= B (bag.map f A))) (assert (= (bag.count (- 2) B) 57)) -(assert (= A (as emptybag (Bag Int)) )) +(assert (= A (as bag.empty (Bag Int)) )) (check-sat) diff --git a/test/regress/regress1/bags/subbag1.smt2 b/test/regress/regress1/bags/subbag1.smt2 index 055e47a17..7a6bf66d7 100644 --- a/test/regress/regress1/bags/subbag1.smt2 +++ b/test/regress/regress1/bags/subbag1.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (assert (= x 1)) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) 5)) (assert (= (bag.count x B) 10)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/subbag2.smt2 b/test/regress/regress1/bags/subbag2.smt2 index 6d5cde362..abdb3b7d9 100644 --- a/test/regress/regress1/bags/subbag2.smt2 +++ b/test/regress/regress1/bags/subbag2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) x)) (assert (= (bag.count y A) x)) (assert (distinct x y)) diff --git a/test/regress/regress1/bags/union_disjoint.smt2 b/test/regress/regress1/bags/union_disjoint.smt2 index d30ed4b14..fdb9d16d3 100644 --- a/test/regress/regress1/bags/union_disjoint.smt2 +++ b/test/regress/regress1/bags/union_disjoint.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_disjoint (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_disjoint (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/union_max1.smt2 b/test/regress/regress1/bags/union_max1.smt2 index d278527b9..d41e1425a 100644 --- a/test/regress/regress1/bags/union_max1.smt2 +++ b/test/regress/regress1/bags/union_max1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/union_max2.smt2 b/test/regress/regress1/bags/union_max2.smt2 index dd4bceff5..1366130bf 100644 --- a/test/regress/regress1/bags/union_max2.smt2 +++ b/test/regress/regress1/bags/union_max2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) -(assert (distinct (as emptybag (Bag Int)) B)) +(assert (distinct (as bag.empty (Bag Int)) B)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 7c9de4c49..0155eecb2 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find -q --decision=justification-old +; COMMAND-LINE: --finite-model-find --decision=justification-old --uf-lazy-ll -q ; EXPECT: sat (set-logic HO_ALL) diff --git a/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 b/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 new file mode 100644 index 000000000..300dc26de --- /dev/null +++ b/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +(set-logic HO_ALL) +(declare-sort n 0) +(declare-fun x () n) +(declare-fun s (n) n) +(declare-fun t ((-> n Bool)) Bool) +(assert (forall ((X n)) (t (lambda ((Xu n)) (= X (s Xu)))))) +(assert (not (t (lambda ((Xu n)) (= x (s Xu)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/set8.smt2 b/test/regress/regress1/quantifiers/set8.smt2 index 209b213c1..17eea7b0a 100644 --- a/test/regress/regress1/quantifiers/set8.smt2 +++ b/test/regress/regress1/quantifiers/set8.smt2 @@ -15,12 +15,12 @@ (assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (set.subset ?s1 ?s2) (set.subset ?s2 ?s1))))) (declare-fun union (Set Set) Set) (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (union ?s1 ?s2)) (or (set.member ?x ?s1) (set.member ?x ?s2))))) -(declare-fun set.intersection (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.intersection ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2))))) +(declare-fun set.inter (Set Set) Set) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.inter ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2))))) (declare-fun difference (Set Set) Set) (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (difference ?s1 ?s2)) (and (set.member ?x ?s1) (not (set.member ?x ?s2)))))) (declare-fun a () Set) (declare-fun b () Set) -(assert (not (seteq (set.intersection a b) (set.intersection b a)))) +(assert (not (seteq (set.inter a b) (set.inter b a)))) (check-sat) (exit) diff --git a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 index 7e80fdd70..8269daf42 100644 --- a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 @@ -20,12 +20,12 @@ (assert (= r (rel.join x y))) (declare-fun e () (Tuple Int Int)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 index 9a35f336e..134a99c73 100644 --- a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 @@ -24,12 +24,12 @@ (assert (= w (set.singleton e))) (assert (set.subset (rel.transpose w) y)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 index fc2d73235..ed894518e 100644 --- a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 @@ -26,12 +26,12 @@ (assert (let ((_let_1 (set.singleton a))) (= w (rel.product _let_1 _let_1)))) (assert (set.subset (rel.transpose w) y)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 index 144566fc5..e5b92a4fc 100644 --- a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 @@ -12,7 +12,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 index 9a2521520..206450142 100644 --- a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index b2732dbd2..fe7e7d7ac 100644 --- a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 index ee24367c3..078b98eef 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 index b0cfe4888..756f0430c 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 index 9ac15e9a4..1e45c21e9 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v66 () Int) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 index 68ed72a93..a3fd883b6 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/card-3.smt2 b/test/regress/regress1/sets/card-3.smt2 index 383395b0d..bbcf1c489 100644 --- a/test/regress/regress1/sets/card-3.smt2 +++ b/test/regress/regress1/sets/card-3.smt2 @@ -8,5 +8,5 @@ (assert (>= (set.card (set.union s u)) 8)) (assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (check-sat) diff --git a/test/regress/regress1/sets/card-4.smt2 b/test/regress/regress1/sets/card-4.smt2 index 019b16a09..9f0e96dc5 100644 --- a/test/regress/regress1/sets/card-4.smt2 +++ b/test/regress/regress1/sets/card-4.smt2 @@ -8,7 +8,7 @@ (assert (>= (set.card (set.union s u)) 8)) ;(assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) diff --git a/test/regress/regress1/sets/card-5.smt2 b/test/regress/regress1/sets/card-5.smt2 index c24ca974a..51ad7971c 100644 --- a/test/regress/regress1/sets/card-5.smt2 +++ b/test/regress/regress1/sets/card-5.smt2 @@ -8,7 +8,7 @@ (assert (>= (set.card (set.union s u)) 8)) ;(assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) diff --git a/test/regress/regress1/sets/card-6.smt2 b/test/regress/regress1/sets/card-6.smt2 index b0ef3a3b9..fc2d34acc 100644 --- a/test/regress/regress1/sets/card-6.smt2 +++ b/test/regress/regress1/sets/card-6.smt2 @@ -7,7 +7,7 @@ (assert (and (= (as set.empty (Set E)) - (set.intersection A B)) + (set.inter A B)) (set.subset C (set.union A B)) (>= (set.card C) 5) (<= (set.card A) 2) diff --git a/test/regress/regress1/sets/comp-intersect.smt2 b/test/regress/regress1/sets/comp-intersect.smt2 index 60d9046bd..5f6f7576b 100644 --- a/test/regress/regress1/sets/comp-intersect.smt2 +++ b/test/regress/regress1/sets/comp-intersect.smt2 @@ -9,6 +9,6 @@ (assert (= x (set.comprehension ((z Int)) (> z 4) (* 5 z)))) (assert (= y (set.comprehension ((z Int)) (< z 10) (+ (* 5 z) 1)))) -(assert (not (= (set.intersection x y) (as set.empty (Set Int))))) +(assert (not (= (set.inter x y) (as set.empty (Set Int))))) (check-sat) diff --git a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 index 7c5e09b5a..93d359b60 100644 --- a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 index aa5b62d09..ec82ddb8b 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -7,6 +7,6 @@ (declare-fun universe () (Set Bool)) (assert (= (set.card A) 2)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set Bool)))) +(assert (= (set.inter A B) (as set.empty (Set Bool)))) (assert (= universe (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 index 91bf1905a..0003349b3 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -8,7 +8,7 @@ (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.inter A B)) 2)) (assert (= (set.card (set.minus A B)) 3)) (assert (= (set.card (set.minus B A)) 3)) (assert (= universe (as set.universe (Set (_ BitVec 3))))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 index adbe51507..5808c4ec7 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -9,7 +9,7 @@ (assert (= (set.card A) 3)) (assert (= (set.card B) 3)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= (set.card (set.minus A B)) 2)) (assert (= (set.card (set.minus B A)) 2)) (assert (not (set.member x A))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 index 2ccbc8a58..81c49e1e3 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -9,7 +9,7 @@ (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.inter A B)) 2)) (assert (= (set.card (set.minus A B)) 3)) (assert (= (set.card (set.minus B A)) 3)) (assert (= universe (as set.universe (Set (_ BitVec 3))))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 index 4c113c84b..62c0bc224 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -9,6 +9,6 @@ (declare-fun x () Rec) (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 index 4c9bdadd5..70e3a88d8 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -8,6 +8,6 @@ (declare-fun universe () (Set Rec)) (assert (= (set.card A) 9)) (assert (= (set.card B) 9)) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/fuzz14418.smt2 b/test/regress/regress1/sets/fuzz14418.smt2 index 2fb60cb72..b09cf1151 100644 --- a/test/regress/regress1/sets/fuzz14418.smt2 +++ b/test/regress/regress1/sets/fuzz14418.smt2 @@ -34,7 +34,7 @@ (let ((e14 (set.minus v2 v2))) (let ((e15 (f1 v1 v4 v1))) (let ((e16 (f1 e14 v1 v4))) -(let ((e17 (set.intersection e16 e15))) +(let ((e17 (set.inter e16 e15))) (let ((e18 (f1 v4 e15 v2))) (let ((e19 (ite (p1 e13) (set.singleton 1) (set.singleton 0)))) (let ((e20 (set.member v0 e17))) diff --git a/test/regress/regress1/sets/fuzz15201.smt2 b/test/regress/regress1/sets/fuzz15201.smt2 index 3094a8d84..bdcbe7d59 100644 --- a/test/regress/regress1/sets/fuzz15201.smt2 +++ b/test/regress/regress1/sets/fuzz15201.smt2 @@ -29,9 +29,9 @@ (let ((e16 (set.minus v2 v1))) (let ((e17 (set.minus v1 v2))) (let ((e18 (set.union e17 e17))) -(let ((e19 (set.intersection e17 v1))) -(let ((e20 (set.intersection e17 e18))) -(let ((e21 (set.intersection v1 e16))) +(let ((e19 (set.inter e17 v1))) +(let ((e20 (set.inter e17 e18))) +(let ((e21 (set.inter v1 e16))) (let ((e22 (set.minus e20 e16))) (let ((e23 (ite (p1 v2 e18 e21) (set.singleton 1) (set.singleton 0)))) (let ((e24 (set.minus e17 e23))) diff --git a/test/regress/regress1/sets/fuzz31811.smt2 b/test/regress/regress1/sets/fuzz31811.smt2 index e86901f9a..ca028488a 100644 --- a/test/regress/regress1/sets/fuzz31811.smt2 +++ b/test/regress/regress1/sets/fuzz31811.smt2 @@ -28,19 +28,19 @@ (let ((e10 (f0 v0 e8 e8))) (let ((e11 (ite (p1 v1) (set.singleton 1) (set.singleton 0)))) (let ((e12 (set.union v3 v3))) -(let ((e13 (set.intersection v3 v1))) +(let ((e13 (set.inter v3 v1))) (let ((e14 (ite (p1 v3) (set.singleton 1) (set.singleton 0)))) -(let ((e15 (set.intersection v2 e14))) +(let ((e15 (set.inter v2 e14))) (let ((e16 (ite (p1 e11) (set.singleton 1) (set.singleton 0)))) (let ((e17 (ite (p1 v4) (set.singleton 1) (set.singleton 0)))) (let ((e18 (set.union e15 v2))) (let ((e19 (ite (p1 e16) (set.singleton 1) (set.singleton 0)))) -(let ((e20 (set.intersection e18 v3))) +(let ((e20 (set.inter e18 v3))) (let ((e21 (set.minus v4 e12))) (let ((e22 (set.union v3 v2))) (let ((e23 (set.minus e12 v4))) (let ((e24 (set.minus v3 e16))) -(let ((e25 (set.intersection e19 e20))) +(let ((e25 (set.inter e19 e20))) (let ((e26 (ite (p1 e15) (set.singleton 1) (set.singleton 0)))) (let ((e27 (set.minus e17 e15))) (let ((e28 (f1 e23 e12))) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 index f6d032f11..57f4344c6 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 @@ -7,6 +7,6 @@ (assert (= (set.card universe) 3)) (assert (= (set.card A) 2)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= (set.inter A B) (as set.empty (Set (Array Int Int))))) (assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 index d7e6a758c..76828576e 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 @@ -7,6 +7,6 @@ (assert (= (set.card universe) 3)) (assert (= (set.card A) 1)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= (set.inter A B) (as set.empty (Set (Array Int Int))))) (assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 index c649c9be2..2cf5e566d 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 @@ -7,6 +7,6 @@ (declare-const B (Set Int)) (assert (= (set.card A) 6)) (assert (= (set.card B) 5)) -(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= (set.inter A B) (as set.empty (Set Int)))) (assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 index b3958e79e..8668b9c27 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 @@ -7,6 +7,6 @@ (declare-const B (Set Int)) (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) -(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= (set.inter A B) (as set.empty (Set Int)))) (assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/regress1/sets/insert_invariant_37_2.smt2 index cac805531..a8f117062 100644 --- a/test/regress/regress1/sets/insert_invariant_37_2.smt2 +++ b/test/regress/regress1/sets/insert_invariant_37_2.smt2 @@ -723,7 +723,7 @@ (assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) (assert (! (or (= prev_2$0 curr_2$0) - (set.member sk_?e_1$0 (set.intersection sk_?X_4$0 sk_?X_3$0)) + (set.member sk_?e_1$0 (set.inter sk_?X_4$0 sk_?X_3$0)) (and (set.member sk_?e_1$0 sk_FP$0) (not (set.member sk_?e_1$0 FP$0))) (and (set.member sk_?e$0 (set.union c1_2$0 c2_2$0)) (not (set.member sk_?e$0 content$0))) (and (set.member sk_?e$0 c1_2$0) diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 index c39ea09ba..d2ffdbd7c 100644 --- a/test/regress/regress1/sets/issue2904.smt2 +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -21,6 +21,6 @@ (assert (> n (+ (* 2 f) m))) -(assert (>= (set.card (set.minus UNIVERALSET (set.intersection (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) +(assert (>= (set.card (set.minus UNIVERALSET (set.inter (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 index fd3bd62eb..f57837d05 100644 --- a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 @@ -2,6 +2,6 @@ (set-info :status unsat) (declare-fun st1 () (Set Int)) (declare-fun st7 () (Set Int)) -(assert (> 0 (set.card (set.intersection st1 (set.union st7 st1))))) +(assert (> 0 (set.card (set.inter st1 (set.union st7 st1))))) (assert (set.subset st1 st7)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 index bc2f103d2..55b4ac581 100644 --- a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun st3 () (Set String)) (declare-fun st9 () (Set String)) -(assert (set.is_singleton (set.intersection st3 st9))) -(assert (< 1 (set.card (set.intersection st3 st9)))) +(assert (set.is_singleton (set.inter st3 st9))) +(assert (< 1 (set.card (set.inter st3 st9)))) (assert (set.is_singleton st9)) (check-sat) diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2 index f7a720436..76e27f5b0 100644 --- a/test/regress/regress1/sets/issue4391-card-lasso.smt2 +++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2 @@ -11,6 +11,6 @@ (assert (= (set.card b) d)) (assert (= (set.card c) 0)) (assert (= 0 (mod 0 d))) -(assert (> (set.card (set.minus e (set.intersection (set.intersection e b) (set.minus e c)))) 1)) +(assert (> (set.card (set.minus e (set.inter (set.inter e b) (set.minus e c)))) 1)) (check-sat) diff --git a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 index ae71a1edb..a5ee519f5 100644 --- a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 @@ -27,7 +27,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/remove_check_free_31_6.smt2 b/test/regress/regress1/sets/remove_check_free_31_6.smt2 index c2ff1da23..9c2bc9be7 100644 --- a/test/regress/regress1/sets/remove_check_free_31_6.smt2 +++ b/test/regress/regress1/sets/remove_check_free_31_6.smt2 @@ -230,7 +230,7 @@ (assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) :named invariant_18_4_69)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_27$0 sk_?X_28$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_27$0 sk_?X_28$0)) :named invariant_18_4_70)) (assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) @@ -246,7 +246,7 @@ (assert (! (= FP_2$0 (set.union (set.minus FP$0 FP_1$0) - (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) + (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) :named framecondition_of_remove_loop_18_4_17)) (assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) @@ -311,7 +311,7 @@ (assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_32$0 sk_?X_31$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_32$0 sk_?X_31$0)) :named invariant_18_4_75)) (assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) @@ -320,7 +320,7 @@ :named invariant_18_4_77)) (assert (! (= sk_?X_29$0 - (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) + (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) :named invariant_18_4_78)) (assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 index cf9cbe092..16b44d115 100644 --- a/test/regress/regress1/sym/sym5.smt2 +++ b/test/regress/regress1/sym/sym5.smt2 @@ -13,6 +13,6 @@ (assert (set.subset A (set.insert g h i (set.singleton f)))) (assert (= C (set.minus A B) )) (assert (set.subset B A)) -(assert (= C (set.intersection A B))) +(assert (= C (set.inter A B))) (assert (set.member j C)) (check-sat) diff --git a/test/regress/regress1/trim.cvc.smt2 b/test/regress/regress1/trim.cvc.smt2 index f05e08572..d823e565d 100644 --- a/test/regress/regress1/trim.cvc.smt2 +++ b/test/regress/regress1/trim.cvc.smt2 @@ -18,9 +18,9 @@ (declare-fun ic0_c () (Set myType)) (assert (forall ((r myType)) (=> (set.member r ic0_i) (forall ((r2 myType)) (=> (set.member r2 (neg (select d r))) (set.member r2 ic0_c)))))) (assert (set.subset (set.singleton A) ic0_i)) -(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.intersection ic0_i ic0_c) emptymyTypeSet))) +(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.inter ic0_i ic0_c) emptymyTypeSet))) (declare-fun ic1_i () (Set myType)) (declare-fun ic1_c () (Set myType)) (assert (forall ((r myType)) (=> (set.member r (pos (select d B))) (set.member r ic1_i)))) -(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.intersection ic1_i ic1_c) emptymyTypeSet))) +(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.inter ic1_i ic1_c) emptymyTypeSet))) (check-sat) diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 11c2e8514..9be9dcefa 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -70,7 +70,11 @@ macro(cvc5_add_unit_test is_white name output_dir) if("${output_dir}" STREQUAL "") set(test_name unit/${name}) else() - set(test_name unit/${output_dir}/${name}) + if("${output_dir}" STREQUAL "api") + set(test_name unit/${output_dir}/cpp/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() endif() add_test(${test_name} ${test_bin_dir}/${name}) set_tests_properties(${test_name} PROPERTIES LABELS "unit") diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index ae6db51ef..0701c3ca6 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -13,17 +13,10 @@ # The build system configuration. ## -# Add unit tests. -cvc5_add_unit_test_black(datatype_api_black api) -cvc5_add_unit_test_black(grammar_black api) -cvc5_add_unit_test_black(op_black api) -cvc5_add_unit_test_white(op_white api) -cvc5_add_unit_test_black(result_black api) -cvc5_add_unit_test_black(solver_black api) -cvc5_add_unit_test_white(solver_white api) -cvc5_add_unit_test_black(sort_black api) -cvc5_add_unit_test_black(term_black api) -cvc5_add_unit_test_white(term_white api) +add_subdirectory(cpp) +if (BUILD_BINDINGS_PYTHON) + add_subdirectory(python) +endif() if (BUILD_BINDINGS_JAVA) add_subdirectory(java) endif() diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt new file mode 100644 index 000000000..e99732ca4 --- /dev/null +++ b/test/unit/api/cpp/CMakeLists.txt @@ -0,0 +1,24 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. +## +cvc5_add_unit_test_black(datatype_api_black api) +cvc5_add_unit_test_black(grammar_black api) +cvc5_add_unit_test_black(op_black api) +cvc5_add_unit_test_white(op_white api) +cvc5_add_unit_test_black(result_black api) +cvc5_add_unit_test_black(solver_black api) +cvc5_add_unit_test_white(solver_white api) +cvc5_add_unit_test_black(sort_black api) +cvc5_add_unit_test_black(term_black api) +cvc5_add_unit_test_white(term_white api) diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 745abc17c..745abc17c 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp index 7b7556539..7b7556539 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/cpp/grammar_black.cpp diff --git a/test/unit/api/op_black.cpp b/test/unit/api/cpp/op_black.cpp index fd45b1c22..fd45b1c22 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp diff --git a/test/unit/api/op_white.cpp b/test/unit/api/cpp/op_white.cpp index 39952739b..39952739b 100644 --- a/test/unit/api/op_white.cpp +++ b/test/unit/api/cpp/op_white.cpp diff --git a/test/unit/api/result_black.cpp b/test/unit/api/cpp/result_black.cpp index 9bf6b8491..9bf6b8491 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 79a4aa63e..51a0f38b5 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -15,8 +15,8 @@ #include <algorithm> -#include "test_api.h" #include "base/output.h" +#include "test_api.h" namespace cvc5 { @@ -341,9 +341,12 @@ TEST_F(TestApiBlackSolver, mkBitVector) ASSERT_EQ(d_solver.mkBitVector(8, "0101", 2), d_solver.mkBitVector(8, "00000101", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), + d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), + d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), + d_solver.mkBitVector(4, "1111", 2)); ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111"); ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10), @@ -592,12 +595,11 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal(val4, val4)); } -TEST_F(TestApiBlackSolver, mkRegexpNone) +TEST_F(TestApiBlackSolver, mkRegexpAll) { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); + ASSERT_NO_THROW(d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); } TEST_F(TestApiBlackSolver, mkRegexpAllchar) @@ -608,6 +610,14 @@ TEST_F(TestApiBlackSolver, mkRegexpAllchar) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } +TEST_F(TestApiBlackSolver, mkRegexpNone) +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + ASSERT_NO_THROW( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); +} + TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } TEST_F(TestApiBlackSolver, mkSepNil) @@ -1351,7 +1361,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo) api::OptionInfo info = d_solver.getOptionInfo("verbosity"); EXPECT_EQ("verbosity", info.name); EXPECT_EQ(std::vector<std::string>{}, info.aliases); - EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(info.valueInfo)); + EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>( + info.valueInfo)); auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo); EXPECT_EQ(0, numInfo.defaultValue); EXPECT_EQ(0, numInfo.currentValue); @@ -1362,7 +1373,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo) auto info = d_solver.getOptionInfo("random-freq"); ASSERT_EQ(info.name, "random-freq"); ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"}); - ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(info.valueInfo)); + ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>( + info.valueInfo)); auto ni = std::get<api::OptionInfo::NumberInfo<double>>(info.valueInfo); ASSERT_EQ(ni.currentValue, 0.0); ASSERT_EQ(ni.defaultValue, 0.0); @@ -2540,7 +2552,6 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } - TEST_F(TestApiBlackSolver, issue7000) { Sort s1 = d_solver.getIntegerSort(); diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 5d7b9eacf..5d7b9eacf 100644 --- a/test/unit/api/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index d0c755cf7..d0c755cf7 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp diff --git a/test/unit/api/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 9e52174b4..c76182e47 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -212,6 +212,21 @@ TEST_F(TestApiBlackTerm, getOp) ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); } +TEST_F(TestApiBlackTerm, hasGetSymbol) +{ + Term n; + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + ASSERT_THROW(n.hasSymbol(), CVC5ApiException); + ASSERT_FALSE(t.hasSymbol()); + ASSERT_TRUE(c.hasSymbol()); + + ASSERT_THROW(n.getSymbol(), CVC5ApiException); + ASSERT_THROW(t.getSymbol(), CVC5ApiException); + ASSERT_EQ(c.getSymbol(), "|\\|"); +} + TEST_F(TestApiBlackTerm, isNull) { Term x; @@ -807,10 +822,12 @@ TEST_F(TestApiBlackTerm, getReal) ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value()); ASSERT_EQ("127/10", real5.getRealValue()); - ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), + real6.getReal64Value()); ASSERT_EQ("1/4294967297", real6.getRealValue()); - ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), + real7.getReal64Value()); ASSERT_EQ("4294967297/1", real7.getRealValue()); ASSERT_EQ("1/18446744073709551617", real8.getRealValue()); diff --git a/test/unit/api/term_white.cpp b/test/unit/api/cpp/term_white.cpp index ace5645dc..ace5645dc 100644 --- a/test/unit/api/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 161854421..6a08d79c6 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -639,6 +639,13 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } + @Test void mkRegexpAll() + { + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); + } + @Test void mkRegexpAllchar() { Sort strSort = d_solver.getStringSort(); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index bf0beb024..b7f111428 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -219,6 +219,21 @@ class TermTest Term nilOpTerm = list.getConstructorTerm("nil"); } + @Test void hasGetSymbol() throws CVC5ApiException + { + Term n = d_solver.getNullTerm(); + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + assertThrows(CVC5ApiException.class, () -> n.hasSymbol()); + assertFalse(t.hasSymbol()); + assertTrue(c.hasSymbol()); + + assertThrows(CVC5ApiException.class, () -> n.getSymbol()); + assertThrows(CVC5ApiException.class, () -> t.getSymbol()); + assertEquals(c.getSymbol(), "|\\|"); + } + @Test void isNull() throws CVC5ApiException { Term x = d_solver.getNullTerm(); diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt new file mode 100644 index 000000000..cbf9629ce --- /dev/null +++ b/test/unit/api/python/CMakeLists.txt @@ -0,0 +1,40 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Aina Niemetz, Mathias Preiner +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. +## + +# Check if the pytest Python module is installed. +check_python_module("pytest") + +# Add Python bindings API tests. +macro(cvc5_add_python_api_unit_test name filename) +# We create test target 'python/unit/api/myapitest' and run it with +# 'ctest -R "python/unit/api/myapitest"'. + set(test_name unit/api/python/${name}) + add_test (NAME ${test_name} + COMMAND ${PYTHON_EXECUTABLE} + -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + # directory for importing the python bindings + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") +endmacro() + +# add specific test files +cvc5_add_python_api_unit_test(pytest_solver test_solver.py) +cvc5_add_python_api_unit_test(pytest_sort test_sort.py) +cvc5_add_python_api_unit_test(pytest_term test_term.py) +cvc5_add_python_api_unit_test(pytest_datatype_api test_datatype_api.py) +cvc5_add_python_api_unit_test(pytest_grammar test_grammar.py) +cvc5_add_python_api_unit_test(pytest_to_python_obj test_to_python_obj.py) +cvc5_add_python_api_unit_test(pytest_op test_op.py) +cvc5_add_python_api_unit_test(pytest_result test_result.py) diff --git a/test/python/unit/api/__init__.py b/test/unit/api/python/__init__.py index e69de29bb..e69de29bb 100644 --- a/test/python/unit/api/__init__.py +++ b/test/unit/api/python/__init__.py diff --git a/test/python/unit/api/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index d8a4c26f7..d8a4c26f7 100644 --- a/test/python/unit/api/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py diff --git a/test/python/unit/api/test_grammar.py b/test/unit/api/python/test_grammar.py index db567a6ba..db567a6ba 100644 --- a/test/python/unit/api/test_grammar.py +++ b/test/unit/api/python/test_grammar.py diff --git a/test/python/unit/api/test_op.py b/test/unit/api/python/test_op.py index 5126a481d..5126a481d 100644 --- a/test/python/unit/api/test_op.py +++ b/test/unit/api/python/test_op.py diff --git a/test/python/unit/api/test_result.py b/test/unit/api/python/test_result.py index bd97646f9..bd97646f9 100644 --- a/test/python/unit/api/test_result.py +++ b/test/unit/api/python/test_result.py diff --git a/test/python/unit/api/test_solver.py b/test/unit/api/python/test_solver.py index 71ab17465..89e99bd9e 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -643,13 +643,19 @@ def test_mk_real(solver): solver.mkReal(val4, val4) -def test_mk_regexp_empty(solver): +def test_mk_regexp_none(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) -def test_mk_regexp_sigma(solver): +def test_mk_regexp_all(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll()) + + +def test_mk_regexp_allchar(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) diff --git a/test/python/unit/api/test_sort.py b/test/unit/api/python/test_sort.py index 98cf76d76..98cf76d76 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/unit/api/python/test_sort.py diff --git a/test/python/unit/api/test_term.py b/test/unit/api/python/test_term.py index 34a79d597..49314638f 100644 --- a/test/python/unit/api/test_term.py +++ b/test/unit/api/python/test_term.py @@ -208,6 +208,23 @@ def test_get_op(solver): assert headTerm == solver.mkTerm(headTerm.getOp(), children) +def test_has_get_symbol(solver): + n = Term(solver) + t = solver.mkBoolean(True) + c = solver.mkConst(solver.getBooleanSort(), "|\\|") + + with pytest.raises(RuntimeError): + n.hasSymbol() + assert not t.hasSymbol() + assert c.hasSymbol() + + with pytest.raises(RuntimeError): + n.getSymbol() + with pytest.raises(RuntimeError): + t.getSymbol() + assert c.getSymbol() == "|\\|" + + def test_is_null(solver): x = Term(solver) assert x.isNull() diff --git a/test/python/unit/api/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index bb30fae8f..bb30fae8f 100644 --- a/test/python/unit/api/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index df8fb9383..8dac2cfda 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -140,8 +140,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) { TypeNode integer = d_nodeManager->integerType(); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x = d_nodeManager->mkBoundVar(integer); Node a = d_skolemManager->mkDummySkolem("a", integer); diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index b170ccbb6..50e766e61 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -732,15 +732,15 @@ TEST_F(TestNodeBlackNode, isConst) Node cons_1_nil = d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); Node cons_1_cons_2_nil = d_nodeManager->mkNode( APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(Rational(2)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); ASSERT_FALSE(cons_x_nil.isConst()); @@ -749,8 +749,8 @@ TEST_F(TestNodeBlackNode, isConst) TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); ASSERT_TRUE(storeAll.isConst()); diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 05ccfc90c..779397e04 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -312,7 +312,7 @@ TEST_F(TestNodeBlackNodeBuilder, append) Node p = d_nodeManager->mkNode( EQUAL, - d_nodeManager->mkConst<Rational>(0), + d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0), d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t)); Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index b02790cb5..ad41155c3 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -140,7 +140,7 @@ TEST_F(TestNodeBlackNodeManager, mkConst_bool) TEST_F(TestNodeBlackNodeManager, mkConst_rational) { Rational r("3/2"); - Node n = d_nodeManager->mkConst(r); + Node n = d_nodeManager->mkConst(CONST_RATIONAL, r); ASSERT_EQ(n.getConst<Rational>(), r); } diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index fe06f85d3..64f6a70f5 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -23,6 +23,7 @@ namespace cvc5 { using namespace cvc5::expr; +using namespace cvc5::kind; namespace test { @@ -33,8 +34,8 @@ class TestNodeWhiteNodeManager : public TestNode TEST_F(TestNodeWhiteNodeManager, mkConst_rational) { Rational i("3"); - Node n = d_nodeManager->mkConst(i); - Node m = d_nodeManager->mkConst(i); + Node n = d_nodeManager->mkConst(CONST_RATIONAL, i); + Node m = d_nodeManager->mkConst(CONST_RATIONAL, i); ASSERT_EQ(n.getId(), m.getId()); } diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index eb6f77bdc..8061526d5 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -49,7 +49,7 @@ TEST_F(TestNodeWhiteNode, iterators) Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y); - Node two = d_nodeManager->mkConst(Rational(2)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x_times_2 = d_nodeManager->mkNode(MULT, x, two); Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y); diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index 9f93017f0..424fee989 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -50,7 +50,8 @@ TEST_F(TestNodeWhiteTypeNode, sub_types) TypeNode bvType = d_nodeManager->mkBitVectorType(32); Node x = d_nodeManager->mkBoundVar("x", realType); - Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0))); + Node xPos = d_nodeManager->mkNode( + GT, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType); Node lambda = d_nodeManager->mkVar("lambda", funtype); std::vector<Node> formals; diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index a6af29315..6687f2459 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -19,10 +19,10 @@ #include "test_smt.h" #include "util/rational.h" -namespace cvc5 { - -using namespace preprocessing::passes; +using namespace cvc5::kind; +using namespace cvc5::preprocessing::passes; +namespace cvc5 { namespace test { class TestPPWhiteForeignTheoryRewrite : public TestSmt @@ -35,7 +35,7 @@ TEST_F(TestPPWhiteForeignTheoryRewrite, simplify) std::cout << "len(x) >= 0 is simplified to true" << std::endl; Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType()); Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x); - Node zero = d_nodeManager->mkConst<Rational>(0); + Node zero = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0); Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero); Node tt = d_nodeManager->mkConst<bool>(true); Node simplified1 = ftr.foreignRewrite(geq1); diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 15c5e8570..9a0a3e26d 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -35,6 +35,7 @@ cvc5_add_unit_test_white(theory_int_opt_white theory) cvc5_add_unit_test_white(theory_opt_multigoal_white theory) cvc5_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) +cvc5_add_unit_test_white(theory_sets_rewriter_white theory) cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory) cvc5_add_unit_test_white(theory_sets_type_rules_white theory) cvc5_add_unit_test_white(theory_strings_skolem_cache_black theory) diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp index 3e0bb6c17..9127fadff 100644 --- a/test/unit/theory/arith_poly_white.cpp +++ b/test/unit/theory/arith_poly_white.cpp @@ -40,9 +40,9 @@ class TestTheoryWhiteArithPolyNorm : public TestSmt TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) { TypeNode intType = d_nodeManager->integerType(); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x = d_nodeManager->mkVar("x", intType); Node y = d_nodeManager->mkVar("y", intType); Node z = d_nodeManager->mkVar("z", intType); @@ -101,10 +101,10 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real) { TypeNode realType = d_nodeManager->realType(); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node half = d_nodeManager->mkConst(Rational(1) / Rational(2)); - Node two = d_nodeManager->mkConst(Rational(2)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node half = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x = d_nodeManager->mkVar("x", realType); Node y = d_nodeManager->mkVar("y", realType); diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index 438f28c2d..4ff6d174f 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -25,10 +25,10 @@ #include "theory/rewriter.h" #include "util/rational.h" -namespace cvc5 { - -using namespace theory; +using namespace cvc5::kind; +using namespace cvc5::theory; +namespace cvc5 { namespace test { class TestTheoryWhiteEvaluator : public TestSmt @@ -103,8 +103,8 @@ TEST_F(TestTheoryWhiteEvaluator, strIdOf) { Node a = d_nodeManager->mkConst(String("A")); Node empty = d_nodeManager->mkConst(String("")); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); std::vector<Node> args; std::vector<Node> vals; @@ -150,14 +150,14 @@ TEST_F(TestTheoryWhiteEvaluator, code) { Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a); Node r = eval.eval(n, args, vals); - ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65))); + ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(65))); } // (str.code "") ---> -1 { Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty); Node r = eval.eval(n, args, vals); - ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1))); + ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); } } } // namespace test diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 165479b78..005e5cc3f 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -28,11 +28,11 @@ #include "util/rational.h" #include "util/string.h" -namespace cvc5 { - -using namespace theory; -using namespace theory::strings; +using namespace cvc5::kind; +using namespace cvc5::theory; +using namespace cvc5::theory::strings; +namespace cvc5 { namespace test { class TestTheoryWhiteSequencesRewriter : public TestSmt @@ -93,11 +93,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one) Node b = d_nodeManager->mkConst(::cvc5::String("B")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); - Node negOne = d_nodeManager->mkConst(Rational(-1)); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); - Node three = d_nodeManager->mkConst(Rational(3)); + Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node i = d_nodeManager->mkVar("i", intType); ASSERT_TRUE(se.checkLengthOne(a)); @@ -128,7 +128,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith) Node z = d_nodeManager->mkVar("z", strType); Node n = d_nodeManager->mkVar("n", intType); - Node one = d_nodeManager->mkConst(Rational(1)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); // 1 >= (str.len (str.substr z n 1)) ---> true Node substr_z = d_nodeManager->mkNode( @@ -150,8 +150,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node y = d_nodeManager->mkVar("y", strType); Node z = d_nodeManager->mkVar("z", intType); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node empty = d_nodeManager->mkConst(::cvc5::String("")); Node a = d_nodeManager->mkConst(::cvc5::String("A")); @@ -184,8 +184,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) ASSERT_TRUE(ae.checkWithAssumption( x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); - Node five = d_nodeManager->mkConst(Rational(5)); - Node six = d_nodeManager->mkConst(Rational(6)); + Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); + Node six = d_nodeManager->mkConst(CONST_RATIONAL, Rational(6)); Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five); Node x_plus_five_lt_six = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six)); @@ -226,11 +226,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) Node a = d_nodeManager->mkConst(::cvc5::String("A")); Node b = d_nodeManager->mkConst(::cvc5::String("B")); Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD")); - Node negone = d_nodeManager->mkConst(Rational(-1)); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); - Node three = d_nodeManager->mkConst(Rational(3)); + Node negone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node s = d_nodeManager->mkVar("s", strType); Node s2 = d_nodeManager->mkVar("s2", strType); @@ -246,7 +246,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) n = d_nodeManager->mkNode( kind::STRING_SUBSTR, a, - d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))), + d_nodeManager->mkNode( + kind::PLUS, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))), x); sameNormalForm(n, empty); @@ -362,8 +363,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat) Node empty = d_nodeManager->mkConst(::cvc5::String("")); Node a = d_nodeManager->mkConst(::cvc5::String("A")); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node three = d_nodeManager->mkConst(Rational(3)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node i = d_nodeManager->mkVar("i", intType); Node s = d_nodeManager->mkVar("s", strType); @@ -468,11 +469,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) Node ccc = d_nodeManager->mkConst(::cvc5::String("CCC")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); - Node negOne = d_nodeManager->mkConst(Rational(-1)); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); - Node three = d_nodeManager->mkConst(Rational(3)); + Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node i = d_nodeManager->mkVar("i", intType); Node j = d_nodeManager->mkVar("j", intType); @@ -549,8 +550,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace) Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node z = d_nodeManager->mkVar("z", strType); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node n = d_nodeManager->mkVar("n", intType); // (str.replace (str.replace x "B" x) x "A") --> @@ -970,10 +971,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains) Node z = d_nodeManager->mkVar("z", strType); Node n = d_nodeManager->mkVar("n", intType); Node m = d_nodeManager->mkVar("m", intType); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); - Node three = d_nodeManager->mkConst(Rational(3)); - Node four = d_nodeManager->mkConst(Rational(4)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); Node t = d_nodeManager->mkConst(true); Node f = d_nodeManager->mkConst(false); @@ -1396,9 +1397,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext) Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a); Node f = d_nodeManager->mkConst(false); Node n = d_nodeManager->mkVar("n", intType); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node three = d_nodeManager->mkConst(Rational(3)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); // Same normal form for: // diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 719b76cab..8d5ca9923 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -37,6 +37,7 @@ namespace cvc5::test { using namespace cvc5; +using namespace cvc5::kind; using namespace cvc5::theory; using namespace cvc5::theory::arith; using namespace cvc5::theory::arith::nl; @@ -54,7 +55,10 @@ class TestTheoryWhiteArithCAD : public TestSmt nodeManager = d_nodeManager; } - Node dummy(int i) const { return d_nodeManager->mkConst(Rational(i)); } + Node dummy(int i) const + { + return d_nodeManager->mkConst(CONST_RATIONAL, Rational(i)); + } Theory::Effort d_level = Theory::EFFORT_FULL; std::unique_ptr<TypeNode> d_realType; @@ -181,14 +185,15 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_simp) Node a = d_nodeManager->mkVar(*d_realType); Node c = d_nodeManager->mkVar(*d_realType); Node orig = d_nodeManager->mkAnd(std::vector<Node>{ - d_nodeManager->mkNode(Kind::EQUAL, a, d_nodeManager->mkConst(d_zero)), + d_nodeManager->mkNode( + Kind::EQUAL, a, d_nodeManager->mkConst(CONST_RATIONAL, d_zero)), d_nodeManager->mkNode( Kind::EQUAL, d_nodeManager->mkNode( Kind::PLUS, d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c), - d_nodeManager->mkConst(d_one)), - d_nodeManager->mkConst(d_zero))}); + d_nodeManager->mkConst(CONST_RATIONAL, d_one)), + d_nodeManager->mkConst(CONST_RATIONAL, d_zero))}); { Node rewritten = Rewriter::rewrite(orig); @@ -356,10 +361,10 @@ void test_delta(const std::vector<Node>& a) TEST_F(TestTheoryWhiteArithCAD, test_delta_one) { std::vector<Node> a; - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node mone = d_nodeManager->mkConst(Rational(-1)); - Node fifth = d_nodeManager->mkConst(Rational(1, 2)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); + Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2)); Node g = make_real_variable("g"); Node l = make_real_variable("l"); Node q = make_real_variable("q"); @@ -379,10 +384,10 @@ TEST_F(TestTheoryWhiteArithCAD, test_delta_one) TEST_F(TestTheoryWhiteArithCAD, test_delta_two) { std::vector<Node> a; - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node mone = d_nodeManager->mkConst(Rational(-1)); - Node fifth = d_nodeManager->mkConst(Rational(1, 2)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); + Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2)); Node g = make_real_variable("g"); Node l = make_real_variable("l"); Node q = make_real_variable("q"); diff --git a/test/unit/theory/theory_arith_pow2_white.cpp b/test/unit/theory/theory_arith_pow2_white.cpp index 697073434..fd942c5b5 100644 --- a/test/unit/theory/theory_arith_pow2_white.cpp +++ b/test/unit/theory/theory_arith_pow2_white.cpp @@ -37,7 +37,7 @@ class TestTheoryWhiteArithPow2 : public TestSmtNoFinishInit d_slvEngine->setOption("produce-models", "true"); d_slvEngine->finishInit(); d_true = d_nodeManager->mkConst<bool>(true); - d_one = d_nodeManager->mkConst<Rational>(Rational(1)); + d_one = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(1)); } Node d_true; Node d_one; diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index a41378106..8805c7119 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -68,7 +68,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteArith, assert) { Node x = d_nodeManager->mkVar(*d_realType); - Node c = d_nodeManager->mkConst<Rational>(d_zero); + Node c = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_zero); Node gt = d_nodeManager->mkNode(GT, x, c); Node leq = Rewriter::rewrite(gt.notNode()); @@ -83,9 +83,9 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) { Node x = d_nodeManager->mkVar(*d_intType); Node xr = d_nodeManager->mkVar(*d_realType); - Node c0 = d_nodeManager->mkConst<Rational>(d_zero); - Node c1 = d_nodeManager->mkConst<Rational>(d_one); - Node c2 = d_nodeManager->mkConst<Rational>(Rational(2)); + Node c0 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_zero); + Node c1 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_one); + Node c2 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(2)); Node geq0 = d_nodeManager->mkNode(GEQ, x, c0); Node geq1 = d_nodeManager->mkNode(GEQ, x, c1); diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 9634d55c2..5f3abfcee 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -72,15 +72,18 @@ TEST_F(TestTheoryWhiteBagsNormalForm, empty_bag_normal_form) TEST_F(TestTheoryWhiteBagsNormalForm, mkBag_constant_element) { std::vector<Node> elements = getNStrings(1); - Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(-1))); - Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(0))); - Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(1))); + Node negative = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); + Node zero = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + Node positive = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); @@ -95,25 +98,31 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) { // Examples // ------- - // (bag.count "x" (emptybag String)) = 0 - // (bag.count "x" (mkBag "y" 5)) = 0 - // (bag.count "x" (mkBag "x" 4)) = 4 - // (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4 - // (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0 - - Node zero = d_nodeManager->mkConst(Rational(0)); - Node four = d_nodeManager->mkConst(Rational(4)); + // (bag.count "x" (as bag.empty (Bag String))) = 0 + // (bag.count "x" (bag "y" 5)) = 0 + // (bag.count "x" (bag "x" 4)) = 4 + // (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4 + // (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0 + + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); Node empty = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node y_5 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5))); - Node z_5 = d_nodeManager->mkBag( - d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(5))); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node y_5 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node z_5 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + z, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty); Node output1 = zero; @@ -127,12 +136,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) Node output3 = four; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node unionDisjointXY = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); + Node unionDisjointXY = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); Node input4 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointXY); Node output4 = four; ASSERT_EQ(output3, NormalForm::evaluate(input3)); - Node unionDisjointYZ = d_nodeManager->mkNode(UNION_DISJOINT, y_5, z_5); + Node unionDisjointYZ = d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_5, z_5); Node input5 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointYZ); Node output5 = zero; ASSERT_EQ(output4, NormalForm::evaluate(input4)); @@ -142,37 +151,46 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) { // Examples // -------- - // - (duplicate_removal (emptybag String)) = (emptybag String) - // - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1) - // - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1) + // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag + // String)) + // - (bag.duplicate_removal (bag "x" 4)) = (bag.empty"x" 1) + // - (bag.duplicate_removal (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // (bag.union_disjoint(bag "x" 1) (bag "y" 1) Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node input1 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, emptybag); + Node input1 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, emptybag); Node output1 = emptybag; ASSERT_EQ(output1, NormalForm::evaluate(input1)); Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); - Node x_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); - - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node y_5 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5))); - - Node input2 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, x_4); + Node x_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node y_5 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + + Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4); Node output2 = x_1; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); - Node input3 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, normalBag); - Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); + Node input3 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, normalBag); + Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -180,35 +198,47 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max) { // Example // ------- - // input: (union_max A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_max A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 4) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 4) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node x_3 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3))); - Node x_7 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7))); - Node z_2 = d_nodeManager->mkBag( - d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); - - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(UNION_MAX, A, B); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node x_3 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node x_7 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + Node z_2 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + z, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); // output Node output = d_nodeManager->mkNode( - UNION_DISJOINT, x_4, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2)); + BAG_UNION_DISJOINT, + x_4, + d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2)); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -219,40 +249,44 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1) std::vector<Node> elements = getNStrings(3); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(2))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(3))); - Node C = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[2], - d_nodeManager->mkConst(Rational(4))); - - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); + Node B = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node C = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[2], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // unionDisjointAB is already in a normal form ASSERT_TRUE(unionDisjointAB.isConst()); ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointAB)); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - // unionDisjointAB is is the normal form of unionDisjointBA + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + // unionDisjointAB is the normal form of unionDisjointBA ASSERT_FALSE(unionDisjointBA.isConst()); ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointBA)); Node unionDisjointAB_C = - d_nodeManager->mkNode(UNION_DISJOINT, unionDisjointAB, C); - Node unionDisjointBC = d_nodeManager->mkNode(UNION_DISJOINT, B, C); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionDisjointAB, C); + Node unionDisjointBC = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, C); Node unionDisjointA_BC = - d_nodeManager->mkNode(UNION_DISJOINT, A, unionDisjointBC); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, unionDisjointBC); // unionDisjointA_BC is the normal form of unionDisjointAB_C ASSERT_FALSE(unionDisjointAB_C.isConst()); ASSERT_TRUE(unionDisjointA_BC.isConst()); ASSERT_EQ(unionDisjointA_BC, NormalForm::evaluate(unionDisjointAB_C)); - Node unionDisjointAA = d_nodeManager->mkNode(UNION_DISJOINT, A, A); - Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(4))); + Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A); + Node AA = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); ASSERT_FALSE(unionDisjointAA.isConst()); ASSERT_TRUE(AA.isConst()); ASSERT_EQ(AA, NormalForm::evaluate(unionDisjointAA)); @@ -262,35 +296,47 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2) { // Example // ------- - // input: (union_disjoint A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_disjoint A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 7) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 7) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node x_3 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3))); - Node x_7 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7))); - Node z_2 = d_nodeManager->mkBag( - d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); - - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node x_3 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node x_7 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + Node z_2 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + z, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // output Node output = d_nodeManager->mkNode( - UNION_DISJOINT, x_7, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2)); + BAG_UNION_DISJOINT, + x_7, + d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2)); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -300,29 +346,39 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min) { // Example // ------- - // input: (intersection_min A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.inter_min A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "x" 3) + // (bag "x" 3) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node x_3 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3))); - Node x_7 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7))); - Node z_2 = d_nodeManager->mkBag( - d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); - - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node x_3 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node x_7 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + Node z_2 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + z, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); // output Node output = x_3; @@ -335,34 +391,46 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract) { // Example // ------- - // input: (difference_subtract A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_subtract A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2)) + // (bag.union_disjoint (bag "x" 1) (bag "z" 2)) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1))); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node x_3 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3))); - Node x_7 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7))); - Node z_2 = d_nodeManager->mkBag( - d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); - - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, B); + Node x_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node x_3 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node x_7 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + Node z_2 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + z, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, B); // output - Node output = d_nodeManager->mkNode(UNION_DISJOINT, x_1, z_2); + Node output = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, z_2); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -372,31 +440,43 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove) { // Example // ------- - // input: (difference_remove A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_remove A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "z" 2) + // (bag "z" 2) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1))); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node x_3 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3))); - Node x_7 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7))); - Node z_2 = d_nodeManager->mkBag( - d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); - - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, B); + Node x_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node x_3 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node x_7 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + Node z_2 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + z, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, B); // output Node output = z_2; @@ -409,31 +489,35 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) { // Examples // -------- - // - (card (emptybag String)) = 0 - // - (choose (MK_BAG "x" 4)) = 4 - // - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5 + // - (bag.card (as bag.empty (Bag String))) = 0 + // - (bag.choose (bag "x" 4)) = 4 + // - (bag.choose (bag.union_disjoint (bag "x" 4) (bag "y" 1))) = 5 Node empty = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); Node input1 = d_nodeManager->mkNode(BAG_CARD, empty); - Node output1 = d_nodeManager->mkConst(Rational(0)); + Node output1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); ASSERT_EQ(output1, NormalForm::evaluate(input1)); Node input2 = d_nodeManager->mkNode(BAG_CARD, x_4); - Node output2 = d_nodeManager->mkConst(Rational(4)); + Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1); + Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_1); Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint); - Node output3 = d_nodeManager->mkConst(Rational(5)); + Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -441,10 +525,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) { // Examples // -------- - // - (bag.is_singleton (emptybag String)) = false - // - (bag.is_singleton (MK_BAG "x" 1)) = true - // - (bag.is_singleton (MK_BAG "x" 4)) = false - // - (bag.is_singleton (union_disjoint (MK_BAG "x" 1) (MK_BAG "y" 1))) = + // - (bag.is_singleton (as bag.empty (Bag String))) = false + // - (bag.is_singleton (bag "x" 1)) = true + // - (bag.is_singleton (bag "x" 4)) = false + // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) = // false Node falseNode = d_nodeManager->mkConst(false); Node trueNode = d_nodeManager->mkConst(true); @@ -453,12 +537,18 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1))); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); + Node x_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty); Node output1 = falseNode; @@ -472,7 +562,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) Node output3 = falseNode; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); Node input4 = d_nodeManager->mkNode(BAG_IS_SINGLETON, union_disjoint); Node output4 = falseNode; ASSERT_EQ(output3, NormalForm::evaluate(input3)); @@ -482,10 +572,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) { // Examples // -------- - // - (bag.from_set (emptyset String)) = (emptybag String) - // - (bag.from_set (singleton "x")) = (mkBag "x" 1) - // - (bag.to_set (union (singleton "x") (singleton "y"))) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1)) + // - (bag.from_set (as set.empty (Bag String))) = (as bag.empty (Bag String)) + // - (bag.from_set (set.singleton "x")) = (bag "x" 1) + // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) = + // (bag.union_disjoint (bag "x" 1) (bag "y" 1)) Node emptyset = d_nodeManager->mkConst( EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); @@ -501,10 +591,14 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y); - Node x_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1))); + Node x_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node y_1 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton); Node output2 = x_1; @@ -513,7 +607,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) // for normal sets, the first node is the largest, not smallest Node normalSet = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton); Node input3 = d_nodeManager->mkNode(BAG_FROM_SET, normalSet); - Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -521,10 +615,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) { // Examples // -------- - // - (bag.to_set (emptybag String)) = (emptyset String) - // - (bag.to_set (mkBag "x" 4)) = (singleton "x") - // - (bag.to_set (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (union (singleton "x") (singleton "y"))) + // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Bag String)) + // - (bag.to_set (bag "x" 4)) = (set.singleton "x") + // - (bag.to_set (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // (set.union (set.singleton "x") (set.singleton "y"))) Node emptyset = d_nodeManager->mkConst( EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); @@ -540,17 +634,21 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y); - Node x_4 = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4))); - Node y_5 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5))); + Node x_4 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node y_5 = + d_nodeManager->mkBag(d_nodeManager->stringType(), + y, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); Node input2 = d_nodeManager->mkNode(BAG_TO_SET, x_4); Node output2 = xSingleton; ASSERT_EQ(output2, NormalForm::evaluate(input2)); // for normal sets, the first node is the largest, not smallest - Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); + Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); Node input3 = d_nodeManager->mkNode(BAG_TO_SET, normalBag); Node output3 = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton); ASSERT_EQ(output3, NormalForm::evaluate(input3)); diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 7250f581c..ee1e89448 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -75,9 +75,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node emptyString = d_nodeManager->mkConst(String("")); - Node constantBag = d_nodeManager->mkBag(d_nodeManager->stringType(), - emptyString, - d_nodeManager->mkConst(Rational(1))); + Node constantBag = + d_nodeManager->mkBag(d_nodeManager->stringType(), + emptyString, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); // (= A A) = true where A is a bag Node n1 = A.eqNode(A); @@ -106,15 +107,18 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element) { std::vector<Node> elements = getNStrings(1); - Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(-1))); - Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(0))); - Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(1))); + Node negative = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); + Node zero = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + Node positive = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -136,16 +140,22 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) { Node skolem = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(), - skolem, - d_nodeManager->mkConst(Rational(-1))); - Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), - skolem, - d_nodeManager->mkConst(Rational(-1))); - Node zero = d_nodeManager->mkBag( - d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(0))); - Node positive = d_nodeManager->mkBag( - d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(1))); + Node variable = d_nodeManager->mkBag( + d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); + Node negative = d_nodeManager->mkBag( + d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); + Node zero = + d_nodeManager->mkBag(d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + Node positive = + d_nodeManager->mkBag(d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -165,21 +175,21 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) TEST_F(TestTheoryWhiteBagsRewriter, bag_count) { - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node three = d_nodeManager->mkConst(Rational(3)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node skolem = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(skolem.getType()))); - // (bag.count x emptybag) = 0 + // (bag.count x (as bag.empty (Bag String))) = 0 Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL && response1.d_node == zero); - // (bag.count x (mkBag x c) = (ite (>= c 1) c 0) + // (bag.count x (bag x c) = (ite (>= c 1) c 0) Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three); Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); @@ -193,14 +203,18 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5))); + Node bag = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - // (duplicate_removal (mkBag x n)) = (mkBag x 1) - Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag); + // (bag.duplicate_removal (bag x n)) = (bag x 1) + Node n = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag); RewriteResponse response = d_rewriter->postRewrite(n); - Node noDuplicate = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1))); + Node noDuplicate = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); ASSERT_TRUE(response.d_node == noDuplicate && response.d_status == REWRITE_AGAIN_FULL); } @@ -211,79 +225,81 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_max) std::vector<Node> elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - - // (union_max A emptybag) = A - Node unionMax1 = d_nodeManager->mkNode(UNION_MAX, A, emptyBag); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + + // (bag.union_max A (as bag.empty (Bag String))) = A + Node unionMax1 = d_nodeManager->mkNode(BAG_UNION_MAX, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(unionMax1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (union_max emptybag A) = A - Node unionMax2 = d_nodeManager->mkNode(UNION_MAX, emptyBag, A); + // (bag.union_max (as bag.empty (Bag String)) A) = A + Node unionMax2 = d_nodeManager->mkNode(BAG_UNION_MAX, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(unionMax2); ASSERT_TRUE(response2.d_node == A && response2.d_status == REWRITE_AGAIN_FULL); - // (union_max A A) = A - Node unionMax3 = d_nodeManager->mkNode(UNION_MAX, A, A); + // (bag.union_max A A) = A + Node unionMax3 = d_nodeManager->mkNode(BAG_UNION_MAX, A, A); RewriteResponse response3 = d_rewriter->postRewrite(unionMax3); ASSERT_TRUE(response3.d_node == A && response3.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_max A B)) = (union_max A B) - Node unionMax4 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxAB); + // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B) + Node unionMax4 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxAB); RewriteResponse response4 = d_rewriter->postRewrite(unionMax4); ASSERT_TRUE(response4.d_node == unionMaxAB && response4.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_max B A)) = (union_max B A) - Node unionMax5 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxBA); + // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A) + Node unionMax5 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxBA); RewriteResponse response5 = d_rewriter->postRewrite(unionMax5); ASSERT_TRUE(response5.d_node == unionMaxBA && response4.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_max A B) A) = (union_max A B) - Node unionMax6 = d_nodeManager->mkNode(UNION_MAX, unionMaxAB, A); + // (bag.union_max (bag.union_max A B) A) = (bag.union_max A B) + Node unionMax6 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxAB, A); RewriteResponse response6 = d_rewriter->postRewrite(unionMax6); ASSERT_TRUE(response6.d_node == unionMaxAB && response6.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_max B A) A) = (union_max B A) - Node unionMax7 = d_nodeManager->mkNode(UNION_MAX, unionMaxBA, A); + // (bag.union_max (bag.union_max B A) A) = (bag.union_max B A) + Node unionMax7 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxBA, A); RewriteResponse response7 = d_rewriter->postRewrite(unionMax7); ASSERT_TRUE(response7.d_node == unionMaxBA && response7.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_disjoint A B)) = (union_disjoint A B) - Node unionMax8 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointAB); + // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B) + Node unionMax8 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointAB); RewriteResponse response8 = d_rewriter->postRewrite(unionMax8); ASSERT_TRUE(response8.d_node == unionDisjointAB && response8.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_disjoint B A)) = (union_disjoint B A) - Node unionMax9 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointBA); + // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A) + Node unionMax9 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointBA); RewriteResponse response9 = d_rewriter->postRewrite(unionMax9); ASSERT_TRUE(response9.d_node == unionDisjointBA && response9.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_disjoint A B) A) = (union_disjoint A B) - Node unionMax10 = d_nodeManager->mkNode(UNION_MAX, unionDisjointAB, A); + // (bag.union_max (bag.union_disjoint A B) A) = (bag.union_disjoint A B) + Node unionMax10 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointAB, A); RewriteResponse response10 = d_rewriter->postRewrite(unionMax10); ASSERT_TRUE(response10.d_node == unionDisjointAB && response10.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_disjoint B A) A) = (union_disjoint B A) - Node unionMax11 = d_nodeManager->mkNode(UNION_MAX, unionDisjointBA, A); + // (bag.union_max (bag.union_disjoint B A) A) = (bag.union_disjoint B A) + Node unionMax11 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointBA, A); RewriteResponse response11 = d_rewriter->postRewrite(unionMax11); ASSERT_TRUE(response11.d_node == unionDisjointBA && response11.d_status == REWRITE_AGAIN_FULL); @@ -295,56 +311,59 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint) std::vector<Node> elements = getNStrings(3); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(n + 1))); - Node C = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[2], - d_nodeManager->mkConst(Rational(n + 2))); - - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxAC = d_nodeManager->mkNode(UNION_MAX, A, C); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (union_disjoint A emptybag) = A - Node unionDisjoint1 = d_nodeManager->mkNode(UNION_DISJOINT, A, emptyBag); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node C = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[2], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2))); + + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxAC = d_nodeManager->mkNode(BAG_UNION_MAX, A, C); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.union_disjoint A (as bag.empty (Bag String))) = A + Node unionDisjoint1 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(unionDisjoint1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint emptybag A) = A - Node unionDisjoint2 = d_nodeManager->mkNode(UNION_DISJOINT, emptyBag, A); + // (bag.union_disjoint (as bag.empty (Bag String)) A) = A + Node unionDisjoint2 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(unionDisjoint2); ASSERT_TRUE(response2.d_node == A && response2.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (union_max A B) (intersection_min B A)) = - // (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.union_max A B) (bag.inter_min B A)) = + // (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint3 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAB, intersectionBA); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAB, intersectionBA); RewriteResponse response3 = d_rewriter->postRewrite(unionDisjoint3); ASSERT_TRUE(response3.d_node == unionDisjointAB && response3.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (intersection_min B A)) (union_max A B) = - // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) = + // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint4 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxBA, intersectionBA); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxBA, intersectionBA); RewriteResponse response4 = d_rewriter->postRewrite(unionDisjoint4); ASSERT_TRUE(response4.d_node == unionDisjointBA && response4.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (intersection_min B A)) (union_max A B) = - // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) = + // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint5 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAC, intersectionAB); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAC, intersectionAB); RewriteResponse response5 = d_rewriter->postRewrite(unionDisjoint5); ASSERT_TRUE(response5.d_node == unionDisjoint5 && response5.d_status == REWRITE_DONE); @@ -356,79 +375,83 @@ TEST_F(TestTheoryWhiteBagsRewriter, intersection_min) std::vector<Node> elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - - // (intersection_min A emptybag) = emptyBag - Node n1 = d_nodeManager->mkNode(INTERSECTION_MIN, A, emptyBag); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + + // (bag.inter_min A (as bag.empty (Bag String)) = + // (as bag.empty (Bag String)) + Node n1 = d_nodeManager->mkNode(BAG_INTER_MIN, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == emptyBag && response1.d_status == REWRITE_AGAIN_FULL); - // (intersection_min emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(INTERSECTION_MIN, emptyBag, A); + // (bag.inter_min (as bag.empty (Bag String)) A) = + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_INTER_MIN, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A A) = A - Node n3 = d_nodeManager->mkNode(INTERSECTION_MIN, A, A); + // (bag.inter_min A A) = A + Node n3 = d_nodeManager->mkNode(BAG_INTER_MIN, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == A && response3.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_max A B) = A - Node n4 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxAB); + // (bag.inter_min A (bag.union_max A B) = A + Node n4 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxAB); RewriteResponse response4 = d_rewriter->postRewrite(n4); ASSERT_TRUE(response4.d_node == A && response4.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_max B A) = A - Node n5 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxBA); + // (bag.inter_min A (bag.union_max B A) = A + Node n5 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxBA); RewriteResponse response5 = d_rewriter->postRewrite(n5); ASSERT_TRUE(response5.d_node == A && response4.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_max A B) A) = A - Node n6 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxAB, A); + // (bag.inter_min (bag.union_max A B) A) = A + Node n6 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxAB, A); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == A && response6.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_max B A) A) = A - Node n7 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxBA, A); + // (bag.inter_min (bag.union_max B A) A) = A + Node n7 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxBA, A); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == A && response7.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_disjoint A B) = A - Node n8 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointAB); + // (bag.inter_min A (bag.union_disjoint A B) = A + Node n8 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == A && response8.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_disjoint B A) = A - Node n9 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointBA); + // (bag.inter_min A (bag.union_disjoint B A) = A + Node n9 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == A && response9.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_disjoint A B) A) = A - Node n10 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointAB, A); + // (bag.inter_min (bag.union_disjoint A B) A) = A + Node n10 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == A && response10.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_disjoint B A) A) = A - Node n11 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointBA, A); + // (bag.inter_min (bag.union_disjoint B A) A) = A + Node n11 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == A && response11.d_status == REWRITE_AGAIN_FULL); @@ -440,81 +463,90 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract) std::vector<Node> elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (difference_subtract A emptybag) = A - Node n1 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, emptyBag); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.difference_subtract A (as bag.empty (Bag String)) = A + Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, emptyBag, A); + // (bag.difference_subtract (as bag.empty (Bag String)) A) = + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A A) = emptybag - Node n3 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, A); + // (bag.difference_subtract A A) = (as bag.empty (Bag String)) + Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == emptyBag && response3.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (union_disjoint A B) A) = B - Node n4 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointAB, A); + // (bag.difference_subtract (bag.union_disjoint A B) A) = B + Node n4 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointAB, A); RewriteResponse response4 = d_rewriter->postRewrite(n4); ASSERT_TRUE(response4.d_node == B && response4.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (union_disjoint B A) A) = B - Node n5 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointBA, A); + // (bag.difference_subtract (bag.union_disjoint B A) A) = B + Node n5 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointBA, A); RewriteResponse response5 = d_rewriter->postRewrite(n5); ASSERT_TRUE(response5.d_node == B && response4.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_disjoint A B)) = emptybag - Node n6 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointAB); + // (bag.difference_subtract A (bag.union_disjoint A B)) = + // (as bag.empty (Bag String)) + Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointAB); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == emptyBag && response6.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_disjoint B A)) = emptybag - Node n7 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointBA); + // (bag.difference_subtract A (bag.union_disjoint B A)) = + // (as bag.empty (Bag String)) + Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointBA); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == emptyBag && response7.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_max A B)) = emptybag - Node n8 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxAB); + // (bag.difference_subtract A (bag.union_max A B)) = + // (as bag.empty (Bag String)) + Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == emptyBag && response8.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_max B A)) = emptybag - Node n9 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxBA); + // (bag.difference_subtract A (bag.union_max B A)) = + // (as bag.empty (Bag String)) + Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == emptyBag && response9.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (intersection_min A B) A) = emptybag - Node n10 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionAB, A); + // (bag.difference_subtract (bag.inter_min A B) A) = + // (as bag.empty (Bag String)) + Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == emptyBag && response10.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (intersection_min B A) A) = emptybag - Node n11 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionBA, A); + // (bag.difference_subtract (bag.inter_min B A) A) = + // (as bag.empty (Bag String)) + Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == emptyBag && response11.d_status == REWRITE_AGAIN_FULL); @@ -526,69 +558,78 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) std::vector<Node> elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (difference_remove A emptybag) = A - Node n1 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, emptyBag); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.difference_remove A (as bag.empty (Bag String)) = A + Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (difference_remove emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, emptyBag, A); + // (bag.difference_remove (as bag.empty (Bag String)) A)= + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A A) = emptybag - Node n3 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, A); + // (bag.difference_remove A A) = (as bag.empty (Bag String)) + Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == emptyBag && response3.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_disjoint A B)) = emptybag - Node n6 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointAB); + // (bag.difference_remove A (bag.union_disjoint A B)) = + // (as bag.empty (Bag String)) + Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointAB); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == emptyBag && response6.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_disjoint B A)) = emptybag - Node n7 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointBA); + // (bag.difference_remove A (bag.union_disjoint B A)) = + // (as bag.empty (Bag String)) + Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointBA); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == emptyBag && response7.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_max A B)) = emptybag - Node n8 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxAB); + // (bag.difference_remove A (bag.union_max A B)) = + // (as bag.empty (Bag String)) + Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == emptyBag && response8.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_max B A)) = emptybag - Node n9 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxBA); + // (bag.difference_remove A (bag.union_max B A)) = + // (as bag.empty (Bag String)) + Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == emptyBag && response9.d_status == REWRITE_AGAIN_FULL); - // (difference_remove (intersection_min A B) A) = emptybag - Node n10 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionAB, A); + // (bag.difference_remove (bag.inter_min A B) A) = + // (as bag.empty (Bag String)) + Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == emptyBag && response10.d_status == REWRITE_AGAIN_FULL); - // (difference_remove (intersection_min B A) A) = emptybag - Node n11 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionBA, A); + // (bag.difference_remove (bag.inter_min B A) A) = + // (as bag.empty (Bag String)) + Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == emptyBag && response11.d_status == REWRITE_AGAIN_FULL); @@ -597,10 +638,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) TEST_F(TestTheoryWhiteBagsRewriter, choose) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node c = d_nodeManager->mkConst(Rational(3)); + Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - // (bag.choose (mkBag x c)) = x where c is a constant > 0 + // (bag.choose (bag x c)) = x where c is a constant > 0 Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == x @@ -612,32 +653,33 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node c = d_nodeManager->mkConst(Rational(3)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); std::vector<Node> elements = getNStrings(2); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(4))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(Rational(5))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - - // TODO(projects#223): enable this test after implementing bags normal form - // // (bag.card emptybag) = 0 - // Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag); - // RewriteResponse response1 = d_rewriter->postRewrite(n1); - // ASSERT_TRUE(response1.d_node == zero && response1.d_status == - // REWRITE_AGAIN_FULL); - - // (bag.card (mkBag x c)) = c where c is a constant > 0 + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node B = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + + // (bag.card (as bag.empty (Bag String)) = 0 + Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == zero + && response1.d_status == REWRITE_AGAIN_FULL); + + // (bag.card (bag x c)) = c where c is a constant > 0 Node n2 = d_nodeManager->mkNode(BAG_CARD, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == c && response2.d_status == REWRITE_AGAIN_FULL); - // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B)) + // (bag.card (bag.union_disjoint A B)) = (+ (bag.card A) (bag.card B)) Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB); Node cardA = d_nodeManager->mkNode(BAG_CARD, A); Node cardB = d_nodeManager->mkNode(BAG_CARD, B); @@ -655,17 +697,16 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - // TODO(projects#223): complete this function - // (bag.is_singleton emptybag) = false - // Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); - // RewriteResponse response1 = d_rewriter->postRewrite(n1); - // ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) - // && response1.d_status == REWRITE_AGAIN_FULL); + // (bag.is_singleton (as bag.empty (Bag String)) = false + Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) + && response1.d_status == REWRITE_AGAIN_FULL); - // (bag.is_singleton (mkBag x c) = (c == 1) + // (bag.is_singleton (bag x c) = (c == 1) Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); - Node one = d_nodeManager->mkConst(Rational(1)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node equal = c.eqNode(one); ASSERT_TRUE(response2.d_node == equal && response2.d_status == REWRITE_AGAIN_FULL); @@ -676,10 +717,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); - // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) + // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1) Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton); RewriteResponse response = d_rewriter->postRewrite(n); - Node one = d_nodeManager->mkConst(Rational(1)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one); ASSERT_TRUE(response.d_node == bag && response.d_status == REWRITE_AGAIN_FULL); @@ -688,10 +729,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) TEST_F(TestTheoryWhiteBagsRewriter, to_set) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5))); + Node bag = + d_nodeManager->mkBag(d_nodeManager->stringType(), + x, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + // (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x) Node n = d_nodeManager->mkNode(BAG_TO_SET, bag); RewriteResponse response = d_rewriter->postRewrite(n); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); @@ -710,7 +753,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, xString); Node lambda = d_nodeManager->mkNode(LAMBDA, bound, empty); - // (bag.map (lambda ((x U)) t) emptybag) = emptybag + // (bag.map (lambda ((x U)) t) (as bag.empty (Bag String)) = + // (as bag.empty (Bag String)) Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == emptybagString @@ -719,22 +763,41 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) std::vector<Node> elements = getNStrings(2); Node a = d_nodeManager->mkConst(String("a")); Node b = d_nodeManager->mkConst(String("b")); - Node A = d_nodeManager->mkBag( - d_nodeManager->stringType(), a, d_nodeManager->mkConst(Rational(3))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), b, d_nodeManager->mkConst(Rational(4))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node A = + d_nodeManager->mkBag(d_nodeManager->stringType(), + a, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); + Node B = + d_nodeManager->mkBag(d_nodeManager->stringType(), + b, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); ASSERT_TRUE(unionDisjointAB.isConst()); - // (bag.map (lambda ((x Int)) "") (union_disjoint (bag "a" 3) (bag "b" 4))) = - // (bag "" 7)) + // (bag.map + // (lambda ((x Int)) "") + // (bag.union_disjoint (bag "a" 3) (bag "b" 4))) = + // (bag "" 7)) Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB); - Node rewritten = Rewriter::rewrite(n2); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), empty, d_nodeManager->mkConst(Rational(7))); - ASSERT_TRUE(rewritten == bag); + Node bag = + d_nodeManager->mkBag(d_nodeManager->stringType(), + empty, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + // - (bag.map f (bag.union_disjoint K1 K2)) = + // (bag.union_disjoint (bag.map f K1) (bag.map f K2)) + Node k1 = d_skolemManager->mkDummySkolem("K1", A.getType()); + Node k2 = d_skolemManager->mkDummySkolem("K2", A.getType()); + Node f = d_skolemManager->mkDummySkolem("f", lambda.getType()); + Node unionDisjointK1K2 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, k1, k2); + Node n3 = d_nodeManager->mkNode(BAG_MAP, f, unionDisjointK1K2); + Node rewritten3 = Rewriter::rewrite(n3); + Node mapK1 = d_nodeManager->mkNode(BAG_MAP, f, k1); + Node mapK2 = d_nodeManager->mkNode(BAG_MAP, f, k2); + Node unionDisjointMapK1K2 = + d_nodeManager->mkNode(BAG_UNION_DISJOINT, mapK1, mapK2); + ASSERT_TRUE(rewritten3 == unionDisjointMapK1K2); } } // namespace test diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 682ae5bb2..7b5b3be2c 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -51,12 +51,13 @@ class TestTheoryWhiteBagsTypeRule : public TestSmt TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) { std::vector<Node> elements = getNStrings(1); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(100))); + Node bag = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(100))); Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag); - Node node = d_nodeManager->mkConst(Rational(10)); + Node node = d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)); // node of type Int is not compatible with bag of type (Bag String) ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true), @@ -66,31 +67,35 @@ TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) { std::vector<Node> elements = getNStrings(1); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(10))); - ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag)); - ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(), + Node bag = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); + ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag)); + ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(), bag.getType()); } TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) { std::vector<Node> elements = getNStrings(1); - Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(-1))); - Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(0))); - Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(1))); + Node negative = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); + Node zero = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + Node positive = + d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); // only positive multiplicity are constants - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative)); - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero)); - ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive)); + ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative)); + ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, zero)); + ASSERT_TRUE(BagMakeTypeRule::computeIsConst(d_nodeManager, positive)); } TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) @@ -105,9 +110,10 @@ TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) { std::vector<Node> elements = getNStrings(1); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(10))); + Node bag = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag)); ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); } @@ -115,9 +121,10 @@ TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) TEST_F(TestTheoryWhiteBagsTypeRule, map_operator) { std::vector<Node> elements = getNStrings(1); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(Rational(10))); + Node bag = d_nodeManager->mkBag( + d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); Node set = d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); @@ -134,7 +141,7 @@ TEST_F(TestTheoryWhiteBagsTypeRule, map_operator) ASSERT_EQ(d_nodeManager->integerType(), mappedBag.getType().getBagElementType()); - Node one = d_nodeManager->mkConst(Rational(1)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node x2 = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType()); std::vector<Node> args2; args2.push_back(x2); diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index d8ae8e468..1aea9e481 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -41,8 +41,8 @@ TEST_F(TestTheoryBlack, array_const) { TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); ASSERT_TRUE(storeAll.isConst()); diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 39ae835e0..106a0a39e 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -40,7 +40,7 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit d_slvEngine->setOption("produce-models", "true"); d_slvEngine->finishInit(); d_true = d_nodeManager->mkConst<bool>(true); - d_one = d_nodeManager->mkConst<Rational>(Rational(1)); + d_one = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(1)); } Node d_true; Node d_one; @@ -64,7 +64,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) IntBlaster intBlaster( env, options::SolveBVAsIntMode::SUM, 1, false); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); - Node seven = d_nodeManager->mkConst(Rational(7)); + Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)); ASSERT_EQ(seven, result); // translating integer constants should not change them diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index 8185c2354..9aeedbfe6 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -80,7 +80,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple) Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType()); // make the expression (PLUS x y (MULT z 0)) - Node zero = d_nodeManager->mkConst(Rational("0")); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero); Node n = d_nodeManager->mkNode(PLUS, x, y, zTimesZero); @@ -111,8 +111,8 @@ TEST_F(TestTheoryWhiteEngine, rewriter_complex) "g", d_nodeManager->mkFunctionType(d_nodeManager->realType(), d_nodeManager->integerType())); - Node one = d_nodeManager->mkConst(Rational("1")); - Node two = d_nodeManager->mkConst(Rational("2")); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational("1")); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational("2")); Node f1 = d_nodeManager->mkNode(APPLY_UF, f, one); Node f2 = d_nodeManager->mkNode(APPLY_UF, f, two); diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 5f440006b..aee6a249b 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -18,11 +18,11 @@ #include "test_smt.h" #include "util/rational.h" -namespace cvc5 { - -using namespace theory; -using namespace smt; +using namespace cvc5::kind; +using namespace cvc5::theory; +using namespace cvc5::smt; +namespace cvc5 { namespace test { class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit @@ -44,8 +44,8 @@ class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteIntOpt, max) { - Node ub = d_nodeManager->mkConst(Rational("100")); - Node lb = d_nodeManager->mkConst(Rational("0")); + Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); + Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); // Objectives to be optimized max_cost is max objective Node max_cost = d_nodeManager->mkVar(*d_intType); @@ -75,8 +75,8 @@ TEST_F(TestTheoryWhiteIntOpt, max) TEST_F(TestTheoryWhiteIntOpt, min) { - Node ub = d_nodeManager->mkConst(Rational("100")); - Node lb = d_nodeManager->mkConst(Rational("0")); + Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); + Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); // Objectives to be optimized max_cost is max objective Node max_cost = d_nodeManager->mkVar(*d_intType); @@ -106,8 +106,8 @@ TEST_F(TestTheoryWhiteIntOpt, min) TEST_F(TestTheoryWhiteIntOpt, result) { - Node ub = d_nodeManager->mkConst(Rational("100")); - Node lb = d_nodeManager->mkConst(Rational("0")); + Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); + Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); // Objectives to be optimized max_cost is max objective Node max_cost = d_nodeManager->mkVar(*d_intType); @@ -134,9 +134,9 @@ TEST_F(TestTheoryWhiteIntOpt, result) TEST_F(TestTheoryWhiteIntOpt, open_interval) { - Node ub1 = d_nodeManager->mkConst(Rational("100")); - Node lb1 = d_nodeManager->mkConst(Rational("0")); - Node lb2 = d_nodeManager->mkConst(Rational("110")); + Node ub1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); + Node lb1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); + Node lb2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("110")); Node cost1 = d_nodeManager->mkVar(*d_intType); Node cost2 = d_nodeManager->mkVar(*d_intType); diff --git a/test/unit/theory/theory_sets_rewriter_white.cpp b/test/unit/theory/theory_sets_rewriter_white.cpp new file mode 100644 index 000000000..49dbe0c73 --- /dev/null +++ b/test/unit/theory/theory_sets_rewriter_white.cpp @@ -0,0 +1,93 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * White box testing of sets rewriter + */ + +#include "expr/dtype.h" +#include "expr/emptyset.h" +#include "test_smt.h" +#include "theory/sets/theory_sets_rewriter.h" +#include "util/rational.h" +#include "util/string.h" + +namespace cvc5 { + +using namespace theory; +using namespace kind; +using namespace theory::sets; + +namespace test { + +typedef expr::Attribute<Node, Node> attribute; + +class TestTheoryWhiteSetsRewriter : public TestSmt +{ + protected: + void SetUp() override + { + TestSmt::SetUp(); + d_rewriter.reset(new TheorySetsRewriter()); + } + std::unique_ptr<TheorySetsRewriter> d_rewriter; +}; + +TEST_F(TestTheoryWhiteSetsRewriter, map) +{ + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + TypeNode stringType = d_nodeManager->stringType(); + TypeNode integerType = d_nodeManager->integerType(); + Node emptysetInteger = + d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(integerType))); + Node emptysetString = + d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(stringType))); + Node x = d_nodeManager->mkBoundVar("x", stringType); + Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, x); + Node lambda = d_nodeManager->mkNode(LAMBDA, bound, one); + + // (set.map (lambda ((x U)) t) (as set.empty (Set String)) = + // (as set.empty (Set Int)) + Node n1 = d_nodeManager->mkNode(SET_MAP, lambda, emptysetString); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == emptysetInteger + && response1.d_status == REWRITE_DONE); + + Node a = d_nodeManager->mkConst(String("a")); + Node b = d_nodeManager->mkConst(String("b")); + Node A = d_nodeManager->mkSingleton(d_nodeManager->stringType(), a); + Node B = d_nodeManager->mkSingleton(d_nodeManager->stringType(), b); + Node unionAB = d_nodeManager->mkNode(SET_UNION, A, B); + + // (set.map + // (lambda ((x String)) 1) + // (set.union (set.singleton "a") (set.singleton "b"))) = (set.singleton 1)) + Node n2 = d_nodeManager->mkNode(SET_MAP, lambda, unionAB); + Node rewritten2 = Rewriter::rewrite(n2); + Node bag = d_nodeManager->mkSingleton(d_nodeManager->integerType(), one); + ASSERT_TRUE(rewritten2 == bag); + + // - (set.map f (set.union K1 K2)) = + // (set.union (set.map f K1) (set.map f K2)) + Node k1 = d_skolemManager->mkDummySkolem("K1", A.getType()); + Node k2 = d_skolemManager->mkDummySkolem("K2", A.getType()); + Node f = d_skolemManager->mkDummySkolem("f", lambda.getType()); + Node unionK1K2 = d_nodeManager->mkNode(SET_UNION, k1, k2); + Node n3 = d_nodeManager->mkNode(SET_MAP, f, unionK1K2); + Node rewritten3 = Rewriter::rewrite(n3); + Node mapK1 = d_nodeManager->mkNode(SET_MAP, f, k1); + Node mapK2 = d_nodeManager->mkNode(SET_MAP, f, k2); + Node unionMapK1K2 = d_nodeManager->mkNode(SET_UNION, mapK1, mapK2); + ASSERT_TRUE(rewritten3 == unionMapK1K2); +} + +} // namespace test +} // namespace cvc5 diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index 2fcd626e3..f5ca53451 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -19,10 +19,9 @@ #include "theory/sets/singleton_op.h" #include "util/rational.h" -namespace cvc5 { - using namespace cvc5::api; +namespace cvc5 { namespace test { class TestTheoryWhiteSetsTypeRuleApi : public TestApi @@ -68,8 +67,9 @@ TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node) d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->integerType())); Node singletonReal = d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->realType())); - Node intConstant = d_nodeManager->mkConst(Rational(1)); - Node realConstant = d_nodeManager->mkConst(Rational(1, 5)); + Node intConstant = d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1)); + Node realConstant = + d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1, 5)); // (singleton (singleton_op Real) 1) ASSERT_NO_THROW( d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant)); diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 24ed0cd06..bb4b8122b 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -21,10 +21,10 @@ #include "util/rational.h" #include "util/string.h" -namespace cvc5 { - -using namespace theory::strings; +using namespace cvc5::kind; +using namespace cvc5::theory::strings; +namespace cvc5 { namespace test { class TestTheoryBlackStringsSkolemCache : public TestSmt @@ -33,7 +33,7 @@ class TestTheoryBlackStringsSkolemCache : public TestSmt TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) { - Node zero = d_nodeManager->mkConst(Rational(0)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType()); Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType()); Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType()); diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index bb7ef871c..ac7472560 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -75,64 +75,64 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arith) { TypeEnumerator te(d_nodeManager->integerType()); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0))); + ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); for (int i = 1; i <= 100; ++i) { ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(i))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(i))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-i))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-i))); } ASSERT_FALSE(te.isFinished()); te = TypeEnumerator(d_nodeManager->realType()); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 3))); + ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 3))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 1))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(6, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-6, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 6))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(6, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-6, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 6))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 6))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(7, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-7, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 7))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 7))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 6))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(7, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-7, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 7))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 7))); ASSERT_FALSE(te.isFinished()); } @@ -265,26 +265,26 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite) // ensure that certain items were found TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zeroes = d_nodeManager->mkConst( - ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(0)))); - Node ones = d_nodeManager->mkConst( - ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(1)))); - Node twos = d_nodeManager->mkConst( - ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(2)))); - Node threes = d_nodeManager->mkConst( - ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(3)))); - Node fours = d_nodeManager->mkConst( - ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(4)))); - Node tens = d_nodeManager->mkConst( - ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(10)))); + Node zeroes = d_nodeManager->mkConst(ArrayStoreAll( + arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))); + Node ones = d_nodeManager->mkConst(ArrayStoreAll( + arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)))); + Node twos = d_nodeManager->mkConst(ArrayStoreAll( + arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)))); + Node threes = d_nodeManager->mkConst(ArrayStoreAll( + arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)))); + Node fours = d_nodeManager->mkConst(ArrayStoreAll( + arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)))); + Node tens = d_nodeManager->mkConst(ArrayStoreAll( + arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)))); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node two = d_nodeManager->mkConst(Rational(2)); - Node three = d_nodeManager->mkConst(Rational(3)); - Node four = d_nodeManager->mkConst(Rational(4)); - Node five = d_nodeManager->mkConst(Rational(5)); - Node eleven = d_nodeManager->mkConst(Rational(11)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); + Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); + Node eleven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(11)); ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)), elts.end()); diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 1272926db..887a214dd 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -18,6 +18,8 @@ #include "test_smt.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { namespace test { @@ -30,15 +32,15 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TypeNode usort = d_nodeManager->mkSort("U"); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->realType()), - d_nodeManager->mkConst(Rational(9, 2))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), - d_nodeManager->mkConst(Rational(0))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->integerType()), - d_nodeManager->mkConst(Rational(0))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); } TEST_F(TestUtilWhiteArrayStoreAll, type_errors) @@ -47,13 +49,14 @@ TEST_F(TestUtilWhiteArrayStoreAll, type_errors) d_nodeManager->mkConst(UninterpretedConstant( d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); - ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(Rational(9, 2))), - IllegalArgumentException); + ASSERT_THROW( + ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), + IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->mkSort("U")), - d_nodeManager->mkConst(Rational(9, 2))), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), IllegalArgumentException); } @@ -70,9 +73,10 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error) IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkNode(kind::PLUS, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkConst(Rational(0)))), + d_nodeManager->mkNode( + kind::PLUS, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))), IllegalArgumentException); } } // namespace test diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 760bb2f75..15dde0cc2 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -21,6 +21,8 @@ #include "test_smt.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { namespace test { @@ -247,7 +249,7 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate) const DType& ldt = listType.getDType(); Node updater = ldt[0][0].getUpdater(); Node gt = listType.mkGroundTerm(); - Node zero = d_nodeManager->mkConst(Rational(0)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); Node truen = d_nodeManager->mkConst(true); // construct an update term Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero); |