summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2021-08-04Refactor managed streams (#6934)Gereon Kremer
2021-08-04Add API function to get list of option names (#6971)Gereon Kremer
2021-08-04[proof] Add getProof to API and use it in GetProofCommand (#6974)Haniel Barbosa
2021-08-03Remove dependencies on smt engine in smt solver (#6965)Andrew Reynolds
2021-08-03Refactor shared solver to use theory builtin inference manager (#6960)Andrew Reynolds
2021-07-28Only use libedit on tty inputs (#6946)Gereon Kremer
2021-07-27Minor changes from proof-new (#6937)Andrew Reynolds
2021-07-26Move public options functions to separate file (#6671)Gereon Kremer
2021-07-22Add std::vector<Term> Op:: getIndices() and operator[] for Op (#6397)mudathirmahgoub
2021-07-16[Unit Tests] Avoid linking against external libs (#6898)Andres Noetzli
2021-07-16[Unit Tests] Reenable `top_scope_context_obj` (#6892)Andres Noetzli
2021-07-15bv: Rename lazy solver to layered solver. (#6889)Mathias Preiner
2021-07-14Add missing space for check macro error messages. (#6875)Mathias Preiner
2021-07-06Integrate Lazard into CAD module (#6812)Gereon Kremer
2021-07-02Add reverse iterators to `Node`/`TNode` (#6825)Andres Noetzli
2021-06-28Rename internal string kinds to match API (#6797)Andrew Reynolds
2021-06-24api: getRealValue: Fix printing of integer values. (#6795)Aina Niemetz
2021-06-21[Attributes] Remove parameter `context_dependent` (#6772)Andres Noetzli
2021-06-21Add Grammar.java to the java API (#6388)mudathirmahgoub
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-06-15[Optimization] Use Result in OptimizationResult (#6740)Ouyancheng
2021-06-09[Optimization] support for push/pop (#6706)Ouyancheng
2021-06-08Remove `binary_name` option (#6693)Gereon Kremer
2021-06-04pow2: header file for pow2 solver (#6676)yoni206
2021-06-04bv: Enable bitblast solver by default. (#6660)Mathias Preiner
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-29Remove `Options::set()` method (#6556)Gereon Kremer
2021-05-28(Optimization) remove popObjective, add resetObjectives, rename pushObjective...Ouyancheng
2021-05-27Add Lexicographic + Pareto Optimizations (#6626)Ouyancheng
2021-05-27Update proof namespaces (#6614)Andrew Reynolds
2021-05-27Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)Andres Noetzli
2021-05-27Add support for Box optimization (#6599)Ouyancheng
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-26Ensure proper types in unit tests (#6598)Gereon Kremer
2021-05-25[Unit tests] Fix path of Java bindings (#6616)Andres Noetzli
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-21Support braced-init-lists with `mkNode()` (#6580)Andres Noetzli
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Minor improvements to the API (#6585)Gereon Kremer
2021-05-20Add more getters for api::Term (#6496)Gereon Kremer
2021-05-18Fix `collectEmptyEqs()` in string utils (#6562)Andres Noetzli
2021-05-18Add Solver.java to the Java API (#6196)mudathirmahgoub
2021-05-14Decouple parser creation from input selection (#6533)Andres Noetzli
2021-05-14Add Result.java to the java API (#6385)mudathirmahgoub
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
2021-04-30Refactor optimization result and objective classes + add preliminary support ...Ouyancheng
2021-04-28Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6...Ouyancheng
2021-04-27Add internal support for datatype update (#6450)Andrew Reynolds
2021-04-22Allow in-place construction of `CDList` items (#6409)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback