summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-09-29Merge branch 'master' into splitEqRewsplitEqRewAndrew Reynolds
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-27Merge branch 'master' into splitEqRewAndrew 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-26fixAndres Noetzli
2019-09-26CVC print support for recoverable failure (#3323)Andrew Reynolds
2019-09-26Fix commentAndres Noetzli
2019-09-26Merge branch 'master' into splitEqRewAndres Noetzli
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-25Add Windows cross-compiling instructions to INSTALL.md. (#3226)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-18Add run script for next SMT-COMP (#3298)Andres Noetzli
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-16Fix spurious meta-info in regression (#3294)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-16Adding new scripts for CASC/TPTP (#3291)Haniel Barbosa
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