summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06Use str.subtr in str.to.int/int.to.str reduction (#3544)Andres Noetzli
2019-12-06Throw exception instead of warning for approximate models (#3542)Andrew Reynolds
2019-12-06Add lemma for str.to.int/int.to.str (#3541)Andres Noetzli
2019-12-06Optimize the rewriter for DT_SYGUS_EVAL (#3529)Andrew Reynolds
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-12-06[proof] Eliminate side-condition from ER signature (#3230)Alex Ozdemir
2019-12-05Introduce the Node-level Datatypes API (#3462)Andrew Reynolds
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ...Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-04Add mkOp for a single Kind (#3522)makaimann
2019-12-04Fix the subtyping relation for functions (#3494)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-12-04Fixes for SyGuS PBE + templated string concatenations + datatypes (#3492)Andrew Reynolds
2019-12-04Fix single invocation solution construction for multiple function case (#3516)Andrew Reynolds
2019-12-03Fix corner case in model construction of strings (#3524)Andres Noetzli
2019-12-03Improve flexibility of lemma output in non-linear solver (#3518)Andrew Reynolds
2019-12-03Rewrite `str.contains` used for character matching (#3519)Andres Noetzli
2019-12-03Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT...makaimann
2019-12-02[SMT2 Printer] Quote symbols starting with digit (#3517)Andres Noetzli
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ AP...makaimann
2019-12-02 Update ownership policy for dynamic quantifiers splitting (#3493)Andrew Reynolds
2019-12-02Fix case of higher-order + sygus inference (#3509)Andrew Reynolds
2019-12-01Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)Andrew Reynolds
2019-12-01Prevent ref count from reaching zero in BV instantiator (#3512)Andres Noetzli
2019-11-29improving parsing error messages related to HOL (#3510)Haniel Barbosa
2019-11-29Fix fast SyGuS enumeration for interpreted constants (#3501)Andrew Reynolds
2019-11-29Check free variables in assertions when using SyGuS (#3504)Andrew Reynolds
2019-11-27Fix sygus inference for choice functions introduced at preprocess (#3500)Andrew Reynolds
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-18Add a few comments to ProofManager (#3477)Alex Ozdemir
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-17Updates to the unit tests, api, and examples for datatypes (#3459)Andrew Reynolds
2019-11-16Add support for ThreadSanitizer instrumentation (#3467)Andres Noetzli
2019-11-15Use standard interface for sygus default grammar construction (#3466)Andrew Reynolds
2019-11-15Introduce SyGuS datatype API (#3465)Andrew Reynolds
2019-11-15Fix wrong kind in sygus version 1 parser (#3463)Andrew Reynolds
2019-11-13Allow (set-logic ...) after (reset) (#3457)Andres Noetzli
2019-11-13Distinguish unknown status for model printing (#3454)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback