summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quantifiers_rewriter.h
AgeCommit message (Collapse)Author
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver.
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2017-11-18Names the Effort enum of QuantConflictFind class. (#1354)Tim King
* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043. * Fixing a missed assertion. Fixing a few compiler warnings. * Switching back to an enum from an enum class.
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-06-01Minor optimizations related to cbqi.ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function ↵ajreynol
definitions, add regression.
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-12Refactor prenex modes.ajreynol
2016-09-03Miniscope top level conjunctions for prenex normal form, allow one level ↵ajreynol
miniscoping in prenex normal form.
2016-09-03Option for prenex normal formajreynol
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-06-03Reduce number of passes in quantifiers rewriter.ajreynol
2016-04-20update from the masterPaulMeng
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-17Refactor quantifiers attributes. Make quantifier elimination robust to ↵ajreynol
preprocessing, implement get-qe-disjunct.
2016-02-09Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing ↵ajreynol
to quantifier instantiations.
2016-01-18Bug fix rewriter for fun defs.ajreynol
2015-12-16Work on purification for quantifiers, minor updates.ajreynol
2015-11-12Minor fixes and improvements to purify quant, relational triggers.ajreynol
2015-11-11Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.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-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-10-26Extend counterexample-guided instantiation to extended theory of Int/Real, ↵ajreynol
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
2015-09-10Fix bug 670. Minor.ajreynol
2015-09-06Improve quantifiers rewriter, minor refactoring.ajreynol
2015-08-21Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. ↵ajreynol
Enable redundant ITE branch elimination in quantifiers rewriter.
2015-07-05Add options --partial-triggers, --elim-taut-quant, improve robustness of ↵ajreynol
--purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching. Avoid unecessary delta lemmas. Update casc scripts.
2015-07-01Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor ↵ajreynol
--ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence. Update casc 25 FOF script.
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-01-27Always miniscope nested quantifiers. Disable miniscoping when cegqi ↵ajreynol
enabled. Simplify option names.
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-11-10Do not eliminate variables only occurring in patterns. Minor improvements ↵ajreynol
to sort inference. Remove unused code.
2014-07-01Update copyrights.Morgan Deters
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-05-02Add option --dt-stc-ind for strengthening skolemization. Refactor ↵Andrew Reynolds
skolemization.
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵Andrew Reynolds
Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge.
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-11-26Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ↵Andrew Reynolds
to improve performance of quantifiers rewriter
2013-04-30Add option in quantifiers for clause splittingAndrew Reynolds
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-30do simple ite rewriting within quantifiersAndrew Reynolds
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive ↵Andrew Reynolds
miniscoping option --ag-miniscope-quant, minor cleanup
2012-11-13refactoring of quantifiers rewriter based on code review from yesterday, ↵Andrew Reynolds
refactoring code out of instantiators in preparation for quantifiers equality engine
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.)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback