summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-26Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong,...Tim King
2012-11-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-11-26Improving arithmetic debugging output.Tim King
2012-11-26don't include internal variables in model outputMorgan Deters
2012-11-26some fixes to language bindings and function visibilityMorgan Deters
2012-11-25This commit fixes two incompleteness bugs (461, 459) introduced in r4611 dues...Tim King
2012-11-24Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimize...Tim King
2012-11-21- Removes getDeltaValueWithNonlinear() entirelyTim King
2012-11-21Adds a number of new capabilities to DeltaRational. This adds DeltaRationalEx...Tim King
2012-11-21Added debugging output to --check-models. I've found this output quite useful...Tim King
2012-11-19Run lastWinner thread for all commands. Earlier behavior was to runKshitij Bansal
2012-11-19Changed the splitting-on-demand lemmas of arithmetic to no longer contain the...Tim King
2012-11-19Fix for bug452.Tim King
2012-11-18Disable predicate subtyping:Morgan Deters
2012-11-18support for quantifiers macros, bug fix for bug 454 involving E-matching Arra...Andrew Reynolds
2012-11-17Fixed last currently known bug in array modelsClark Barrett
2012-11-17* enable previously-failing (now succeeding) datatype example that uses recordsMorgan Deters
2012-11-17fix for language bindings (fixes debian build fail last night)Morgan Deters
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-16Fix for bug451Clark Barrett
2012-11-16fixing and refactoring the equality iteratorDejan Jovanović
2012-11-16Fix dumping of array-select expressions in CVC native language.Morgan Deters
2012-11-16fix a compiler warning in modelsMorgan Deters
2012-11-15some fixes for --threads=1Kshitij Bansal
2012-11-15More fixes to model generation, with previously failing testcasesClark Barrett
2012-11-15forgot to uncomment setLogicInternal for THEORY_BVLiana Hadarean
2012-11-15changed logic options so that justification is turned on for QF_ABV and QF_UF...Liana Hadarean
2012-11-15d_incomplete is context-dependent; we shouldn't be saving its value and resto...Morgan Deters
2012-11-15Fix for bug 447.Tim King
2012-11-15Fixed another AUFBV model bug. BV equality subtheory needed to do somethingClark Barrett
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ...Tim King
2012-11-14replaced all static member data from rewrite rule triggers, added infrastruct...Andrew Reynolds
2012-11-14Fixed a typo in r4576Tim King
2012-11-14Beautifying smt_engine.cpp.Tim King
2012-11-14Fix to bug449. Adds shared constants to the set of DeltaRationals that must b...Tim King
2012-11-14bug fixes to models, array rewriter with previously failing testcasesClark Barrett
2012-11-14Quantifiers enabled with portfolio, closing bug 423.Kshitij Bansal
2012-11-14fix a race problem. due to interrupt mechanism minisat returned true instead ...Kshitij Bansal
2012-11-13More bugfixes for modelsClark Barrett
2012-11-13SmtEngine::checkModel() should only be called if the result is sat or unknown...Tim King
2012-11-13refactoring of quantifiers rewriter based on code review from yesterday, refa...Andrew Reynolds
2012-11-13fixed failed bv regressions by refactoring out some rewrite rules from smt_en...Liana Hadarean
2012-11-13added support for division by zero for bit-vector division operatorsLiana Hadarean
2012-11-13Relaxing too-strict assertionClark Barrett
2012-11-13Fixed an array rewriting bug found by fuzzerClark Barrett
2012-11-13Fixed bug in array constant normalization found by fuzzer.Clark Barrett
2012-11-12Improved error reporting for improperly using non-linear division in linear a...Tim King
2012-11-12Delta is now generated in arithmetic to keep consistent the total order of De...Tim King
2012-11-12changed BitVector::unsignedRem to match the behavior of the bit-blasted circu...Liana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback