summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_util.h
AgeCommit message (Collapse)Author
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-02-24Fixes for quantifiers documentation (#3811)Andrew Reynolds
Minor fixes discovered during development of sygus-inst.
2019-09-11Refactoring finite bounds in Quantifiers Engine (#3261)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-04-18Fail fast strategy for propagating instances (#2939)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-09-17Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-30Fixes for quantifiers + incremental (#2009)Andrew Reynolds
2017-11-30Remove remaining references to QuantArith (#1408)Andrew Reynolds
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-14Make QEffort an enum (#1366)Andrew Reynolds
* Make QEffort an enum. * Format * Minor * Fix
2017-11-01(Move-only) Split quant util (#1306)Andrew Reynolds
* Initial draft of splitting quant util. * Minor * Document recursive term builder. * Rename file, minor. * Clang format
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-10-27Document quant arith (#1271)Andrew Reynolds
* Initial documentation, incomplete. * Document arith utilities in quantifiers. * Minor * Clang format * Minor * Clang format. * Minor * Apply new clang format. * Document ordering.
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-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-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-07Update copyright headers.Mathias Preiner
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge ↵Tim King
commit for nlAlgMaster.
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
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-15Refactor setIncomplete in quantifiers.ajreynol
2016-09-14Lemma cache in theory sep. Minor optimization for sets. Minor improvements ↵ajreynol
to EPR
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-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-03Updating the copyright headers and scripts.Tim King
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor ↵ajreynol
updates to datatypes lemmas, other minor changes.
2016-03-28Minor cleanup from last commit (quant util, equality infer). Do not set ↵ajreynol
fmfBoundIntLazy for stringsExp.
2016-03-28Implement equality inference module for arithmetic terms. Optimization for ↵ajreynol
entailment checks. Other minor infrastructure.
2016-03-10Faster conditional rewriting for and/or beneath quantifiers. Improvements to ↵ajreynol
sort inference, related to constants. Add several quantifiers options, minor refactoring.
2015-11-25Infrastructure for partially single invocation properties. Bug fix for ↵ajreynol
unconstrained functions in sygus solver.
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by ↵ajreynol
default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add ↵ajreynol
regressions.
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. ↵ajreynol
Refactor.
2015-02-04Start work on simplifying single inv solutions. Minor.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation ↵ajreynol
--cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.
2015-01-29Restrict LtePartialInst instantiations based on E-matching, promote to ↵ajreynol
quantifiers module. Refactor QuantifiersEngine registration and check.
2015-01-24Variable patterns only look at eligible terms. Minor refactoring of ↵ajreynol
quantifiers check for sat.
2015-01-22Add option --lte-partial-inst. Remove inst-closure.ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified ↵Andrew Reynolds
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback