mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
a7779de22d
This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.
26 lines
851 B
Python
26 lines
851 B
Python
##############################################################################
|
|
# Top contributors (to current version):
|
|
# Yoni Zohar
|
|
#
|
|
# 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.
|
|
# ############################################################################
|
|
#
|
|
# Test for issue #5074
|
|
##
|
|
|
|
import cvc5
|
|
from cvc5 import Kind
|
|
|
|
slv = cvc5.Solver()
|
|
c1 = slv.mkConst(slv.getIntegerSort())
|
|
t6 = slv.mkTerm(Kind.StringFromCode, c1)
|
|
t12 = slv.mkTerm(Kind.StringToRegexp, t6)
|
|
t14 = slv.mkTerm(Kind.StringReplaceRe, t6, t12, t6)
|
|
t16 = slv.mkTerm(Kind.StringContains, t14, t14)
|
|
slv.checkSatAssuming(t16.notTerm())
|