git.libre-soc.org Git - cvc5.git/search

2019-11-27	Andrew Reynolds	Fix sygus inference for choice functions introduced...	commit \| commitdiff \| tree
2019-11-27	Haniel Barbosa	Enable sygusRecFun by default and fixes SyGuS+RecFun...	commit \| commitdiff \| tree
2019-11-27	Andrew Reynolds	Fix indexof range lemma (#3499)	commit \| commitdiff \| tree
2019-11-22	Andrew Reynolds	Minor refactoring of compute model value for nl (#3489)	commit \| commitdiff \| tree
2019-11-21	Haniel Barbosa	hard limit for rec-fun eval (#3485)	commit \| commitdiff \| tree
2019-11-21	Andrew Reynolds	Evaluation unfolding for symbolic SyGuS constructors...	commit \| commitdiff \| tree
2019-11-18	Andres Noetzli	Use -Wimplicit-fallthrough (#3464)	commit \| commitdiff \| tree
2019-11-18	Andrew Reynolds	Use standard sygus interface for abduction and rewrite...	commit \| commitdiff \| tree
2019-11-18	Andrew Reynolds	Improve interface for sygus datatype, fix utilities...	commit \| commitdiff \| tree
2019-11-18	Andrew Reynolds	Updates to the unit tests, api, and examples for datatypes...	commit \| commitdiff \| tree
2019-11-17	Andres Noetzli	Add support for ThreadSanitizer instrumentation (#3467)	commit \| commitdiff \| tree
2019-11-16	Andrew Reynolds	Use standard interface for sygus default grammar constructio...	commit \| commitdiff \| tree
2019-11-15	Andrew Reynolds	Introduce SyGuS datatype API (#3465)	commit \| commitdiff \| tree
2019-11-13	Andres Noetzli	Allow (set-logic ...) after (reset) (#3457)	commit \| commitdiff \| tree
2019-11-13	Andrew Reynolds	Distinguish unknown status for model printing (#3454)	commit \| commitdiff \| tree
2019-11-13	Andrew Reynolds	Refactor non-linear extension for model-based refinement...	commit \| commitdiff \| tree
2019-11-11	Andrew Reynolds	Add missing utilities for Node-level Datatype API ...	commit \| commitdiff \| tree
2019-11-11	Andrew Reynolds	Eliminate remaining references to type/expr in datatype...	commit \| commitdiff \| tree
2019-11-08	Mathias Preiner	cmake: Disable C++ GNU extensions. (#3446)	commit \| commitdiff \| tree
2019-11-06	Andrew Reynolds	Support for SyGuS PBE + recursive functions (#3433)	commit \| commitdiff \| tree
2019-11-05	Andrew Reynolds	Separate model object in non-linear extension (#3426)	commit \| commitdiff \| tree
2019-11-05	Andrew Reynolds	Refactor type matcher utility (#3439)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Make check synth solution robust to auxiliary assertions...	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Fix ho extensionality in collect model info (#3435)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Avoid non-well-founded sygus grammars (#3434)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Make getSynthSolution return a Bool (#3306)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Eliminate deprecated utility function from sygus (...	commit \| commitdiff \| tree
2019-11-01	Andrew Reynolds	Fix non-termination in datatype type enumerator (#3369)	commit \| commitdiff \| tree
2019-11-01	Andres Noetzli	Fix and refactor TheoryStrings::checkFlatForms() (...	commit \| commitdiff \| tree
2019-11-01	Andrew Reynolds	Eagerly beta reduce during sygus to builtin term conversion...	commit \| commitdiff \| tree
2019-11-01	Andrew Reynolds	Rename datatypes sygus solver (#3417)	commit \| commitdiff \| tree
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	commit \| commitdiff \| tree
2019-10-30	Andrew Reynolds	Split some generic utilities from the non-linear extension...	commit \| commitdiff \| tree
2019-10-28	Andrew Reynolds	Fix for non-linear models (#3410)	commit \| commitdiff \| tree
2019-10-22	Aina Niemetz	NodeValue: Eliminate redundant NBITS macros. (#3400)	commit \| commitdiff \| tree
2019-10-17	Andrew Reynolds	Move datatype utility functions to own file (#3397)	commit \| commitdiff \| tree
2019-10-15	Andres Noetzli	Fix line numbers in templates (#3391)	commit \| commitdiff \| tree
2019-10-15	Andres Noetzli	Remove remaining references to Boost and Autotools...	commit \| commitdiff \| tree
2019-10-15	Andres Noetzli	Fix OOB access (#3383)	commit \| commitdiff \| tree
2019-10-15	Andres Noetzli	Fix regression (#3393)	commit \| commitdiff \| tree
2019-10-14	Andres Noetzli	Disable regression test for competition build (#3388)	commit \| commitdiff \| tree
2019-10-14	Andrew Reynolds	Remove benchmark (#3389)	commit \| commitdiff \| tree
2019-10-14	Andrew Reynolds	Support UF in default sygus grammars (#3319)	commit \| commitdiff \| tree
2019-10-14	Andrew Reynolds	Apply sygus repair constant techniques restricted to...	commit \| commitdiff \| tree
2019-10-14	Andrew Reynolds	Ensure lemmas from sygus repair const are guarded ...	commit \| commitdiff \| tree
2019-10-14	Andrew Reynolds	Minor refactor in strings rewriter (#3387)	commit \| commitdiff \| tree
2019-10-11	Andrew Reynolds	Check that logic is set when synth-fun command is encountere...	commit \| commitdiff \| tree
2019-10-11	Andres Noetzli	Add support for UBSan instrumentation (#3382)	commit \| commitdiff \| tree
2019-10-11	Aina Niemetz	Make order of theories explicit in the source code...	commit \| commitdiff \| tree
2019-10-10	Andrew Reynolds	Warning instead of assertion for failing propagating...	commit \| commitdiff \| tree
2019-10-10	Mathias Preiner	test: Add TS_UTILS_EXPECT_ABORT macro for unit tests...	commit \| commitdiff \| tree
2019-10-09	Andres Noetzli	Avoid printing success for `--force-logic` (#3363)	commit \| commitdiff \| tree
2019-10-09	Mathias Preiner	cmake: Fix include of CVC4JavaTargets.cmake. (#3373)	commit \| commitdiff \| tree
2019-10-09	Aina Niemetz	New C++ API: Term: Add missing checks for null. (#3364)	commit \| commitdiff \| tree
2019-10-08	Aina Niemetz	New C++ API: Add Term::getId(). (#3360)	commit \| commitdiff \| tree
2019-10-08	Andres Noetzli	[SMT2 Parser] Move code of `rewriterulesCommand` (...	commit \| commitdiff \| tree
2019-10-03	Aina Niemetz	Travis: Reenable building and running of examples....	commit \| commitdiff \| tree
2019-10-03	Andres Noetzli	Add missing type definitions to CDHashMap iterator...	commit \| commitdiff \| tree
2019-10-03	Andres Noetzli	[SMT2 Parser] Move code of `sygusCommand` (#3335)	commit \| commitdiff \| tree
2019-10-03	Aina Niemetz	Fix compiler warning. (#3348)	commit \| commitdiff \| tree
2019-10-02	Andres Noetzli	[SMT-COMP] Remove --unconstrained-simp for incremental...	commit \| commitdiff \| tree
2019-09-30	Andrew Reynolds	Add help for sygus 2.0 (#3318)	commit \| commitdiff \| tree
2019-09-30	Andrew Reynolds	Avoid cases of empty sygus grammars (#3301)	commit \| commitdiff \| tree
2019-09-29	Andrew Reynolds	Fail single invocation techniques when utility inference...	commit \| commitdiff \| tree
2019-09-29	Andres Noetzli	Introduce template classes for simple type rules (...	commit \| commitdiff \| tree
2019-09-28	Andrew Reynolds	Support smt2 language "match" term (#3258)	commit \| commitdiff \| tree
2019-09-27	Andrew Reynolds	Fix case of disjunctive conclusion in strings (#3254)	commit \| commitdiff \| tree
2019-09-27	Andres Noetzli	Make substitution index context-independent (#2474)	commit \| commitdiff \| tree
2019-09-25	Andrew Reynolds	Add isParameterized function to Expr (#3303)	commit \| commitdiff \| tree
2019-09-25	Mathias Preiner	Use separate CMake project for CVC4 examples. (#3196)	commit \| commitdiff \| tree
2019-09-25	Mathias Preiner	Add Windows cross-compiling instructions to INSTALL...	commit \| commitdiff \| tree
2019-09-25	Andrew Reynolds	Fix printing of instantiation patterns (#3305)	commit \| commitdiff \| tree
2019-09-25	Andrew Reynolds	Return choice functions for approximate values in get...	commit \| commitdiff \| tree
2019-09-19	Andrew Reynolds	Support context-(in)dependent decision strategies....	commit \| commitdiff \| tree
2019-09-19	makaimann	Add support for creating constant arrays to the new...	commit \| commitdiff \| tree
2019-09-18	Andrew Reynolds	Decouple fmf-bound and finite-model-find (#3297)	commit \| commitdiff \| tree
2019-09-18	Andrew Reynolds	Minor cleaning (#3295)	commit \| commitdiff \| tree
2019-09-17	Andrew Reynolds	Encapsulate relevant domain (#3293)	commit \| commitdiff \| tree
2019-09-17	Andrew Reynolds	Avoid computing cardinality when constructing models...	commit \| commitdiff \| tree
2019-09-17	Andrew Reynolds	Remove parameterized check (#3290)	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Fix spurious meta-info in regression (#3294)	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Remove equality inference option for quantifiers (...	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Move specific attributes out of term util (#3279)	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Sygus type info class (#3187)	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Fix HO model construction for functions having Boolean...	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Move virtual term substitution utilities to own file...	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Return RecoverableModalException when model is not...	commit \| commitdiff \| tree
2019-09-16	Haniel Barbosa	Adding new scripts for CASC/TPTP (#3291)	commit \| commitdiff \| tree
2019-09-16	Andrew Reynolds	Initialize fields in sets inference manager (#3289)	commit \| commitdiff \| tree
2019-09-13	Andrew Reynolds	Disallow let in sygus grammars, check for free variables...	commit \| commitdiff \| tree
2019-09-13	Andrew Reynolds	Move higher-order matching predicate (#3280)	commit \| commitdiff \| tree
2019-09-13	Andrew Reynolds	Split, refactor and document the theory of sets (#3085)	commit \| commitdiff \| tree
2019-09-12	Andrew Reynolds	Rename UF with cardinality extension (#3241)	commit \| commitdiff \| tree
2019-09-12	Andrew Reynolds	Update to standard implementation of contains term...	commit \| commitdiff \| tree
2019-09-12	Andrew Reynolds	Fix default grammar construction for arrays when no...	commit \| commitdiff \| tree
2019-09-12	Andrew Reynolds	Encapsulate synth engine (#3271)	commit \| commitdiff \| tree
2019-09-12	Andrew Reynolds	Refactoring finite bounds in Quantifiers Engine (#3261)	commit \| commitdiff \| tree
2019-09-11	Andrew Reynolds	Fix type assertion in getSynthSolutions (#3252)	commit \| commitdiff \| tree
2019-09-11	Andrew Reynolds	Infrastructure for instantiation rewriter (#3262)	commit \| commitdiff \| tree
2019-09-11	Andrew Reynolds	Fix constructor type printing (#3246)	commit \| commitdiff \| tree
next

RSS Atom