summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2019-11-29Unfold regexps two waysregexpBidirUnfoldAndres Noetzli
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-27 Fix indexof range lemma (#3499)Andrew Reynolds
2019-11-25Better front-end type checking for SyGuS (#3496)Andrew Reynolds
2019-11-22Minor refactoring of compute model value for nl (#3489)Andrew Reynolds
2019-11-21hard limit for rec-fun eval (#3485)Haniel Barbosa
2019-11-21Evaluation unfolding for symbolic SyGuS constructors (#3483)Andrew Reynolds
2019-11-20Lazy evaluation via rec-funs of ITE expressions (#3482)Haniel Barbosa
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-18Use standard sygus interface for abduction and rewrite rule synthesis (#3471)Andrew Reynolds
2019-11-18Improve interface for sygus datatype, fix utilities (#3473)Andrew Reynolds
2019-11-15Use standard interface for sygus default grammar construction (#3466)Andrew Reynolds
2019-11-15Introduce SyGuS datatype API (#3465)Andrew Reynolds
2019-11-12Refactor non-linear extension for model-based refinement (#3452)Andrew Reynolds
2019-11-11Eliminate remaining references to type/expr in datatype type rules. (#3450)Andrew Reynolds
2019-11-10Fix bugs related to sygus higher-order + recursive functions (#3448)Andrew Reynolds
2019-11-09Fixes in relations related to datatypes not passed by reference (#3449)Andrew Reynolds
2019-11-06Move more string utility functions (#3398)Andrew Reynolds
2019-11-06Migrate more datatype methods to the Node level (#3443)Andrew Reynolds
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-05Separate model object in non-linear extension (#3426)Andrew Reynolds
2019-11-05Refactor type matcher utility (#3439)Andrew Reynolds
2019-11-04Make check synth solution robust to auxiliary assertions (#3432)Andrew Reynolds
2019-11-04Fix ho extensionality in collect model info (#3435)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-11-04Eliminate deprecated utility function from sygus (#3431)Andrew Reynolds
2019-11-01Fix non-termination in datatype type enumerator (#3369)Andrew Reynolds
2019-11-01Fix and refactor TheoryStrings::checkFlatForms() (#3326)Andres Noetzli
2019-11-01Eagerly beta reduce during sygus to builtin term conversion (#3418)Andrew Reynolds
2019-10-31Rename datatypes sygus solver (#3417)Andrew Reynolds
2019-10-31Fix Unimplemented() macros missed in #3366. (#3424)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback