projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Use inference manager for nl_solver (#5125)
2020-09-26
Gereon Kremer
Use inference manager for nl_solver (#5125)
commit
|
commitdiff
|
tree
2020-09-23
Gereon Kremer
Make IAND solver use inference manager. (#5126)
commit
|
commitdiff
|
tree
2020-09-22
Gereon Kremer
ICP-based solver for nonlinear arithmetic (#5017)
commit
|
commitdiff
|
tree
2020-09-17
Gereon Kremer
(cad-solver) Fix square-free-basis computation (#5085)
commit
|
commitdiff
|
tree
2020-09-04
Gereon Kremer
Use arith::InferenceManager for CAD lemmas (#5015)
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Added a new rule to simplify (bvugt (bvurem T x) x...
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Basic integration of arith::InferenceManager (#4999)
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Make nonlinear extension (more) deterministic (#4996)
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Remove #line directives from generated files. (#5005)
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Use std::unique_ptr instead of std::shared_ptr for...
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Add ArithLemma and arith::InferenceManager (#4960)
commit
|
commitdiff
|
tree
2020-08-31
Gereon Kremer
Fix --ackermann in the presence on syntactically different...
commit
|
commitdiff
|
tree
2020-08-28
Gereon Kremer
(cad-solver) Fixed excluding lemma generation. (#4958)
commit
|
commitdiff
|
tree
2020-08-28
Gereon Kremer
Make iand lemmas use proper Inference types. (#4956)
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
(cad solver) Add a partial check method. (#4904)
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
Changes assertion (about maximum set cardinality) to...
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
Fix SmtEngine::reset() (#4917)
commit
|
commitdiff
|
tree
2020-08-16
Gereon Kremer
(cad solver) Use the current model as initial assignment...
commit
|
commitdiff
|
tree
2020-08-14
Gereon Kremer
Inspect roots to avoid certain resultants (Algorithm...
commit
|
commitdiff
|
tree
2020-08-12
Gereon Kremer
Add naive support for integer variables. (#4835)
commit
|
commitdiff
|
tree
2020-08-12
Gereon Kremer
Fix infinite loop in arith_ite_simp (#4805)
commit
|
commitdiff
|
tree
2020-08-05
Gereon Kremer
Improve error message for unsupported exponents (#4852)
commit
|
commitdiff
|
tree
2020-08-05
Gereon Kremer
Add dummy returns if libpoly is unavailable. (#4845)
commit
|
commitdiff
|
tree
2020-08-04
Gereon Kremer
Properly initialize d_fullyInited. (#4840)
commit
|
commitdiff
|
tree
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
commit
|
commitdiff
|
tree
2020-07-30
Gereon Kremer
Cad implementation (#4774)
commit
|
commitdiff
|
tree
2020-07-30
Gereon Kremer
Adds the interface for the CAD-based arithmetic solver...
commit
|
commitdiff
|
tree
2020-07-17
Gereon Kremer
Integration of libpoly (#4679)
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Resource manager cleanup (#4732)
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Remove cumulative time limits and cpu time limits ...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Fixes memory leak when an exception goes through runCvc4...
commit
|
commitdiff
|
tree
2020-07-15
Gereon Kremer
Add missing header (Fixes #4743) (#4749)
commit
|
commitdiff
|
tree
2020-07-13
Gereon Kremer
Implement --tlimit for windows (#4716)
commit
|
commitdiff
|
tree
2020-07-10
Gereon Kremer
Add deps/install/lib to RPATH and warn user when using...
commit
|
commitdiff
|
tree
2020-07-08
Gereon Kremer
Re-implement handling of --tlimit (#4655)
commit
|
commitdiff
|
tree