summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/relevant_domain.h
AgeCommit message (Collapse)Author
2021-05-21Fix and refactor relevant domain (#6528)Andrew Reynolds
In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables. This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility. Fixes #6476. The benchmark from that issue now times out.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-30Miscellaneous elimination of dependencies on quantifiers engine (#6238)Andrew Reynolds
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class. Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
2021-01-28Use standard equality engine information in quantifiers state (#5824)Andrew Reynolds
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState. This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
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
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
* Add arithmetic monomial sum utility. * Clang format * Fix * Address review. * Fix missed comment. * Format * Fix
2017-10-28Document term db (#1220)Andrew Reynolds
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206. * Minor * Minor * Change namespace style. * Address review * Fix incorrectly merged portion that led to regression failures. * New clang format, fully document relevant domain. * Clang format again. * Minor
2017-07-07Update copyright headers.Mathias Preiner
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ↵ajreynol
Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
2016-11-02Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.ajreynol
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-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-09-29Address some coverity warnings, add another stat.ajreynol
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
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-04-20update from the masterPaulMeng
2016-04-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ↵ajreynol
instantiation propagator.
2016-04-03Updating the copyright headers and scripts.Tim King
2015-11-17Improve relevant domain computation for arithmetic, full saturation ↵ajreynol
strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.
2015-11-12Minor fixes and improvements to purify quant, relational triggers.ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out ↵Andrew Reynolds
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
2014-01-26More optimization of QCF. Fixed InstMatchTrie for caching instantiations. ↵Andrew Reynolds
Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-09add relevant domain computationAndrew Reynolds
2013-05-23Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.Andrew Reynolds
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan 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-08-31merge from fmf-devel branch. more updates to models: now with ↵Andrew Reynolds
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-07-31Moving some instantiation-related stuff from src/theory to ↵Morgan Deters
src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat. The namespaces weren't changed, only the file locations.
2012-07-27Minor cleanup after today's commits:Morgan Deters
* change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and ↵Andrew Reynolds
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback