projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[proof] ITE translation fix (#3484)
[cvc5.git] / test /
2019-12-31 Alex Ozdemir[proof] ITE translation fix (#3484) tree | commitdiff
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) tree | commitdiff
2019-12-18 Andrew ReynoldsIncrement Taylor degree for tangent and secant plane... tree | commitdiff
2019-12-18 Andres NoetzliAvoid calling rewriter from type checker (#3548) tree | commitdiff
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array consta... tree | commitdiff
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... tree | commitdiff
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) tree | commitdiff
2019-12-13 Andrew ReynoldsDisable check-synth-sol in regression with recursive... tree | commitdiff
2019-12-12 Andrew ReynoldsMake CEGIS sampling robust to non-vanilla CEGIS (#3559) tree | commitdiff
2019-12-12 Haniel BarbosaFix Unif+PI algorithm with symbolic unfolding (#3558) tree | commitdiff
2019-12-12 Andrew ReynoldsFixes for regressions (#3557) tree | commitdiff
2019-12-12 Andrew ReynoldsFix CEGIS refinement for recursive functions evaluation... tree | commitdiff
2019-12-11 Andrew ReynoldsDo not substitute beneath arithmetic terms in the non... tree | commitdiff
2019-12-10 Haniel BarbosaFix ufho issues (#3551) tree | commitdiff
2019-12-10 Andrew ReynoldsAllow unsat cores with sygus inference (#3550) tree | commitdiff
2019-12-09 Andrew ReynoldsFix case of uninterpreted constant instantiation in... tree | commitdiff
2019-12-08 Andres Noetzli[Regressions] Require proof support for abduction ... tree | commitdiff
2019-12-07 Andres NoetzliSimplify rewrite for character matching (#3545) tree | commitdiff
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... tree | commitdiff
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535) tree | commitdiff
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... tree | commitdiff
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from... tree | commitdiff
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) tree | commitdiff
2019-12-05 Andres NoetzliBi-directional unrolling of R* regular expressions... tree | commitdiff
2019-12-05 makaimannAdd mkOp for a single Kind (#3522) tree | commitdiff
2019-12-05 Andrew ReynoldsFix the subtyping relation for functions (#3494) tree | commitdiff
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486) tree | commitdiff
2019-12-04 Andrew ReynoldsFix (#3530) tree | commitdiff
2019-12-04 Andrew ReynoldsFix single invocation solution construction for multipl... tree | commitdiff
2019-12-03 Andres NoetzliRewrite `str.contains` used for character matching... tree | commitdiff
2019-12-03 makaimannMinor refactor: rename opterm_black to op_black (#3521) tree | commitdiff
2019-12-02 Andres Noetzli[SMT2 Printer] Quote symbols starting with digit (... tree | commitdiff
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... tree | commitdiff
2019-12-02 Andrew Reynolds Update ownership policy for dynamic quantifiers splitt... tree | commitdiff
2019-12-02 Andrew ReynoldsFix case of higher-order + sygus inference (#3509) tree | commitdiff
2019-12-02 Andrew ReynoldsEnsure quantifiers options are set with --no-strings... tree | commitdiff
2019-12-01 Andres NoetzliPrevent ref count from reaching zero in BV instantiator... tree | commitdiff
2019-11-30 Andres NoetzliCompetition build: Skip parsing error regression (... tree | commitdiff
2019-11-30 Andrew ReynoldsFix fast SyGuS enumeration for interpreted constants... tree | commitdiff
2019-11-27 Andrew ReynoldsFix sygus inference for choice functions introduced... tree | commitdiff
2019-11-27 Haniel BarbosaEnable sygusRecFun by default and fixes SyGuS+RecFun... tree | commitdiff
2019-11-27 Andrew Reynolds Fix indexof range lemma (#3499) tree | commitdiff
2019-11-25 Andrew ReynoldsBetter front-end type checking for SyGuS (#3496) tree | commitdiff
2019-11-22 Haniel Barbosafixing stupid typo (#3488) tree | commitdiff
2019-11-21 Haniel Barbosahard limit for rec-fun eval (#3485) tree | commitdiff
2019-11-20 Haniel BarbosaLazy evaluation via rec-funs of ITE expressions (... tree | commitdiff
2019-11-19 Andres NoetzliFix reduction of `sqrt` (#3478) tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-18 Andrew ReynoldsUpdates to the unit tests, api, and examples for dataty... tree | commitdiff
2019-11-15 Andrew ReynoldsFix wrong kind in sygus version 1 parser (#3463) tree | commitdiff
2019-11-14 Alex OzdemirUse Shebang in cxxtestgen when appropriate (#3458) tree | commitdiff
2019-11-13 Andres NoetzliAllow (set-logic ...) after (reset) (#3457) tree | commitdiff
2019-11-10 Andrew ReynoldsFix bugs related to sygus higher-order + recursive... tree | commitdiff
2019-11-06 Andres Noetzli[Regressions] Remove leading whitespace in output ... tree | commitdiff
2019-11-06 Andrew ReynoldsSupport for SyGuS PBE + recursive functions (#3433) tree | commitdiff
2019-11-05 Andres Noetzli[Regressions] Support for running w/ default args ... tree | commitdiff
2019-11-04 Andrew ReynoldsAvoid non-well-founded sygus grammars (#3434) tree | commitdiff
2019-11-04 Andrew ReynoldsMake getSynthSolution return a Bool (#3306) tree | commitdiff
2019-11-01 Andrew ReynoldsFix non-termination in datatype type enumerator (#3369) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-28 Andrew ReynoldsFix for non-linear models (#3410) tree | commitdiff
2019-10-28 Andres NoetzliFix integer division rewrite (#3415) tree | commitdiff
2019-10-27 Andres NoetzliFix global-declarations support (#3403) tree | commitdiff
2019-10-23 Andrew ReynoldsFixes for SyGuS + regular expressions (#3313) tree | commitdiff
2019-10-18 makaimannUpdate overflow check to handle negative numbers (... tree | commitdiff
2019-10-15 Andres NoetzliFix regression (#3393) tree | commitdiff
2019-10-14 Andres NoetzliDisable regression test for competition build (#3388) tree | commitdiff
2019-10-14 Andrew ReynoldsRemove benchmark (#3389) tree | commitdiff
2019-10-14 Andrew ReynoldsSupport UF in default sygus grammars (#3319) tree | commitdiff
2019-10-14 Andrew ReynoldsApply sygus repair constant techniques restricted to... tree | commitdiff
2019-10-14 Andrew ReynoldsEnsure lemmas from sygus repair const are guarded ... tree | commitdiff
2019-10-13 Andrew ReynoldsEliminate negative constant coefficients in div/mod... tree | commitdiff
2019-10-11 Andrew ReynoldsCheck that logic is set when synth-fun command is encou... tree | commitdiff
2019-10-10 Mathias Preinertest: Add TS_UTILS_EXPECT_ABORT macro for unit tests... tree | commitdiff
2019-10-09 Andres NoetzliAvoid printing success for `--force-logic` (#3363) tree | commitdiff
2019-10-09 Aina NiemetzNew C++ API: Term: Add missing checks for null. (#3364) tree | commitdiff
2019-10-08 Andrew ReynoldsLimit cases of sygus inference based on type (#3370) tree | commitdiff
2019-10-08 Andrew ReynoldsFix method for getting arithmetic function definition... tree | commitdiff
2019-10-08 Andres Noetzli[CVC Parser] Add support for regular expressions (... tree | commitdiff
2019-10-08 Andres NoetzliDisallow --proof and --incremental (#3332) tree | commitdiff
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... tree | commitdiff
2019-10-08 Aina NiemetzNew C++ API: Add Term::getId(). (#3360) tree | commitdiff
2019-10-06 Andrew ReynoldsFix typo in regression (#3359) tree | commitdiff
2019-10-06 Andrew ReynoldsFix str to int reduction (#3358) tree | commitdiff
2019-10-03 yoni206Disable proofs for unsupported logics (#3327) tree | commitdiff
2019-10-01 Andrew ReynoldsTrivial solve method for single invocation sygus (... tree | commitdiff
2019-09-30 Andres NoetzliAdd rewrite for splitting equalities (#2957) tree | commitdiff
2019-09-30 Andrew ReynoldsAvoid cases of empty sygus grammars (#3301) tree | commitdiff
2019-09-29 Andrew ReynoldsFail single invocation techniques when utility inferenc... tree | commitdiff
2019-09-28 Andrew ReynoldsSupport smt2 language "match" term (#3258) tree | commitdiff
2019-09-27 Andrew ReynoldsFix case of disjunctive conclusion in strings (#3254) tree | commitdiff
2019-09-27 Andrew ReynoldsCVC print support for recoverable failure (#3323) tree | commitdiff
2019-09-25 Andrew Reynolds Fix off by one error in strings flat form explanation... tree | commitdiff
2019-09-25 Andrew ReynoldsAdd isParameterized function to Expr (#3303) tree | commitdiff
2019-09-25 Mathias PreinerUse separate CMake project for CVC4 examples. (#3196) tree | commitdiff
2019-09-25 Andrew ReynoldsReturn choice functions for approximate values in get... tree | commitdiff
2019-09-19 Andrew ReynoldsSupport context-(in)dependent decision strategies.... tree | commitdiff
2019-09-19 makaimannAdd support for creating constant arrays to the new... tree | commitdiff
2019-09-18 Andrew ReynoldsDecouple fmf-bound and finite-model-find (#3297) tree | commitdiff
2019-09-17 Andrew ReynoldsAvoid computing cardinality when constructing models... tree | commitdiff
next