projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2020-11-13
Andrew Reynolds
(proof-new) Enable proofs for datatypes (#5436)
commit
|
commitdiff
|
tree
2020-11-13
yoni206
Model declarations printing options (#5432)
commit
|
commitdiff
|
tree
2020-11-13
Andrew Reynolds
Add more features to symbol manager (#5434)
commit
|
commitdiff
|
tree
2020-11-13
Andrew Reynolds
Make regular expression difference left associative...
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
Simplify sygus solver and sygus stream (#5389)
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
Fix printing of define named function (#5425)
commit
|
commitdiff
|
tree
2020-11-12
yoni206
Models standard (#5415)
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
(proof-new) Separate explanation stages in proof equali...
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
Fix redundant refinement lemma in sygus solver (#5399)
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
(proof-new) Proofs for skolemization (#5339)
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
(proof-new) Fix true explanations of propagations in...
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
(proof-new) Improve printing and debugging for pedantic...
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
(proof-new) Add datatypes inference to proof constructo...
commit
|
commitdiff
|
tree
2020-11-12
Andrew Reynolds
Make symbol manager context dependent (#5424)
commit
|
commitdiff
|
tree
2020-11-11
Andrew Reynolds
Move symbol manager to src/expr/ (#5420)
commit
|
commitdiff
|
tree
2020-11-11
Andrew Reynolds
Rewrite witness terms at prerewrite (#5419)
commit
|
commitdiff
|
tree
2020-11-11
Andrew Reynolds
Add simple substitution utility (#5397)
commit
|
commitdiff
|
tree
2020-11-11
Andrew Reynolds
Pass symbol manager to commands (#5410)
commit
|
commitdiff
|
tree
2020-11-11
Andrew Reynolds
Fix preregistration in TheorySep before declare-heap...
commit
|
commitdiff
|
tree
2020-11-10
Andrew Reynolds
Do not mark extended functions as reduced based on...
commit
|
commitdiff
|
tree
2020-11-10
Alex Ozdemir
Pin LFSC version (#5412)
commit
|
commitdiff
|
tree
2020-11-10
Andrew Reynolds
Make mkGroundTerm deterministic (#5347)
commit
|
commitdiff
|
tree
2020-11-10
Andrew Reynolds
Add getSubtermKinds to node algorithm (#5398)
commit
|
commitdiff
|
tree
2020-11-10
Andrew Reynolds
Add proper support for the declare-heap command for...
commit
|
commitdiff
|
tree
2020-11-10
Andrew Reynolds
Migrate some documentation about attributes (#5390)
commit
|
commitdiff
|
tree
2020-11-09
Andrew Reynolds
Add symbol manager (#5380)
commit
|
commitdiff
|
tree
2020-11-09
Andrew Reynolds
Simplify handling of subtypes in smt2 printer (#5401)
commit
|
commitdiff
|
tree
2020-11-09
Gereon Kremer
Properly clear interrupt for solve() as well. (#5403)
commit
|
commitdiff
|
tree
2020-11-09
Andrew Reynolds
Do not regress explanations of datatype lemmas (#5376)
commit
|
commitdiff
|
tree
2020-11-06
mudathirmahgoub
Fix issue #5342 (#5349)
commit
|
commitdiff
|
tree
2020-11-06
Andrew Reynolds
(proof-new) Miscellaneous changes to strings for proofs...
commit
|
commitdiff
|
tree
2020-11-06
Andrew Reynolds
Split sygus template inference to its own file (#5388)
commit
|
commitdiff
|
tree
2020-11-06
Andrew Reynolds
Simplify printing with respect to expression types...
commit
|
commitdiff
|
tree
2020-11-05
mudathirmahgoub
Remove mkSingleton from the API (#5366)
commit
|
commitdiff
|
tree
2020-11-04
Andres Noetzli
Add constants from equality engine evaluation to model...
commit
|
commitdiff
|
tree
2020-11-03
Andrew Reynolds
Add scope methods constructing types in API (#5393)
commit
|
commitdiff
|
tree
2020-11-03
Andres Noetzli
Add support for printing `re.loop` and `re.^` (#5392)
commit
|
commitdiff
|
tree
2020-11-03
Andrew Reynolds
Reset built model flag at presolve in nonlinear (#5386)
commit
|
commitdiff
|
tree
2020-11-03
Andrew Reynolds
Move sygus qe preproc to its own file (#5375)
commit
|
commitdiff
|
tree
2020-11-03
makaimann
Run python tests during make check (#5226)
commit
|
commitdiff
|
tree
2020-11-02
Aina Niemetz
contrib: Remove dependency directories. (#5367)
commit
|
commitdiff
|
tree
2020-11-02
Andrew Reynolds
Update strings proxy variable map to be context indepen...
commit
|
commitdiff
|
tree
2020-11-02
Andrew Reynolds
Miscellaneous cleaning of parser (#5369)
commit
|
commitdiff
|
tree
2020-11-02
Andrew Reynolds
Avoid dynamic allocation in symbol table implementation...
commit
|
commitdiff
|
tree
2020-10-30
Gereon Kremer
Use BoundInference in nonlinear extension (#5359)
commit
|
commitdiff
|
tree
2020-10-30
Andrew Reynolds
Update api::Sort to use TypeNode instead of Type (...
commit
|
commitdiff
|
tree
2020-10-29
Andrew Reynolds
Set strings pending conflict flag (#5364)
commit
|
commitdiff
|
tree
2020-10-29
mudathirmahgoub
Add mkInteger to the API (#5274)
commit
|
commitdiff
|
tree
2020-10-29
Andrew Reynolds
(proof-new) Update the strings inference manager for...
commit
|
commitdiff
|
tree
next