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

Age	Commit message (Collapse)	Author
2016-08-15	Enable bounded set membership with --fmf-bound. Map to term models for ↵	ajreynol
	bounded set membership.
2016-08-12	Minor fixes to model construction to take singleton equivalence classes into ↵	ajreynol
	account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
2016-07-28	Fix bug 749.	ajreynol

2016-07-26	Add option to minimize sygus solutions based on using weakest implicants of ↵	ajreynol
	instantiations in unsat cores.
2016-07-20	Infrastructure for storing and printing heap models for separation logic. ↵	ajreynol
	Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
2016-07-20	Print only instantiations that are in the unsat core when --proof is ↵	ajreynol
	enabled. Add option to minimize sygus solutions based on unsat core (disabled by default).
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-07-05	Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵	ajreynol
	not drop patterns from merged prenex (fixes bug 743).
2016-06-17	Cleanup from last commit, treat sep.nil as variable kind.	ajreynol

2016-06-17	Support for separation logic. Enable cbqi by default for pure BV.	ajreynol

2016-06-03	Remove NodeListMap from datatypes and equality inference. Add option ↵	ajreynol
	--dt-blast-splits.
2016-06-03	Simple memory fixes, minor cleanup in quantifiers.	ajreynol

2016-06-03	Reduce number of passes in quantifiers rewriter.	ajreynol

2016-06-01	Fix to ignore a case of triggers with no free variables.	ajreynol

2016-06-01	Initial infrastructure for bounded set quantification (disabled). ↵	ajreynol
	Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
2016-05-26	Use term indexing in TheoryUF::computeCareGraph. Do not reject model value ↵	ajreynol
	instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
2016-05-24	Improvements to symmetry breaking in sygus search. Minor fix for getting ↵	ajreynol
	instantiations of non-registered quantifiers in sygus.
2016-05-23	Fix related to parametric sorts whose interpretation is finite due to ↵	ajreynol
	uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
2016-05-20	Improvements to theory combination + strings: do not return trivial care ↵	ajreynol
	graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
2016-05-18	Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵	ajreynol
	Minor fixes for inst max level.
2016-05-17	Minor fix cbqi for constant monomials.	ajreynol

2016-05-16	Enable --sygus-direct-eval by default, limit to terms that do not induce ↵	ajreynol
	Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
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-12	Add casc scripts. Improvements to qcf related to nested quantifiers and ↵	ajreynol
	variable ordering.
2016-05-10	Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor ↵	ajreynol
	optimizations to sygus and qcf.
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-05-02	Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵	ajreynol
	do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
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-13	Handle parametric datatypes with --quant-ind. Minor updates.	ajreynol

2016-04-12	Bug fixes related to parametric datatypes + theory combination + ↵	ajreynol
	quantifiers. Add regression.
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-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	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-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-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	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	Fixing memory leaks in Trigger and TriggerTrie.	Tim King

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