]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 15599d1) | patch
Partial fix of bvsmod, bvsrem. Both operations still report spurious division by...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 27 Jul 2009 11:59:44 +0000 (11:59 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 27 Jul 2009 11:59:44 +0000 (11:59 +0000)
commitd454241c653d3d25514ae0ffe4b954b2b1affa5a
tree156efc157cf513476604e992531ff925d5e92d25tree | snapshot
parent15599d18443655e8974cc4e07755182fc2abb011commit | diff
Partial fix of bvsmod, bvsrem. Both operations still report spurious division by zero errors. They work much better than they used to. But not perfectly. See the test cases in misc-tests for examples they currently fail on.

Also, updated BVTypeCheck to return a boolean (so it is easy to use in asserts()). A trivial recursive typecheck function.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@90 e59a4935-1847-0410-ae03-e826735625c1
AST/AST.cpp diff | blob | history
AST/AST.h diff | blob | history
AST/ToSAT.cpp diff | blob | history
AST/Transform.cpp diff | blob | history
AST/genkinds.pl diff | blob | history
bitvec/consteval.cpp diff | blob | history
simplifier/simplifier.cpp diff | blob | history
STP Constraint Solver.