summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2021-04-22Remove unused stuff from options setup (#6422)Gereon Kremer
2021-04-22 Reorganizing use of skolem definition manager in prop engine (#6415)Andrew Reynolds
2021-04-22api docs: Rename doxygen output directory. (#6426)Aina Niemetz
2021-04-22api docs: Remove file reintroduced in past merge. (#6426)Aina Niemetz
2021-04-22Fix models for sygus-inference, bv2int, real2int (#6421)Andrew Reynolds
2021-04-22Reconciling proofs and unsat cores (#6405)Haniel Barbosa
2021-04-22Allow in-place construction of `CDList` items (#6409)Andres Noetzli
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback