projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Incorporate rewriting on demand in the evaluator (#3549)
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