summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-30Ensure literals in FMF decision strategies are in the CNF stream (#3669)Andrew Reynolds
2020-01-30Weaken assertion for models with approximations (#3667)Andrew Reynolds
2020-01-30Move disequality list to solver state in strings (#3678)Andrew Reynolds
2020-01-30Example minimize evaluation utility. (#3671)Andrew Reynolds
2020-01-30External cache argument for evaluator (#3672)Andrew Reynolds
2020-01-30Do not debug check model for models with approximations (#3673)Andrew Reynolds
2020-01-29Better heuristics for marking congruent variables (#3677)Andres Noetzli
2020-01-29Modularize more steps in the strings strategy (#3676)Andrew Reynolds
2020-01-29Minor updates to string utilities (#3675)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback