projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Signature documentation update (#3476)
[cvc5.git]
/
test
/
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-18
Andrew Reynolds
Updates to the unit tests, api, and examples for dataty...
tree
|
commitdiff
2019-11-15
Andrew Reynolds
Fix wrong kind in sygus version 1 parser (#3463)
tree
|
commitdiff
2019-11-14
Alex Ozdemir
Use Shebang in cxxtestgen when appropriate (#3458)
tree
|
commitdiff
2019-11-13
Andres Noetzli
Allow (set-logic ...) after (reset) (#3457)
tree
|
commitdiff
2019-11-10
Andrew Reynolds
Fix bugs related to sygus higher-order + recursive...
tree
|
commitdiff
2019-11-06
Andres Noetzli
[Regressions] Remove leading whitespace in output ...
tree
|
commitdiff
2019-11-06
Andrew Reynolds
Support for SyGuS PBE + recursive functions (#3433)
tree
|
commitdiff
2019-11-05
Andres Noetzli
[Regressions] Support for running w/ default args ...
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Make getSynthSolution return a Bool (#3306)
tree
|
commitdiff
2019-11-01
Andrew Reynolds
Fix non-termination in datatype type enumerator (#3369)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-28
Andrew Reynolds
Fix for non-linear models (#3410)
tree
|
commitdiff
2019-10-28
Andres Noetzli
Fix integer division rewrite (#3415)
tree
|
commitdiff
2019-10-27
Andres Noetzli
Fix global-declarations support (#3403)
tree
|
commitdiff
2019-10-23
Andrew Reynolds
Fixes for SyGuS + regular expressions (#3313)
tree
|
commitdiff
2019-10-18
makaimann
Update overflow check to handle negative numbers (...
tree
|
commitdiff
2019-10-15
Andres Noetzli
Fix regression (#3393)
tree
|
commitdiff
2019-10-14
Andres Noetzli
Disable regression test for competition build (#3388)
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Remove benchmark (#3389)
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Support UF in default sygus grammars (#3319)
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Apply sygus repair constant techniques restricted to...
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Ensure lemmas from sygus repair const are guarded ...
tree
|
commitdiff
2019-10-13
Andrew Reynolds
Eliminate negative constant coefficients in div/mod...
tree
|
commitdiff
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
tree
|
commitdiff
2019-10-10
Mathias Preiner
test: Add TS_UTILS_EXPECT_ABORT macro for unit tests...
tree
|
commitdiff
2019-10-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
tree
|
commitdiff
2019-10-09
Aina Niemetz
New C++ API: Term: Add missing checks for null. (#3364)
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Fix method for getting arithmetic function definition...
tree
|
commitdiff
2019-10-08
Andres Noetzli
[CVC Parser] Add support for regular expressions (...
tree
|
commitdiff
2019-10-08
Andres Noetzli
Disallow --proof and --incremental (#3332)
tree
|
commitdiff
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
tree
|
commitdiff
2019-10-08
Aina Niemetz
New C++ API: Add Term::getId(). (#3360)
tree
|
commitdiff
2019-10-06
Andrew Reynolds
Fix typo in regression (#3359)
tree
|
commitdiff
2019-10-06
Andrew Reynolds
Fix str to int reduction (#3358)
tree
|
commitdiff
2019-10-03
yoni206
Disable proofs for unsupported logics (#3327)
tree
|
commitdiff
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
tree
|
commitdiff
2019-09-30
Andres Noetzli
Add rewrite for splitting equalities (#2957)
tree
|
commitdiff
2019-09-30
Andrew Reynolds
Avoid cases of empty sygus grammars (#3301)
tree
|
commitdiff
2019-09-29
Andrew Reynolds
Fail single invocation techniques when utility inferenc...
tree
|
commitdiff
2019-09-28
Andrew Reynolds
Support smt2 language "match" term (#3258)
tree
|
commitdiff
2019-09-27
Andrew Reynolds
Fix case of disjunctive conclusion in strings (#3254)
tree
|
commitdiff
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Fix off by one error in strings flat form explanation...
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Add isParameterized function to Expr (#3303)
tree
|
commitdiff
2019-09-25
Mathias Preiner
Use separate CMake project for CVC4 examples. (#3196)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
tree
|
commitdiff
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
tree
|
commitdiff
2019-09-19
makaimann
Add support for creating constant arrays to the new...
tree
|
commitdiff
2019-09-18
Andrew Reynolds
Decouple fmf-bound and finite-model-find (#3297)
tree
|
commitdiff
2019-09-17
Andrew Reynolds
Avoid computing cardinality when constructing models...
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Fix spurious meta-info in regression (#3294)
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Remove equality inference option for quantifiers (...
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Fix HO model construction for functions having Boolean...
tree
|
commitdiff
2019-09-13
Andrew Reynolds
Disallow let in sygus grammars, check for free variable...
tree
|
commitdiff
2019-09-12
Andrew Reynolds
Fix default grammar construction for arrays when no...
tree
|
commitdiff
2019-09-11
Andrew Reynolds
Fix constructor type printing (#3246)
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
tree
|
commitdiff
2019-09-04
Mathias Preiner
Remove duplicate regression tests. (#3227)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Infer emptiness instead of splitting when a string...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Exclude redundant lemmas when tracking inst lemmas...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Update dynamic splitting strategy for quantifiers ...
tree
|
commitdiff
2019-08-22
Andrew Reynolds
Local substitutions for context-depdendent simplificat...
tree
|
commitdiff
2019-08-20
Andrew Reynolds
Fixes for sygus inference on quantifier free problems...
tree
|
commitdiff
2019-08-19
Aina Niemetz
New C++ API: Add checks for Solver::checkValid and...
tree
|
commitdiff
2019-08-18
Andrew Reynolds
Context-independent regular expression unfolding (...
tree
|
commitdiff
2019-08-14
Andrew Reynolds
Update to standard implementation of getting free...
tree
|
commitdiff
2019-08-13
Aina Niemetz
New C++ API: Add checks and tests for Solver::simplify...
tree
|
commitdiff
2019-08-13
Aina Niemetz
New C++ API: Fix test names of solver_black unit test...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Add string rewrite involving allchar stars (#3167)
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Properly implement logic info for separation logic...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Implement check abduct feature (#3152)
tree
|
commitdiff
2019-08-11
makaimann
New C++ API: Add templated getIndices method for OpTerm...
tree
|
commitdiff
2019-08-08
Mathias Preiner
Fix issues with Ninja build system and add configure...
tree
|
commitdiff
2019-08-07
Aina Niemetz
New C++ API: Add checks and tests for push/pop. (#3121)
tree
|
commitdiff
2019-08-06
Andrew Reynolds
Properly parse qualified identifiers (#3111)
tree
|
commitdiff
2019-08-04
Mathias Preiner
Fix regression script for incremental SMT-LIB v2 benchm...
tree
|
commitdiff
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Flip the polarity of the argument of get-abduct (#3153)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Remove simplification specialized for sygus si solution...
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Support default sygus grammar for strings (#3148)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Fix solution filtering for streaming abducts (#3143)
tree
|
commitdiff
2019-08-02
Mathias Preiner
Fix BVGauss unit tests. (#3142)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Enable sygus logic when produce-abducts is true (#3144)
tree
|
commitdiff
2019-08-01
Andrew Reynolds
Regular expression intersection modes (#3134)
tree
|
commitdiff
2019-07-31
Haniel Barbosa
Parsing THF and adding several regressions (#3131)
tree
|
commitdiff
2019-07-31
yoni206
adding bv_gauss unit test to build files (#3135)
tree
|
commitdiff
2019-07-30
Andrew Reynolds
Minor improvement for rewriter for str.replace (#3124)
tree
|
commitdiff
2019-07-30
Andrew Reynolds
Handle RE intersections modulo equality (#3120)
tree
|
commitdiff
2019-07-30
Haniel Barbosa
Remove hard coded option for TPTP regressions in run_re...
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Model blocker feature (#3112)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
tree
|
commitdiff
2019-07-24
Andrew Reynolds
Fix null node when using no-strings-lazy-pp (#3114)
tree
|
commitdiff
2019-07-23
Andrew Reynolds
Fix sygus datatype parsing in sygus v1 format (#3113)
tree
|
commitdiff
2019-07-23
yoni206
Get operators in node (#3094)
tree
|
commitdiff
2019-07-19
Andrew Reynolds
Fixes for sygus with datatypes (#3103)
tree
|
commitdiff
next