summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-24Length requirements in conclusionscav2020Andres Noetzli
2020-01-24Revert "Fix"Andres Noetzli
2020-01-23Make skolem depurification an optionAndres Noetzli
2020-01-23FixAndres Noetzli
2020-01-23DepurificationAndres Noetzli
2020-01-22SK_ID_DC_SPT_REM > 0Andres Noetzli
2020-01-22split differentAndres Noetzli
2020-01-22fixAndres Noetzli
2020-01-21Fix edge caseAndres Noetzli
2020-01-21Add regexp concat skolemAndres Noetzli
2020-01-21fixAndres Noetzli
2020-01-21fixAndres Noetzli
2020-01-21prepare for base runAndres Noetzli
2020-01-21split len constsAndres Noetzli
2020-01-21fixAndres Noetzli
2020-01-21more aggressive elimAndres Noetzli
2020-01-21regexp skolemsAndres Noetzli
2020-01-21revert changeAndres Noetzli
2020-01-21Improve skolem normalizationAndres Noetzli
2020-01-21skolem hackAndres Noetzli
2020-01-21Allow define-funs over regexpsAndres Noetzli
2020-01-21Add option to toggle skolem sharingAndres Noetzli
2020-01-17LIRA proof: Arithmetic predicates & reification thereof (#3612)Alex Ozdemir
2020-01-17LIRA sig: int, real terms, and conversions (#3610)Alex Ozdemir
2020-01-17Use axioms when checking goal entailment for abduction algorithm (#3611)Andrew Reynolds
2020-01-15New C++ API: Add nullary constructor for Result. (#3603)Aina Niemetz
2020-01-14Generalize example-based sym breaking to conjectures with constant function a...Andrew Reynolds
2020-01-14Disable unsat cores for regression that times out (#3607)Andres Noetzli
2020-01-13Support arbitrary unsigned integer attributes (#3591)Andres Noetzli
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Fix enum names in AIG bitblaster. (#3599)Mathias Preiner
2020-01-10Fix printing of models of uninterpreted sorts (#3597)Andres Noetzli
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-09Optimize str.substr reduction (#3595)Andres Noetzli
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Universe set cardinality for finite types with finite cardinality (#3392)mudathirmahgoub
2020-01-07Fix unary minus parse check (#3594)Andrew Reynolds
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2020-01-04Fix finiteness check for bounded fmf (#3589)Andrew Reynolds
2019-12-30[proof] ITE translation fix (#3484)Alex Ozdemir
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-19Define all options modified by ENABLE_BEST using cvc4_option (#3578)Simon Dierl
2019-12-19Fix typo in smt_options.toml. (#3579)Mathias Preiner
2019-12-18Increment Taylor degree for tangent and secant plane inferences for transcend...Andrew Reynolds
2019-12-18Avoid calling rewriter from type checker (#3548)Andres Noetzli
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-17Fix spurious parse error for rational real array constants (#3554)Andrew Reynolds
2019-12-16Use the evaluator utility in the function definition evaluator (#3576)Andrew Reynolds
2019-12-16Extend model construction with assignment exclusion set (#3377)Andrew Reynolds
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback