summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2020-09-22Add simple BV solver (#5065)Mathias Preiner
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-22ICP-based solver for nonlinear arithmetic (#5017)Gereon Kremer
2020-09-11(proof-new) Add SMT proof manager (#5054)Andrew Reynolds
2020-09-08Make CVC/API BV div/mod semantics match SMT-LIB (#4997)Andres Noetzli
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-25Add the combination engine (#4939)Andrew Reynolds
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear arithm...Andrew Reynolds
2020-08-21Remove BV equality slicer (#4928)Andrew Reynolds
2020-08-14correctly parse sygus lang option (#4884)E Polgreen
2020-08-12(proof-new) Improve interfaces to proof generators (#4803)Andrew Reynolds
2020-08-11(proof-new) Extensions to proof checker interface (#4857)Andrew Reynolds
2020-08-11Remove instantiation model true option (#4861)Andrew Reynolds
2020-08-05[Strings] Add eager context-dependent evaluation (#4847)Andres Noetzli
2020-08-04Add CAD-based solver (#4834)Gereon Kremer
2020-07-28Remove arrays lazy rintro option (#4806)Andrew Reynolds
2020-07-17Replace options listener infrastructure (#4764)Andrew Reynolds
2020-07-17Support for using 'libedit' over 'readline' #4571 (#4579)Andrew V. Jones
2020-07-17(proof-new) Updates to strings core solver (#4642)Andrew Reynolds
2020-07-17Add option manager and simpler option listener (#4745)Andrew Reynolds
2020-07-17Integration of libpoly (#4679)Gereon Kremer
2020-07-16Resource manager cleanup (#4732)Gereon Kremer
2020-07-16Remove cumulative time limits and cpu time limits (#4711)Gereon Kremer
2020-07-14Make use of options in setDefaults more consistent (#4729)Andrew Reynolds
2020-07-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Fix options messages that were inverted (#4734)Haniel Barbosa
2020-07-13 User-facing print debug option for sygus candidates (#4720)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-11Changing bv_to_int options (#4721)yoni206
2020-07-08Re-implement handling of --tlimit (#4655)Gereon Kremer
2020-07-08Add getName() method to options. (#4704)Mathias Preiner
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-07-02Remove SWIG bindings (#4683)Andres Noetzli
2020-07-01Add solver for integer AND (#4681)Andrew Reynolds
2020-06-30Interpolation step 1 (#4638)Ying Sheng
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
2020-06-25Update option --nl-ext to enable/disable incremental linearization solver onl...Andrew Reynolds
2020-06-23Add support for eqrange predicate (#4562)Mathias Preiner
2020-06-22(proof-new) Add proof-new to options file (#4641)Andrew Reynolds
2020-06-22fix (#4637)yoni206
2020-06-18Improve memory management in Java bindings (#4629)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
2020-06-10(proof-new) Remove arith-snorm option. (#4591)Andrew Reynolds
2020-06-05Datatypes with nested recursion are not handled in TheoryDatatypes unless opt...Andrew Reynolds
2020-06-05Printing FP values as binary or indexed BVs according to option (#4554)Haniel Barbosa
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-06-02Use prenex normal form when using cegqi-nested-qe (#4522)Andrew Reynolds
2020-05-28Fix term registry for constant case, simplify. (#4538)Andrew Reynolds
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-22Add support for SAT solver Kissat. (#4514)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback