projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
FloatingPoint: Separate out symFPU glue code. (#5492)
[cvc5.git]
/
src
/
theory
/
arrays
/
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
tree
|
commitdiff
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
tree
|
commitdiff
2020-10-01
Andrew Reynolds
(proof-new) Make arrays proof producing (#5112)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-21
Andrew Reynolds
(proof-new) Add the arrays proof checker (#5047)
tree
|
commitdiff
2020-09-18
Andrew Reynolds
Logic exception for arrays indexed by arrays (#5073)
tree
|
commitdiff
2020-09-16
Abdalrhman Mohamed
Dump commands in internal code using command printing...
tree
|
commitdiff
2020-09-02
Andrew Reynolds
(new theory) Update TheoryArrays to the new standard...
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-31
Andrew Reynolds
Simplify interface for computing relevant terms. (...
tree
|
commitdiff
2020-08-24
Andrew Reynolds
Extend the standard Theory template based on equality...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Limit trigger terms to shared terms in arrays (#4932)
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Remove spurious theory methods calls (#4931)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Add TheoryState objects to each Theory (#4920)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Standardize collectModelInfo and theory-specific collec...
tree
|
commitdiff
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
tree
|
commitdiff
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
tree
|
commitdiff
2020-07-31
Andrew Reynolds
Standardize explanations in arrays (#4804)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use TypeNode/Node in ArrayStoreAll (#4728)
tree
|
commitdiff
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
tree
|
commitdiff
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
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-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-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2020-02-03
Clark Barrett
Fix corner case - might need to REWRITE_AGAIN (#3706)
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-08
Piotr Trojanek
prefer prefix ++ operator for iterators
tree
|
commitdiff
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
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
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-19
Andrew Reynolds
Decision strategy: incorporate arrays. (#2495)
tree
|
commitdiff
2018-08-16
Andres Noetzli
Move node algorithms to separate file (#2311)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Remove unused tuple classes (#2313)
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-04
Andrew Reynolds
Move assertion. (#2051)
tree
|
commitdiff
2018-05-30
Andres Noetzli
Fix for issue #2002 (#2012)
tree
|
commitdiff
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
tree
|
commitdiff
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
tree
|
commitdiff
2018-02-06
Tim King
Resolving warnings from -Winconsistent-missing-override...
tree
|
commitdiff
2018-01-10
Tim King
Removing throw specifiers for TypeRules. (#1501)
tree
|
commitdiff
2018-01-10
Tim King
Removing throw specifiers from type enumerators. (...
tree
|
commitdiff
2018-01-09
Tim King
Removing more miscellaneous throw specifiers. (#1488)
tree
|
commitdiff
2017-12-08
Andrew Reynolds
Make collect model info return a Bool (#1421)
tree
|
commitdiff
2017-11-15
Tim King
Adding garbage collection for Proof objects. (#1294)
tree
|
commitdiff
2017-10-25
Tim King
Switching EqProof to use shared_ptr everywhere. (...
tree
|
commitdiff
2017-10-11
Tim King
Cleaning up ProofArray class. (#1208)
tree
|
commitdiff
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
tree
|
commitdiff
2017-07-21
Tim King
Moving from the gnu extensions for hash maps to the...
tree
|
commitdiff
2017-07-13
Aina Niemetz
Merge pull request #188 from aniemetz/cx11
tree
|
commitdiff
2017-07-12
ajreynol
Make type rules more strict for operators whose type...
tree
|
commitdiff
2017-07-07
Mathias Preiner
Update copyright headers.
tree
|
commitdiff
2017-06-30
ajreynol
Minor change to trigger selection, fixes related to...
tree
|
commitdiff
2017-06-21
Andrew Reynolds
Merge pull request #175 from CVC4/fix_uninit
tree
|
commitdiff
2017-06-16
Clark Barrett
Merge pull request #170 from CVC4/fix_2_6_parser3
tree
|
commitdiff
2017-06-16
Clark Barrett
Fix for bug 639.
tree
|
commitdiff
2017-04-28
Clark Barrett
Partial fix for bug 717.
tree
|
commitdiff
2017-04-22
Clark Barrett
Merge pull request #151 from 4tXJ7f/fix_debug
tree
|
commitdiff
2017-04-21
Clark Barrett
Fix for bug 681 (now gives reasonable error message...
tree
|
commitdiff
2017-04-19
Clark Barrett
Merge pull request #147 from makaimann/coverage_fix
tree
|
commitdiff
2017-04-18
Clark Barrett
Fix for bug 639.
tree
|
commitdiff
2017-04-04
ajreynol
Simplify Theory::collectModelInfo interface to not...
tree
|
commitdiff
2017-03-27
Clark Barrett
Merge pull request #137 from 4tXJ7f/throw_quals
tree
|
commitdiff
2017-03-27
Andres Notzli
Remove throw qualifiers in type enumerators
tree
|
commitdiff
2017-03-18
Clark Barrett
Fix to help with bug 717
tree
|
commitdiff
2017-03-02
ajreynol
Eliminate Boolean term conversion. Generalizes removeIT...
tree
|
commitdiff
2017-01-18
Andres Noetzli
Fix non-idempotent rewrite in Array rewriter
tree
|
commitdiff
2016-11-03
ajreynol
Add priorities to getNextDecision. Properly handle...
tree
|
commitdiff
2016-10-11
Paul Meng
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
tree
|
commitdiff
2016-09-17
guykatzz
In a ROW guard proof, if the transitivity proof does...
tree
|
commitdiff
2016-09-17
guykatzz
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2016-09-16
Guy
Handling a corner case where a ROW's guard is a constan...
tree
|
commitdiff
2016-08-24
PaulMeng
Merge remote-tracking branch 'origin/master'
tree
|
commitdiff
2016-07-06
Guy
A few proof bugs fixed
tree
|
commitdiff
2016-07-05
PaulMeng
Merge branch 'master' of https://github.com/CVC4/CVC4.git
tree
|
commitdiff
2016-06-06
guykatzz
Merge pull request #85 from CVC4/master_for_proof_merge
tree
|
commitdiff
2016-06-02
Guy
Merge from proof branch
tree
|
commitdiff
2016-06-02
Guy
Revert "Merging proof branch"
tree
|
commitdiff
2016-06-02
Guy
Merging proof branch
tree
|
commitdiff
2016-04-20
PaulMeng
update from the master
tree
|
commitdiff
2016-04-15
Guy
Rolling back the rewrite code
tree
|
commitdiff
2016-04-14
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2016-04-14
Guy
Remove some no-longer-required rewrites of array lemmas
tree
|
commitdiff
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2016-04-04
Tim King
Updating the copyright headers and scripts.
tree
|
commitdiff
2016-04-03
Guy
Removed the theory-specific merge reason types. Instead...
tree
|
commitdiff
2016-03-24
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2016-03-24
Guy
Refactored the equality engine in order to remove theor...
tree
|
commitdiff
2016-03-23
guykatzz
Merge pull request #82 from CVC4/master_for_merge
tree
|
commitdiff
2016-03-23
Guy
squash-merge from proof branch
tree
|
commitdiff
2016-03-07
ajreynol
Minor change to F-Length inference in strings. No inter...
tree
|
commitdiff
next