summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_util.cpp
AgeCommit message (Collapse)Author
2019-04-18Fail fast strategy for propagating instances (#2939)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2017-11-30Remove remaining references to QuantArith (#1408)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-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-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.
2017-03-29Add quantifiers options related to model and master equality engine.ajreynol
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-12-06Improve bounds for global heap in sep, refactor preprocessing. Minor ↵ajreynol
improvement to sets.
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-09-13Minor changes to sep logic, epr, quantifier splitting.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-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-04-28More work on inst propagate. Optimization for qcf to check instances ↵ajreynol
eagerly. Improvements to equality query for disequalities.
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
2016-04-01Improvements to equality inference module: add missing cases for solvable ↵ajreynol
variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.
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-02-11More aggressive conditional rewriting for quantified formulas. Bug fix set ↵ajreynol
incomplete for fmc.
2015-11-25Infrastructure for partially single invocation properties. Bug fix for ↵ajreynol
unconstrained functions in sygus solver.
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-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2015-08-24Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ↵ajreynol
symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
2015-08-21Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. ↵ajreynol
Enable redundant ITE branch elimination in quantifiers rewriter.
2015-06-16Avoid completion for large finite types. Fix bug for --fmf-fun.ajreynol
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-11-16Add term db mode. Minor changes to quantifiers rewriter: split ITE's where ↵ajreynol
equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup.
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.
2013-05-22Significant work on bounded integer quantification to handle non-trivial ↵Andrew Reynolds
bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback