cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2018-08-24	Clean up quantifiers engine initialization. (#2371)	Andrew Reynolds

2018-07-02	Remove miscellaneous dead and unused code from quantifiers (#2121)	Andrew Reynolds

2018-06-25	Updated copyright headers.	Aina Niemetz

2018-05-30	Fixes for quantifiers + incremental (#2009)	Andrew Reynolds

2018-05-27	Fix cegqi assertions for quantified non-linear cases. (#1999)	Andrew Reynolds

2018-03-23	Remove unused code (#1700)	Andrew Reynolds

2018-03-06	Simplify initialization of quantifiers engine (#1641)	Andrew Reynolds

2018-02-02	Option to check solutions produced by SyGuS solver (#1553)	Haniel Barbosa

2017-12-06	Remove CDChunkList (#1414)	Andres Noetzli

2017-11-24	(Refactor) Instantiate utility (#1387)	Andrew Reynolds

2017-11-14	Make 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-11-01	(Refactor) Split term util (#1303)	Andrew Reynolds
	* Fix some documentation. * Move model basis out of term db. * Moving * Finished moving. * Document Skolemize and term enumeration. * Minor * Model basis to first order model. * Change function name. * Minor * Clang format. * Minor * Format * Minor * Format * Address review.
2017-10-28	(Move only) Move enumerative instantiation strategy to its own file and ↵	Andrew Reynolds
	document (#1290) * Move, document, and rename enumerative instantiation. * Clang format.
2017-10-28	Document 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-10	Fix memory leak in quantifiers engine (#1219)	Andres Noetzli
	Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak where d_quant_attr was not deleted when the QuantifiersEngine was destroyed. This commit fixes the issue by turning d_quant_attr into an std::unique_ptr.
2017-10-09	Split 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-09-29	Simplify representation of inversion Skolems for bv cegqi (#1164)	Andrew Reynolds
	* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression. * Enable other regression
2017-07-20	Moving from the gnu extensions for hash maps to the c++11 hash maps	Tim 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-07	Update copyright headers.	Mathias Preiner

2017-06-01	Minor optimizations related to cbqi.	ajreynol

2017-05-15	Make conflict-based instantiation abort if a ground conflict is found in the ↵	ajreynol
	master equality engine during term indexing, fixes bug 801.
2017-03-29	Add quantifiers options related to model and master equality engine.	ajreynol

2017-03-27	Making ppNotifyAssertions take a const vector.	Tim King

2016-12-29	Adding a destructor to InstantiationNotify.	Tim King

2016-12-07	Refactoring, generalization of bounded inference module. Simplification of ↵	ajreynol
	rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
2016-11-21	Refactoring related to track instantiation option.	ajreynol

2016-11-03	Add priorities to getNextDecision. Properly handle case for finite types + ↵	ajreynol
	unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-10-28	Add get instantiations utilities to API.	ajreynol

2016-09-29	Address some coverity warnings, add another stat.	ajreynol

2016-09-29	Minor cleanup and additions to quantifiers statistics.	ajreynol

2016-09-14	Lemma cache in theory sep. Minor optimization for sets. Minor improvements ↵	ajreynol
	to EPR
2016-09-01	Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested ↵	ajreynol
	quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
2016-08-26	Basic support for EPR+CBQI. Minor cleanup.	ajreynol

2016-08-25	Minor cleanup preprocessing, add ppNotifyAssertions.	ajreynol

2016-07-26	Add option to minimize sygus solutions based on using weakest implicants of ↵	ajreynol
	instantiations in unsat cores.
2016-07-19	Add 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-05-15	Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. ↵	ajreynol
	Enable e-matching when --strings-exp is enabled.
2016-05-06	Minor clean up, fixes related to sygus.	ajreynol

2016-05-05	Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵	ajreynol
	irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
2016-04-28	More work on inst propagate. Optimization for qcf to check instances ↵	ajreynol
	eagerly. Improvements to equality query for disequalities.
2016-04-13	Minor improvements for alpha equivalence and partial quantifier elimination ↵	ajreynol
	in incremental mode. Change defaults to addInstantiation method.
2016-04-12	Optimizations for QCF to check relevant domain of variable argument ↵	ajreynol
	positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
2016-04-10	More work on instantiation propagation. Enable external filtering of ↵	ajreynol
	instantiations. All quantifiers strategies terminate when a conflict can be established.
2016-04-09	Minor refactoring of entailment tests and quantifiers util. Initial draft of ↵	ajreynol
	instantiation propagator.
2016-04-07	Refactor 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-04	New 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-03	Updating the copyright headers and scripts.	Tim King

2016-04-01	Improvements 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-28	Implement equality inference module for arithmetic terms. Optimization for ↵	ajreynol
	entailment checks. Other minor infrastructure.