summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-10-25Merge branch 'master' into python3.5regpython3.5regAndrew Reynolds
2021-10-25[Regression Script] Support older Python versionsAndres Noetzli
2021-10-24Delete redundant file option_Info.cpp (#7477)mudathirmahgoub
2021-10-24Add new eager conflict detection in strings for integer equivalence classes (...Andrew Reynolds
2021-10-23Remove spurious assertoin (#7458)Andrew Reynolds
2021-10-22Add requires libpoly to regression (#7467)Andrew Reynolds
2021-10-22Refactor java package name from cvc5 to io.github.cvc5.api (#7340)mudathirmahgoub
2021-10-22Remove options::X__name (#7414)Gereon Kremer
2021-10-22Remove stale pointer to proof node manager from skolemize utility (#7471)Andrew Reynolds
2021-10-22[proof] Fixing CHAIN_RESOLUTION checker (#7465)Haniel Barbosa
2021-10-22Fix out-of-sync pruning in CDCAC proofs (#7470)Gereon Kremer
2021-10-22Fix another double negation proof issue (#7468)Gereon Kremer
2021-10-22Remove `--uf-ho` option (#7463)Andrew Reynolds
2021-10-22Fix symmetry issue in theory engine conflicts (#7469)Andrew Reynolds
2021-10-22Add more abduction regressions (#7461)Andrew Reynolds
2021-10-22[proofs] Alethe: Translate FACTORING rule (#7398)Lachnitt
2021-10-22[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)Lachnitt
2021-10-22Make CAD proofs user context dependent (#7466)Gereon Kremer
2021-10-22Refactor theory inference manager constructor (#7457)Andrew Reynolds
2021-10-22Making `IntBlaster` inherit from `EnvObj` (#7431)yoni206
2021-10-22Do not use global proxy variable attribute for strings (#7460)Andrew Reynolds
2021-10-22Fix memory management of `ErrorInformation` (#7388)Andres Noetzli
2021-10-22Add missing methods to Solver.java (#7299)mudathirmahgoub
2021-10-22Make expression mining use configurable options and logic (#7426)Andrew Reynolds
2021-10-21docs: Use light gray for background on the right. (#7438)Aina Niemetz
2021-10-21Also fix case of negated ite (#7454)Gereon Kremer
2021-10-21Fix symmetric proof issue for ITE in circuit propagator (#7452)Gereon Kremer
2021-10-21Split utilites from CEGIS core connective module (#7441)Andrew Reynolds
2021-10-21[Regression Script] Fix printing of error diff (#7451)Andres Noetzli
2021-10-21[proofs] Fix open proof in SAT solver due to cycles (#7448)Haniel Barbosa
2021-10-21Add regression (#7447)Gereon Kremer
2021-10-21Fix incorrect proof from ITE in circuit propagator (#7446)Gereon Kremer
2021-10-21Refactor regressions script (#7249)Andres Noetzli
2021-10-21Make cardinality constraint a nullary operator (#7333)Andrew Reynolds
2021-10-21Working on windows builds (#7381)Gereon Kremer
2021-10-21Add setup to generate graphs for cmake target dependencies (#7383)Gereon Kremer
2021-10-21Enable and fix dump test (#7387)Andres Noetzli
2021-10-20Fix (#7437)Gereon Kremer
2021-10-20Enable some previously failing regressions (#7434)Andrew Reynolds
2021-10-20Fix docs upload (again) (#7435)Gereon Kremer
2021-10-20api: Add Solver::mkSepEmp(). (#7432)Aina Niemetz
2021-10-20api: Improve documentation for special cases with nullary ops. (#7433)Aina Niemetz
2021-10-20Move variadic trie utility to its own file (#7410)Andrew Reynolds
2021-10-20Add regressions for fixed issues (#7421)Andrew Reynolds
2021-10-20Add `isNull` and `isUpdater` to `Sort` class of python API (#7423)yoni206
2021-10-20Throw exception if checking model with separation logic heap (#7422)Andrew Reynolds
2021-10-20Check for higher-order variables in TheoryUF::ppRewrite (#7408)Andrew Reynolds
2021-10-20Fix inadvertent failure of workflow step (#7420)Gereon Kremer
2021-10-20Eliminate last static calls to rewriter from smt layer (#7355)Andrew Reynolds
2021-10-20Make SyGuS solver robust to non-closed enumerable sorts (#7417)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback