R Under development (unstable) (2022-09-04 r82801) -- "Unsuffered Consequences" Copyright (C) 2022 The R Foundation for Statistical Computing Platform: x86_64-pc-linux-gnu (64-bit) R is free software and comes with ABSOLUTELY NO WARRANTY. You are welcome to redistribute it under certain conditions. Type 'license()' or 'licence()' for distribution details. Natural language support but running in an English locale R is a collaborative project with many contributors. Type 'contributors()' for more information and 'citation()' on how to cite R or R packages in publications. Type 'demo()' for some demos, 'help()' for on-line help, or 'help.start()' for an HTML browser interface to help. Type 'q()' to quit R. > pkgname <- "rpicosat" > source(file.path(R.home("share"), "R", "examples-header.R")) > options(warn = 1) > library('rpicosat') > > base::assign(".oldSearch", base::search(), pos = 'CheckExEnv') > base::assign(".old_wd", base::getwd(), pos = 'CheckExEnv') > cleanEx() > nameEx("picosat_sat") > ### * picosat_sat > > flush(stderr()); flush(stdout()) > > ### Name: picosat_sat > ### Title: Solve SAT problems with the 'PicoSAT' solver > ### Aliases: picosat_sat > > ### ** Examples > > # solve a boolean formula > # (not a or b) and (not b or c) > # each variable is an integer > # negations are negative integers > formula <- list( + c(-1L, 2L), + c(-2L, 3L) + ) > res <- picosat_sat(formula) picosat.c:2820:37: runtime error: applying zero offset to null pointer #0 0x7f1a01f286d2 in fix_impl_lits /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:2820:37 #1 0x7f1a01f286d2 in enlarge /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:2928:7 #2 0x7f1a01f29012 in inc_max_var /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:4487:5 #3 0x7f1a01f30ca0 in import_lit /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:6379:2 #4 0x7f1a01f3063e in picosat_add /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:6873:13 #5 0x7f1a01f77301 in rpicosat_solve /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/r_picosat.c:12:5 #6 0x6e6376 in R_doDotCall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:604:17 #7 0x732e09 in do_dotcall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:1284:11 #8 0x8400e5 in bcEval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:7126:14 #9 0x82ab1e in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:748:8 #10 0x893013 in R_execClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c #11 0x88ecbf in Rf_applyClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:1844:16 #12 0x82b558 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:871:12 #13 0x89f111 in do_set /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:2981:8 #14 0x82af08 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:823:12 #15 0x95be26 in Rf_ReplIteration /data/gannet/ripley/R/svn/R-devel/src/main/main.c:264:2 #16 0x95f370 in R_ReplConsole /data/gannet/ripley/R/svn/R-devel/src/main/main.c:316:11 #17 0x95f179 in run_Rmainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1194:5 #18 0x95f4b2 in Rf_mainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1201:5 #19 0x4f30ba in main /data/gannet/ripley/R/svn/R-devel/src/main/Rmain.c:29:5 #20 0x7f1a115a1b74 in __libc_start_main (/lib64/libc.so.6+0x27b74) (BuildId: 08df60634339b221bb854d4e10b7278cafde70c4) #21 0x43231d in _start (/data/gannet/ripley/R/R-clang-SAN/bin/exec/R+0x43231d) SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior picosat.c:2820:37 in picosat.c:3432:33: runtime error: applying non-zero offset 24 to null pointer #0 0x7f1a01f740f8 in satisfied /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:3432:33 #1 0x7f1a01f36c3f in sat /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:5911:7 #2 0x7f1a01f36864 in picosat_sat /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:7151:9 #3 0x7f1a01f77405 in rpicosat_solve /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/r_picosat.c:22:13 #4 0x6e6376 in R_doDotCall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:604:17 #5 0x732e09 in do_dotcall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:1284:11 #6 0x8400e5 in bcEval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:7126:14 #7 0x82ab1e in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:748:8 #8 0x893013 in R_execClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c #9 0x88ecbf in Rf_applyClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:1844:16 #10 0x82b558 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:871:12 #11 0x89f111 in do_set /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:2981:8 #12 0x82af08 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:823:12 #13 0x95be26 in Rf_ReplIteration /data/gannet/ripley/R/svn/R-devel/src/main/main.c:264:2 #14 0x95f370 in R_ReplConsole /data/gannet/ripley/R/svn/R-devel/src/main/main.c:316:11 #15 0x95f179 in run_Rmainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1194:5 #16 0x95f4b2 in Rf_mainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1201:5 #17 0x4f30ba in main /data/gannet/ripley/R/svn/R-devel/src/main/Rmain.c:29:5 #18 0x7f1a115a1b74 in __libc_start_main (/lib64/libc.so.6+0x27b74) (BuildId: 08df60634339b221bb854d4e10b7278cafde70c4) #19 0x43231d in _start (/data/gannet/ripley/R/R-clang-SAN/bin/exec/R+0x43231d) SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior picosat.c:3432:33 in picosat.c:3904:13: runtime error: applying zero offset to null pointer #0 0x7f1a01f66691 in prop2 /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:3904:13 #1 0x7f1a01f66691 in bcp /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:4334:4 #2 0x7f1a01f52c34 in flbcp /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:4990:3 #3 0x7f1a01f52c34 in faillits /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:5119:7 #4 0x7f1a01f2c9d4 in simplify /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:5355:3 #5 0x7f1a01f3aff5 in sat /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:5915:5 #6 0x7f1a01f36864 in picosat_sat /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:7151:9 #7 0x7f1a01f77405 in rpicosat_solve /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/r_picosat.c:22:13 #8 0x6e6376 in R_doDotCall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:604:17 #9 0x732e09 in do_dotcall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:1284:11 #10 0x8400e5 in bcEval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:7126:14 #11 0x82ab1e in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:748:8 #12 0x893013 in R_execClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c #13 0x88ecbf in Rf_applyClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:1844:16 #14 0x82b558 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:871:12 #15 0x89f111 in do_set /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:2981:8 #16 0x82af08 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:823:12 #17 0x95be26 in Rf_ReplIteration /data/gannet/ripley/R/svn/R-devel/src/main/main.c:264:2 #18 0x95f370 in R_ReplConsole /data/gannet/ripley/R/svn/R-devel/src/main/main.c:316:11 #19 0x95f179 in run_Rmainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1194:5 #20 0x95f4b2 in Rf_mainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1201:5 #21 0x4f30ba in main /data/gannet/ripley/R/svn/R-devel/src/main/Rmain.c:29:5 #22 0x7f1a115a1b74 in __libc_start_main (/lib64/libc.so.6+0x27b74) (BuildId: 08df60634339b221bb854d4e10b7278cafde70c4) #23 0x43231d in _start (/data/gannet/ripley/R/R-clang-SAN/bin/exec/R+0x43231d) SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior picosat.c:3904:13 in picosat.c:4712:31: runtime error: applying zero offset to null pointer #0 0x7f1a01f5d60d in collect_clauses /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:4712:31 #1 0x7f1a01f2d5f9 in simplify /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:5426:3 #2 0x7f1a01f3aff5 in sat /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:5915:5 #3 0x7f1a01f36864 in picosat_sat /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/picosat.c:7151:9 #4 0x7f1a01f77405 in rpicosat_solve /data/gannet/ripley/R/packages/tests-clang-SAN/rpicosat/src/r_picosat.c:22:13 #5 0x6e6376 in R_doDotCall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:604:17 #6 0x732e09 in do_dotcall /data/gannet/ripley/R/svn/R-devel/src/main/dotcode.c:1284:11 #7 0x8400e5 in bcEval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:7126:14 #8 0x82ab1e in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:748:8 #9 0x893013 in R_execClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c #10 0x88ecbf in Rf_applyClosure /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:1844:16 #11 0x82b558 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:871:12 #12 0x89f111 in do_set /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:2981:8 #13 0x82af08 in Rf_eval /data/gannet/ripley/R/svn/R-devel/src/main/eval.c:823:12 #14 0x95be26 in Rf_ReplIteration /data/gannet/ripley/R/svn/R-devel/src/main/main.c:264:2 #15 0x95f370 in R_ReplConsole /data/gannet/ripley/R/svn/R-devel/src/main/main.c:316:11 #16 0x95f179 in run_Rmainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1194:5 #17 0x95f4b2 in Rf_mainloop /data/gannet/ripley/R/svn/R-devel/src/main/main.c:1201:5 #18 0x4f30ba in main /data/gannet/ripley/R/svn/R-devel/src/main/Rmain.c:29:5 #19 0x7f1a115a1b74 in __libc_start_main (/lib64/libc.so.6+0x27b74) (BuildId: 08df60634339b221bb854d4e10b7278cafde70c4) #20 0x43231d in _start (/data/gannet/ripley/R/R-clang-SAN/bin/exec/R+0x43231d) SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior picosat.c:4712:31 in > picosat_solution_status(res) [1] "PICOSAT_SATISFIABLE" > > # set a variable to a fixed value > # e.g. a = TRUE and b = TRUE > res <- picosat_sat(formula, assumptions = c(1L, 2L)) > picosat_solution_status(res) [1] "PICOSAT_SATISFIABLE" > > # get further information about the solution process > picosat_variables(res) [1] 3 > picosat_added_original_clauses(res) [1] 2 > picosat_decisions(res) [1] 1 > picosat_propagations(res) [1] 10 > picosat_visits (res) [1] 6 > picosat_seconds(res) [1] 4e-05 > > > > > ### *