summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-27Merge branch 'master' into issue4151issue4151Aina Niemetz
2020-03-27Fix expected output on arith regression (#4162)Andrew Reynolds
2020-03-27Merge branch 'master' into issue4151Aina Niemetz
2020-03-27Move string utility file (#4164)Andrew Reynolds
2020-03-27Do not require that function sorts are first class internally (#4128)Andrew Reynolds
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-26AddressAndres Noetzli
2020-03-26Move set defaults function to its own file (#4154)Andrew Reynolds
2020-03-26more formattingAndres Noetzli
2020-03-26minorAndres Noetzli
2020-03-26Fix issues with unsat cores and reset-assertionsAndres Noetzli
2020-03-26Added unit-cube-like test for branch and bound (#3922)Amalee
2020-03-26Disable slow regression (#4157)Andrew Reynolds
2020-03-26Add stats for string reductions, lemmas and conflicts (#4149)Andrew Reynolds
2020-03-26Generalize more string-specific functions (#4152)Andrew Reynolds
2020-03-25Care graphs based on polymorphic operators in strings (#4150)Andrew Reynolds
2020-03-25Support async-signal-safe printing of inferences (#4148)Andres Noetzli
2020-03-25bv2int : linear mult opt (#4142)Ahmed Irfan
2020-03-25 Generalize more uses of string-specific functions (#4145)Andrew Reynolds
2020-03-24Int2BV fail on demand (#4079)yoni206
2020-03-24Restrict partial triggers to standard quantified formulas (#4144)Andrew Reynolds
2020-03-23Restrict cases of sygus grammar reduction based on argument variants (#4131)Andrew Reynolds
2020-03-23Infer when sygus operators are equivalent to builtin kinds (#4140)Andrew Reynolds
2020-03-23Simplify auxiliary variable handling in CEGQI (#4141)Andrew Reynolds
2020-03-23Throw exception for non-well-founded unimplemented SyGuS types. (#4125)Andrew Reynolds
2020-03-23Change transcendental function app slave list to unordered_set (#4139)Andrew Reynolds
2020-03-22Collect statistics about normal form inferences (#4127)Andres Noetzli
2020-03-22Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)Andrew Reynolds
2020-03-21Convert V1 Sygus files to V2. (#4136)Abdalrhman Mohamed
2020-03-21Simplify heuristic in `processNEqc` (#4129)Andres Noetzli
2020-03-20Don't run bv_nat parse test with competition build (#4126)Andres Noetzli
2020-03-20Generalize mkConcat for types (#4123)Andrew Reynolds
2020-03-20Fix variable shadowing issue in sygus-inference (#4121)Andrew Reynolds
2020-03-20Fix sort comparison within assertion in cegis (#4113)Andrew Reynolds
2020-03-20Guard cases of sort inference in quantifier free logics in uf cardinality (#4...Andrew Reynolds
2020-03-20Split string-specific operators from TheoryStringsRewriter (#3920)Andrew Reynolds
2020-03-20Do not assign higher-order representative if function does not exist (#4073)Andrew Reynolds
2020-03-20Handle failures for sygus QE preprocess (#4072)Andrew Reynolds
2020-03-20Parse error for SyGuS version 1.0 vs 2.0 (#4057)Andrew Reynolds
2020-03-20Make handling of illegal internal representatives in quantifiers engine more ...Andrew Reynolds
2020-03-20Refactor enumerator for strings (#4014)Andrew Reynolds
2020-03-19Fix regression output related to sygus+bv-div-zero (#4122)Andrew Reynolds
2020-03-19Bv2int fail on demandyoni206
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
2020-03-19SyGuS must use total bitvector division (#4119)Andrew Reynolds
2020-03-18Only allow bv2nat/int2bv with BV and integer logic (#4118)Andres Noetzli
2020-03-19Remove spurious assertion (#4117)Andrew Reynolds
2020-03-18Explicitly handle isFinite for rounding modes (#4115)Andrew Reynolds
2020-03-18Always enable cbqi literal dependency (#4116)Andrew Reynolds
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback