summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2021-04-21Arithmetic: Move implementation of type rules to cpp. (#6419)Aina Niemetz
2021-04-21UF: Move implementation of type rules to cpp. (#6403)Aina Niemetz
2021-04-21Add explicit dependencies for base lib (#6410)Gereon Kremer
2021-04-21Pass GMP to libpoly (#6411)Gereon Kremer
2021-04-21Datatypes: Move implementation of type rules to cpp. (#6418)Aina Niemetz
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-21cmake: Add optional module name argument for check_python_module helper. (#6406)Mathias Preiner
2021-04-21Sets: Move implementation of type rules to cpp. (#6401)Aina Niemetz
2021-04-21Arrays: Move implementation of type rules to cpp. (#6407)Aina Niemetz
2021-04-21Add unit test for abduction (#6400)Andrew Reynolds
2021-04-21Add basic utilities for new implementation of justification heuristic (#6333)Andrew Reynolds
2021-04-21Add getNumIndices to Op (#6386)mudathirmahgoub
2021-04-20Split FP expand definitions to own module (#6392)Andrew Reynolds
2021-04-20BV: Move implementation of type rules from header to .cpp. (#6360)Aina Niemetz
2021-04-20Sep: Move implementation of type rules to cpp. (#6402)Aina Niemetz
2021-04-20Quantifiers: Move implementation of type rules to cpp. (#6404)Aina Niemetz
2021-04-20Add InferenceId as resources (#6339)Gereon Kremer
2021-04-20Add instantiation pool feature to the API (#6358)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback