summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.h
AgeCommit message (Collapse)Author
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-08-22 More unused code elimination (#2358)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-07Update copyright headers.Mathias Preiner
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.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-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and ↵ajreynol
minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
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-13Minor improvements for alpha equivalence and partial quantifier elimination ↵ajreynol
in incremental mode. Change defaults to addInstantiation method.
2016-04-10More work on instantiation propagation. Enable external filtering of ↵ajreynol
instantiations. All quantifiers strategies terminate when a conflict can be established.
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-24Fixing a memory leak in CDInstMatchTrie::d_data.Tim King
2016-02-17Refactor quantifiers attributes. Make quantifier elimination robust to ↵ajreynol
preprocessing, implement get-qe-disjunct.
2016-02-16Public interface for quantifier elimination. Minor changes to datatypes ↵ajreynol
rewriter.
2015-11-28Initial work on --cegqi-si-partial, refactoring.ajreynol
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-09-25Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ↵ajreynol
of term database, other refactoring. Bug fixes for cbqi+datatypes.
2015-04-26Bug fixes and improvements for mbqi with theory symbols, TheoryModel ↵ajreynol
fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
2014-07-01Update copyrights.Morgan Deters
2014-05-14Finish --dump-instantiations option. Update scripts.Andrew Reynolds
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ↵Andrew Reynolds
assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
2014-05-08Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. ↵Andrew Reynolds
Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
2014-01-28More optimizations of quantifier instantiation data structures.Andrew Reynolds
2014-01-27More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.Andrew Reynolds
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-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ↵Andrew Reynolds
for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as ↵Andrew Reynolds
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2013-01-28made QuantifiersEngine::d_inst_match_trie and ↵Andrew Reynolds
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
2012-11-18support for quantifiers macros, bug fix for bug 454 involving E-matching ↵Andrew Reynolds
Array select terms (thanks for the bug report Francois)
2012-11-02more minor updates to inst gen and representative selection, clean up of ↵Andrew Reynolds
equality query
2012-10-31cleaning up some of the equality query stuff, implemented a new ↵Andrew Reynolds
representative selection strategy for quantifier instantiation
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific ↵Andrew Reynolds
code from quantifiers-specific code
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of ↵Andrew Reynolds
quantifiers code
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-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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback