summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/trigger.h
AgeCommit message (Collapse)Author
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2017-12-02Minor improvements to inst match generator (#1415)Andrew Reynolds
2017-11-28Improve trigger filter instances (#1402)Andrew Reynolds
2017-11-18Ho instantiation (#1204)Andrew Reynolds
* Higher-order instantiation. * Add missing files. * Document inst match generators, make collectHoVarApplyTerms iterative. * More documentation. * More documentation. * More documentation. * More documentation * Refactoring, documentation. * More documentation. * Fix comment, reference issue. * More documentation. Fix ho trigger for the changes from master. * Minor * More documentation. * More documentation. * More * More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive. * More * Minor improvements to comments. * Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator. * Improve documentation for ho_trigger. * Update ho trigger to not access now private member of TermDb. * Address comments. * Address * Clang format
2017-07-07Update copyright headers.Mathias Preiner
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, ↵ajreynol
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2017-03-30Minor fixes for trigger selection max.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-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ajreynol
default in EPR mode.
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ajreynol
not drop patterns from merged prenex (fixes bug 743).
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-06-01Fix to ignore a case of triggers with no free variables.ajreynol
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵ajreynol
do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
2016-04-20update from the masterPaulMeng
2016-04-07Refactor trigger selection, revisions to --relational-trigger. Properly ↵ajreynol
process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
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-03-31Improvements to trigger selection, min triggers by default. Optimizations ↵ajreynol
for E-matching. Minor work to equality infer.
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor ↵ajreynol
updates to datatypes lemmas, other minor changes.
2016-03-23Fixing memory leaks in Trigger and TriggerTrie.Tim King
2016-03-22Bug fix for define functions + incremental. Minor work on relational triggers.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to ↵ajreynol
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-22Enable counterexample-guided quantifier instantiation by default for ↵ajreynol
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
2015-08-16More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. ↵ajreynol
Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
2015-05-15Fixes related to cbqi + E-matching.ajreynol
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ↵ajreynol
how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not ↵ajreynol
assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
2014-09-23Support :no-pattern.ajreynol
2014-09-09Accept user-provided triggers with variable terms. Flush lemmas before ↵ajreynol
quantifiers check. Minor fix for conjecture generation.
2014-08-29Do not use pure theory terms as single triggers. Minor cleanup.ajreynol
2014-08-25New option --purify-triggers. Refactoring of InstMatchGenerator.ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-02-14Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add ↵Andrew Reynolds
support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
2014-01-28More optimizations of quantifier instantiation data structures.Andrew Reynolds
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-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for ↵Andrew Reynolds
boolean terms, improvement for pre skolemization
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed ↵Andrew Reynolds
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2012-11-14replaced all static member data from rewrite rule triggers, added ↵Andrew Reynolds
infrastructure for recognizing quantifier macros
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific ↵Andrew Reynolds
code from quantifiers-specific 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-10-10cleanup up some static data members in the quantifiers codeAndrew Reynolds
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