summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
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
2016-05-26Changed aig_bitblaster to work with cryptominisatlianah
2016-05-26Fix for aig_bitblaster.cppKshitij Bansal
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
2016-03-22Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.Tim King
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-02-01Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-15Type enumerators take optional argument indicating fixed cardinalities of uni...ajreynol
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-08-24Added threshold for core bv cardinality lemmasLiana Hadarean
2015-08-24Fix for bv core cardinality lemma generationLiana Hadarean
2015-08-24eager bit-blasting gives models for boolean variables too (fixes bug618)Liana Hadarean
2015-08-20fix to bug659 due to algebraic solver model buildingLiana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback