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

Age	Commit message (Collapse)	Author
2014-04-29	Fix warnings, cleanup in strings typechecker.	Morgan Deters

2014-04-29	Fix compiler warning re: TheoryUF destructor.	Morgan Deters

2014-04-29	Fix simplify output for SMT2 printer.	Morgan Deters

2014-04-29	Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and ↵	Morgan Deters
	rewrite-divk.
2014-04-29	Mostly resolves bug #561 memory leaks, and more.	Morgan Deters

2014-04-29	Fix for --force-logic to extend its reach to the parser.	Morgan Deters

2014-04-29	fixed couple of more warnings	Kshitij Bansal

2014-04-29	fix was compiler warning in antlr_input, crashing test case with the old fix	Kshitij Bansal

2014-04-29	Revert a compiler warning fix from ea6a5a6.	Morgan Deters

2014-04-29	fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr	Tianyi Liang

2014-04-29	add leading zeros support for str.to.int	Tianyi Liang

2014-04-29	Significantly improve performance for producing datatypes models.	ajreynol

2014-04-28	Merge remote-tracking branch 'upstream/master' into sets	Kshitij Bansal

2014-04-28	Merge branch 'master' of github.com:tiliang/CVC4	Tianyi Liang

2014-04-28	add strings-opt2 for regular splitting	Tianyi Liang

2014-04-28	cleanup	Kshitij Bansal

2014-04-28	minor change with kshitij's change	Tianyi Liang

2014-04-28	nodemanager robust skolem numbering	Kshitij Bansal

2014-04-28	add strings-opt2 for regular splitting	Tianyi Liang

2014-04-28	Merge pull request #25 from kbansal/sets	Kshitij Bansal
	Sets
2014-04-28	Preparation for models for co-inductive datatypes. Minor cleanup.	Andrew Reynolds

2014-04-28	Optimizations for datatypes: check for clashes modulo equality. Avoid ↵	ajreynol
	building model at fullModel=false when possible. Minor cleanup.
2014-04-28	minor fix	Kshitij Bansal

2014-04-28	Merge remote-tracking branch 'upstream/master' into sets	Kshitij Bansal

2014-04-28	travis, please!	Kshitij Bansal

2014-04-27	attempt to improve CVC4's "parse error" message	Kshitij Bansal

2014-04-27	rm undocument/non-working* "feature"	Kshitij Bansal
	*test of unsigned for negative
2014-04-24	minor change: add a heuristic for preventing constant splitting.	Tianyi Liang

2014-04-24	optimization	Kshitij Bansal

2014-04-24	Avoid assigning constructor terms to 1-constructor datatype eqcs, when ↵	ajreynol
	possible, to ensure termination for codatatypes. Minor changes.
2014-04-24	Compute care graph for datatypes. Preliminary results show 20x speed up on ↵	Andrew Reynolds
	larger problems. Improve datatypes rewriter.
2014-04-24	Add --inst-max-level=N option for Kshitij. Support define-const command in ↵	Andrew Reynolds
	Smt2.
2014-04-22	Minor fix to avoid rewriting datatype equalities into non-equalitiers, as ↵	Andrew Reynolds
	required. Add APPLY_UF to congruence types to avoid model construction bugs.
2014-04-19	Eh, what?	Kshitij Bansal

2014-04-19	fix warnings in strings/	Kshitij Bansal

2014-04-17	Allow fmf-bound-int to be set with set-option and via API.	Morgan Deters

2014-04-17	simplify mkSkolem naming system: don't use $$	Kshitij Bansal
	Short summary: By default NODEID is appeneded, just continue doing what you were, just don't add the _$$ at the end. Long summary: Before this commit there were four (yes!) ways to specify the names for new skolems, which result in names as given below 1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 2) mkSkolem("name", ..., SKOLEM_EXACT_NAME) -> "name" 3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me" After this commit, only 1) and 2) stay. 90% usage is of 1) or 3), which results in exact same behavior (and looking at the source code it doesn't look like everyone realized that the _$$ is just redundant). Almost no one used 4), which is the only reason to even have $$. Post this commit if you really want a number in the middle, manually construct the name and use the SKOLEM_EXACT_NAME flag.
2014-04-17	use internal skolem numbering	Kshitij Bansal

2014-04-17	Minor refactoring and optimizing.	Andrew Reynolds

2014-04-14	Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵	Andrew Reynolds
	Improve datatypes rewrite, make option for previous dt semantics.
2014-04-14	Add initial support for co-datatypes.	Andrew Reynolds

2014-04-11	Better support for building with mingw64; thanks to Nicolas Roche @ Altran ↵	Morgan Deters
	for the fix.
2014-04-10	setType -> setOfType, resolves bug 556	Morgan Deters

2014-04-10	Fix the build; --check-proof works for UF but not for the new UFC logic.	Morgan Deters

2014-04-10	Expand definitions in theory datatypes, now has the expected semantics for ↵	Andrew Reynolds
	incorrectly applied selector terms.
2014-04-10	Boolean terms conversion fix for datatypes, fixes a problem Andy discovered ↵	Morgan Deters
	on his branch.
2014-04-10	Merge branch 'master' of github.com:tiliang/CVC4	Tianyi Liang

2014-04-10	minor fix for strings	Tianyi Liang

2014-04-10	minor fix for strings	Tianyi Liang

2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.