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

Age	Commit message (Collapse)	Author
2016-04-11	Minor fixes for inst match generators. Updates to qip.google	ajreynol

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	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-04-09	Made ProofArray's printing functions non-static, and consequently the data ↵	Guy
	members non-static as well
2016-04-09	cardinality operation for finite sets (based on my thesis / ijcar16 paper)	Kshitij Bansal
	Some further cleanup/fixes pending This is squash of 39 commits (kbansal/card branch + cleanup): * add card operator * local reasoning * towards graph building * first implementation * close cardinality terms * model building * more * more * more * Add aggressive sets rewriting. * Recursively aggressive rewrite sets. * Fix * incomplete card2 implementation * ... * Avoid using auto in sets. * fix merge * more * ... * more * ... * Fixed for loops * Slight modification to computeRelevantTerms * more * .. * more * ... * mv empty set lemma generation to later point * more options/reordering * debug related * more trace * ... * fix merge_nodes, models * rm warnigns * fix compile errors * warning * bug fixes/cleanup * mroe fixes * cleanup * ...
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-03	s_ prefix for static members	Guy

2016-04-03	Removed the theory-specific merge reason types. Instead, added a mechanism ↵	Guy
	for dynamically allocating these tags upon request.
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-31	Improvements to trigger selection, min triggers by default. Optimizations ↵	ajreynol
	for E-matching. Minor work to equality infer.
2016-03-30	Updates to E-matching to avoid entailed instantiations earlier. Minor ↵	ajreynol
	updates to datatypes lemmas, other minor changes.
2016-03-30	Updating the mailmap for git.	Tim King

2016-03-28	Minor cleanup from last commit (quant util, equality infer). Do not set ↵	ajreynol
	fmfBoundIntLazy for stringsExp.
2016-03-28	Implement equality inference module for arithmetic terms. Optimization for ↵	ajreynol
	entailment checks. Other minor infrastructure.
2016-03-24	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-03-24	Refactored the equality engine in order to remove theory-specific logic from ↵	Guy
	equality path reconstruction
2016-03-24	Fixing a garbage collection issue in simplifyWithCare(). Bug 729.	Tim King

2016-03-24	Deleting allocated NodeVecs in ITESimplifier.	Tim King

2016-03-24	Freeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of ↵	Tim King
	CegConjecture.
2016-03-24	Fixing a memory leak in CDInstMatchTrie::d_data.	Tim King

2016-03-24	Fix for a memory leak in InstStrategyCegqi.	Tim King

2016-03-24	Fixing a memory leak in QuantInfo::d_var_mg.	Tim King

2016-03-23	Merge pull request #82 from CVC4/master_for_merge	guykatzz
	Squash-merge from the proof branch
2016-03-23	squash-merge from proof branch	Guy

2016-03-23	Fixing memory leaks in Trigger and TriggerTrie.	Tim King

2016-03-23	Fixed help for tear-down-incremental option	Clark Barrett

2016-03-23	Fixing two garbage collection issues in Region and SortModel.	Tim King

2016-03-22	Deleting the CDInstMatchTries in QuantifiersEngine::d_c_inst_match_trie.	Tim King

2016-03-22	Garbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info.	Tim King

2016-03-22	Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.	Tim King

2016-03-22	Bug fix for define functions + incremental. Minor work on relational triggers.	ajreynol

2016-03-21	Deleting the contents of d_modelGlobalsCommands before it is cleared.	Tim King

2016-03-21	New version of the recursive options parsing strategy.	Tim King

2016-03-18	Limit duplicate propagating instances to avoid exponential behavior in ↵	ajreynol
	QuantConflictFind.
2016-03-16	Change internal representative selection for finite domains that do not ↵	ajreynol
	involve uninterpreted sorts, including bounded integer quantification.
2016-03-12	Add options related to interleaving quantifiers and theory combination, ↵	ajreynol
	changes default behavior.
2016-03-10	Faster conditional rewriting for and/or beneath quantifiers. Improvements to ↵	ajreynol
	sort inference, related to constants. Add several quantifiers options, minor refactoring.
2016-03-08	Extend synthesis solver to handle single invocation with additional ↵	ajreynol
	universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.
2016-03-07	Minor change to F-Length inference in strings. No internal tracking of ↵	ajreynol
	cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
2016-03-03	Add missing code to track dependencies recursively for string explanations ↵	ajreynol
	as well.
2016-03-02	Work towards complete instantiation for datatypes.	ajreynol

2016-03-01	Shorter explanations for strings based on tracking which parts of normal ↵	ajreynol
	forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
2016-02-29	Minor options to datatypes.	ajreynol

2016-02-26	Refactoring of inferences in strings. Add several options.	ajreynol

2016-02-25	Minor improvement to partial qe. Add options for representative selection in ↵	ajreynol
	FMF.
2016-02-24	Add entailment checks between length terms to reduce splitting in strings ↵	ajreynol
	solver. Minor additions to datatypes and qcf.
2016-02-24	Adding the missing clause_id.h file.	Tim King