summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
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
2015-08-20fix for bug660 and bug658 due to incorrect bit-blasting of divison by zeroLiana Hadarean
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-05-29changed resource step options to unsignedlianah
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-03-25change const are triggers from false to true in equality enginesKshitij Bansal
2015-03-14Bug fix for BVTianyi Liang
2015-01-22Narrow sygus search space based on NNF and rewriting constant arguments.ajreynol
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-11-18clear model cache in BVQuickCheck clearSolver() (fixes bug 587)Liana Hadarean
2014-11-17added command line option for extractArith bv rewritelianah
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-12BV inequality graph TNode fix.Morgan Deters
2014-11-12Fix BV inequality solver caching.Morgan Deters
2014-11-07Remove some unused variables.Morgan Deters
2014-11-07Fix memory issues in bitvector theory, which is now valgrind-clean (mostly re...Morgan Deters
2014-10-29Added new, much faster, care graph computation for arraysClark Barrett
2014-10-23Fixed inefficiency in bit-vector rewrite rule.lianah
2014-10-14fix for memory leak in BVQuickChecklianah
2014-09-27Merge branch '1.4.x'Morgan Deters
2014-09-27Fix infinite loop in --bitblast-aig/--bv-aig-simp options.Morgan Deters
2014-09-26Merge branch '1.4.x'Morgan Deters
2014-09-26Fix bv options doc.Morgan Deters
2014-09-26Fix AIG bitblaster for unsat cores.Morgan Deters
2014-09-03check() optimizationKshitij Bansal
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-18Making getEqualityStatus more powerful for bit-vector theory.lianah
2014-08-05fixed bug575 for bv modelslianah
2014-08-05fixed bug575 for bv modelslianah
2014-07-10Merge remote-tracking branch 'origin/master' into segfaultfixKshitij Bansal
2014-07-04initialize variablesKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback