projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2019-12-16 Andrew ReynoldsUse the evaluator utility in the function definition... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsExtend model construction with assignment exclusion... commit | commitdiff | tree
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsMove Datatype management to ExprManager (#3568) commit | commitdiff | tree
2019-12-16 Andrew ReynoldsFix evaluator for non-evaluatable nodes (#3575) commit | commitdiff | tree
2019-12-16 Andrew ReynoldsRevert evaluate as node. (#3574) commit | commitdiff | tree
2019-12-16 makaimannTrace tags for dumping the decision tree in org-mode... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsMinor improvement to evaluator (#3570) commit | commitdiff | tree
2019-12-15 Andrew ReynoldsSimple optimizations for the core rewriter (#3569) commit | commitdiff | tree
2019-12-13 Andrew ReynoldsEliminate Expr-level calls in TypeNode (#3562) commit | commitdiff | tree
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) commit | commitdiff | tree
2019-12-13 Andrew ReynoldsDisable check-synth-sol in regression with recursive... commit | commitdiff | tree
2019-12-13 Aina Niemetz FP converter: convert: Use std::vector as instead... commit | commitdiff | tree
2019-12-12 Andrew ReynoldsMake CEGIS sampling robust to non-vanilla CEGIS (#3559) commit | commitdiff | tree
2019-12-12 Haniel BarbosaFix Unif+PI algorithm with symbolic unfolding (#3558) commit | commitdiff | tree
2019-12-12 Andrew ReynoldsUse the node-level datatypes API (#3556) commit | commitdiff | tree
2019-12-12 Andrew ReynoldsFixes for regressions (#3557) commit | commitdiff | tree
2019-12-12 Andrew ReynoldsFix CEGIS refinement for recursive functions evaluation... commit | commitdiff | tree
2019-12-12 Andrew ReynoldsActivate node-level datatype API (#3540) commit | commitdiff | tree
2019-12-11 Andrew ReynoldsDo not substitute beneath arithmetic terms in the non... commit | commitdiff | tree
2019-12-11 Andrew ReynoldsSupport symbolic unfolding in UNIF+PI (#3553) commit | commitdiff | tree
2019-12-10 Andrew ReynoldsIncorporate rewriting on demand in the evaluator (... commit | commitdiff | tree
2019-12-10 Haniel BarbosaFix ufho issues (#3551) commit | commitdiff | tree
2019-12-10 Andrew ReynoldsAllow unsat cores with sygus inference (#3550) commit | commitdiff | tree
2019-12-09 Andrew ReynoldsDisable sygus inference when combined with incremental... commit | commitdiff | tree
2019-12-09 Andrew ReynoldsFix case of uninterpreted constant instantiation in... commit | commitdiff | tree
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) commit | commitdiff | tree
2019-12-08 Andres Noetzli[Regressions] Require proof support for abduction ... commit | commitdiff | tree
2019-12-07 Andres NoetzliSimplify rewrite for character matching (#3545) commit | commitdiff | tree
2019-12-07 Andres NoetzliUse str.subtr in str.to.int/int.to.str reduction (... commit | commitdiff | tree
2019-12-06 Andrew ReynoldsThrow exception instead of warning for approximate... commit | commitdiff | tree
2019-12-06 Andres NoetzliAdd lemma for str.to.int/int.to.str (#3541) commit | commitdiff | tree
2019-12-06 Andrew ReynoldsOptimize the rewriter for DT_SYGUS_EVAL (#3529) commit | commitdiff | tree
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... commit | commitdiff | tree
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535) commit | commitdiff | tree
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... commit | commitdiff | tree
2019-12-06 Mathias Preinercontrib: Setup all dependencies in deps/ directory... commit | commitdiff | tree
2019-12-06 Andrew ReynoldsIntroduce the Node-level Datatypes API (#3462) commit | commitdiff | tree
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from... commit | commitdiff | tree
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) commit | commitdiff | tree
2019-12-05 Andres NoetzliBi-directional unrolling of R* regular expressions... commit | commitdiff | tree
2019-12-05 makaimannAdd mkOp for a single Kind (#3522) commit | commitdiff | tree
2019-12-05 Andrew ReynoldsFix the subtyping relation for functions (#3494) commit | commitdiff | tree
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486) commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFix (#3530) commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFixes for SyGuS PBE + templated string concatenations... commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFix single invocation solution construction for multipl... commit | commitdiff | tree
2019-12-04 Andres NoetzliFix corner case in model construction of strings (... commit | commitdiff | tree
2019-12-03 Andrew ReynoldsImprove flexibility of lemma output in non-linear solve... commit | commitdiff | tree
2019-12-03 Aina NiemetzFix clang-format file for brace wrapping with case... commit | commitdiff | tree
2019-12-03 Andres NoetzliRewrite `str.contains` used for character matching... commit | commitdiff | tree
2019-12-03 makaimannAdd isNullHelper to avoid calling API function isNull... commit | commitdiff | tree
2019-12-03 makaimannMinor refactor: rename opterm_black to op_black (#3521) commit | commitdiff | tree
2019-12-02 Andres Noetzli[SMT2 Printer] Quote symbols starting with digit (... commit | commitdiff | tree
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... commit | commitdiff | tree
2019-12-02 Andrew Reynolds Update ownership policy for dynamic quantifiers splitt... commit | commitdiff | tree
2019-12-02 Andrew ReynoldsFix case of higher-order + sygus inference (#3509) commit | commitdiff | tree
2019-12-02 Andrew ReynoldsEnsure quantifiers options are set with --no-strings... commit | commitdiff | tree
2019-12-01 Andres NoetzliPrevent ref count from reaching zero in BV instantiator... commit | commitdiff | tree
2019-11-30 Haniel Barbosaimproving parsing error messages related to HOL (#3510) commit | commitdiff | tree
2019-11-30 Andres NoetzliCompetition build: Skip parsing error regression (... commit | commitdiff | tree
2019-11-30 Andrew ReynoldsFix fast SyGuS enumeration for interpreted constants... commit | commitdiff | tree
2019-11-29 Andrew ReynoldsCheck free variables in assertions when using SyGuS... commit | commitdiff | tree
2019-11-27 Andrew ReynoldsFix sygus inference for choice functions introduced... commit | commitdiff | tree
2019-11-27 Haniel BarbosaEnable sygusRecFun by default and fixes SyGuS+RecFun... commit | commitdiff | tree
2019-11-27 Andrew Reynolds Fix indexof range lemma (#3499) commit | commitdiff | tree
2019-11-25 Andrew ReynoldsBetter front-end type checking for SyGuS (#3496) commit | commitdiff | tree
2019-11-22 Andrew ReynoldsMinor refactoring of compute model value for nl (#3489) commit | commitdiff | tree
2019-11-22 Haniel Barbosafixing stupid typo (#3488) commit | commitdiff | tree
2019-11-21 Haniel Barbosahard limit for rec-fun eval (#3485) commit | commitdiff | tree
2019-11-21 Andrew ReynoldsEvaluation unfolding for symbolic SyGuS constructors... commit | commitdiff | tree
2019-11-20 Haniel BarbosaLazy evaluation via rec-funs of ITE expressions (... commit | commitdiff | tree
2019-11-19 Andres NoetzliFix reduction of `sqrt` (#3478) commit | commitdiff | tree
2019-11-19 Alex OzdemirAdd a few comments to ProofManager (#3477) commit | commitdiff | tree
2019-11-19 Alex OzdemirSignature documentation update (#3476) commit | commitdiff | tree
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) commit | commitdiff | tree
2019-11-18 Andrew ReynoldsUse standard sygus interface for abduction and rewrite... commit | commitdiff | tree
2019-11-18 Andrew ReynoldsImprove interface for sygus datatype, fix utilities... commit | commitdiff | tree
2019-11-18 Andrew ReynoldsUpdates to the unit tests, api, and examples for dataty... commit | commitdiff | tree
2019-11-17 Andres NoetzliAdd support for ThreadSanitizer instrumentation (#3467) commit | commitdiff | tree
2019-11-16 Andrew ReynoldsUse standard interface for sygus default grammar constr... commit | commitdiff | tree
2019-11-15 Andrew ReynoldsIntroduce SyGuS datatype API (#3465) commit | commitdiff | tree
2019-11-15 Andrew ReynoldsFix wrong kind in sygus version 1 parser (#3463) commit | commitdiff | tree
2019-11-14 Alex OzdemirUse Shebang in cxxtestgen when appropriate (#3458) commit | commitdiff | tree
2019-11-13 Andres NoetzliAllow (set-logic ...) after (reset) (#3457) commit | commitdiff | tree
2019-11-13 Andrew ReynoldsDistinguish unknown status for model printing (#3454) commit | commitdiff | tree
2019-11-13 Andrew ReynoldsRefactor non-linear extension for model-based refinemen... commit | commitdiff | tree
2019-11-11 Andrew ReynoldsAdd missing utilities for Node-level Datatype API ... commit | commitdiff | tree
2019-11-11 Andres NoetzliFix mkConst<RoundingMode>() for Python bindings (#3447) commit | commitdiff | tree
2019-11-11 yoni206Update README according to the new website (#3438) commit | commitdiff | tree
2019-11-11 Andrew ReynoldsEliminate remaining references to type/expr in datatype... commit | commitdiff | tree
2019-11-10 Andrew ReynoldsFix bugs related to sygus higher-order + recursive... commit | commitdiff | tree
2019-11-09 Andrew ReynoldsFixes in relations related to datatypes not passed... commit | commitdiff | tree
2019-11-08 Mathias Preinercmake: Disable C++ GNU extensions. (#3446) commit | commitdiff | tree
2019-11-06 Andrew ReynoldsMove more string utility functions (#3398) commit | commitdiff | tree
2019-11-06 Andrew ReynoldsMigrate more datatype methods to the Node level (#3443) commit | commitdiff | tree
2019-11-06 Andres Noetzli[Regressions] Remove leading whitespace in output ... commit | commitdiff | tree
2019-11-06 Andrew ReynoldsSupport for SyGuS PBE + recursive functions (#3433) commit | commitdiff | tree
2019-11-06 Andres NoetzliRemove casts to subclasses of Type in API (#3420) commit | commitdiff | tree
2019-11-05 Andrew ReynoldsSeparate model object in non-linear extension (#3426) commit | commitdiff | tree
next