projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Add option for using bound inference for relevant assertions (#7152)
[cvc5.git]
/
src
/
theory
/
arith
/
nl
/
nonlinear_extension.cpp
2021-09-08
Andrew Reynolds
Add option for using bound inference for relevant asser...
blob
|
commitdiff
|
raw
2021-09-07
Andres Noetzli
Use `EnvObj` methods instead of `Theory` methods (...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-26
Gereon Kremer
Improve integration of nonlinear arithmetic into the...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-20
Gereon Kremer
Use Env class in nonlinear extension (#7039)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-19
Gereon Kremer
Start using Options via Env in arithmetic (#7032)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-16
Gereon Kremer
Use InferenceManager in ExtTheory (#7006)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-26
yoni206
pow2 -- final changes (#6800)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-02
Gereon Kremer
Fix issues when poly is disabled (#6668)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-17
Gereon Kremer
Improve integration of CAD with nl-Ext (#6542)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-09
Andrew Reynolds
Add identifiers for extended function reductions (...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-08
Andrew Reynolds
Add identifiers for sources of incompleteness (#6311)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Andrew Reynolds
Fix non-linear for unknown case (#6252)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-25
Gereon Kremer
Ensure nonlinear extensions properly reconsiders its...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-15
Andrew Reynolds
Make nonlinear extension account for relevant term...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-11
Gereon Kremer
Make linear arithmetic use its inference manager (...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-24
Gereon Kremer
(proof-new) Add proofs for CAD solver (#5981)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-19
Gereon Kremer
Cleanup of inferences in arithmetic theory (#5927)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-15
Gereon Kremer
Remove now obsolete sendLemmas and inferences stat...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-11
Gereon Kremer
Add InferenceId member to TheoryInference, adapt all...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-11
Gereon Kremer
Merge InferenceIds into one enum (#5892)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-08
Andrew Reynolds
Avoid spurious traversal of terms during preregistratio...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-02
Andrew Reynolds
Improvements for NL traces (#5846)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-21
Gereon Kremer
(proof-new) Make nl-ext factoring lemmas proof producin...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-18
Gereon Kremer
(proof-new) Setup proof infrastructure for transcendent...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-18
Gereon Kremer
Add proof for split zero check. (#5699)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-17
Gereon Kremer
(proof-new) Prepare nonlinear extension and nl-ext...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-07
Gereon Kremer
Refactor initial phase of transcendental solver (#5599)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-16
Gereon Kremer
Improve accuracy of resource limitation (#4763)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-05
mudathirmahgoub
Remove mkSingleton from the API (#5366)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-03
Andrew Reynolds
Reset built model flag at presolve in nonlinear (#5386)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-30
Gereon Kremer
Use BoundInference in nonlinear extension (#5359)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-28
Andrew Reynolds
Fixes for unconstrained variables in nonlinear model...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-28
Gereon Kremer
Split NlSolver in multiple subsolvers (#5315)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-30
Gereon Kremer
Add strategy for nonlinear extension (#5160)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-29
Gereon Kremer
Clean up nonlinear extension (#5149)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-26
Gereon Kremer
Use inference manager for nl_solver (#5125)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-23
Gereon Kremer
Make IAND solver use inference manager. (#5126)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Gereon Kremer
ICP-based solver for nonlinear arithmetic (#5017)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-17
Gereon Kremer
Use new inference manager in transcendental solver...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-04
Gereon Kremer
Use arith::InferenceManager for CAD lemmas (#5015)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-03
Gereon Kremer
Basic integration of arith::InferenceManager (#4999)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-03
Gereon Kremer
Make nonlinear extension (more) deterministic (#4996)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-03
Andrew Reynolds
Make ExtTheory independent of Theory (#5010)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-02
Gereon Kremer
Add ArithLemma and arith::InferenceManager (#4960)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-24
Andrew Reynolds
Do not use relevance during non-linear check model...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-21
Gereon Kremer
Preparations for a CAD-based arithmetic solver (#4762)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-16
Andrew Reynolds
Make ExtTheory a utility and not a member of Theory...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-09
Andrew Reynolds
Associate all lemmas in non-linear arithmetic with...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
blob
|
commitdiff
|
raw
|
diff to current
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-06-06
Andrew Reynolds
Use NlLemma utility for all lemmas in non-linear. ...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
blob
|
commitdiff
|
raw
|
diff to current