abenkhadra / gosat Goto Github PK
View Code? Open in Web Editor NEWSMT solver for the theory of floating-point arithmetic
License: MIT License
gosat's People
Contributors
Stargazers
Watchers
gosat's Issues
Error emitted on trivial unsat benchmark
goSAT emits an error on this simple example
(assert false)
It emits
,error,0.003,INF,-2
compile error in src/IRGen/FPIRGenerator.cpp
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?
gosat gives `unsat` to satisfiable benchmark
gosat reports this benchmark as unsat even though it is sat
(set-info :smt-lib-version 2.6)
(set-info :category "crafted")
(set-info :source |Christoph M. Wintersteiger ([email protected]). Randomly generated floating-point testcases.|)
; Rounding mode: to zero
; Precision: double (11/53)
; X = 1.1972111975184838161823108748649246990680694580078125p756 {+ 888160275657533 756 (4.53782e+227)}
; Y = 1.791115761572864339967736668768338859081268310546875p645 {+ 3562868649026478 645 (2.61499e+194)}
; 1.1972111975184838161823108748649246990680694580078125p756 = 1.791115761572864339967736668768338859081268310546875p645 == 0
; bres: 0
; hwf : 0
(set-logic QF_FP)
(set-info :status sat)
(define-sort FPN () (_ FloatingPoint 11 53))
(declare-fun x () FPN)
(declare-fun y () FPN)
(assert (= x (fp #b0 #b11011110011 #b0011001001111100011011101101101110111111001100111101)))
(assert (= y (fp #b0 #b11010000100 #b1100101010000110100100000000001101001110001110101110)))
(assert (= (fp.eq x y) false))
(check-sat)
(exit)
This is the eq-has-solution-1355.smt2 benchmark taken from SMT-COMP's QF_FP benchmark suite.
Crash on simple example
goSAT crashes on this simple example
(declare-const x Float32)(assert (and (fp.isNaN x) (not (fp.isNaN x))))
potentially unsound answers
Hi,
We've found the following answers of gosat to be probably incorrect (sat that should be unsat and vice versa).
The filenames below come from my bag of benchmarks. https://github.com/florianschanda/smtlib_schanda I've tried my best to make sure the various status are correct by mistakes are of course possible.
nyxbrain/crafted-edge-cases/RNE:IEEE_equality_is_almost_zero_difference_5_unsat.smt2
nyxbrain/crafted-edge-cases/RNE:the_answer_is_NaN_5_unsat.smt2
nyxbrain/crafted-edge-cases/RTN:IEEE_equality_is_almost_zero_difference_5_unsat.smt2
nyxbrain/crafted-edge-cases/RTN:the_answer_is_NaN_5_unsat.smt2
nyxbrain/crafted-edge-cases/RTP:IEEE_equality_is_almost_zero_difference_5_unsat.smt2
nyxbrain/crafted-edge-cases/RTP:the_answer_is_NaN_5_unsat.smt2
nyxbrain/crafted-edge-cases/RTZ:IEEE_equality_is_almost_zero_difference_5_unsat.smt2
nyxbrain/crafted-edge-cases/RTZ:the_answer_is_NaN_5_unsat.smt2
random/fp.cast/cast_rna_20033.smt2
random/fp.cast/cast_rna_20193.smt2
random/fp.cast/cast_rna_20201.smt2
random/fp.cast/cast_rna_20202.smt2
random/fp.cast/cast_rna_20204.smt2
random/fp.cast/cast_rna_20208.smt2
random/fp.cast/cast_rne_19904.smt2
random/fp.cast/cast_rne_19908.smt2
random/fp.cast/cast_rne_19916.smt2
random/fp.cast/cast_rne_19929.smt2
random/fp.cast/cast_rne_19930.smt2
random/fp.cast/cast_rtn_20753.smt2
random/fp.cast/cast_rtn_20760.smt2
random/fp.cast/cast_rtn_20761.smt2
random/fp.cast/cast_rtn_20763.smt2
random/fp.cast/cast_rtn_20775.smt2
random/fp.cast/cast_rtz_20828.smt2
random/fp.cast/cast_rtz_20879.smt2
random/fp.cast/cast_rtz_20966.smt2
random/fp.cast/cast_rtz_21033.smt2
random/fp.cast/cast_rtz_21034.smt2
random/fp.cast/cast_rtz_21036.smt2
random/fp.cast/cast_rtz_21037.smt2
random/fp.cast/cast_rtz_21040.smt2
random/fp.cast/cast_rtz_21054.smt2
wintersteiger/mul/mul-has-no-other-solution-10044.smt2
wintersteiger/mul/mul-has-no-other-solution-13484.smt2
wintersteiger/mul/mul-has-no-other-solution-15092.smt2
wintersteiger/mul/mul-has-no-other-solution-15226.smt2
wintersteiger/mul/mul-has-no-other-solution-15435.smt2
wintersteiger/mul/mul-has-no-other-solution-15552.smt2
wintersteiger/mul/mul-has-no-other-solution-19889.smt2
wintersteiger/mul/mul-has-no-other-solution-3202.smt2
wintersteiger/mul/mul-has-no-other-solution-3804.smt2
wintersteiger/mul/mul-has-no-other-solution-7814.smt2
wintersteiger/mul/mul-has-no-other-solution-8691.smt2
Crash in llvm::ConstantHoistingPass
When run on the following example gosat SEGFAULTs.
(set-logic QF_FP)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(declare-fun x () (_ FloatingPoint 8 24))
(define-fun _t_10 () (_ FloatingPoint 8 24) (fp #b0 #b01111111 #b00000000000000000000001))
(define-fun _t_15 () Bool (fp.leq x _t_10))
(assert _t_15)
(assert (fp.isNaN x))
(check-sat)
The backtrace is as follows
#0 0x0000000000c81fda in llvm::ConstantHoistingPass::collectConstantCandidates(llvm::DenseMap<llvm::ConstantInt*, unsigned int, llvm::DenseMapInfo<llvm::ConstantInt*>, llvm::detail::DenseMa
pPair<llvm::ConstantInt*, unsigned int> >&, llvm::Instruction*) ()
#1 0x0000000000c82146 in llvm::ConstantHoistingPass::collectConstantCandidates(llvm::Function&) ()
#2 0x0000000000c821a9 in llvm::ConstantHoistingPass::runImpl(llvm::Function&, llvm::TargetTransformInfo&, llvm::DominatorTree&, llvm::BasicBlock&) ()
#3 0x0000000000ebe492 in llvm::FPPassManager::runOnFunction(llvm::Function&) ()
#4 0x0000000000ebe82b in llvm::FPPassManager::runOnModule(llvm::Module&) ()
#5 0x0000000000ebe0df in llvm::legacy::PassManagerImpl::run(llvm::Module&) ()
#6 0x00000000006b37d2 in llvm::MCJIT::emitObject(llvm::Module*) ()
#7 0x00000000006b3cb5 in llvm::MCJIT::generateCodeForModule(llvm::Module*) ()
#8 0x00000000006b0e64 in llvm::MCJIT::finalizeObject() ()
#9 0x00000000005deace in main (argc=3, argv=0x7fffffffe6a8) at /home/user/gosat/src/src/main.cpp:196
This is on Ubuntu 16.04LTS using the llvm 3.9 that ships with the distribution.
$ llvm-config-3.9 --version
3.9.1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.