summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-05-18Fix `collectEmptyEqs()` in string utilsHEADmasterAndres Noetzli
2021-05-18Adding python API test part 2 (#6551)Ying Sheng
2021-05-18(proof-new) Miscellaneous updates to strings from proof-new (#6557)Andrew Reynolds
2021-05-18Fix smt2 printing (#6558)Andrew Reynolds
2021-05-18Add Solver.java to the Java API (#6196)mudathirmahgoub
2021-05-17Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)Andres Noetzli
2021-05-17Adding python API test (#6546)Ying Sheng
2021-05-17Move and enhance python API grammar tests (#6538)yoni206
2021-05-17Replace smt_name by aliases (#6541)Gereon Kremer
2021-05-17Include cinttypes instead of inttypes.h (#6548)Andres Noetzli
2021-05-17Improve integration of CAD with nl-Ext (#6542)Gereon Kremer
2021-05-14Decouple parser creation from input selection (#6533)Andres Noetzli
2021-05-14Restrict additional CI jobs (#6539)Gereon Kremer
2021-05-14Stop using the solver for printing sygus synthesis solutions. (#6530)Abdalrhman Mohamed
2021-05-14Add getId function to python API (#6523)Alex Ozdemir
2021-05-14Add Result.java to the java API (#6385)mudathirmahgoub
2021-05-14bv: Assert input facts on user-level 0. (#6515)Mathias Preiner
2021-05-13api docs: Tweak style to be consistent with website style. (#6537)Aina Niemetz
2021-05-13Always parse streams with line buffer (#6532)Andres Noetzli
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-13Split options holder class (#6527)Gereon Kremer
2021-05-13Adding functions to the python API and testing them -- part 2 (#6517)yoni206
2021-05-13Fix error message in toPythonObj (#6524)Alex Ozdemir
2021-05-12Move docs upload to a different workflow (#6512)Gereon Kremer
2021-05-12Preliminary draft of changes for SMT comp 2021 (#6522)Andrew Reynolds
2021-05-12Ensure sequences of Booleans generate Boolean term variable skolems when appl...Andrew Reynolds
2021-05-12Use signal(sig, SIG_DFL); raise(sig); instead of abort() (#6518)Gereon Kremer
2021-05-10Remove header for option modules (#6514)Gereon Kremer
2021-05-10Remove read_only from options. (#6513)Gereon Kremer
2021-05-10Unify top-level substitutions and model substitutions (#6499)Andrew Reynolds
2021-05-10Add doc to Kind.java (#6498)mudathirmahgoub
2021-05-08Adding functions to the python API and testing them (#6477)yoni206
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
2021-05-07Move slow regressions and update guidelines. (#6508)Aina Niemetz
2021-05-07Fix and add missing REQUIRE labels for FP regression tests. (#6506)Aina Niemetz
2021-05-07Integrate documentation build with the regular CI workflow (#6490)Gereon Kremer
2021-05-07Properly printing INST_PATTERN_LIST by itself (#6507)Haniel Barbosa
2021-05-07Simplifications to expand definitions (#6487)Andrew Reynolds
2021-05-07Fix for toPythonObj of integer value with real sort (#6505)makaimann
2021-05-06[proof-new] Updating documentation for Subs/Rw ids (#6502)Haniel Barbosa
2021-05-06Discard duplicate terms in patterns (#6501)Andrew Reynolds
2021-05-06Update README.md and remove last CVC4 references. (#6497)Mathias Preiner
2021-05-06Use constant folding for evaluating BV eager atom (#6494)Andrew Reynolds
2021-05-05Do not have quantifiers model inherit from theory model (#6493)Andrew Reynolds
2021-05-05Save block comments associated with each kind when parsing kinds file (#6489)makaimann
2021-05-05Add helper functions for multi-objective optimization + refactoring (#6473)Ouyancheng
2021-05-04Move current decision engine to decision engine old (#6466)Andrew Reynolds
2021-05-04Move env into smt solver, theory engine, prop engine (#6486)Andrew Reynolds
2021-05-04Do not use proof CNF stream with assumptions-based cores (#6488)Haniel Barbosa
2021-05-04Use proper commit hash for PRs (#6485)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback