drio # formula x
drio # x := 1 > 1
drio # x

I think it should return false.

@soonhokong

Hi Soonho,

Do you know anything about this? I can't seem to find why cmake is running the custom command "bison" and generating the files twice.

Jichao

There is currently an error with CMake, such that in a clean build (OSX 10.9) it will fail giving the error.

clang: error: no such file or directory: '/Users/sun/dReal/drio/build/shell/lexer.yy.cc'
clang: error: no input files

This is due to CMake not generating the lexer.yy.cc file.

[ 43%] Generating lexer.yy.cc
/usr/local/Cellar/cmake/2.8.12.2/bin/cmake -E cmake_progress_report /Users/sun/dReal/drio/build/CMakeFiles 10
[ 52%] Building CXX object shell/CMakeFiles/SH_UTIL.dir/lexer.yy.cc.o

I'm not sure why this is behaving this way, however if I save the file src/CMakeList.txt, then run "make" it will compile nicely. Not sure why this is happening. Will update.

There is a known issue with mac-ports version of flex that generates a file which uses (size_t) instead of (int)^[1]. All unmodified flex versions uses (int)

size_t LexerInput( char* buf, size_t max_size );
void LexerOutput( const char* buf, size_t size );

vs

int LexerInput( char* buf, int max_size );
void LexerOutput( const char* buf, int size );

So to allow for cross platform we need to be able to check when we are using a macports version of flex or unmodified flex. I'm still figuring out how to do that, but currently for all OSX we use FlexLexer_osx.h and the original file for all else

[1] https://bugs.launchpad.net/zorba/+bug/1034582

Currently while bison is generating the parse tree, for each "operation" we have a stack allocated "expr" object. Which then has a pointer to the heap allocated "expr_cell".

Currently if you define a formula and evaluate it, the program segfaults. I think this is due to the stack objects being free'd and the "fmla_scoped_env map" is only storing the root expr object of the "expr" tree. Resulting in calls do dealloc'd objects.

Currently working on workaround.