summaryrefslogtreecommitdiff
path: root/src/theory/subs_minimize.cpp
AgeCommit message (Collapse)Author
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-06Remove template argument from `NodeBuilder` (#6290)Andres Noetzli
Currently, NodeBuilder takes a single template argument: An integer that determines the expected number of arguments. This argument is used to determine the size of the d_inlineNvChildSpace array. This array is used to construct nodes inline. The advantage of this is that we don't have to allocate a NodeValue on the heap for the node under construction until we are sure that the node is new. While templating the array size may save some stack space (or avoid a heap allocation if we statically know that we a fixed number of children and that number is greater than 10), it complicates the code and leads to longer compile times. Thus, this commit removes the template argument and moves some of the NodeBuilder code to a source file for faster compilation. CPU build time before change (debug build): 2429.68s CPU build time after change (debug build): 2228.44s Signed-off-by: Andres Noetzli noetzli@amazon.com
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-06-16Update copyright headers.Aina Niemetz
2020-04-15Convert more cases of strings to words (#4206)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. Co-authored-by: Clark Barrett <barrett@cs.stanford.edu> Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com> Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com> Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu> Co-authored-by: makaimann <makaim@stanford.edu> Co-authored-by: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> Co-authored-by: AleksandarZeljic <zeljic@stanford.edu> Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com> Co-authored-by: Amalee <amaleewilson@gmail.com> Co-authored-by: Scott Kovach <dskovach@gmail.com> Co-authored-by: ntsis <nekuna@gmail.com>
2019-03-26Update copyright headers.Aina Niemetz
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-09-11Support model cores via option --produce-model-cores. (#2407)Andrew Reynolds
This adds support for model cores, fixes #1233. It includes some minor cleanup and additions to utility functions.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback