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

2019-12-10	Andrew Reynolds	Incorporate rewriting on demand in the evaluator (...	commit \| commitdiff \| tree
2019-12-10	Andrew Reynolds	Allow unsat cores with sygus inference (#3550)	commit \| commitdiff \| tree
2019-12-09	Andrew Reynolds	Disable sygus inference when combined with incremental...	commit \| commitdiff \| tree
2019-12-09	Andres Noetzli	Make theory rewriters non-static (#3547)	commit \| commitdiff \| tree
2019-12-07	Andres Noetzli	Use str.subtr in str.to.int/int.to.str reduction (...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Throw exception instead of warning for approximate...	commit \| commitdiff \| tree
2019-12-06	Andres Noetzli	Add lemma for str.to.int/int.to.str (#3541)	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	New algorithm for interpolation and abduction based...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Add ExprManager as argument to Datatype (#3535)	commit \| commitdiff \| tree
2019-12-06	Alex Ozdemir	[proof] Eliminate side-condition from ER signature...	commit \| commitdiff \| tree
2019-12-05	Andrew Reynolds	Make nonlinear solver intercept model assignments from...	commit \| commitdiff \| tree
2019-12-05	Andrew Reynolds	Refactor mode options for Unif+PI (#3531)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	New grammar construction modes for SyGuS (#3486)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fix (#3530)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fixes for SyGuS PBE + templated string concatenations...	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fix single invocation solution construction for multiple...	commit \| commitdiff \| tree
2019-12-04	Andres Noetzli	Fix corner case in model construction of strings (...	commit \| commitdiff \| tree
2019-12-03	Andrew Reynolds	Improve flexibility of lemma output in non-linear solver...	commit \| commitdiff \| tree
2019-12-03	Aina Niemetz	Fix clang-format file for brace wrapping with case...	commit \| commitdiff \| tree
2019-12-03	makaimann	Minor refactor: rename opterm_black to op_black (#3521)	commit \| commitdiff \| tree
2019-12-02	makaimann	OpTerm Refactor: Allow retrieving OpTerm used to create...	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Update ownership policy for dynamic quantifiers splitting...	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Fix case of higher-order + sygus inference (#3509)	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Ensure quantifiers options are set with --no-strings...	commit \| commitdiff \| tree
2019-11-30	Andrew Reynolds	Fix fast SyGuS enumeration for interpreted constants...	commit \| commitdiff \| tree
2019-11-29	Andrew Reynolds	Check free variables in assertions when using SyGuS...	commit \| commitdiff \| tree
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-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-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-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
next

RSS Atom