summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2020-11-29updateAndres Noetzli
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
2020-11-16Improve accuracy of resource limitation (#4763)Gereon Kremer
2020-11-13Model declarations printing options (#5432)yoni206
2020-11-12(proof-new) Improve printing and debugging for pedantic checking (#5337)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-10-27Disable --nl-cad option by default (#5350)Gereon Kremer
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-12Remove uf-ss-totality option (#5251)Andrew Reynolds
2020-10-11SyGuS instantiation modes (#5228)Mathias Preiner
2020-10-05Make sygus more robust to unknown responses in solution verification (#5199)Andrew Reynolds
2020-10-01Add additional ground terms to SyGuS instantiation grammar (#5167)Mathias Preiner
2020-10-01Allow to use the initial assignment for CAD (#5177)Gereon Kremer
2020-09-23bv2int: new options for bvand translation (#5096)yoni206
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback