summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2019-10-29Split some generic utilities from the non-linear extension (#3419)Andrew Reynolds
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-27Fix collect model info for higher-order (#3409)Andrew Reynolds
2019-10-23Fixes for SyGuS + regular expressions (#3313)Andrew Reynolds
2019-10-22Refactoring skolems for sets (#3381)Andrew Reynolds
2019-10-22NodeValue: Eliminate redundant NBITS macros. (#3400)Aina Niemetz
2019-10-17 Move datatype utility functions to own file (#3397)Andrew Reynolds
2019-10-16Solver state for theory of strings (#3181)Andrew Reynolds
2019-10-15Fix OOB access (#3383)Andres Noetzli
2019-10-14Support UF in default sygus grammars (#3319)Andrew Reynolds
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-10-14Ensure lemmas from sygus repair const are guarded (#3385)Andrew Reynolds
2019-10-14Minor refactor in strings rewriter (#3387)Andrew Reynolds
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
2019-10-11Add support for UBSan instrumentation (#3382)Andres Noetzli
2019-10-10Make order of theories explicit in the source code. (#3379)Aina Niemetz
2019-10-10Warning instead of assertion for failing propagating instance (#3380)Andrew Reynolds
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-10-08Fix method for getting arithmetic function definition body (#3371)Andrew Reynolds
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
2019-10-08pass parameters by reference where it affects performancePiotr Trojanek
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
2019-10-04Avoid duplicate lemmas in datatypes (#3310)Andrew Reynolds
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
2019-09-27Support smt2 language "match" term (#3258)Andrew Reynolds
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-17 Encapsulate relevant domain (#3293)Andrew Reynolds
2019-09-16Avoid computing cardinality when constructing models (#3268)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16Move specific attributes out of term util (#3279)Andrew Reynolds
2019-09-16Sygus type info class (#3187)Andrew Reynolds
2019-09-16 Fix HO model construction for functions having Boolean arguments (#3158)Andrew Reynolds
2019-09-16Move virtual term substitution utilities to own file and document (#3278)Andrew Reynolds
2019-09-16Return RecoverableModalException when model is not available. (#3283)Andrew Reynolds
2019-09-16Initialize fields in sets inference manager (#3289)Andrew Reynolds
2019-09-13Move higher-order matching predicate (#3280)Andrew Reynolds
2019-09-13Split, refactor and document the theory of sets (#3085)Andrew Reynolds
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
2019-09-12Update to standard implementation of contains term (#3270)Andrew Reynolds
2019-09-12 Fix default grammar construction for arrays when no free variables are prese...Andrew Reynolds
2019-09-12Encapsulate synth engine (#3271)Andrew Reynolds
2019-09-11Refactoring finite bounds in Quantifiers Engine (#3261)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback