projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2020-12-04
Aina Niemetz
google test: context: Migrate cdmap_white. (#5585)
commit
|
commitdiff
|
tree
2020-12-04
Andrew Reynolds
Fix bug in hasBoundVar (#5600)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: api: Migrate sort_black. (#5594)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: context: Migrate cdmap_black. (#5584)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: context: Migrate cdlist_black. (#5582)
commit
|
commitdiff
|
tree
2020-12-04
Alex Ozdemir
Use NodeDfsIterable for makeBinary (#5595)
commit
|
commitdiff
|
tree
2020-12-04
Mathias Preiner
update-copyright: Preserve file permissions. (#5597)
commit
|
commitdiff
|
tree
2020-12-03
Andrew Reynolds
(proof-new) Updates to SMT proof manager and SmtEngine...
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
google test: api: Migrate solver_black. (#5570)
commit
|
commitdiff
|
tree
2020-12-03
Gereon Kremer
Use mkAnd where the number of children may be less...
commit
|
commitdiff
|
tree
2020-12-03
yoni206
Models as (#5581)
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
google test: Add fixture for context tests. (#5590)
commit
|
commitdiff
|
tree
2020-12-03
Andrew Reynolds
Refactor handling of global declarations (#5577)
commit
|
commitdiff
|
tree
2020-12-03
Gereon Kremer
Make run_regression.py executable. (#5588)
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
Update copyright headers.
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
google test: base: Migrate map_util_black. (#5580)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
Fix RoundingMode mapping in API. (#5578)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Remove Record object and convert to Node-level API...
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Remove dagification visitor (#5574)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate term_black. (#5571)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Use individual fixture for datatype_b...
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Add associative utilities to node manager (#5530)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate op_black. (#5567)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate grammar_black. (#5566)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Use new let binding for cvc printer (#5561)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
(proof-new) Proofs for expand definitions (#5562)
commit
|
commitdiff
|
tree
2020-12-02
Gereon Kremer
Add regressions from #3687. (#5553)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate result_black. (#5569)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
Remove use of this-> in FP literal. (#5565)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Remove assertion related to CEGQI dependency lemmas...
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: Infrastructure and first api test. (#5548)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Fix issues related to model declarations (#5560)
commit
|
commitdiff
|
tree
2020-12-01
Andres Noetzli
Improve rewriting of str.<= (#4848)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Refactor transcendental solver (#5539)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Add regressions from #5099 (#5557)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Add regression for #4335. (#5554)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Add regressions for #4707. (#5555)
commit
|
commitdiff
|
tree
2020-12-01
Andrew Reynolds
More fixes for quantifier elimination (#5533)
commit
|
commitdiff
|
tree
2020-12-01
yoni206
fix metadata for a test (#5546)
commit
|
commitdiff
|
tree
2020-11-30
Aina Niemetz
fp_converter: Properly separate out symbolic glue code...
commit
|
commitdiff
|
tree
2020-11-30
Andrew Reynolds
Use new let binding in AST printer (#5529)
commit
|
commitdiff
|
tree
2020-11-30
Aina Niemetz
floatingpoint: Use unique_ptr for FloatingPointLiteral...
commit
|
commitdiff
|
tree
2020-11-30
Abdalrhman...
Eliminate uses of SExpr from the parser. (#5496)
commit
|
commitdiff
|
tree
2020-11-30
Andrew Reynolds
Remove includes for old API from internal code (#5536)
commit
|
commitdiff
|
tree
2020-11-30
Andrew Reynolds
(proof-new) Proofs for regular expression elimination...
commit
|
commitdiff
|
tree
2020-11-26
Gereon Kremer
Make CAD solver work for empty set of assertions (...
commit
|
commitdiff
|
tree
2020-11-26
Andrew Reynolds
Removing infrastructure related to SMT model (#5527)
commit
|
commitdiff
|
tree
2020-11-26
Andrew Reynolds
Move expand definitions to its own file (#5528)
commit
|
commitdiff
|
tree
2020-11-26
Andrew Reynolds
Fully decouple SmtEngine and the Expr layer (#5532)
commit
|
commitdiff
|
tree
2020-11-26
Andrew Reynolds
Fix missed case of theory preprocessing (#5531)
commit
|
commitdiff
|
tree
2020-11-26
Andrew Reynolds
Disable fact vs lemma optimization in datatypes for...
commit
|
commitdiff
|
tree
2020-11-25
Andrew Reynolds
Add regressions for closed issues (#5526)
commit
|
commitdiff
|
tree
2020-11-25
Gereon Kremer
Fix transcendental secant plane lemmas (#5525)
commit
|
commitdiff
|
tree
2020-11-25
Andrew Reynolds
Use symbol manager for printing responses get-model...
commit
|
commitdiff
|
tree
2020-11-25
Andrew Reynolds
Allow printing of null node in let binder (#5523)
commit
|
commitdiff
|
tree
2020-11-25
Gereon Kremer
Refactor transcendental solver (#5514)
commit
|
commitdiff
|
tree
2020-11-23
Andrew Reynolds
Fix regular expression consume for nested star (#5518)
commit
|
commitdiff
|
tree
2020-11-23
Andrew Reynolds
Change UF ho to ppRewrite instead of expand definition...
commit
|
commitdiff
|
tree
2020-11-23
Andrew Reynolds
Fix for sygusToBuiltinEval for non-ground composite...
commit
|
commitdiff
|
tree
2020-11-23
Andrew Reynolds
(proof-new) Miscellaneous changes from proof-new (...
commit
|
commitdiff
|
tree
2020-11-23
Andrew Reynolds
Add declare model symbol methods to SymbolManager and...
commit
|
commitdiff
|
tree
2020-11-23
Gereon Kremer
Add get-info :time. (#5485)
commit
|
commitdiff
|
tree
2020-11-23
Andrew Reynolds
Fix quantifiers scope issue in strings preprocessor...
commit
|
commitdiff
|
tree
2020-11-21
mudathirmahgoub
Add posRewriteEqual to bags rewriter (#5498)
commit
|
commitdiff
|
tree
2020-11-21
Aina Niemetz
Rename symfpu_literal.(h.in|cpp) -> floatingpoint_liter...
commit
|
commitdiff
|
tree
2020-11-21
Aina Niemetz
Rename floatingpoint.h.in -> floatingpoin.h. (#5500)
commit
|
commitdiff
|
tree
2020-11-20
Andrew Reynolds
Fix remove term formula policy for terms beneath quanti...
commit
|
commitdiff
|
tree
2020-11-20
Aina Niemetz
RoundingMode: Rename enum values to conform to code...
commit
|
commitdiff
|
tree
2020-11-20
Aina Niemetz
FloatingPoint: Separate out symFPU glue code. (#5492)
commit
|
commitdiff
|
tree
2020-11-20
Aina Niemetz
Fix #5493. (#5495)
commit
|
commitdiff
|
tree
2020-11-20
Andrew Reynolds
Support nested quantifier elimination for get-qe comman...
commit
|
commitdiff
|
tree
2020-11-20
Andrew Reynolds
Updates to API in preparation for using symbol manager...
commit
|
commitdiff
|
tree
2020-11-20
Aina Niemetz
Fix compiler warnings. (#5493)
commit
|
commitdiff
|
tree
2020-11-20
Andrew Reynolds
Fix use of declaration sequence command in cvc parser...
commit
|
commitdiff
|
tree
2020-11-20
Gereon Kremer
(proof-new) Replace LazyCDProofSet by generic CDProofSe...
commit
|
commitdiff
|
tree
2020-11-20
Gereon Kremer
Allow to pass ProofGenerator to arithmetic inference...
commit
|
commitdiff
|
tree
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
commit
|
commitdiff
|
tree
2020-11-19
Aina Niemetz
floatingpoint.h: Split in preparation to cleanly separa...
commit
|
commitdiff
|
tree
2020-11-19
Andrew Reynolds
Use new let binding utility in smt2 printer (#5472)
commit
|
commitdiff
|
tree
2020-11-19
Aina Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
commit
|
commitdiff
|
tree
2020-11-19
Andrew Reynolds
Add nested quantifier elimination module (#5422)
commit
|
commitdiff
|
tree
2020-11-19
Andrew Reynolds
Fix issues related to eliminating extended arithmetic...
commit
|
commitdiff
|
tree
2020-11-19
Andrew Reynolds
Use symbol manager for unsat cores (#5468)
commit
|
commitdiff
|
tree
2020-11-18
Mathias Preiner
Add -> operator overload for cd* iterators. (#5464)
commit
|
commitdiff
|
tree
2020-11-18
Andrew Reynolds
Disable slow nl regression (#5467)
commit
|
commitdiff
|
tree
2020-11-18
Andrew Reynolds
Add let binding utility (#5444)
commit
|
commitdiff
|
tree
2020-11-18
Andrew Reynolds
Minor cleanup of SmtEngine (#5450)
commit
|
commitdiff
|
tree
2020-11-18
Andrew Reynolds
Do not expand definitions of extended arithmetic operat...
commit
|
commitdiff
|
tree
2020-11-18
Andrew Reynolds
Use symbol manager for get assignment (#5451)
commit
|
commitdiff
|
tree
2020-11-18
Andrew Reynolds
Fix asan issues related to solver and symbol manager...
commit
|
commitdiff
|
tree
2020-11-18
Aina Niemetz
FloatingPoint: Use uint32_t instead of unsigned. (...
commit
|
commitdiff
|
tree
2020-11-18
Aina Niemetz
FloatingPoint: Clean up and document header, format...
commit
|
commitdiff
|
tree
2020-11-18
Mathias Preiner
ci: Simplify Python dependency installs for Linux and...
commit
|
commitdiff
|
tree
2020-11-17
Gereon Kremer
Fix tangent plane lemmas (#5455)
commit
|
commitdiff
|
tree
2020-11-16
Gereon Kremer
Refactor tangent plane lemmas (#5449)
commit
|
commitdiff
|
tree
2020-11-16
Andrew Reynolds
Cleaning up scopes in preparation for symbol manager...
commit
|
commitdiff
|
tree
2020-11-16
Gereon Kremer
Improve accuracy of resource limitation (#4763)
commit
|
commitdiff
|
tree
2020-11-14
Andrew Reynolds
Fix double conflict in extended string solver (#5435)
commit
|
commitdiff
|
tree
2020-11-14
Andrew Reynolds
(proof-new) Proofs for non-clausal simplification ...
commit
|
commitdiff
|
tree
next