summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-12-16Trace tags for dumping the decision tree in org-mode format (#2871)makaimann
2019-12-15Minor improvement to evaluator (#3570)Andrew Reynolds
2019-12-14Simple optimizations for the core rewriter (#3569)Andrew Reynolds
2019-12-13Eliminate Expr-level calls in TypeNode (#3562)Andrew Reynolds
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-13Disable check-synth-sol in regression with recursive functions (#3560)Andrew Reynolds
2019-12-12 FP converter: convert: Use std::vector as instead of std::stack. (#3563)Aina Niemetz
2019-12-12Make CEGIS sampling robust to non-vanilla CEGIS (#3559)Andrew Reynolds
2019-12-12Fix Unif+PI algorithm with symbolic unfolding (#3558)Haniel Barbosa
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-12-12Fixes for regressions (#3557)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-11Activate node-level datatype API (#3540)Andrew Reynolds
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-11Support symbolic unfolding in UNIF+PI (#3553)Andrew Reynolds
2019-12-10Incorporate rewriting on demand in the evaluator (#3549)Andrew Reynolds
2019-12-10Fix ufho issues (#3551)Haniel Barbosa
2019-12-10Allow unsat cores with sygus inference (#3550)Andrew Reynolds
2019-12-09Disable sygus inference when combined with incremental and proofs (#3539)Andrew Reynolds
2019-12-09Fix case of uninterpreted constant instantiation in FMF (#3543)Andrew Reynolds
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-12-08[Regressions] Require proof support for abduction (#3546)Andres Noetzli
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06Use str.subtr in str.to.int/int.to.str reduction (#3544)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback