summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-13Disable unconstrainedSimp pass when proofs enabled (#1976)Andres Noetzli
2018-06-08Reset decisions at SAT level after solving (#2059)Andres Noetzli
2018-06-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
2018-05-30Ignore license key in set-info command. (#2021)Aina Niemetz
2018-05-30Fixes for quantifiers + incremental (#2009)Andrew Reynolds
2018-05-29 Make user's SMT2 version override file version (#2004)Andres Noetzli
2018-05-29Disable minisat elimination when nonlinear is enabled (#2006)Andrew Reynolds
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
2018-05-22Disable symmetry breaker for unsat cores (#1958)Andres Noetzli
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
2018-05-15Refactor static learning preprocessing pass (#1857)yoni206
2018-05-14Minor improvements to --nl-ext-purify (#1896)Andrew Reynolds
2018-05-11Fix ackermannize preprocessing pass. (#1904)Aina Niemetz
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-05-10Refactored BVAckermann preprocessing pass. (#1889)Aina Niemetz
2018-05-09Better option names for PBE (#1891)Andrew Reynolds
2018-05-09Make symmetry-breaker-exp into a preprocessing pass (#1890)Andrew Reynolds
2018-05-09Add the symmetry breaker module (#1847)PaulMeng
2018-05-08Refactor bv-abstraction preprocessing pass. (#1860)Mathias Preiner
2018-05-08Infrastructure for approximations in model output (#1884)Andrew Reynolds
2018-05-08Fix order of preprocessing pass registration. (#1887)Aina Niemetz
2018-05-03Refactor bv-intro-pow2 preprocessing pass. (#1851)Mathias Preiner
2018-05-03Fix redundant internalPush calls. (#1865)Mathias Preiner
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-04-30Refactor real2int (#1813)Haniel Barbosa
2018-04-30Remove subsort symmetry breaking (#1807)Andrew Reynolds
2018-04-25Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)yoni206
2018-04-25Add benchmark requiring subgoal generation with induction. Disable option. (#...Andrew Reynolds
2018-04-20Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enab...yoni206
2018-04-20Symmetry detection module (#1749)PaulMeng
2018-04-19Refactor pbRewrites preprocessing pass (#1767)Andres Noetzli
2018-04-16RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)Andres Noetzli
2018-04-13allowing --bool-to-bv without quantifiers (#1771)yoni206
2018-04-12Fixes for free variables in assertions (#1762)Andrew Reynolds
2018-04-10Refactored BVGauss preprocessing pass. (#1766)Aina Niemetz
2018-04-10 Improve accuracy of stats for sygus sampler (#1755)Andrew Reynolds
2018-04-09Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)Aina Niemetz
2018-04-05Add more general SignExtendUltConst rewriting. (#1385)Mathias Preiner
2018-04-03Refactor IntToBV preprocessing pass (#1716)Andres Noetzli
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
2018-04-02Remove references to nyu (#1721)Clark Barrett
2018-03-25Check model only when sat (#1694)Andrew Reynolds
2018-03-13SmtEngine::getModel() is now public. (#1665)Aina Niemetz
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback