summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2020-12-23Dumping unsat cores after check-sat-assuming/QUERY (#5724)Haniel Barbosa
2020-12-23Remove quant EPR option (#5716)Andrew Reynolds
2020-12-22Remove preregister instantiation heuristic (#5713)Andrew Reynolds
2020-12-16Simplify preprocessing (#5647)Andrew Reynolds
2020-12-15Remove bv divide by zero option (#5672)Andrew Reynolds
2020-12-14Properly implement datatype selector triggers (#5624)Andrew Reynolds
2020-12-08update doc (#5619)yoni206
2020-12-07Disable algebraic BV subtheory by default and make experimental. (#5596)Mathias Preiner
2020-12-07Fix issue with free variables introduced by quantifier rewriter (#5602)Andrew Reynolds
2020-12-04Change generated options to be thread_local. (#5583)Everett Maus
2020-12-03Models as (#5581)yoni206
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback