projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Introduce quantifiers inference manager (#5821)
[cvc5.git]
/
src
/
theory
/
rewriter.cpp
2020-11-20
Aina Niemetz
Fix compiler warnings. (#5493)
blob
|
commitdiff
|
raw
2020-11-16
Gereon Kremer
Improve accuracy of resource limitation (#4763)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-21
Andrew Reynolds
(proof-new) Fixes for proofs in rewriter (#5307)
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-02
Andrew Reynolds
(proof-new) Updates to builtin proof checker (#4962)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-15
Andres Noetzli
Use TypeNode in UninterpretedConstant (#4748)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-14
Andrew Reynolds
(proof-new) Skeleton proof support in the Rewriter...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-11
Andres Noetzli
Introduce tables in the rewriter (#3742)
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-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
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-15
Andrew Reynolds
Simple optimizations for the core rewriter (#3569)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
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-08-01
Mathias Preiner
Fix memory leak in rewriter (debug mode). (#3141)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-26
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
blob
|
commitdiff
|
raw
|
diff to current
2018-06-25
Aina Niemetz
Updated copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-01-27
Tim King
Removing structurally dead code. (#1540)
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-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-03-02
ajreynol
Eliminate Boolean term conversion. Generalizes removeIT...
blob
|
commitdiff
|
raw
|
diff to current
2017-01-18
Andrew Reynolds
Merge pull request #128 from 4tXJ7f/fix_lfsc_perf
blob
|
commitdiff
|
raw
|
diff to current
2017-01-14
Clark Barrett
Merge pull request #130 from chadbrewbaker/master
blob
|
commitdiff
|
raw
|
diff to current
2017-01-11
Clark Barrett
Merge pull request #129 from timothy-king/regression...
blob
|
commitdiff
|
raw
|
diff to current
2017-01-11
Tim King
Adding regression test scrubbing.
blob
|
commitdiff
|
raw
|
diff to current
2016-04-20
PaulMeng
update from the master
blob
|
commitdiff
|
raw
|
diff to current
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-04-04
Tim King
Updating the copyright headers and scripts.
blob
|
commitdiff
|
raw
|
diff to current
2016-01-27
Liana Hadarean
Merged bit-vector and uf proof branch.
blob
|
commitdiff
|
raw
|
diff to current
2016-01-09
Tim King
Adding a new Listener utility class. Changing the Resou...
blob
|
commitdiff
|
raw
|
diff to current
2016-01-09
Tim King
Removing StatisticsRegistry's static functions current...
blob
|
commitdiff
|
raw
|
diff to current
2015-12-15
Tim King
Refactoring Options Handler & Library Cycle Breaking
blob
|
commitdiff
|
raw
|
diff to current
2015-05-28
Liana Hadarean
added options for controlling resource step-count for...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-27
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-11-17
Liana Hadarean
Resource-limiting work.
blob
|
commitdiff
|
raw
|
diff to current
2014-07-10
Kshitij Bansal
Merge remote-tracking branch 'origin/master' into segfa...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-01
Morgan Deters
Update copyrights.
blob
|
commitdiff
|
raw
|
diff to current
2013-12-05
Morgan Deters
Update copyrights, add missing file-level documentation...
blob
|
commitdiff
|
raw
|
diff to current
2013-12-03
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-12-03
lianah
fixed rewriter bug where postRewrite was not caching...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-02
Morgan Deters
Regenerated copyrights: canonicalized names, no emails
blob
|
commitdiff
|
raw
|
diff to current
2013-04-02
Morgan Deters
update copyrights
blob
|
commitdiff
|
raw
|
diff to current
2012-10-11
Morgan Deters
Standardizing copyright notice. Touches **ALL** source...
blob
|
commitdiff
|
raw
|
diff to current
2012-10-06
Morgan Deters
* Fix some regressions' expected outputs.
blob
|
commitdiff
|
raw
|
diff to current
2012-07-31
Morgan Deters
fixes for portfolio
blob
|
commitdiff
|
raw
|
diff to current
2012-06-16
Dejan Jovanović
changing theoryOf in shared mode with arrays to move...
blob
|
commitdiff
|
raw
|
diff to current
2012-06-14
Dejan Jovanović
* removing rewriteEquality from the rewriter
blob
|
commitdiff
|
raw
|
diff to current
2012-06-13
Clark Barrett
Fixes lots of problems in bv rewrite rules and adds...
blob
|
commitdiff
|
raw
|
diff to current
2012-06-12
Dejan Jovanović
bufixes and the bugs
blob
|
commitdiff
|
raw
|
diff to current
2012-06-11
Clark Barrett
OK, now the rewrite issues are fixed
blob
|
commitdiff
|
raw
|
diff to current
2012-06-11
Clark Barrett
Fix for array bug with decision heuristic
blob
|
commitdiff
|
raw
|
diff to current
2012-06-10
Clark Barrett
Added a very fruitful assertion to the rewriter: checks...
blob
|
commitdiff
|
raw
|
diff to current
2012-05-28
Clark Barrett
Added some BV rewrites, fixed bugs in array theory...
blob
|
commitdiff
|
raw
|
diff to current
2012-03-28
Dejan Jovanović
adding an extra cache check in the rewriter, speeds...
blob
|
commitdiff
|
raw
|
diff to current
2011-10-17
Dejan Jovanović
Sharing work
blob
|
commitdiff
|
raw
|
diff to current
2011-09-02
Morgan Deters
Merge from my post-smtcomp branch. Includes:
blob
|
commitdiff
|
raw
|
diff to current
2011-07-12
Morgan Deters
fix bug 272, array unsoundness, and some array cleanup
blob
|
commitdiff
|
raw
|
diff to current
2011-02-26
Morgan Deters
Commit to fix bug 241 (improper "using namespace std...
blob
|
commitdiff
|
raw
|
diff to current
2011-01-05
Dejan Jovanović
Commit for the theory engine and rewriter changes....
blob
|
commitdiff
|
raw
|
diff to current