summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-29Prefer old variable heuristicoldVarHeuristicAndres Noetzli
2020-01-27Stats per skolem idcav2020submissionAndres Noetzli
2020-01-27Count misses instead of hitsAndres Noetzli
2020-01-27Fix statsAndres Noetzli
2020-01-25Add statsAndres Noetzli
2020-01-25normal form fixAndres Noetzli
2020-01-25Make regexp first classAndres Noetzli
2020-01-25Adds stats and optionAndres Noetzli
2020-01-24Fix skolem lengthAndres Noetzli
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix subtyping for instantiations where internal representatives are chosen (#...Andrew Reynolds
2020-01-22Fix substitution in nl solver (#3638)Andrew Reynolds
2020-01-22Fix single invocation partition for non-function non-atomic types (#3642)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-21Types and side conditions for affine bounds (#3631)Alex Ozdemir
2020-01-21Affine Axioms (#3630)Alex Ozdemir
2020-01-21Types & side-conditions for linear and affine fns (#3627)Alex Ozdemir
2020-01-21Axioms (and side conditions) for tightening bounds (#3613)Alex Ozdemir
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
2019-12-16Move Datatype management to ExprManager (#3568)Andrew Reynolds
2019-12-16Fix evaluator for non-evaluatable nodes (#3575)Andrew Reynolds
2019-12-16Revert evaluate as node. (#3574)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback