projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-04-09 Andrew ReynoldsDisable slow sygus regression (#4232) commit | commitdiff | tree
2020-04-09 Andrew ReynoldsSplit ProcessAssertions module from SmtEngine (#4210) commit | commitdiff | tree
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) commit | commitdiff | tree
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) commit | commitdiff | tree
2020-04-08 Andrew ReynoldsFix dump models and dump proofs (#4230) commit | commitdiff | tree
2020-04-08 Andrew ReynoldsEliminate call to currentNM within NodeManager (#4227) commit | commitdiff | tree
2020-04-07 Andrew ReynoldsCleanup deprecated quantifiers attribute features ... commit | commitdiff | tree
2020-04-07 Andrew ReynoldsDisable slow regression (#4221) commit | commitdiff | tree
2020-04-07 Andrew ReynoldsEnum for all remaining string inferences (#4220) commit | commitdiff | tree
2020-04-06 Andrew ReynoldsRemove links field in all toml files (#4201) commit | commitdiff | tree
2020-04-06 Andres NoetzliRefactor disequality processing in string solver (... commit | commitdiff | tree
2020-04-06 Aina NiemetzNew C++ API: Rename Solver::mkTermInternal. (#4217) commit | commitdiff | tree
2020-04-05 Andrew ReynoldsAdd missing stat for lemmas based on inferences (#4214) commit | commitdiff | tree
2020-04-05 Andres NoetzliAdd safe_print() support for Kind enum (#4213) commit | commitdiff | tree
2020-04-05 Andrew ReynoldsType-independent preregistration of empty word (#4205) commit | commitdiff | tree
2020-04-04 Aina NiemetzNew C++ API: Remove Op::getSort(). (#4208) commit | commitdiff | tree
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... commit | commitdiff | tree
2020-04-03 Andrew ReynoldsOnly rewrite lambdas via array representations when... commit | commitdiff | tree
2020-04-03 Andrew ReynoldsSplit sequences rewriter (#4194) commit | commitdiff | tree
2020-04-02 Andres NoetzliRemove undocumented/uncommon aliases (#4177) commit | commitdiff | tree
2020-04-02 Andrew ReynoldsIntroduce enums for all string inferences, excluding... commit | commitdiff | tree
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) commit | commitdiff | tree
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188) commit | commitdiff | tree
2020-04-01 Mathias PreinerFix install for ANTLR contrib script and CI dependency... commit | commitdiff | tree
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) commit | commitdiff | tree
2020-03-31 Mathias PreinerSwitch to GitHub actions for CI (#4190) commit | commitdiff | tree
2020-03-31 Andrew ReynoldsFix fmf benchmark (#4193) commit | commitdiff | tree
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186) commit | commitdiff | tree
2020-03-31 Andrew ReynoldsFix strange bound regression (#4192) commit | commitdiff | tree
2020-03-31 Andrew ReynoldsConvert more uses of string-specific functions (#4158) commit | commitdiff | tree
2020-03-31 Andrew ReynoldsFixing regressions (#4189) commit | commitdiff | tree
2020-03-30 Andrew ReynoldsRewrites for all remaining return statements in strings... commit | commitdiff | tree
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) commit | commitdiff | tree
2020-03-30 Andrew ReynoldsRemove ref skolem datatype option (#4185) commit | commitdiff | tree
2020-03-30 Mathias PreinerAdd coverage badge. (#4187) commit | commitdiff | tree
2020-03-30 Andrew ReynoldsFix arguments to print callback (#4171) commit | commitdiff | tree
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175) commit | commitdiff | tree
2020-03-29 Andrew ReynoldsEnumeration for String rewrites (#4173) commit | commitdiff | tree
2020-03-28 Abdalrhman... Change is-cons to (_ is cons) in Sygus benchmarks.... commit | commitdiff | tree
2020-03-28 Abdalrhman... Convert the last few Sygus benchmarks to V2. (#4172) commit | commitdiff | tree
2020-03-28 Abdalrhman... Stop printing datatype declaration for Sygus V1 grammar... commit | commitdiff | tree
2020-03-28 Alex OzdemirNode traversal iterator (#3845) commit | commitdiff | tree
2020-03-28 Andrew ReynoldsSplit transcendental solver to its own file (#4156) commit | commitdiff | tree
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... commit | commitdiff | tree
2020-03-27 Andrew ReynoldsFix expected output on arith regression (#4162) commit | commitdiff | tree
2020-03-27 Andrew ReynoldsMove string utility file (#4164) commit | commitdiff | tree
2020-03-27 Andrew ReynoldsDo not require that function sorts are first class... commit | commitdiff | tree
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... commit | commitdiff | tree
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154) commit | commitdiff | tree
2020-03-26 AmaleeAdded unit-cube-like test for branch and bound (#3922) commit | commitdiff | tree
2020-03-26 Andrew ReynoldsDisable slow regression (#4157) commit | commitdiff | tree
2020-03-26 Andrew ReynoldsAdd stats for string reductions, lemmas and conflicts... commit | commitdiff | tree
2020-03-26 Andrew ReynoldsGeneralize more string-specific functions (#4152) commit | commitdiff | tree
2020-03-26 Andrew ReynoldsCare graphs based on polymorphic operators in strings... commit | commitdiff | tree
2020-03-25 Andres NoetzliSupport async-signal-safe printing of inferences (... commit | commitdiff | tree
2020-03-25 Ahmed Irfanbv2int : linear mult opt (#4142) commit | commitdiff | tree
2020-03-25 Andrew Reynolds Generalize more uses of string-specific functions... commit | commitdiff | tree
2020-03-24 yoni206Int2BV fail on demand (#4079) commit | commitdiff | tree
2020-03-24 Andrew ReynoldsRestrict partial triggers to standard quantified formul... commit | commitdiff | tree
2020-03-24 Andrew ReynoldsRestrict cases of sygus grammar reduction based on... commit | commitdiff | tree
2020-03-23 Andrew ReynoldsInfer when sygus operators are equivalent to builtin... commit | commitdiff | tree
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141) commit | commitdiff | tree
2020-03-23 Andrew ReynoldsThrow exception for non-well-founded unimplemented... commit | commitdiff | tree
2020-03-23 Andrew ReynoldsChange transcendental function app slave list to unorde... commit | commitdiff | tree
2020-03-23 Andres NoetzliCollect statistics about normal form inferences (#4127) commit | commitdiff | tree
2020-03-22 Andrew ReynoldsSort inference does not handle APPLY_UF when higher... commit | commitdiff | tree
2020-03-22 Abdalrhman... Convert V1 Sygus files to V2. (#4136) commit | commitdiff | tree
2020-03-21 Andres NoetzliSimplify heuristic in `processNEqc` (#4129) commit | commitdiff | tree
2020-03-21 Andres NoetzliDon't run bv_nat parse test with competition build... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsGeneralize mkConcat for types (#4123) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsFix variable shadowing issue in sygus-inference (#4121) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsFix sort comparison within assertion in cegis (#4113) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsGuard cases of sort inference in quantifier free logics... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsSplit string-specific operators from TheoryStringsRewri... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsDo not assign higher-order representative if function... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsHandle failures for sygus QE preprocess (#4072) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsParse error for SyGuS version 1.0 vs 2.0 (#4057) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsMake handling of illegal internal representatives in... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsRefactor enumerator for strings (#4014) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsFix regression output related to sygus+bv-div-zero... commit | commitdiff | tree
2020-03-19 yoni206Bv2int fail on demand commit | commitdiff | tree
2020-03-19 Andres NoetzliOnly apply testConstStringInRegExp to const regexp... commit | commitdiff | tree
2020-03-19 Andrew ReynoldsSyGuS must use total bitvector division (#4119) commit | commitdiff | tree
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... commit | commitdiff | tree
2020-03-19 Andrew ReynoldsRemove spurious assertion (#4117) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsExplicitly handle isFinite for rounding modes (#4115) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsAlways enable cbqi literal dependency (#4116) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsFix issue with multiple infinities in CEGQI for LIRA... commit | commitdiff | tree
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) commit | commitdiff | tree
2020-03-17 Aina NiemetzSmtEngine: Convert members owned by SmtEngine to unique... commit | commitdiff | tree
2020-03-16 Alex OzdemirRemove AlwaysAssert(false) for hole. commit | commitdiff | tree
2020-03-16 Alex Ozdemirclang-format commit | commitdiff | tree
2020-03-16 Alex OzdemirFix simplicity check in prop commit | commitdiff | tree
2020-03-16 Alex OzdemirFix antecedent loop. Whoops commit | commitdiff | tree
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes commit | commitdiff | tree
2020-03-16 Alex OzdemirExpand the definition of a "simple" farkas proof. commit | commitdiff | tree
2020-03-16 Aina NiemetzDecisionEngine: Use single unique pointer for ITE strat... commit | commitdiff | tree
2020-03-16 Aina NiemetzIssue 4077: Add unit test to reproduce issue. (#4107) commit | commitdiff | tree
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... commit | commitdiff | tree
2020-03-16 Andrew ReynoldsHandle cases in --sygus-rr where evaluation is not... commit | commitdiff | tree
next