summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/alpha_equivalence.cpp
AgeCommit message (Collapse)Author
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