projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-05-19
Andrew Reynolds
Minor deleting of unused code (#8800)
commit
|
commitdiff
|
tree
2022-05-19
Andrew Reynolds
Add options and regressions to increase coverage (...
commit
|
commitdiff
|
tree
2022-05-18
Andrew Reynolds
Basic cleanup of sep theory (#8790)
commit
|
commitdiff
|
tree
2022-05-18
Andrew Reynolds
Make skolem definition manager robust to definitions...
commit
|
commitdiff
|
tree
2022-05-18
Andrew Reynolds
Eliminate subtypes (#8783)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Refactor declare oracle command (#8742)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Minor cleanup of datatypes theory (#8791)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Fix LFSC proof construction for concat clash of sequenc...
commit
|
commitdiff
|
tree
2022-05-17
Mathias Preiner
docs: Remove references to checkEntailed(). (#8789)
commit
|
commitdiff
|
tree
2022-05-17
Andrew Reynolds
Generalize pto constraint tracking for multiple heaps...
commit
|
commitdiff
|
tree
2022-05-17
Ying Sheng
Add getInterpolant with a grammar in the unit test...
commit
|
commitdiff
|
tree
2022-05-17
yoni206
new test for resolved issue (#8784)
commit
|
commitdiff
|
tree
2022-05-16
Andrew Reynolds
Last remaining fixes for eliminating subtyping (#8772)
commit
|
commitdiff
|
tree
2022-05-16
Haniel Barbosa
[proofs] Generalize handling of constants merged in...
commit
|
commitdiff
|
tree
2022-05-16
Haniel Barbosa
Rename equality engine trace to print E-graph (#8780)
commit
|
commitdiff
|
tree
2022-05-15
Andrew Reynolds
Eliminate the use of CAST_TO_REAL (#8759)
commit
|
commitdiff
|
tree
2022-05-15
Andrew Reynolds
Eliminate ops for parameterized type constructors ...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Make arith substitute its own utility (#8765)
commit
|
commitdiff
|
tree
2022-05-13
Amalee Wilson
Add heap-trail partitioning strategy, checks between...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Fixes and improvement for IAND solver (#8771)
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Eliminate use of getBaseType (#8764)
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Add utilities in preparation for supporting str.nth...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Fix debug failures in LFSC proofs due to curried arithm...
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Refactor logic exceptions during preregistration for...
commit
|
commitdiff
|
tree
2022-05-13
Gereon Kremer
Update CoCoALib version (#8757)
commit
|
commitdiff
|
tree
2022-05-13
Andrew Reynolds
Minor refactoring for sep theory (#8753)
commit
|
commitdiff
|
tree
2022-05-12
Andrew Reynolds
Fix type of null terminator for ADD/MULT for LFSC ...
commit
|
commitdiff
|
tree
2022-05-12
Andrew Reynolds
Eliminate use of subtypes from remainder of type rules...
commit
|
commitdiff
|
tree
2022-05-12
Andrew Reynolds
Preserve types in rewriter and make core type rules...
commit
|
commitdiff
|
tree
2022-05-12
Haniel Barbosa
[docs] Marking internal comment in proofs docs (#8747)
commit
|
commitdiff
|
tree
2022-05-12
Gereon Kremer
Make regular options access const (#8754)
commit
|
commitdiff
|
tree
2022-05-11
Gereon Kremer
Remove --build from GMP configure line (#8752)
commit
|
commitdiff
|
tree
2022-05-11
Andrew Reynolds
Relax an assertion in the evaluator (#8751)
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Ensure substitutions in nonlinear solver are properly...
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Fix some issues with the Python API tests (#8746)
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Add test coverage for almost everything from the Java...
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Compress debug symbols to make libcvc5 smaller (#8743)
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Improvements for evaluation in model (#8738)
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Do not depend on subtyping for APPLY_UF in TPTP parser...
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Add unit tests for getInstantiations (#8741)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
Do not rely on subtyping in real-to-int preprocessing...
commit
|
commitdiff
|
tree
2022-05-07
Abdalrhman...
Disable proof testers for delicate regressions. (#8735)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
More preparation for strict type rules (#8733)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
Fix proofs for ppAssert for theory Bool (#8708)
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Fallback for sequential substitution proof reconstructi...
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Eliminate arithmetic subtyping for (dis)equalities...
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Separate ill-typed portion of arith models (#8734)
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Fix LFSC side condition for matching premise of concat_...
commit
|
commitdiff
|
tree
2022-05-05
Gereon Kremer
Add test coverage for almost everything from the Python...
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Preparation for making equality strictly typed (#8728)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Fix cache in learned rewrite preprocessing pass (#8725)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Fix more issues with subtypes in regressions (#8727)
commit
|
commitdiff
|
tree
2022-05-05
mudathirmahgoub
Add operators table.aggr and table.join (#8681)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Use purification for set comprehension reduction (...
commit
|
commitdiff
|
tree
2022-05-04
Andres Noetzli
Improve finding Python library/includes (#8718)
commit
|
commitdiff
|
tree
2022-05-04
yoni206
fix link to `Testing cvc5` in `INSTALL.md` (#8675)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Make equality solver the entry point for all equality...
commit
|
commitdiff
|
tree
2022-05-04
Gereon Kremer
Make printStatisticsSafe public (#8721)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Add declareOracleFun interface to SolverEngine (#8622)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Refactor oracles using new std::function backend (...
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Remove unecessary calls to equality engine from congrue...
commit
|
commitdiff
|
tree
2022-05-04
Gereon Kremer
Remove obsolete private methods from API (#8716)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Fix rewrite for to_real in division by zero (#8714)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Add support for oracle constant nodes (#8707)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Fix LFSC node converter for 0-ary tuples (#8706)
commit
|
commitdiff
|
tree
2022-05-03
Andres Noetzli
Update LFSC version (#8713)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Use (non-recursive) unpurified form instead of original...
commit
|
commitdiff
|
tree
2022-05-03
Aina Niemetz
docs: Some fixes in options docs. (#8710)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Change option name for mbqi in fmf (#8701)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Simplify representation of datatypes at the TypeNode...
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Final preparation for CONST_INTEGER (#8700)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Migrate basic EqualityEngine management from Congruence...
commit
|
commitdiff
|
tree
2022-05-02
Amalee Wilson
Add strict-cube and decision-trail partitioning strateg...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
More robust treatment of flattening in arith rewriter...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
Make arith msum utility agnostic to Int (#8694)
commit
|
commitdiff
|
tree
2022-05-02
Gereon Kremer
Add missing tests for some corners of the API (#8688)
commit
|
commitdiff
|
tree
2022-05-02
Aina Niemetz
docs: Do not use explicit line numbers in literalinclud...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
Further refactoring in preparation for CONST_INTEGER...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
Fix tuple printing in LFSC (#8696)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Properly represent Tuples in the TypeNode AST (#8648)
commit
|
commitdiff
|
tree
2022-04-29
Andres Noetzli
Add simple type rule for real-or-int arguments (#8685)
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Towards proper usage of TO_REAL (#8680)
commit
|
commitdiff
|
tree
2022-04-29
Andres Noetzli
Document non-standard string operators (#8679)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Ensure mkConstInt is used on integral rationals only...
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Refactor interfaces for E-matching (#8665)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Make extended rewriter use standard Subs utility (...
commit
|
commitdiff
|
tree
2022-04-29
Abdalrhman...
Add an option to enable all testers. (#8676)
commit
|
commitdiff
|
tree
2022-04-29
yoni206
Add missing parenthesis for bags documentation (#8673)
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Add unit test for code not exposed by java API (#8678)
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Add unit test for code not exposed by python API (...
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Add some missing API tests (#8669)
commit
|
commitdiff
|
tree
2022-04-28
Gereon Kremer
Move tests around (#8670)
commit
|
commitdiff
|
tree
2022-04-28
yoni206
int-blaster: not allowing higher order functions (...
commit
|
commitdiff
|
tree
2022-04-28
Andrew Reynolds
Move datatype split inference scheme to its own method...
commit
|
commitdiff
|
tree
2022-04-28
Andrew Reynolds
Clean code for datatypes split (#8667)
commit
|
commitdiff
|
tree
2022-04-28
Andrew Reynolds
Make labelled separation logic asserts preserve labels...
commit
|
commitdiff
|
tree
2022-04-28
Andrey Andreyevich...
Fix PyUnicode_AsWideCharString signature (#8522)
commit
|
commitdiff
|
tree
2022-04-28
Gereon Kremer
Add resource limiting to coverings solver (#8672)
commit
|
commitdiff
|
tree
2022-04-27
Andrew Reynolds
Add option to apply constant propagation for all learne...
commit
|
commitdiff
|
tree
next