cvc5.git
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910)
2020-04-16 Andrew ReynoldsAdd ProofNodeManager and ProofChecker (#4317)
2020-04-16 Andrew ReynoldsEliminate remaining references to parent TheoryStrings...
2020-04-15 Andrew ReynoldsAdd ProofNode data structure (#4311)
2020-04-15 Andrew ReynoldsMove regular expression inclusion test to RegExpEntail...
2020-04-15 Andrew ReynoldsChange option names --default-dag-thresh and --default...
2020-04-15 Andrew ReynoldsSplit TermRegistry object from TheoryStrings (#4312)
2020-04-15 Andrew ReynoldsDo not mark string extended functions as eliminated...
2020-04-15 Andrew ReynoldsFix assertion in enumerative instantiation (#4313)
2020-04-15 Andrew ReynoldsConvert more cases of strings to words (#4206)
2020-04-15 Andrew ReynoldsAbort if in conflict in enumerative instantiation ...
2020-04-15 Andrew ReynoldsAlways flush lemmas from downwards closure in sets...
2020-04-15 Andrew ReynoldsDo not normalize to representatives for variable equali...
2020-04-15 Andrew ReynoldsAlways assign function values in higher order (#4279)
2020-04-15 Andrew ReynoldsFix combinations of cegqi and non-standard triggers...
2020-04-15 Andrew ReynoldsDisable preregistration of instantiations for cegqi...
2020-04-14 Andrew ReynoldsDisable macros when higher-order (#4266)
2020-04-14 Andrew ReynoldsFix relevant domain computation for nested quantifiers...
2020-04-14 Andrew ReynoldsRemove a few options (#4295)
2020-04-14 Andrew ReynoldsRemove a few spurious assertions (#4294)
2020-04-14 Andrew ReynoldsRemove early type check option (#4234)
2020-04-14 Andrew ReynoldsRemove argument extender (#4223)
2020-04-14 Andrew ReynoldsRemove mergePredicates from EqualityEngine interface...
2020-04-14 Andrew ReynoldsFix dump-unsat-cores-full (#4303)
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming...
2020-04-12 Andrew ReynoldsFixes for extended rewriter (#4278)
2020-04-12 Andrew ReynoldsMove slow nl regression to regress3 (#4276)
2020-04-11 Alex OzdemirAdd skip predicate to node traversal. (#4222)
2020-04-11 Andrew ReynoldsEnsure exported sygus solutions match grammar (#4270)
2020-04-11 Andrew ReynoldsSplit the non-linear solver (#4219)
2020-04-10 Andrew ReynoldsExplain non-emptiness by non-zero length in strings...
2020-04-10 Andrew ReynoldsAdd a few stats to strings (#4252)
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233)
2020-04-09 Mathias PreinerCI: Add a step to list dependencies. (#4255)
2020-04-09 Andrew ReynoldsDisable slow sygus regression (#4232)
2020-04-09 Andrew ReynoldsSplit ProcessAssertions module from SmtEngine (#4210)
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211)
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044)
2020-04-08 Andrew ReynoldsFix dump models and dump proofs (#4230)
2020-04-08 Andrew ReynoldsEliminate call to currentNM within NodeManager (#4227)
2020-04-07 Andrew ReynoldsCleanup deprecated quantifiers attribute features ...
2020-04-07 Andrew ReynoldsDisable slow regression (#4221)
2020-04-07 Andrew ReynoldsEnum for all remaining string inferences (#4220)
2020-04-06 Andrew ReynoldsRemove links field in all toml files (#4201)
2020-04-06 Andres NoetzliRefactor disequality processing in string solver (...
2020-04-06 Aina NiemetzNew C++ API: Rename Solver::mkTermInternal. (#4217)
2020-04-05 Andrew ReynoldsAdd missing stat for lemmas based on inferences (#4214)
2020-04-05 Andres NoetzliAdd safe_print() support for Kind enum (#4213)
2020-04-05 Andrew ReynoldsType-independent preregistration of empty word (#4205)
2020-04-04 Aina NiemetzNew C++ API: Remove Op::getSort(). (#4208)
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings...
2020-04-03 Andrew ReynoldsOnly rewrite lambdas via array representations when...
2020-04-03 Andrew ReynoldsSplit sequences rewriter (#4194)
2020-04-02 Andres NoetzliRemove undocumented/uncommon aliases (#4177)
2020-04-02 Andrew ReynoldsIntroduce enums for all string inferences, excluding...
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197)
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188)
2020-04-01 Mathias PreinerFix install for ANTLR contrib script and CI dependency...
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191)
2020-03-31 Mathias PreinerSwitch to GitHub actions for CI (#4190)
2020-03-31 Andrew ReynoldsFix fmf benchmark (#4193)
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186)
2020-03-31 Andrew ReynoldsFix strange bound regression (#4192)
2020-03-31 Andrew ReynoldsConvert more uses of string-specific functions (#4158)
2020-03-31 Andrew ReynoldsFixing regressions (#4189)
2020-03-30 Andrew ReynoldsRewrites for all remaining return statements in strings...
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167)
2020-03-30 Andrew ReynoldsRemove ref skolem datatype option (#4185)
2020-03-30 Mathias PreinerAdd coverage badge. (#4187)
2020-03-30 Andrew ReynoldsFix arguments to print callback (#4171)
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175)
2020-03-29 Andrew ReynoldsEnumeration for String rewrites (#4173)
2020-03-28 Abdalrhman... Change is-cons to (_ is cons) in Sygus benchmarks....
2020-03-28 Abdalrhman... Convert the last few Sygus benchmarks to V2. (#4172)
2020-03-28 Abdalrhman... Stop printing datatype declaration for Sygus V1 grammar...
2020-03-28 Alex OzdemirNode traversal iterator (#3845)
2020-03-28 Andrew ReynoldsSplit transcendental solver to its own file (#4156)
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (...
2020-03-27 Andrew ReynoldsFix expected output on arith regression (#4162)
2020-03-27 Andrew ReynoldsMove string utility file (#4164)
2020-03-27 Andrew ReynoldsDo not require that function sorts are first class...
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape...
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154)
2020-03-26 AmaleeAdded unit-cube-like test for branch and bound (#3922)
2020-03-26 Andrew ReynoldsDisable slow regression (#4157)
2020-03-26 Andrew ReynoldsAdd stats for string reductions, lemmas and conflicts...
2020-03-26 Andrew ReynoldsGeneralize more string-specific functions (#4152)
2020-03-26 Andrew ReynoldsCare graphs based on polymorphic operators in strings...
2020-03-25 Andres NoetzliSupport async-signal-safe printing of inferences (...
2020-03-25 Ahmed Irfanbv2int : linear mult opt (#4142)
2020-03-25 Andrew Reynolds Generalize more uses of string-specific functions...
2020-03-24 yoni206Int2BV fail on demand (#4079)
2020-03-24 Andrew ReynoldsRestrict partial triggers to standard quantified formul...
2020-03-24 Andrew ReynoldsRestrict cases of sygus grammar reduction based on...
2020-03-23 Andrew ReynoldsInfer when sygus operators are equivalent to builtin...
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141)
2020-03-23 Andrew ReynoldsThrow exception for non-well-founded unimplemented...
2020-03-23 Andrew ReynoldsChange transcendental function app slave list to unorde...
2020-03-23 Andres NoetzliCollect statistics about normal form inferences (#4127)
2020-03-22 Andrew ReynoldsSort inference does not handle APPLY_UF when higher...
next