projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Statistics on instantiations per quantified formula. (#4719)
[cvc5.git]
/
src
/
theory
/
arith
/
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
tree
|
commitdiff
2020-07-09
Andrew Reynolds
Associate all lemmas in non-linear arithmetic with...
tree
|
commitdiff
2020-07-08
Andrew Reynolds
Improve and fix secant and tangent lemmas in the transc...
tree
|
commitdiff
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Add internal support for integer and operator (#4668)
tree
|
commitdiff
2020-06-28
Alex Ozdemir
Proof Rules and Checker for Arithmetic (#4665)
tree
|
commitdiff
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
tree
|
commitdiff
2020-06-22
Andrew Reynolds
Add trascendental function kinds to list of unevaluated...
tree
|
commitdiff
2020-06-19
Andrew Reynolds
(proof-new) Split operator elimination from arithmetic...
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-11
Andrew Reynolds
(proof-new) Remove arith-snorm option. (#4591)
tree
|
commitdiff
2020-06-08
Andres Noetzli
Fix Coverity issues (#4587)
tree
|
commitdiff
2020-06-06
Andrew Reynolds
Use NlLemma utility for all lemmas in non-linear. ...
tree
|
commitdiff
2020-06-05
Andrew Reynolds
(proof-new) Rename ProofSkolemCache to SkolemManager...
tree
|
commitdiff
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
tree
|
commitdiff
2020-05-31
Andres Noetzli
Do not cache operator eliminations in arith (#4542)
tree
|
commitdiff
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
tree
|
commitdiff
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
tree
|
commitdiff
2020-04-11
Andrew Reynolds
Split the non-linear solver (#4219)
tree
|
commitdiff
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
tree
|
commitdiff
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-28
Andrew Reynolds
Split transcendental solver to its own file (#4156)
tree
|
commitdiff
2020-03-26
Amalee
Added unit-cube-like test for branch and bound (#3922)
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Change transcendental function app slave list to unorde...
tree
|
commitdiff
2020-03-16
Alex Ozdemir
clang-format
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Fix simplicity check in prop
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Fix antecedent loop. Whoops
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Only save farkas+tightening proofs. Error on holes
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Expand the definition of a "simple" farkas proof.
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Remove assertion in resolution bound inferences (#3980)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Do not set values for non-linear mult terms in collectM...
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Fix type issue in arith rewrite equality (#3972)
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Fixes for bounds on transcendental functions (#3832)
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Rewrite again full for DIV rewrite (#3945)
tree
|
commitdiff
2020-03-05
Alex Ozdemir
Add a new arith constraint proof rule: IntTightenAP...
tree
|
commitdiff
2020-03-05
Alex Ozdemir
Revert "Add a new arith constraint proof rule: IntTight...
tree
|
commitdiff
2020-03-05
Andres Noetzli
Add a new arith constraint proof rule: IntTightenAP...
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Infrastructure for tautological literals in nonlinear...
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Use side effect utility for non-linear lemmas (#3780)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Support for witnessing choice in models (#3781)
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2020-02-19
Andrew Reynolds
Fix approximate bounds for transcendental functions...
tree
|
commitdiff
2020-02-17
Andrew Reynolds
Fix soundness bug in reduction of integer div/mod...
tree
|
commitdiff
2020-02-12
Andrew Reynolds
Fix non-linear equality solving that involves mixed...
tree
|
commitdiff
2020-02-07
Andrew Reynolds
Fix exact sqrt (#3721)
tree
|
commitdiff
2020-02-04
Alex Ozdemir
Articulate proof-related debug statements in arith...
tree
|
commitdiff
2020-02-03
Andrew Reynolds
Split on model values when repaired model from non...
tree
|
commitdiff
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix substitution in nl solver (#3638)
tree
|
commitdiff
2019-12-18
Andrew Reynolds
Increment Taylor degree for tangent and secant plane...
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-11
Andrew Reynolds
Do not substitute beneath arithmetic terms in the non...
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
tree
|
commitdiff
2019-12-03
Andrew Reynolds
Improve flexibility of lemma output in non-linear solve...
tree
|
commitdiff
2019-12-02
makaimann
OpTerm Refactor: Allow retrieving OpTerm used to create...
tree
|
commitdiff
2019-11-22
Andrew Reynolds
Minor refactoring of compute model value for nl (#3489)
tree
|
commitdiff
2019-11-19
Andres Noetzli
Fix reduction of `sqrt` (#3478)
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-13
Andrew Reynolds
Refactor non-linear extension for model-based refinemen...
tree
|
commitdiff
2019-11-05
Andrew Reynolds
Separate model object in non-linear extension (#3426)
tree
|
commitdiff
2019-10-31
Mathias Preiner
Fix Unimplemented() macros missed in #3366. (#3424)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-30
Andrew Reynolds
Split some generic utilities from the non-linear extens...
tree
|
commitdiff
2019-10-28
Andrew Reynolds
Fix for non-linear models (#3410)
tree
|
commitdiff
2019-10-28
Andres Noetzli
Fix integer division rewrite (#3415)
tree
|
commitdiff
2019-10-13
Andrew Reynolds
Eliminate negative constant coefficients in div/mod...
tree
|
commitdiff
2019-10-08
Piotr Trojanek
prefer prefix ++ operator for iterators
tree
|
commitdiff
2019-09-29
Andres Noetzli
Introduce template classes for simple type rules (...
tree
|
commitdiff
2019-09-04
Andrew Reynolds
Fixes related to destructing null (#3231)
tree
|
commitdiff
2019-08-24
Piotr Trojanek
fix mismatch between "delete" and "new []" (#2795)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Fix argument in nonlinear extension. (#3216)
tree
|
commitdiff
2019-06-11
Ahmed Irfan
NA Tangent reverse implication (#3050)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-14
Andrew Reynolds
Use zero slope tangent planes for transcendental functi...
tree
|
commitdiff
2019-01-03
Alex Ozdemir
[LRA proof] Recording & Printing LRA Proofs (#2758)
tree
|
commitdiff
2018-12-20
Aina Niemetz
Add missing type rules for parameterized operator kinds...
tree
|
commitdiff
2018-12-15
Alex Ozdemir
[LRA Proof] Storage for LRA proofs (#2747)
tree
|
commitdiff
2018-12-14
Aina Niemetz
Fixed typos.
tree
|
commitdiff
2018-12-07
Alex Ozdemir
Arith Constraint Proof Loggin (#2732)
tree
|
commitdiff
2018-10-01
Aina Niemetz
Fix compiler warnings. (#2555)
tree
|
commitdiff
2018-09-27
Andrew Reynolds
Fix Taylor overapproximation for large exponentials...
tree
|
commitdiff
2018-09-25
Andrew Reynolds
Improve non-linear check model error handling (#2497)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Remove unused CMakeLists.txt
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-13
Andrew Reynolds
Simplify storing of transcendental function application...
tree
|
commitdiff
2018-09-13
Andrew Reynolds
Decision strategy: incorporate CEGQI (#2460)
tree
|
commitdiff
2018-09-05
Mathias Preiner
Use std::uniqe_ptr for d_eq_infer to make Coverity...
tree
|
commitdiff
2018-08-30
Andres Noetzli
Use useBland option in FCSimplexDecisionProcedure ...
tree
|
commitdiff
2018-08-23
Aina Niemetz
Refactor ITE simplification preprocessing pass. (#2360)
tree
|
commitdiff
2018-08-16
Andres Noetzli
Move node algorithms to separate file (#2311)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
tree
|
commitdiff
2018-07-26
Tim King
Changing the arithmetic static learner to use CDHashMap...
tree
|
commitdiff
2018-07-25
Tim King
Changing ArithIteUtils to use CDInsertHashMap. (#2206)
tree
|
commitdiff
2018-07-17
Andrew Reynolds
Purify applications of exp to transcendental arguments...
tree
|
commitdiff
next