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

Age	Commit message (Collapse)	Author
2016-08-26	Basic support for EPR+CBQI. Minor cleanup.	ajreynol

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

2016-08-25	Options for counterexample guided instantiation.	ajreynol

2016-08-16	Initial infrastructure for ExtTheory, generalize extended term handling in ↵	ajreynol
	TheoryStrings to use this.
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-08-11	Minor change to strings, introduce proxy vars only when necessary.	ajreynol

2016-08-10	Improvements to strings: work on propagations for reverse normal form ↵	ajreynol
	processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
2016-08-09	Fixes for sep star rewrite.	ajreynol

2016-07-30	Prioritize inferences when processing normal forms in strings.	ajreynol

2016-07-28	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-07-28	Bug fix involving negated lemmas	Guy

2016-07-28	Fix bug 749.	ajreynol

2016-07-28	Add the negative conjunction case	Guy

2016-07-27	Proper instrumentation of the preprocessing phase	Guy

2016-07-27	proper handling of ITEs	Guy

2016-07-27	Proper handling of IFF lemmas in the unsat core.	Guy
	Don't return duplicates in the unsat core
2016-07-26	Add option to minimize sygus solutions based on using weakest implicants of ↵	ajreynol
	instantiations in unsat cores.
2016-07-26	Minor improvements to strings related to constant splitting, including a few ↵	ajreynol
	options (disabled by default).
2016-07-25	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-07-24	cleanup	Guy

2016-07-24	Proper handling for lemmas that are conjuncts:	Guy
	Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked. Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.
2016-07-22	Minor, error handling for polymorphism + sep logic.	ajreynol

2016-07-21	Fixes for strings, explanations for constant split propagations, substr ↵	ajreynol
	under concat rewrite. Avoid duplicate re.range length lemmas.
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-20	Infer conflicts in strings based on abstracting equality as contains. Minor ↵	ajreynol
	cleanup.
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-16	Refactor strings extf evaluation info. Ensure strings eager preprocess ↵	ajreynol
	eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.
2016-07-15	The ProofManager now allows theory solvers to get their lemmas that ↵	Guy
	participate in the unsat cores. Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations and conflict lemmas.
2016-07-15	Minor simplification to normal form explanations.	ajreynol

2016-07-08	Minor fix to last commit.	ajreynol

2016-07-07	Simplifications for strings normal forms, fix case for concat reps in normal ↵	ajreynol
	forms.
2016-07-07	Ensure heap disjointness in sep refinements.	ajreynol

2016-07-07	Refactoring of strings preprocess module. When enabled, apply eager ↵	ajreynol
	preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
2016-07-06	A few proof bugs fixed	Guy

2016-07-06	Minor cleanup in strings, mostly related to negated str.contains.	ajreynol

2016-07-06	Add comment field for model, resolves hack for printing sep logic models.	ajreynol

2016-07-05	Refactor last call for theories, only create one model when quantifiers are ↵	ajreynol
	enabled. Fix sep.nil preregistration in TheorySep.
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-20	Minor change to sep/kinds	ajreynol

2016-06-20	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-06-20	Fixed a bug where the proofManager's init() call was not getting called, ↵	Guy
	resutling a null point deference
2016-06-18	Fix unit test.	ajreynol

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-06	Merge pull request #85 from CVC4/master_for_proof_merge	guykatzz
	Merge from proof branch
2016-06-03	Remove NodeListMap from datatypes and equality inference. Add option ↵	ajreynol
	--dt-blast-splits.
2016-06-03	Remove NodeListMap from strings, fixes memory leaks. Fix for regexp ↵	ajreynol
	intersection.
2016-06-03	Simple memory fixes, minor cleanup in quantifiers.	ajreynol