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

Age	Commit message (Collapse)	Author
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-25	Fixed unit test	Liana Hadarean

2016-05-24	Fixed build issue due to dummy Cryptominisat constructor.	Liana Hadarean

2016-05-24	Forgot to add second patch file.	Liana Hadarean

2016-05-24	Merged cryptominisat from experimental branch.	Liana Hadarean

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-21	Minor fix for strings.	ajreynol

2016-05-20	Minor fix to strings, cleanup in datatypes.	ajreynol

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-20	Updated AUTHORS file	Clark Barrett

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	Fix memory leak in interactive_shell.cpp	Clark Barrett

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	Fix for --inst-max-level	ajreynol

2016-05-10	Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor ↵	ajreynol
	optimizations to sygus and qcf.
2016-05-09	Re-enabling ite simplification in incremental mode - no reason why	Clark Barrett
	it should be a problem.
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-05	Removing a null pointer reference that was found by -fsanitize=null.	Tim King

2016-05-04	Update to COPYING	Clark Barrett

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-30	Reviewed Tim's Asan changes and improved SatProof comments.	Liana Hadarean

2016-04-28	Workaround for a problem in clang	Clark Barrett

2016-04-28	More work on inst propagate. Optimization for qcf to check instances ↵	ajreynol
	eagerly. Improvements to equality query for disequalities.
2016-04-27	Adding an example lsan supression file.	Tim King

2016-04-26	Fixing memory leaks for garbage collection of ResChains in the sat proof ↵	Tim King
	implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.
2016-04-26	Fixing a memory leak of the ProofManager.	Tim King

2016-04-19	Fixed typo	Clark Barrett

2016-04-18	More fixes for python interface	Clark Barrett

2016-04-15	Rolling back the rewrite code	Guy

2016-04-15	Fix for bug 717	Clark Barrett

2016-04-15	Fixes for python bindings	Clark Barrett

2016-04-14	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-04-14	Remove some no-longer-required rewrites of array lemmas	Guy

2016-04-14	Add option --snorm-infer-eq to infer equalities based on normalization in ↵	ajreynol
	ArithCongruenceManager at standard effort (disabled by default).
2016-04-14	Add missing function for regexp to expr manager.	ajreynol

2016-04-13	Update native language support for strings.	ajreynol

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	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 * ...