search

abenkhadra / gosat

SMT solver for the theory of floating-point arithmetic
MIT License
25 stars 8 forks source link

compile error in src/IRGen/FPIRGenerator.cpp #7

Closed florianschanda closed 6 years ago

florianschanda commented 6 years ago

Hi,

I am trying to follow your build instructions (With LLVM 5.0.1 and debian default nlopt), but I get the following compile error:

/home/florian/source/gosat/src/IRGen/FPIRGenerator.cpp: In member function 'const gosat::IRSymbol* gosat::FPIRGenerator::genFuncRecursive(llvm::IRBuilder<>&, z3::expr, bool)':
/home/florian/source/gosat/src/IRGen/FPIRGenerator.cpp:173:52: error: lvalue required as increment operand
         Argument* arg2 = &(*(++m_gofunc->arg_begin()));

We're trying to include gosat in benchmarks, is there possible a chance you could provide me a statically linked x86_64 executable for Linux?

abenkhadra commented 6 years ago

LLVM is a fast moving project, it's difficult to keep code compatible with it. Currently, we support LLVM v4.0.1 which is not compatible with the version you are using.

Build instructions and exact list of dependencies can be found in the README.

florianschanda commented 6 years ago

Indeed, that allowed me to build gosat, thanks!

I should note that I've tried running it and it generally works on the "griggio" benchmarks, but it does throw a lot of exceptions on pretty much anything else (even if its clearly in the QF_FP logic). Is that expected?

abenkhadra commented 6 years ago

It depends. Support for QF_FP is still incomplete which means that some exceptions are expected. I remember encountering those on the wintersteiger benchmark set. These benchmarks can be found in the same package together with the griggio benchmarks.

Time didn't permit to look further into those. If you are interested in specific QF_FP constructs you may post some examples here. I'll come back to them later.