Get models in SMTLIB2 format without printing ASSERTs (Mac specific issue?)

[gussmith23]

Hi all. We're trying to add support for STP to Rosette. One of the main blockers are the ASSERT statements that get printed out when the -p switch is enabled:

fortyfort ➜ stp  /Users/gus/rosette/test/tmp/rosette17023399591702339959206.smt2 
sat
unsupported
fortyfort ➜  stp -p /Users/gus/rosette/test/tmp/rosette17023399591702339959206.smt2
ASSERT( c3 = 0x8 );
ASSERT( c5<=>FALSE );
ASSERT( c1 = 0x8 );
sat
(
( define-fun |c3| () (_ BitVec 4)(_ bv8 4) )
( define-fun |c5| () Bool  )
( define-fun |c1| () (_ BitVec 4)(_ bv8 4) )
)

We need -p so that we get the model out (as seen in the second command), but -p also adds those unnecessary ASSERTs. Is there an easy way to disable those while still enabling model production?

[gussmith23]

Huh, I'm realizing now that, for example, c5 in this example above doesn't have its value encoded in the outputted model after sat. Why is that? Shouldn't it be

( define-fun |c5| () Bool  false)

?

[TrevorHansen]

Thanks @gussmith23, Can you please attach the file that produces the incorrect model? Thanks!

[gussmith23]

Yup, here you go!

(define-fun e0 () (_ BitVec 4) (bvneg (_ bv8 4)))
(declare-fun c1 () (_ BitVec 4))
(define-fun e2 () Bool (= e0 c1))
(assert e2)
(declare-fun c3 () (_ BitVec 4))
(define-fun e4 () Bool (= e0 c3))
(assert e4)
(declare-fun c5 () Bool)
(define-fun e6 () Bool (bvslt c1 c3))
(define-fun e7 () Bool (and (=> c5 e6) (=> e6 c5)))
(assert e7)
(check-sat)
(get-model)

[gussmith23]

And my version info:

STP version 2.3.3
STP version SHA string GITDIR-NOTFOUND
STP compilation options CMAKE_CXX_COMPILER = clang++ | CMAKE_CXX_FLAGS =  -stdlib=libc++ -Wall -Wextra -Wunused -pedantic -Wsign-compare -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wheader-guard -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code | COMPILE_DEFINES =  -DNDEBUG -D__STDC_LIMIT_MACROS -DUSE_CRYPTOMINISAT | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATICCOMPILE = OFF | TUNE_NATIVE = OFF | COVERAGE = OFF | FORCE_CMS = OFF | LIBS = /usr/local/lib/libminisat.dylib | ENABLE_TESTING = OFF | ENABLE_PYTHON_INTERFACE = ON | PYTHON_EXECUTABLE = /usr/local/opt/python@3.11/bin/python3.11 | PYTHON_LIBRARY = /usr/local/opt/python@3.11/Frameworks/Python.framework/Versions/3.11/lib/libpython3.11.dylib | PYTHON_INCLUDE_DIRS = /usr/local/opt/python@3.11/Frameworks/Python.framework/Versions/3.11/include/python3.11 |  | compilation date time = Jun 13 2023 08:46:07
c compiled with gcc version Apple LLVM 13.0.0 (clang-1300.0.29.30)

[TrevorHansen]

Seems to work fine for me:

sat
(model
( define-fun |c1| () (_ BitVec 4) #x8 )
( define-fun |c3| () (_ BitVec 4) #x8 )
( define-fun |c5| () Bool false )
)

on

STP version 2.3.3
STP version SHA string f0e9c0e0535d58a124d00888f625dba1b6b7cf87
STP compilation options CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -fno-omit-frame-pointer | COMPILE_DEFINES =  -D__STDC_LIMIT_MACROS -DUSE_CRYPTOMINISAT | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATICCOMPILE = OFF | TUNE_NATIVE = OFF | COVERAGE = OFF | FORCE_CMS = OFF | LIBS = /home/thansen/solvers/stp/deps/install/lib/libminisat.so | ENABLE_TESTING = ON | ENABLE_PYTHON_INTERFACE = ON | PYTHON_EXECUTABLE = /usr/bin/python | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  |  | compilation date time = Dec 12 2023 14:09:25
c compiled with gcc version 11.4.0

Can you rebuild from the main branch?

[gussmith23]

Hm, I am on Mac so I used Homebrew. Will that give me the latest version? The same problem is still manifesting. Version info isn't super useful this time:

STP version 2.3.3
STP version SHA string GITDIR-NOTFOUND
STP compilation options CMAKE_CXX_COMPILER = clang++ | CMAKE_CXX_FLAGS =  -stdlib=libc++ -Wall -Wextra -Wunused -pedantic -Wsign-compare -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wheader-guard -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code | COMPILE_DEFINES =  -DNDEBUG -D__STDC_LIMIT_MACROS -DUSE_CRYPTOMINISAT | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATICCOMPILE = OFF | TUNE_NATIVE = OFF | COVERAGE = OFF | FORCE_CMS = OFF | LIBS = /usr/local/lib/libminisat.dylib | ENABLE_TESTING = OFF | ENABLE_PYTHON_INTERFACE = ON | PYTHON_EXECUTABLE = /usr/local/opt/python@3.12/bin/python3.12 | PYTHON_LIBRARY = /usr/local/opt/python@3.12/Frameworks/Python.framework/Versions/3.12/lib/libpython3.12.dylib | PYTHON_INCLUDE_DIRS = /usr/local/opt/python@3.12/Frameworks/Python.framework/Versions/3.12/include/python3.12 |  | compilation date time = Dec 12 2023 06:02:30
c compiled with gcc version Apple LLVM 13.0.0 (clang-1300.0.29.30)

[aytey]

Are you on Apple silicon? What version of macOS?

(I have access to an M1, but not until next week)

[gussmith23]

I'm on Mac x86 (2018 Macbook Pro) running MacOS 11.7.8.

[gussmith23]

Just verified that it works as expected on Ubuntu. So this does seem to be a problem specifically on Mac. Still a significant issue for me b/c I mainly develop on Mac!

[gussmith23]

Is it possible to build from source on Mac? I tried the build instructions and ran into an issue immediately, so I defaulted to the Homebrew install instead. It seems, though, that I do need the latest build on Mac. Are there Mac instructions?