abenkhadra / gosat Goto Github PK
View Code? Open in Web Editor NEWSMT solver for the theory of floating-point arithmetic
License: MIT License
SMT solver for the theory of floating-point arithmetic
License: MIT License
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
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.
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?
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
goSAT crashes on this simple example
(declare-const x Float32)(assert (and (fp.isNaN x) (not (fp.isNaN x))))
goSAT emits an error on this simple example
(assert false)
It emits
,error,0.003,INF,-2
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.