summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-25Merge branch 'master' into safePrintInferencessafePrintInferencesAndrew Reynolds
2020-03-25bv2int : linear mult opt (#4142)Ahmed Irfan
2020-03-25 Generalize more uses of string-specific functions (#4145)Andrew Reynolds
2020-03-24minorAndres Noetzli
2020-03-24formatAndres Noetzli
2020-03-24Address offline discussionAndres Noetzli
2020-03-24Support async-signal-safe printing of inferencesAndres Noetzli
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
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
2020-03-16SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)Aina Niemetz
2020-03-16Remove AlwaysAssert(false) for hole.Alex Ozdemir
2020-03-16clang-formatAlex Ozdemir
2020-03-16Fix simplicity check in propAlex Ozdemir
2020-03-16Fix antecedent loop. WhoopsAlex Ozdemir
2020-03-16Only save farkas+tightening proofs. Error on holesAlex Ozdemir
2020-03-16Expand the definition of a "simple" farkas proof.Alex Ozdemir
2020-03-16DecisionEngine: Use single unique pointer for ITE strategy . (#4078)Aina Niemetz
2020-03-16Issue 4077: Add unit test to reproduce issue. (#4107)Aina Niemetz
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
2020-03-15Handle cases in --sygus-rr where evaluation is not constant (#4100)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback