projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2019-01-15
Andrew Reynolds
Only check disequal terms with sygus-rr-verify (#2793)
commit
|
commitdiff
|
tree
2019-01-14
Alex Ozdemir
ClausalBitvectorProof (#2786)
commit
|
commitdiff
|
tree
2019-01-13
Alex Ozdemir
LFSC LRAT Output (#2787)
commit
|
commitdiff
|
tree
2019-01-12
Alex Ozdemir
LratInstruction inheritance (#2784)
commit
|
commitdiff
|
tree
2019-01-11
Alex Ozdemir
Fixed linking against drat2er, and use drat2er (#2785)
commit
|
commitdiff
|
tree
2019-01-11
Aina Niemetz
New C++ API: Add unit tests for setInfo, setLogic,...
commit
|
commitdiff
|
tree
2019-01-10
Aina Niemetz
New C++ API: Get rid of mkConst functions (simplify...
commit
|
commitdiff
|
tree
2019-01-09
Andrew Reynolds
Do not rewrite 1-constructor sygus testers to true...
commit
|
commitdiff
|
tree
2019-01-09
Alex Ozdemir
[BV Proofs] Option for proof format (#2777)
commit
|
commitdiff
|
tree
2019-01-09
Alex Ozdemir
Clause proof printing (#2779)
commit
|
commitdiff
|
tree
2019-01-09
Alex Ozdemir
LFSC drat output (#2776)
commit
|
commitdiff
|
tree
2019-01-07
Aina Niemetz
New C++ API: Add missing getType() calls to kick off...
commit
|
commitdiff
|
tree
2019-01-06
Alex Ozdemir
[DRAT] DRAT data structure (#2767)
commit
|
commitdiff
|
tree
2019-01-05
Mathias Preiner
cmake: Disable unit tests for static builds. (#2775)
commit
|
commitdiff
|
tree
2019-01-04
Andres Noetzli
C++ API: Fix OOB read in unit test (#2774)
commit
|
commitdiff
|
tree
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
next