projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Refactor transcendental solver (#5514)
[cvc5.git]
/
src
/
theory
/
arith
/
theory_arith_private.cpp
2020-11-20
Aina Niemetz
Fix #5493. (#5495)
blob
|
commitdiff
|
raw
2020-11-20
Aina Niemetz
Fix compiler warnings. (#5493)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-19
Aina Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
blob
|
commitdiff
|
raw
|
diff to current
2020-11-18
Andrew Reynolds
Do not expand definitions of extended arithmetic operat...
blob
|
commitdiff
|
raw
|
diff to current
2020-11-16
Gereon Kremer
Improve accuracy of resource limitation (#4763)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-21
Alex Ozdemir
(proof-new) arith: dedup literals in flattenImpl (...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-15
Alex Ozdemir
(proof-new) TheoryArithPrivate: farkas lemma proof...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-14
Alex Ozdemir
(proof-new) pfs in TheoryArith(Private) explainations...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-14
Alex Ozdemir
(proof-new) pfs for conflicts in TheoryArithPrivate...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-14
Alex Ozdemir
(proof-new) Prove lemmas in Constraint (#5254)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-09
Alex Ozdemir
use right arith explanation fn to fix regressions ...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-09
Alex Ozdemir
(proof-new) proofs for arith-constraint explanations...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-07
Alex Ozdemir
(proof-new) proofs in ee -> arith pipeline (#5215)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-02
Andrew Reynolds
Decouple modules from TheoryArithPrivate (#5184)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-02
Alex Ozdemir
(proof-new) New proofs in arith::Constraint::externalEx...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-01
Andrew Reynolds
Update theory of arithmetic to standard check (#5178)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-29
Alex Ozdemir
(proof-new) Add proof managers and eager gens to arith...
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-16
Andrew Reynolds
Refactor collectModelInfo in TheoryArith (#5027)
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-01
Haniel Barbosa
Removes old proof code (#4964)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-01
FabianWolff
Fix spelling errors (#4977)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-31
Andrew Reynolds
Simplify interface for computing relevant terms. (...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-27
Andrew Reynolds
(proof-new) Arithmetic operator elim proof producing...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-27
Alex Ozdemir
Consider negation's proof before triggering arith pfs...
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-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-19
Andrew Reynolds
(proof-new) Split operator elimination from arithmetic...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-06-05
Andrew Reynolds
(proof-new) Rename ProofSkolemCache to SkolemManager...
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
2020-05-31
Andres Noetzli
Do not cache operator eliminations in arith (#4542)
blob
|
commitdiff
|
raw
|
diff to current
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
blob
|
commitdiff
|
raw
|
diff to current
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
blob
|
commitdiff
|
raw
|
diff to current
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-26
Amalee
Added unit-cube-like test for branch and bound (#3922)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-16
Alex Ozdemir
clang-format
blob
|
commitdiff
|
raw
|
diff to current
2020-03-16
Alex Ozdemir
Fix simplicity check in prop
blob
|
commitdiff
|
raw
|
diff to current
2020-03-16
Alex Ozdemir
Only save farkas+tightening proofs. Error on holes
blob
|
commitdiff
|
raw
|
diff to current
2020-03-09
Andrew Reynolds
Fix type issue in arith rewrite equality (#3972)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Alex Ozdemir
Add a new arith constraint proof rule: IntTightenAP...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Alex Ozdemir
Revert "Add a new arith constraint proof rule: IntTight...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Andres Noetzli
Add a new arith constraint proof rule: IntTightenAP...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-17
Andrew Reynolds
Fix soundness bug in reduction of integer div/mod...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-04
Alex Ozdemir
Articulate proof-related debug statements in arith...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-03
Andrew Reynolds
Split on model values when repaired model from non...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-19
Andres Noetzli
Fix reduction of `sqrt` (#3478)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
blob
|
commitdiff
|
raw
|
diff to current
2019-03-26
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2019-01-03
Alex Ozdemir
[LRA proof] Recording & Printing LRA Proofs (#2758)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-23
Aina Niemetz
Refactor ITE simplification preprocessing pass. (#2360)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-16
Andres Noetzli
Move node algorithms to separate file (#2311)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
blob
|
commitdiff
|
raw
|
diff to current
2018-07-06
Andrew Reynolds
Split ext theory to own file and document (#1809)
blob
|
commitdiff
|
raw
|
diff to current
2018-06-25
Aina Niemetz
Updated copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-04-03
Andrew Reynolds
Use choice when expanding definitions for inverse trans...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-27
Andrew Reynolds
Option to not use partial function semantics for arithm...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-20
Andrew Reynolds
Minor fixes and additions for transcendental functions...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-07
Andrew Reynolds
Add remaining transcendental functions (#1551)
blob
|
commitdiff
|
raw
|
diff to current
2018-01-23
Tim King
Commenting out throw specifiers for DeltaRationExceptio...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-10
Tim King
Cleaning up throw specifiers on Exception and subclasse...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-08
Tim King
Removes RationalFromDoubleException. Replaces this...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-03
Andrew Reynolds
Global negate (#1466)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-08
Andrew Reynolds
Make collect model info return a Bool (#1421)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-17
Aina Niemetz
Add random number generator. (#1370)
blob
|
commitdiff
|
raw
|
diff to current
2017-08-31
Andres Noetzli
Use thread_local instead of compiler extensions (#210)
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Moving from the gnu extensions for hash maps to the...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-10
ajreynol
Merge ntExt branch. Adds support for transcendental...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-05-31
ajreynol
Minor fix to last commit.
blob
|
commitdiff
|
raw
|
diff to current
2017-05-31
ajreynol
Change to-int, div, int-div skolems from CDAttribute...
blob
|
commitdiff
|
raw
|
diff to current
2017-05-28
Clark Barrett
Merge pull request #164 from CVC4/fix_comp
blob
|
commitdiff
|
raw
|
diff to current
2017-05-26
Tim King
Checking that equalities belong to the arithmetic theor...
blob
|
commitdiff
|
raw
|
diff to current
2017-05-17
Clark Barrett
Merge pull request #155 from makaimann/conditional_coverage
blob
|
commitdiff
|
raw
|
diff to current
2017-05-16
Clark Barrett
Merge pull request #161 from 4tXJ7f/fix_parser
blob
|
commitdiff
|
raw
|
diff to current
2017-05-16
Andrew Reynolds
Merge pull request #156 from 4tXJ7f/fix_safe_print
blob
|
commitdiff
|
raw
|
diff to current
2017-05-15
ajreynol
Cleanup handling of division (possible fix for bugs...
blob
|
commitdiff
|
raw
|
diff to current
2017-04-28
ajreynol
Fix bug for real division.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-24
Andrew Reynolds
Merge pull request #152 from timothy-king/delta-rationa...
blob
|
commitdiff
|
raw
|
diff to current
2017-04-22
Tim King
Updating TheoryArithPrivate::getDeltaValue() to eagerly...
blob
|
commitdiff
|
raw
|
diff to current
2017-04-07
ajreynol
Change option names for nl.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-06
Clark Barrett
Merge pull request #143 from FabianWolff/master
blob
|
commitdiff
|
raw
|
diff to current
2017-04-05
ajreynol
Fix bug 698.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-04
ajreynol
Simplify Theory::collectModelInfo interface to not...
blob
|
commitdiff
|
raw
|
diff to current
2017-04-04
Clark Barrett
Merge pull request #141 from 4tXJ7f/remove_def
blob
|
commitdiff
|
raw
|
diff to current
2017-04-03
Andrew Reynolds
Merge pull request #142 from timothy-king/nlAlgMerge
blob
|
commitdiff
|
raw
|
diff to current
2017-04-03
Tim King
Adding a model based axiom instantiation scheme for...
blob
|
commitdiff
|
raw
|
diff to current
2016-10-11
Paul Meng
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
blob
|
commitdiff
|
raw
|
diff to current
2016-10-01
Tim King
Merge pull request #93 from timothy-king/clang-format
blob
|
commitdiff
|
raw
|
diff to current
2016-09-25
Tim King
Fixing a potential use after free coming from a pop_bac...
blob
|
commitdiff
|
raw
|
diff to current
next