summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2020-03-31Remove replay and use-theory options and idl (#4186)Andrew Reynolds
2020-03-31Convert more uses of string-specific functions (#4158)Andrew Reynolds
2020-03-30Rewrites for all remaining return statements in strings rewriter (#4178)Andrew Reynolds
2020-03-30Support indexed operators re.loop and re.^ (#4167)Andrew Reynolds
2020-03-30Remove ref skolem datatype option (#4185)Andrew Reynolds
2020-03-30Frontend support for the choice operator (#4175)mudathirmahgoub
2020-03-28Enumeration for String rewrites (#4173)Andrew Reynolds
2020-03-27Split transcendental solver to its own file (#4156)Andrew Reynolds
2020-03-27Move string utility file (#4164)Andrew Reynolds
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-26Added unit-cube-like test for branch and bound (#3922)Amalee
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-25 Generalize more uses of string-specific functions (#4145)Andrew Reynolds
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-21Simplify heuristic in `processNEqc` (#4129)Andres Noetzli
2020-03-20Generalize mkConcat for types (#4123)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-20Make handling of illegal internal representatives in quantifiers engine more ...Andrew Reynolds
2020-03-20Refactor enumerator for strings (#4014)Andrew Reynolds
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
2020-03-19Remove spurious assertion (#4117)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-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-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
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-13Generalize type rules for strings to sequences (#3987)Andrew Reynolds
2020-03-13Fix case of non-constant value for sygus sampling (#4051)Andrew Reynolds
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
2020-03-12Ensure legal candidate equalities when using relational triggers (#4035)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback