summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-29Merge branch 'master' into oldVarHeuristicPRoldVarHeuristicPRAndrew Reynolds
2020-01-29Modularize more steps in the strings strategy (#3676)Andrew Reynolds
2020-01-29Minor updates to string utilities (#3675)Andrew Reynolds
2020-01-29Better heuristics for marking congruent variablesAndres Noetzli
2020-01-29expectedType in proof-printing code (#3665)Alex Ozdemir
2020-01-29Fix isLeq function in String utility (#3659)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
2020-01-28Avoid PLUS with one child for bv2nat elimination (#3639)Andrew Reynolds
2020-01-25Axioms for affine function bounds. Tests. (#3632)Alex Ozdemir
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