summaryrefslogtreecommitdiff
path: root/src/theory/substitutions.cpp
AgeCommit message (Collapse)Author
2021-04-22Minor improvements to substitutions (#6380)Andrew Reynolds
In preparation for using this class as part of our proof checker. This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
This renames everything but GitHub links and build system related macros. Switching the build system to cvc5 will be the last step in the renaming process.
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-02-26Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)Gereon Kremer
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943). This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior. We now use this new option in an assertion in the non-clausal simplification. Fixes #5943.
2020-12-02Rename macro Message to CVC4Message. (#5576)Aina Niemetz
2020-10-02Minor simplifications to substitution map class (#5180)Andrew Reynolds
This class is an important utility in preprocessing, which we are adding proof support for. This simplifies the interface of this class with regards to unused interfaces for clarity.
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-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-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-06-25Updated copyright headers.Aina Niemetz
2017-07-07Update copyright headers.Mathias Preiner
2016-04-20update from the masterPaulMeng
2014-07-01Update copyrights.Morgan Deters
2014-03-28rm old unused codeKshitij Bansal
2013-09-24Reduce compiler dependencies on substitutions.h,Clark Barrett
Some new functionality in substitutions.h/cpp
2013-09-23Revert Clark's last commit, at his request; there are some bugs.Morgan Deters
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
for faster compilation
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-10Abstract values for SMT-LIB.Morgan Deters
Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-12Adding model assertions after SAT responses.Morgan Deters
To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too. By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems: make regress CVC4_REGRESSION_ARGS=--check-models To see it work, use -v in addition to --check-models. There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state. --check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting). Also: * TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants) * The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2) * The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
2012-06-14New substitutions implementation - fixes performance issue seen in nonclausalClark Barrett
simplification for some benchmarks
2012-06-14The "no-tears-in-competition-mode" commit. Change all (non-driver, ↵Morgan Deters
non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.
2012-06-12Adding constant propagation code - needs more testing - off by defaultClark Barrett
2012-06-06disabling a super-expensive assertions to speed up debug runsDejan Jovanović
2012-06-05Fixed a performance issue with unconstrained simplifierClark Barrett
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2011-10-05remove some debugging code that slowed down last night's regressionsMorgan Deters
2011-10-04fixes to context-dependent caching substitutionsMorgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback