8000 str.contains Performance Issue · Issue #11460 · cvc5/cvc5 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

str.contains Performance Issue #11460

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
rachelcleaveland opened this issue Dec 18, 2024 · 0 comments
Open

str.contains Performance Issue #11460

rachelcleaveland opened this issue Dec 18, 2024 · 0 comments
Assignees
@ajreynol

Comments

@rachelcleaveland
Copy link

Describe the bug
assertions.smt2.txt
Not a bug but a performance issue. In the above assertions, adding in the very last assertion makes the solve time go from 0.5 seconds to ~30 seconds on my machine. However, the last assertion clearly makes the set of assertions unsat, because the assertion on line 79 ((not (str.contains (str.substr stdin0 (+ 2 i1 i2) i3) "\u{a}"))) prevents the substring (str.substr stdin0 (+ 1 i1 i2 i3) 1) on the last line from being equal to "\u{a}" (whose code point is 10).

Command line arguments:
cvc5 version/commit: This is cvc5 version 1.1.3-dev.441.2d09b3c91 [git 2d09b3c on branch main with local modifications]
Operating system: Ubuntu 22.04.4 LTS

configure.sh options

configure.sh output
-- The C compiler identification is GNU 11.4.0
-- The CXX compiler identification is GNU 11.4.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found Git: /usr/bin/git (found version "2.34.1")
-- Building Production build
-- Performing Test HAVE_C_FLAG_O3
-- Performing Test HAVE_C_FLAG_O3 - Success
-- Configuring with C flag '-O3'
-- Performing Test HAVE_CXX_FLAG_O3
-- Performing Test HAVE_CXX_FLAG_O3 - Success
-- Configuring with CXX flag '-O3'
-- Performing Test HAVE_C_FLAG_Wall
-- Performing Test HAVE_C_FLAG_Wall - Success
-- Configuring with C flag '-Wall'
-- Performing Test HAVE_CXX_FLAG_Wall
-- Performing Test HAVE_CXX_FLAG_Wall - Success
-- Configuring with CXX flag '-Wall'
-- Performing Test HAVE_C_FLAG_Wunused_private_field
-- Performing Test HAVE_C_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_C_FLAG_Wdangling_reference
-- Performing Test HAVE_C_FLAG_Wdangling_reference - Failed
-- Performing Test HAVE_CXX_FLAG_Wdangling_reference
-- Performing Test HAVE_CXX_FLAG_Wdangling_reference - Failed
-- Performing Test HAVE_C_FLAG_fexceptions
-- Performing Test HAVE_C_FLAG_fexceptions - Success
-- Configuring with C flag '-fexceptions'
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override - Success
-- Configuring with CXX flag '-Wsuggest-override'
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor - Success
-- Configuring with CXX flag '-Wnon-virtual-dtor'
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough - Success
-- Configuring with C flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough - Success
-- Configuring with CXX flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_C_FLAG_Wshadow
-- Performing Test HAVE_C_FLAG_Wshadow - Success
-- Configuring with C flag '-Wshadow'
-- Performing Test HAVE_CXX_FLAG_Wshadow
-- Performing Test HAVE_CXX_FLAG_Wshadow - Success
-- Configuring with CXX flag '-Wshadow'
-- Performing Test HAVE_C_FLAG_fno_operator_names
-- Performing Test HAVE_C_FLAG_fno_operator_names - Failed
-- Performing Test HAVE_CXX_FLAG_fno_operator_names
-- Performing Test HAVE_CXX_FLAG_fno_operator_names - Success
-- Configuring with CXX flag '-fno-operator-names'
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init - Success
-- Configuring with CXX flag '-fno-extern-tls-init'
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess - Success
-- Configuring with CXX flag '-Wno-class-memaccess'
-- Using GNU gold linker.
-- Disabling unit tests since assertions are disabled.
-- Found Python: /usr/bin/python3 (found version "3.10.12") found components: Interpreter
-- Found GMP 6.2.1: /usr/lib/x86_64-linux-gnu/libgmp.so
-- Looking for getc_unlocked
-- Looking for getc_unlocked - not found
-- Building CaDiCaL rel-1.7.4: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/lib/libcadical.a
-- Building Poly 0.1.13: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/lib/libpoly.so, /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/lib/libpolyxx.so
-- Building SymFPU: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/include/
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS - Failed
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD - Failed
-- Looking for unistd.h
-- Looking for unistd.h - found
-- Looking for sys/wait.h
-- Looking for sys/wait.h - found
-- Looking for C++ include ext/stdio_filebuf.h
-- Looking for C++ include ext/stdio_filebuf.h - found
-- Looking for clock_gettime
-- Looking for clock_gettime - found
-- Looking for ffs
-- Looking for ffs - found
-- Looking for optreset
-- Looking for optreset - not found
-- Looking for sigaltstack
-- Looking for sigaltstack - found
-- Looking for strerror_r
-- Looking for strerror_r - found
-- Looking for strtok_r
-- Looking for strtok_r - found
-- Looking for setitimer
-- Looking for setitimer - found
-- Performing Test STRERROR_R_CHAR_P
-- Performing Test STRERROR_R_CHAR_P - Failed
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success

cvc5 1.1.3-dev

Build profile : production

Assertions : off
Debug symbols : off
Debug context mem mgr : off

Muzzle : off
Statistics : on
Tracing : off

ASan : off
UBSan : off
TSan : off
Coverage (gcov) : off
Profiling (gprof) : off
Unit tests : off
Valgrind : off

Shared build : on
Python bindings : off
Java bindings : off
Interprocedural opt. : off

CryptoMiniSat : off
GLPK : off
Kissat : off
LibPoly : on (local)
CoCoALib : off
MP library : gmp (system)
Editline : off

Api docs : off

CPPLAGS (-D...): NDEBUG CVC5_STATISTICS_ON CVC5_USE_POLY
CXXFLAGS : -O3 -Wall -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -fno-operator-names -fno-extern-tls-init -Wno-class-memaccess
CFLAGS : -O3 -Wall -fexceptions -Wimplicit-fallthrough -Wshadow
Linker flags : -fuse-ld=gold

Install prefix : /usr/local

cvc5 license: modified BSD

Note that this configuration is NOT built against any GPL'ed libraries, so
it is covered by the (modified) BSD license. To build against GPL'ed
libraries which can improve cvc5's performance on arithmetic and bit-vector
logics, use the 'configure.sh' script to re-configure with '--best --gpl'.

Now change to 'build' and type 'make', followed by 'make check' or 'make install'.

-- Configuring done
-- Generating done
-- Build files have been written to: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build
@ajreynol ajreynol self-assigned this Dec 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ajreynol ajreynol

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ajreynol @mpreiner @rachelcleaveland
0