summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2015-06-15Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-experimentalajreynol
2015-06-14Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-14mergeLiana Hadarean
2015-06-14changes to run script and minor bvLiana Hadarean
2015-06-15Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyPr...Tim King
2015-06-14Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-14Handing the case in replay where a cut is directly in conflict with an existi...Tim King
2015-06-14added ackermanization for eager bit-blastingLiana Hadarean
2015-06-14Guarding the new axiom list for arithmetic division symbols a bit stronger.Tim King
2015-06-14Potential fix for non-linear axioms in incremental mode.Tim King
2015-06-14Strengthening the Assertions for QF_NIA -> QF_BV pass.Tim King
2015-06-14Fix for UMINUS translation in intToBV passClark Barrett
2015-06-14Fix for potential cache problem in intToBV passClark Barrett
2015-06-14Added option for converting QF_NIA to bitvectorsClark Barrett
2015-06-14Fixes for shared term normalization in replay for constraint construction.Tim King
2015-06-14Fixes for shared term normalization in replay for constraint construction.Tim King
2015-06-14Turning off aggressive arith ite simplifications during incremental solving.Tim King
2015-06-14Turning off aggressive arith ite simplifications during incremental solving.Tim King
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Robust check to avoid store all instantiations. Fix prior commit for sort inf...ajreynol
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Restricting TheoryArith to computeRelevantTerms.Tim King
2015-06-13Fixed bug in iteSimpClark Barrett
2015-06-13Fixed bug in iteSimpClark Barrett
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Fix for assertion failure:Clark Barrett
2015-06-13Fix for sort inference involving mixed Int/Real equalities.ajreynol
2015-06-13A return value for an ApproxGLPK::loadVB() failure case was incorrect.Tim King
2015-06-13A return value for an ApproxGLPK::loadVB() failure case was incorrect.Tim King
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Avoid instantiating with array constants.ajreynol
2015-06-13Ensure mkRep instantiation strategies do not violate types.ajreynol
2015-06-13Ensure mkRep instantiation strategies do not violate types.ajreynol
2015-06-12Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-12Fix crash in non-linear cbqi.ajreynol
2015-06-12Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-12In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or n...Tim King
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-06-12Accelerate sygus solution reconstruction for constants and id functions. Min...ajreynol
2015-06-12Adding missing new sendAtoms flag in OutputChannel::lemma() into the unit tests.Tim King
2015-06-11Ready to merge weak equivalence array decision procedure into experimental.Clark Barrett
2015-06-11Removed debugging codeClark Barrett
2015-06-11Passes regressionsClark Barrett
2015-06-11Working version of SMTInterpol algorithmClark Barrett
2015-06-11Added support for glucose, cryptominisat and riss as eager bit-blasting sat-s...Liana Hadarean
2015-06-11Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St...ajreynol
2015-06-11Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A...ajreynol
2015-06-11Update experimental scripts. Support top-level non-terminals in sygus gramma...ajreynol
2015-06-10Bug fix parsing constant constructor sygus.ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback