projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2019-01-04
Alex Ozdemir
[LRAT] A C++ data structure for LRAT. (#2737)
commit
|
commitdiff
|
tree
2019-01-04
Aina Niemetz
New C++ API: Add missing catch blocks for std::invalid_...
commit
|
commitdiff
|
tree
2019-01-03
Andres Noetzli
API/Smt2 parser: refactor termAtomic (#2674)
commit
|
commitdiff
|
tree
2019-01-03
Andres Noetzli
C++ API: Reintroduce zero-value mkBitVector method...
commit
|
commitdiff
|
tree
2019-01-03
Alex Ozdemir
[LRA proof] Recording & Printing LRA Proofs (#2758)
commit
|
commitdiff
|
tree
2019-01-03
Aina Niemetz
New C++ API: Add tests for mk-functions in solver objec...
commit
|
commitdiff
|
tree
2018-12-20
Aina Niemetz
Clean up BV kinds and type rules. (#2766)
commit
|
commitdiff
|
tree
2018-12-20
Aina Niemetz
Add missing type rules for parameterized operator kinds...
commit
|
commitdiff
|
tree
2018-12-19
Andrew Reynolds
Fix issues with REWRITE_DONE in floating point rewriter...
commit
|
commitdiff
|
tree
2018-12-18
Aina Niemetz
Remove noop. (#2763)
commit
|
commitdiff
|
tree
2018-12-17
Alex Ozdemir
Configured for linking against drat2er (#2754)
commit
|
commitdiff
|
tree
2018-12-17
Aina Niemetz
New C++ API: Add tests for term object. (#2755)
commit
|
commitdiff
|
tree
2018-12-17
Alex Ozdemir
DRAT Signature (#2757)
commit
|
commitdiff
|
tree
2018-12-15
Andres Noetzli
Revert "Move ss-combine rewrite to extended rewriter...
commit
|
commitdiff
|
tree
2018-12-15
Alex Ozdemir
[LRA Proof] Storage for LRA proofs (#2747)
commit
|
commitdiff
|
tree
2018-12-14
Aina Niemetz
Fixed typos.
commit
|
commitdiff
|
tree
2018-12-14
Aina Niemetz
New C++ API: Add tests for opterm object. (#2756)
commit
|
commitdiff
|
tree
2018-12-14
Andrew Reynolds
Fix extended rewriter for binary associative operators...
commit
|
commitdiff
|
tree
2018-12-14
Andrew Reynolds
Make single invocation and invariant pre/post condition...
commit
|
commitdiff
|
tree
2018-12-13
Aina Niemetz
New C++ API: Add tests for sort functions of solver...
commit
|
commitdiff
|
tree
2018-12-13
Andrew Reynolds
Remove spurious map (#2750)
commit
|
commitdiff
|
tree
2018-12-13
Aina Niemetz
Fix compiler warnings. (#2748)
commit
|
commitdiff
|
tree
2018-12-12
Andres Noetzli
API: Add simple empty/sigma regexp unit tests (#2746)
commit
|
commitdiff
|
tree
2018-12-12
Alex Ozdemir
[LRA proof] More complete LRA example proofs. (#2722)
commit
|
commitdiff
|
tree
2018-12-12
Alex Ozdemir
[LRAT] signature robust against duplicate literals...
commit
|
commitdiff
|
tree
2018-12-11
Andrew Reynolds
Remove alternate versions of mbqi (#2742)
commit
|
commitdiff
|
tree
2018-12-11
Alex Ozdemir
LRAT signature (#2731)
commit
|
commitdiff
|
tree
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
commit
|
commitdiff
|
tree
2018-12-07
Andres Noetzli
Strings: Make EXTF_d inference more conservative (...
commit
|
commitdiff
|
tree
2018-12-07
Alex Ozdemir
Arith Constraint Proof Loggin (#2732)
commit
|
commitdiff
|
tree
2018-12-07
Alex Ozdemir
Enable BV proofs when using an eager bitblaster (#2733)
commit
|
commitdiff
|
tree
2018-12-06
Andres Noetzli
Fix use-after-free due to destruction order (#2739)
commit
|
commitdiff
|
tree
2018-12-06
Andrew Reynolds
Take into account minimality and types for cached...
commit
|
commitdiff
|
tree
2018-12-04
Andrew Reynolds
Apply extended rewriting on PBE static symmetry breakin...
commit
|
commitdiff
|
tree
2018-12-04
Andrew Reynolds
Enable regular expression elimination by default. ...
commit
|
commitdiff
|
tree
2018-12-03
Andrew Reynolds
Skip non-cardinality types in sets min card inference...
commit
|
commitdiff
|
tree
2018-12-03
Alex Ozdemir
Bit vector proof superclass (#2599)
commit
|
commitdiff
|
tree
2018-12-02
Andrew Reynolds
Optimizations for PBE strings (#2728)
commit
|
commitdiff
|
tree
2018-11-29
Andrew Reynolds
Infrastructure for sygus side conditions (#2729)
commit
|
commitdiff
|
tree
2018-11-29
Andrew Reynolds
Combine sygus stream with PBE (#2726)
commit
|
commitdiff
|
tree
2018-11-28
Andrew Reynolds
Improve interface for sygus grammar cons (#2727)
commit
|
commitdiff
|
tree
2018-11-28
Andrew Reynolds
Information gain heuristic for PBE (#2719)
commit
|
commitdiff
|
tree
2018-11-28
Andrew Reynolds
Optimize re-elim for re.allchar components (#2725)
commit
|
commitdiff
|
tree
2018-11-28
Andres Noetzli
Improve skolem caching by normalizing skolem args ...
commit
|
commitdiff
|
tree
2018-11-28
Andrew Reynolds
Generalize sygus stream solution filtering to logical...
commit
|
commitdiff
|
tree
2018-11-28
Andrew Reynolds
Improve cegqi engine trace. (#2714)
commit
|
commitdiff
|
tree
2018-11-27
Andrew Reynolds
Make (T)NodeTrie a general utility (#2489)
commit
|
commitdiff
|
tree
2018-11-27
Andrew Reynolds
Fix coverity warnings in datatypes (#2553)
commit
|
commitdiff
|
tree
2018-11-27
Andrew Reynolds
Lazy model construction in TheoryEngine (#2633)
commit
|
commitdiff
|
tree
2018-11-27
Andres Noetzli
Reduce lookahead when parsing string literals (#2721)
commit
|
commitdiff
|
tree
2018-11-27
Alex Ozdemir
LRA proof signature fixes and a first proof for linear...
commit
|
commitdiff
|
tree
2018-11-23
Tom Smeding
Use https for antlr3.org downloads (#2701)
commit
|
commitdiff
|
tree
2018-11-22
Andres Noetzli
Move ss-combine rewrite to extended rewriter (#2703)
commit
|
commitdiff
|
tree
2018-11-22
Andres Noetzli
Add rewrite for (str.substr s x y) --> "" (#2695)
commit
|
commitdiff
|
tree
2018-11-21
Andrew Reynolds
Cache evaluations for PBE (#2699)
commit
|
commitdiff
|
tree
2018-11-21
Andrew Reynolds
Quickly recognize when PBE conjectures are infeasible...
commit
|
commitdiff
|
tree
2018-11-21
Martin
Obvious rewrites to floating-point < and <=. (#2706)
commit
|
commitdiff
|
tree
2018-11-21
Andrew Reynolds
Support string replace all (#2704)
commit
|
commitdiff
|
tree
2018-11-21
Andrew Reynolds
Fix type enumerator for FP (#2717)
commit
|
commitdiff
|
tree
2018-11-20
Andrew Reynolds
Fix real2int regression. (#2716)
commit
|
commitdiff
|
tree
2018-11-20
Alex Ozdemir
Change lemma proof step storage & iterators (#2712)
commit
|
commitdiff
|
tree
2018-11-20
Andrew Reynolds
Clausify context-dependent simplifications in ext...
commit
|
commitdiff
|
tree
2018-11-19
Andrew Reynolds
Fix E-matching for case where candidate generator is...
commit
|
commitdiff
|
tree
2018-11-15
Andrew Reynolds
Expand definitions prior to model core computation...
commit
|
commitdiff
|
tree
2018-11-14
Mathias Preiner
cmake: Require boost 1.50.0 for examples. (#2710)
commit
|
commitdiff
|
tree
2018-11-08
Mathias Preiner
cmake: Add option to explicitely enable/disable static...
commit
|
commitdiff
|
tree
2018-11-08
Andres Noetzli
Evaluator: add support for str.code (#2696)
commit
|
commitdiff
|
tree
2018-11-07
Haniel Barbosa
Adding default SyGuS grammar construction for arrays...
commit
|
commitdiff
|
tree
2018-11-07
Andres Noetzli
Fix collectEmptyEqs in string rewriter (#2692)
commit
|
commitdiff
|
tree
2018-11-07
Andrew Reynolds
Fix for itos reduction (#2691)
commit
|
commitdiff
|
tree
2018-11-06
Andrew Reynolds
Incorporate static PBE symmetry breaking lemmas into...
commit
|
commitdiff
|
tree
2018-11-05
Andrew Reynolds
Change default sygus enumeration mode to auto (#2689)
commit
|
commitdiff
|
tree
2018-11-05
Andrew Reynolds
Fix coverity warnings in sygus enumerator (#2687)
commit
|
commitdiff
|
tree
2018-11-05
Aina Niemetz
New C++ API: Split unit tests. (#2688)
commit
|
commitdiff
|
tree
2018-11-05
yoni206
Increasing coverage (#2683)
commit
|
commitdiff
|
tree
2018-11-05
Andres Noetzli
API: Fix assignment operators (#2680)
commit
|
commitdiff
|
tree
2018-11-05
Andres Noetzli
configure.sh: Fix option parsing to match --help (...
commit
|
commitdiff
|
tree
2018-11-05
Andrew Reynolds
Allow partial models with optimized sygus enumeration...
commit
|
commitdiff
|
tree
2018-11-05
Andrew Reynolds
Implement option to turn off symmetry breaking for...
commit
|
commitdiff
|
tree
2018-11-03
Haniel Barbosa
Refactor default grammars construction (#2681)
commit
|
commitdiff
|
tree
2018-11-02
yoni206
fixes to regression docs (#2679)
commit
|
commitdiff
|
tree
2018-10-31
Andrew Reynolds
Add optimized sygus enumeration (#2677)
commit
|
commitdiff
|
tree
2018-10-31
Andres Noetzli
Record assumption info in AssertionPipeline (#2678)
commit
|
commitdiff
|
tree
2018-10-24
Andrew Reynolds
Minor improvement to sygus trace (#2675)
commit
|
commitdiff
|
tree
2018-10-24
Andres Noetzli
CMake: Set RPATH on installed binary (#2671)
commit
|
commitdiff
|
tree
2018-10-23
Andrew Reynolds
Do not use lazy trie for sygus-rr-verify (#2668)
commit
|
commitdiff
|
tree
2018-10-22
makaimann
Fail for SWIG 3.0.8 (#2656)
commit
|
commitdiff
|
tree
2018-10-22
Andres Noetzli
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
commit
|
commitdiff
|
tree
2018-10-22
Andres Noetzli
Only build CryptoMiniSat library, no binary (#2657)
commit
|
commitdiff
|
tree
2018-10-22
Andres Noetzli
Recover from wrong use of get-info :reason-unknown...
commit
|
commitdiff
|
tree
2018-10-20
Mathias Preiner
Remove antlr_undefines.h. (#2664)
commit
|
commitdiff
|
tree
2018-10-20
Andres Noetzli
Add substr, contains and equality rewrites (#2665)
commit
|
commitdiff
|
tree
2018-10-20
Andres Noetzli
Disable dumping test for non-dumping builds (#2662)
commit
|
commitdiff
|
tree
2018-10-20
Andres Noetzli
Travis: run examples and avoid building them twice...
commit
|
commitdiff
|
tree
2018-10-20
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp with special...
commit
|
commitdiff
|
tree
2018-10-20
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X...
commit
|
commitdiff
|
tree
2018-10-20
Andrew Reynolds
Sygus streaming non-implied predicates (#2660)
commit
|
commitdiff
|
tree
2018-10-19
Mathias Preiner
Remove autotools build system. (#2639)
commit
|
commitdiff
|
tree
2018-10-19
Andres Noetzli
Fix util::Random for macOS builds (#2655)
commit
|
commitdiff
|
tree
2018-10-19
Andres Noetzli
Add helper to detect length one string terms (#2654)
commit
|
commitdiff
|
tree
next