summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-10-07[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)Andres Noetzli
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
2019-10-04Avoid duplicate lemmas in datatypes (#3310)Andrew Reynolds
2019-10-03Disable proofs for unsupported logics (#3327)yoni206
2019-10-03Add missing type definitions to CDHashMap iterator (#3330)Andres Noetzli
2019-10-03[SMT2 Parser] Move code of `sygusCommand` (#3335)Andres Noetzli
2019-10-02Fix compiler warning. (#3348)Aina Niemetz
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-09-29Add help for sygus 2.0 (#3318)Andrew Reynolds
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
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-27Make substitution index context-independent (#2474)Andres Noetzli
2019-09-26CVC print support for recoverable failure (#3323)Andrew Reynolds
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
2019-09-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-25Fix printing of instantiation patterns (#3305)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-18Add support for creating constant arrays to the new C++ API (#3296)makaimann
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-18Minor cleaning (#3295)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 parameterized check (#3290)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-16Fix compiler warning in options.cpp. (#3284)Aina Niemetz
2019-09-16Initialize fields in sets inference manager (#3289)Andrew Reynolds
2019-09-16parser: Improve error message for unrecognized input file format. (#3285)Aina Niemetz
2019-09-13Disallow let in sygus grammars, check for free variables in sygus constructor...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
2019-09-11Fix not to output all warnings (#2778)Ken Matsui
2019-09-11Fix type assertion in getSynthSolutions (#3252)Andrew Reynolds
2019-09-11Infrastructure for instantiation rewriter (#3262)Andrew Reynolds
2019-09-11Fix constructor type printing (#3246)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback