projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
[cvc5.git]
/
src
/
2019-01-10
Aina Niemetz
New C++ API: Get rid of mkConst functions (simplify...
tree
|
commitdiff
2019-01-09
Andrew Reynolds
Do not rewrite 1-constructor sygus testers to true...
tree
|
commitdiff
2019-01-09
Alex Ozdemir
[BV Proofs] Option for proof format (#2777)
tree
|
commitdiff
2019-01-09
Alex Ozdemir
Clause proof printing (#2779)
tree
|
commitdiff
2019-01-09
Alex Ozdemir
LFSC drat output (#2776)
tree
|
commitdiff
2019-01-07
Aina Niemetz
New C++ API: Add missing getType() calls to kick off...
tree
|
commitdiff
2019-01-06
Alex Ozdemir
[DRAT] DRAT data structure (#2767)
tree
|
commitdiff
2019-01-04
Alex Ozdemir
[LRAT] A C++ data structure for LRAT. (#2737)
tree
|
commitdiff
2019-01-04
Aina Niemetz
New C++ API: Add missing catch blocks for std::invalid_...
tree
|
commitdiff
2019-01-03
Andres Noetzli
API/Smt2 parser: refactor termAtomic (#2674)
tree
|
commitdiff
2019-01-03
Andres Noetzli
C++ API: Reintroduce zero-value mkBitVector method...
tree
|
commitdiff
2019-01-03
Alex Ozdemir
[LRA proof] Recording & Printing LRA Proofs (#2758)
tree
|
commitdiff
2019-01-03
Aina Niemetz
New C++ API: Add tests for mk-functions in solver objec...
tree
|
commitdiff
2018-12-20
Aina Niemetz
Clean up BV kinds and type rules. (#2766)
tree
|
commitdiff
2018-12-20
Aina Niemetz
Add missing type rules for parameterized operator kinds...
tree
|
commitdiff
2018-12-19
Andrew Reynolds
Fix issues with REWRITE_DONE in floating point rewriter...
tree
|
commitdiff
2018-12-18
Aina Niemetz
Remove noop. (#2763)
tree
|
commitdiff
2018-12-17
Alex Ozdemir
Configured for linking against drat2er (#2754)
tree
|
commitdiff
2018-12-17
Aina Niemetz
New C++ API: Add tests for term object. (#2755)
tree
|
commitdiff
2018-12-15
Andres Noetzli
Revert "Move ss-combine rewrite to extended rewriter...
tree
|
commitdiff
2018-12-15
Alex Ozdemir
[LRA Proof] Storage for LRA proofs (#2747)
tree
|
commitdiff
2018-12-14
Aina Niemetz
Fixed typos.
tree
|
commitdiff
2018-12-14
Aina Niemetz
New C++ API: Add tests for opterm object. (#2756)
tree
|
commitdiff
2018-12-14
Andrew Reynolds
Fix extended rewriter for binary associative operators...
tree
|
commitdiff
2018-12-14
Andrew Reynolds
Make single invocation and invariant pre/post condition...
tree
|
commitdiff
2018-12-13
Aina Niemetz
New C++ API: Add tests for sort functions of solver...
tree
|
commitdiff
2018-12-13
Andrew Reynolds
Remove spurious map (#2750)
tree
|
commitdiff
2018-12-13
Aina Niemetz
Fix compiler warnings. (#2748)
tree
|
commitdiff
2018-12-11
Andrew Reynolds
Remove alternate versions of mbqi (#2742)
tree
|
commitdiff
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
tree
|
commitdiff
2018-12-07
Andres Noetzli
Strings: Make EXTF_d inference more conservative (...
tree
|
commitdiff
2018-12-07
Alex Ozdemir
Arith Constraint Proof Loggin (#2732)
tree
|
commitdiff
2018-12-07
Alex Ozdemir
Enable BV proofs when using an eager bitblaster (#2733)
tree
|
commitdiff
2018-12-06
Andres Noetzli
Fix use-after-free due to destruction order (#2739)
tree
|
commitdiff
2018-12-06
Andrew Reynolds
Take into account minimality and types for cached...
tree
|
commitdiff
2018-12-04
Andrew Reynolds
Apply extended rewriting on PBE static symmetry breakin...
tree
|
commitdiff
2018-12-04
Andrew Reynolds
Enable regular expression elimination by default. ...
tree
|
commitdiff
2018-12-03
Andrew Reynolds
Skip non-cardinality types in sets min card inference...
tree
|
commitdiff
2018-12-03
Alex Ozdemir
Bit vector proof superclass (#2599)
tree
|
commitdiff
2018-12-02
Andrew Reynolds
Optimizations for PBE strings (#2728)
tree
|
commitdiff
2018-11-29
Andrew Reynolds
Infrastructure for sygus side conditions (#2729)
tree
|
commitdiff
2018-11-29
Andrew Reynolds
Combine sygus stream with PBE (#2726)
tree
|
commitdiff
2018-11-28
Andrew Reynolds
Improve interface for sygus grammar cons (#2727)
tree
|
commitdiff
2018-11-28
Andrew Reynolds
Information gain heuristic for PBE (#2719)
tree
|
commitdiff
2018-11-28
Andrew Reynolds
Optimize re-elim for re.allchar components (#2725)
tree
|
commitdiff
2018-11-28
Andres Noetzli
Improve skolem caching by normalizing skolem args ...
tree
|
commitdiff
2018-11-28
Andrew Reynolds
Generalize sygus stream solution filtering to logical...
tree
|
commitdiff
2018-11-28
Andrew Reynolds
Improve cegqi engine trace. (#2714)
tree
|
commitdiff
2018-11-27
Andrew Reynolds
Make (T)NodeTrie a general utility (#2489)
tree
|
commitdiff
2018-11-27
Andrew Reynolds
Fix coverity warnings in datatypes (#2553)
tree
|
commitdiff
2018-11-27
Andrew Reynolds
Lazy model construction in TheoryEngine (#2633)
tree
|
commitdiff
2018-11-27
Andres Noetzli
Reduce lookahead when parsing string literals (#2721)
tree
|
commitdiff
2018-11-22
Andres Noetzli
Move ss-combine rewrite to extended rewriter (#2703)
tree
|
commitdiff
2018-11-22
Andres Noetzli
Add rewrite for (str.substr s x y) --> "" (#2695)
tree
|
commitdiff
2018-11-21
Andrew Reynolds
Cache evaluations for PBE (#2699)
tree
|
commitdiff
2018-11-21
Andrew Reynolds
Quickly recognize when PBE conjectures are infeasible...
tree
|
commitdiff
2018-11-21
Martin
Obvious rewrites to floating-point < and <=. (#2706)
tree
|
commitdiff
2018-11-21
Andrew Reynolds
Support string replace all (#2704)
tree
|
commitdiff
2018-11-21
Andrew Reynolds
Fix type enumerator for FP (#2717)
tree
|
commitdiff
2018-11-20
Alex Ozdemir
Change lemma proof step storage & iterators (#2712)
tree
|
commitdiff
2018-11-20
Andrew Reynolds
Clausify context-dependent simplifications in ext...
tree
|
commitdiff
2018-11-19
Andrew Reynolds
Fix E-matching for case where candidate generator is...
tree
|
commitdiff
2018-11-15
Andrew Reynolds
Expand definitions prior to model core computation...
tree
|
commitdiff
2018-11-08
Mathias Preiner
cmake: Add option to explicitely enable/disable static...
tree
|
commitdiff
2018-11-08
Andres Noetzli
Evaluator: add support for str.code (#2696)
tree
|
commitdiff
2018-11-07
Haniel Barbosa
Adding default SyGuS grammar construction for arrays...
tree
|
commitdiff
2018-11-07
Andres Noetzli
Fix collectEmptyEqs in string rewriter (#2692)
tree
|
commitdiff
2018-11-07
Andrew Reynolds
Fix for itos reduction (#2691)
tree
|
commitdiff
2018-11-06
Andrew Reynolds
Incorporate static PBE symmetry breaking lemmas into...
tree
|
commitdiff
2018-11-05
Andrew Reynolds
Change default sygus enumeration mode to auto (#2689)
tree
|
commitdiff
2018-11-05
Andrew Reynolds
Fix coverity warnings in sygus enumerator (#2687)
tree
|
commitdiff
2018-11-05
Andres Noetzli
API: Fix assignment operators (#2680)
tree
|
commitdiff
2018-11-05
Andrew Reynolds
Allow partial models with optimized sygus enumeration...
tree
|
commitdiff
2018-11-05
Andrew Reynolds
Implement option to turn off symmetry breaking for...
tree
|
commitdiff
2018-11-03
Haniel Barbosa
Refactor default grammars construction (#2681)
tree
|
commitdiff
2018-10-31
Andrew Reynolds
Add optimized sygus enumeration (#2677)
tree
|
commitdiff
2018-10-31
Andres Noetzli
Record assumption info in AssertionPipeline (#2678)
tree
|
commitdiff
2018-10-24
Andrew Reynolds
Minor improvement to sygus trace (#2675)
tree
|
commitdiff
2018-10-23
Andrew Reynolds
Do not use lazy trie for sygus-rr-verify (#2668)
tree
|
commitdiff
2018-10-22
makaimann
Fail for SWIG 3.0.8 (#2656)
tree
|
commitdiff
2018-10-22
Andres Noetzli
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
tree
|
commitdiff
2018-10-22
Andres Noetzli
Recover from wrong use of get-info :reason-unknown...
tree
|
commitdiff
2018-10-20
Mathias Preiner
Remove antlr_undefines.h. (#2664)
tree
|
commitdiff
2018-10-20
Andres Noetzli
Add substr, contains and equality rewrites (#2665)
tree
|
commitdiff
2018-10-20
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp with special...
tree
|
commitdiff
2018-10-20
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X...
tree
|
commitdiff
2018-10-20
Andrew Reynolds
Sygus streaming non-implied predicates (#2660)
tree
|
commitdiff
2018-10-19
Mathias Preiner
Remove autotools build system. (#2639)
tree
|
commitdiff
2018-10-19
Andres Noetzli
Fix util::Random for macOS builds (#2655)
tree
|
commitdiff
2018-10-19
Andres Noetzli
Add helper to detect length one string terms (#2654)
tree
|
commitdiff
2018-10-19
Andres Noetzli
Add OptionException handling during initialization...
tree
|
commitdiff
2018-10-19
Andrew Reynolds
Non-implied mode for model cores (#2653)
tree
|
commitdiff
2018-10-18
Andrew Reynolds
Non-contributing find replace rewrite (#2652)
tree
|
commitdiff
2018-10-18
Andrew Reynolds
Improve reduction for str.to.int (#2636)
tree
|
commitdiff
2018-10-18
Haniel Barbosa
Introducing internal commands for SyGuS commands (...
tree
|
commitdiff
2018-10-18
Andrew Reynolds
Constant length regular expression elimination (#2646)
tree
|
commitdiff
2018-10-18
Andres Noetzli
Show if ASAN build in --show-config (#2650)
tree
|
commitdiff
2018-10-18
Andrew Reynolds
Sygus query generator (#2465)
tree
|
commitdiff
2018-10-17
Andrew Reynolds
Fix context-dependent for positive contains reduction...
tree
|
commitdiff
2018-10-17
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O...
tree
|
commitdiff
next