summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/alpha_equivalence.cpp
AgeCommit message (Collapse)Author
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Eliminate dependencies on quantifiers engine in internal quantifiers code ↵Andrew Reynolds
(#6240) This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned. Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-01Simplify alpha equivalence module (#5839)Andrew Reynolds
This class uses a discrimination tree which can compute subsumption as well as alpha-equivalence. This class was initially designed to also support subsumption. However, we were only using this class for alpha-equivalence and hence (canonized) Node comparison suffices and the class can be simplified. It also makes minor cosmetic updates to the module. If we plan to support subsumption checking later, we will write a new module, and use this class https://github.com/CVC4/CVC4/blob/master/src/expr/match_trie.h which is a more mature version of the class deleted by this PR. Note: I verified that the new and old implementation was equivalent using a temporary AlwaysAssert.
2021-01-26Use term canonizer utility locally in quantifiers (#5823)Andrew Reynolds
Term canonization was used in two places, which are unrelated and don't need to share the instance. Also removes a few unnecessary methods from QuantifiersEngine.
2020-12-02Update copyright headers.Aina Niemetz
2020-10-23Apply alpha equivalence to annotated quantified formulas (#5324)Andrew Reynolds
Previously, alpha equivalence was not applied to quantified formulas with attributes, likely motivated by keeping alpha equivalent quantified formulas with different user patterns. It's not clear this is a good a idea. Moreover, this also implies that quantified formulas with user-provided names (which happens in e.g. Boogie benchmarks) also do not have alpha equivalence applied. This makes it so that we apply alpha equivalence regardless of annotations. FYI @barrettcw
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-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-08-01Move some generic utilities out of quantifiers (#3139)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-08-31Refactor and document alpha equivalence. (#2402)Andrew Reynolds
2018-08-28 Split term canonize utility to own file and document (#2398)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2017-10-09Split term database (#1206)Andrew Reynolds
* Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues.
2017-07-07Update copyright headers.Mathias Preiner
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
Conflicts: proofs/signatures/Makefile.am src/Makefile.am src/expr/datatype.cpp src/options/datatypes_options src/options/options_template.cpp src/options/quantifiers_options src/proof/arith_proof.cpp src/proof/arith_proof.h src/proof/array_proof.cpp src/proof/array_proof.h src/proof/bitvector_proof.cpp src/proof/bitvector_proof.h src/proof/cnf_proof.cpp src/proof/cnf_proof.h src/proof/proof_manager.cpp src/proof/proof_manager.h src/proof/sat_proof.h src/proof/sat_proof_implementation.h src/proof/skolemization_manager.h src/proof/theory_proof.cpp src/proof/theory_proof.h src/proof/uf_proof.cpp src/proof/uf_proof.h src/prop/cnf_stream.cpp src/prop/cnf_stream.h src/prop/minisat/core/Solver.cc src/prop/prop_engine.cpp src/prop/prop_engine.h src/prop/theory_proxy.cpp src/smt/smt_engine.cpp src/smt/smt_engine_check_proof.cpp src/theory/arrays/array_proof_reconstruction.cpp src/theory/arrays/theory_arrays.cpp src/theory/bv/eager_bitblaster.cpp src/theory/bv/lazy_bitblaster.cpp src/theory/datatypes/theory_datatypes.cpp src/theory/quantifiers/alpha_equivalence.cpp src/theory/quantifiers/candidate_generator.cpp src/theory/quantifiers/candidate_generator.h src/theory/quantifiers/ce_guided_single_inv.cpp src/theory/quantifiers/ceg_instantiator.cpp src/theory/quantifiers/conjecture_generator.cpp src/theory/quantifiers/equality_infer.cpp src/theory/quantifiers/equality_infer.h src/theory/quantifiers/inst_match_generator.cpp src/theory/quantifiers/inst_propagator.cpp src/theory/quantifiers/inst_propagator.h src/theory/quantifiers/inst_strategy_e_matching.cpp src/theory/quantifiers/inst_strategy_e_matching.h src/theory/quantifiers/instantiation_engine.cpp src/theory/quantifiers/model_builder.cpp src/theory/quantifiers/model_engine.cpp src/theory/quantifiers/quant_conflict_find.cpp src/theory/quantifiers/quant_conflict_find.h src/theory/quantifiers/quant_split.cpp src/theory/quantifiers/quant_util.cpp src/theory/quantifiers/quantifiers_rewriter.cpp src/theory/quantifiers/quantifiers_rewriter.h src/theory/quantifiers/term_database.cpp src/theory/quantifiers/term_database.h src/theory/quantifiers/trigger.cpp src/theory/quantifiers/trigger.h src/theory/quantifiers_engine.cpp src/theory/quantifiers_engine.h src/theory/sets/kinds src/theory/sets/theory_sets_private.cpp src/theory/sets/theory_sets_private.h src/theory/sets/theory_sets_rewriter.cpp src/theory/sets/theory_sets_type_rules.h src/theory/strings/theory_strings.cpp src/theory/strings/theory_strings.h src/theory/theory_engine.cpp src/theory/theory_engine.h src/theory/uf/equality_engine.cpp test/regress/regress0/fmf/Makefile.am test/regress/regress0/quantifiers/Makefile.am test/regress/regress0/strings/Makefile.am test/regress/regress0/sygus/Makefile.am test/regress/regress0/sygus/max2-univ.sy
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value ↵ajreynol
instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
2016-04-20update from the masterPaulMeng
2016-04-13Minor improvements for alpha equivalence and partial quantifier elimination ↵ajreynol
in incremental mode. Change defaults to addInstantiation method.
2016-04-04New options for trigger selection, add option --strict-triggers. Do not ↵ajreynol
infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of ↵ajreynol
reductions in quantifiers engine.
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-09-18Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding ↵ajreynol
quantified formulas with non-constant polarity.
2015-09-10Fix bug 670. Minor.ajreynol
2015-06-29Module to infer alpha equivalence of quantified formulas. Minor clean up of ↵ajreynol
options.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback