summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-05-03Add CI jobs to build docs (#6413)Gereon Kremer
2021-05-03SymFPU: Automatically apply patch from 2020-11-14. (#6471)Aina Niemetz
2021-05-03Python API tests for terms -- Part 1 (#6468)yoni206
2021-04-30bv: Refactor ppAssert and move to TheoryBV. (#6470)Mathias Preiner
2021-04-30Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)Aina Niemetz
2021-04-30Refactor optimization result and objective classes + add preliminary support ...Ouyancheng
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
2021-04-29Add assertion list utility for justification heuristic (#6414)Andrew Reynolds
2021-04-29Simplify generated code for getOption() and setOption() (#6462)Gereon Kremer
2021-04-29Add missing include. (#6463)Gereon Kremer
2021-04-29Avoid exponential explosion of small constant in CEGQI (#6461)Gereon Kremer
2021-04-28Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6...Ouyancheng
2021-04-28Refactor resource manager options (#6446)Gereon Kremer
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-28Make sure reference stats are reset properly (#6457)Gereon Kremer
2021-04-28Clean up options holder class (#6458)Gereon Kremer
2021-04-28Cleanup DidYouMean (#6454)Gereon Kremer
2021-04-27Add internal support for datatype update (#6450)Andrew Reynolds
2021-04-27Move slow regression to regress3 (#6451)Andrew Reynolds
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)Andrew Reynolds
2021-04-27Simplify making function types (#6447)Andrew Reynolds
2021-04-27Initial setup for docs of python API (#6445)Gereon Kremer
2021-04-27Use std::hash for API types (#6432)Gereon Kremer
2021-04-27Bool: Move implementation of type rules to cpp. (#6420)Aina Niemetz
2021-04-26Generate docs conf.py by cmake (#6441)Gereon Kremer
2021-04-26Protect int stats methods (#6442)Gereon Kremer
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-26Fix theoryOf for Boolean equalities (#6444)Andrew Reynolds
2021-04-26New design in DOT representation, nodes colored based on visions(basic and pr...Diego Della Rocca de Camargos
2021-04-26Ensure dependency is tracked for all substitutions (#6438)Andrew Reynolds
2021-04-26Enable print-inst-full by default (#6435)Andrew Reynolds
2021-04-26Fix assertions in SAT solver (#6443)Haniel Barbosa
2021-04-26Do not process looping word equations over sequences (#6434)Andrew Reynolds
2021-04-25Use fast enumeration by default for Boolean predicate synthesis (#6440)Andrew Reynolds
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-04-23Add assumption-based unsat cores. (#6427)Mathias Preiner
2021-04-23Add missing dependency for CaDiCaL (#6431)Gereon Kremer
2021-04-23(proof-new) Proofs for sets purification lemmas (#6416)Andrew Reynolds
2021-04-23Add new substitution apply methods fixpoint, sequential, simultaneous (#6429)Andrew Reynolds
2021-04-23Make sure a ReferenceStat is set to values of the correct type (#6430)Gereon Kremer
2021-04-23Enable strings exp by default for strings specific logics (#6424)Andrew Reynolds
2021-04-23BV: Add proof logging for bit-blasting. (#6373)Aina Niemetz
2021-04-23Move implementation of UF rewriter to cpp (#6393)Andrew Reynolds
2021-04-22Make trust substitution map generate proofs lazily (#6379)Andrew Reynolds
2021-04-22Minor improvements to substitutions (#6380)Andrew Reynolds
2021-04-22Minor changes to unsat core default setting (#6425)Andrew Reynolds
2021-04-22cmake: Do not require --auto-download for already downloaded dependencies. (#...Mathias Preiner
2021-04-22Update INSTALL.md (#6412)Gereon Kremer
2021-04-22Add API documentation for statistics (#6364)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback