projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Do not cache operator eliminations in arith (#4542)
[cvc5.git] / test / regress / regress0 /
2020-05-31 Andres NoetzliDo not cache operator eliminations in arith (#4542) tree | commitdiff
2020-05-26 MartinFix an incorrect limit in conversion from real to float... tree | commitdiff
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) tree | commitdiff
2020-05-22 Andrew Reynolds(proof-new) Add rewrite corresponding to regular expres... tree | commitdiff
2020-05-21 Andrew ReynoldsFix missing check for cardinality one in unconstrained... tree | commitdiff
2020-05-20 Andrew ReynoldsNormal form equality conflicts and uniqueness check... tree | commitdiff
2020-05-20 Andrew ReynoldsFix parametric datatype instantiation (#4493) tree | commitdiff
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... tree | commitdiff
2020-05-20 Andrew ReynoldsFix cached free variable identifiers in sygus term... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-05-05 Andrew ReynoldsAlways introduce fresh variable for unconstrained APPLY... tree | commitdiff
2020-04-28 Andrew ReynoldsSupport the SMT-LIB Unicode string standard by default... tree | commitdiff
2020-04-22 Abdalrhman MohamedConvert V2.5 SMT regressions to V2.6. (#4319) tree | commitdiff
2020-04-22 Andres NoetzliReinstantiate support for conjunctions in facts (#4377) tree | commitdiff
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) tree | commitdiff
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) tree | commitdiff
2020-04-15 Andrew ReynoldsDo not normalize to representatives for variable equali... tree | commitdiff
2020-04-15 Andrew ReynoldsAlways assign function values in higher order (#4279) tree | commitdiff
2020-04-14 Andrew ReynoldsFix dump-unsat-cores-full (#4303) tree | commitdiff
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming... tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-08 Andrew ReynoldsFix dump models and dump proofs (#4230) tree | commitdiff
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188) tree | commitdiff
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) tree | commitdiff
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) tree | commitdiff
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175) tree | commitdiff
2020-03-28 Abdalrhman MohamedConvert the last few Sygus benchmarks to V2. (#4172) tree | commitdiff
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... tree | commitdiff
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... tree | commitdiff
2020-03-26 AmaleeAdded unit-cube-like test for branch and bound (#3922) tree | commitdiff
2020-03-24 yoni206Int2BV fail on demand (#4079) tree | commitdiff
2020-03-22 Abdalrhman MohamedConvert V1 Sygus files to V2. (#4136) tree | commitdiff
2020-03-21 Andres NoetzliDon't run bv_nat parse test with competition build... tree | commitdiff
2020-03-19 Andres NoetzliOnly apply testConstStringInRegExp to const regexp... tree | commitdiff
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... tree | commitdiff
2020-03-19 Andrew ReynoldsFix issue with multiple infinities in CEGQI for LIRA... tree | commitdiff
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... tree | commitdiff
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... tree | commitdiff
2020-03-12 Aina NiemetzNew C++ API: Remove support for (reset). (#4037) tree | commitdiff
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine... tree | commitdiff
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) tree | commitdiff
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016) tree | commitdiff
2020-03-10 Andrew ReynoldsFix sort inference for top-level Boolean variables... tree | commitdiff
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) tree | commitdiff
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979) tree | commitdiff
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and... tree | commitdiff
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965) tree | commitdiff
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu... tree | commitdiff
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) tree | commitdiff
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... tree | commitdiff
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) tree | commitdiff
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) tree | commitdiff
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... tree | commitdiff
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) tree | commitdiff
2020-02-29 Andrew ReynoldsFix assertion related to assignability in the model... tree | commitdiff
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... tree | commitdiff
2020-02-27 Andrew ReynoldsFix large models for strings (#3835) tree | commitdiff
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe... tree | commitdiff
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) tree | commitdiff
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-24 Andres NoetzliMake lambda rewriter more robust (#3806) tree | commitdiff
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) tree | commitdiff
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) tree | commitdiff
2020-02-08 Andres NoetzliMake "unknown" non-critical for unsat cores check ... tree | commitdiff
2020-02-07 Andrew ReynoldsRefactor check-model handling in SmtEngine (#3723) tree | commitdiff
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721) tree | commitdiff
2020-02-04 Alex OzdemirRegression tests for arithmetic proofs. (#3701) tree | commitdiff
2020-02-03 Andrew ReynoldsMinor fixes to regressions (#3702) tree | commitdiff
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasib... tree | commitdiff
2020-01-31 Andres NoetzliFix arithmetic rewriter for exponential (#3688) tree | commitdiff
2020-01-30 Andrew ReynoldsEnsure literals in FMF decision strategies are in the... tree | commitdiff
2020-01-30 Andrew ReynoldsDo not debug check model for models with approximations... tree | commitdiff
2020-01-29 Andrew ReynoldsFix isLeq function in String utility (#3659) tree | commitdiff
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (... tree | commitdiff
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus defau... tree | commitdiff
2020-01-10 Andres NoetzliFix printing of models of uninterpreted sorts (#3597) tree | commitdiff
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 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-10 Haniel BarbosaFix ufho issues (#3551) 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 Andrew ReynoldsFix the subtyping relation for functions (#3494) tree | commitdiff
2019-12-02 Andres Noetzli[SMT2 Printer] Quote symbols starting with digit (... tree | commitdiff
2019-12-02 Andrew ReynoldsEnsure quantifiers options are set with --no-strings... tree | commitdiff
2019-11-30 Andres NoetzliCompetition build: Skip parsing error regression (... 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-19 Andres NoetzliFix reduction of `sqrt` (#3478) tree | commitdiff
2019-11-13 Andres NoetzliAllow (set-logic ...) after (reset) (#3457) tree | commitdiff
2019-11-04 Andrew ReynoldsAvoid non-well-founded sygus grammars (#3434) 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
next