summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2018-01-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2017-12-20Add rewriting rule for ranking benchmarks. (#1448)Mathias Preiner
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-29Adding missing break statements. CID 1362756. (#1394)Tim King
2017-10-20Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)Mathias Preiner
2017-10-20Simplify atoms introduced while bitblasting. (#1267)Mathias Preiner
2017-10-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-09-26Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)Tim King
2017-09-25Fixing CID 1362895: Initializing d_bvp to nullptr. (#1137)Tim King
2017-08-31Replace CVC4_THREADLOCAL in interactive_shell (#1065)Andres Noetzli
2017-08-23Fix typosAndres Noetzli
2017-08-21Cleanup: use Assert rather than C assert. (#1052)Aina Niemetz
2017-08-09Remove AigBitblaster implementation if ABC is not compiled (#212)Mathias Preiner
2017-08-09Fix Assertion (compiler warning) in theory/bv/theory_bv.cppAina Niemetz
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-07Update copyright headers.Mathias Preiner
2017-06-14Remove UdivSelf rewrite, add UdivZero rewriteAndres Noetzli
2017-06-03Fix compile errorClark Barrett
2017-05-31Fix model construction for BV with cbqi. Minor change to defaults.ajreynol
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-03-28Fix for bug 733Clark Barrett
2017-03-27Minor cleanups to ExtTheory.Tim King
2017-03-27Merge pull request #137 from 4tXJ7f/throw_qualsClark Barrett
2017-03-27Making the ExtTheory object a private member of Theory.Tim King
2017-03-27Remove throw qualifiers in type enumeratorsAndres Notzli
2017-03-06Adding support for bool-to-bvClark Barrett
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-12-29Changing a set of TNodes to a set of Nodes in the BV inequality solver. The r...Tim King
2016-12-08Fix (inactive) `MultSlice` rewriteAndres Notzli
2016-12-02Fix for bug 734Clark Barrett
2016-11-30Remove wrong `ExtractMultLeadingBit` ruleAndres Notzli
2016-11-21Fix `MultDistrib` rewrite ruleAndres Notzli
2016-11-14Minor improvement to caching for extf bv inferences.ajreynol
2016-11-11Enable eager bitblasting for QF_ABV when no stores are present.Clark Barrett
2016-11-11Add simple inferences for extended bitvector functions, add a few related opt...ajreynol
2016-11-10Add option for enabling/disabling lazy extended function reduction in bitvect...ajreynol
2016-11-07Fixing a memory leak in the eager bitblaster.Tim King
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-10-02Removing the throw specifiers from theory_bv_type_rules.h.Tim King
2016-09-25Deleting the eager bitblasting solver if present in TheoryBV.Tim King
2016-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the con...Tim King
2016-08-16Initial infrastructure for ExtTheory, generalize extended term handling in Th...ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-05-27Merged QF_UFBV support from experimental branchClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback