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

Age	Commit message (Collapse)	Author
2014-11-10	Bug 593 fix: if the type is finite, it is now considered for detecting ↵	Dejan Jovanović
	theories of nested terms.
2014-11-10	Do not eliminate variables only occurring in patterns. Minor improvements ↵	ajreynol
	to sort inference. Remove unused code.
2014-11-09	Merge branch '1.4.x'	Morgan Deters

2014-11-09	Work around an apparent bug in libc++ that was causing crashes on Mac..	Morgan Deters

2014-11-09	Fix a deterministic assignment-ordering for get-assignment (fixes a ↵	Morgan Deters
	regression failure on Mac).
2014-11-09	Fix dt shared terms issue, reenable regression.	ajreynol

2014-11-08	Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵	ajreynol
	bug484, enable parsing_ringer.
2014-11-07	Remove some unused variables.	Morgan Deters

2014-11-07	Fixed bug in model builder with subtypes	Clark Barrett

2014-11-07	Remove some dead code.	Morgan Deters

2014-11-07	Fix a memory leak in SatSolverRegistry (re: bug #594).	Morgan Deters

2014-11-07	Fix memory issues in bitvector theory, which is now valgrind-clean (mostly ↵	Morgan Deters
	resolves bug #594).
2014-11-07	Merge branch '1.4.x'	Morgan Deters
	Conflicts: src/smt/model_postprocessor.cpp test/regress/regress0/Makefile.am
2014-11-07	Fix missing case in Boolean terms rewriting. (Resolves bug #596.)	Morgan Deters

2014-11-07	Merge branch '1.4.x'	Morgan Deters
	Conflicts: src/smt/model_postprocessor.cpp
2014-11-07	Corrected fix for missing case in model postprocessor (resolves bug #595).	Morgan Deters

2014-11-07	Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor ↵	ajreynol
	improvement to performance of E-matching.
2014-11-07	Revert "Fix missing case in model postprocessor (resolves bug #595)."	Morgan Deters
	This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.
2014-11-07	Revert "Fix missing case in model postprocessor (resolves bug #595)."	Morgan Deters
	This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am
2014-11-07	Merge branch '1.4.x'	Morgan Deters
	Conflicts: test/regress/regress0/Makefile.am
2014-11-07	Fix missing case in model postprocessor (resolves bug #595).	Morgan Deters

2014-11-07	Properly distinguish which EQC to assign values in datatypes, use ↵	ajreynol
	assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
2014-11-06	Minor fix for getInstCons	ajreynol

2014-11-06	Reenable regression. Add (for now, disabled) changes to datatypes theory ↵	ajreynol
	combination. Relax communication of dt facts.
2014-11-05	Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.	ajreynol

2014-11-05	More work on datatypes theory combination: fix bug in care graph, do not ↵	ajreynol
	assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
2014-11-01	Added cache to getModelValue	Clark Barrett

2014-11-01	Fix cegqi for synthesis without syntax.	ajreynol

2014-11-01	Simplify which lemmas to communicate in dt.	ajreynol

2014-11-01	Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in ↵	ajreynol
	lemmas being rewritten). Minor improvement to dt care graph. Reenable regressions.
2014-11-01	Fix some mistakes in datatypes theory combination, disable two regressions. ↵	ajreynol
	Minor fix for fun defs.
2014-10-31	Do not allow duplication of function definitions. Set incomplete flag in ↵	ajreynol
	model builder.
2014-10-30	Be more lazy about generating array lemmas	Clark Barrett

2014-10-29	Added new, much faster, care graph computation for arrays	Clark Barrett
	Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors
2014-10-28	Preprocessing step for finding finite runs of well-defined function ↵	ajreynol
	definitions using FMF.
2014-10-28	Initial infrastructure for function definition quantifiers, internal parsing ↵	ajreynol
	format for Smt2.
2014-10-28	Improve stats in conjecture generator, minor cleanup.	ajreynol

2014-10-25	Minor fix for --user-pat=resort	ajreynol

2014-10-24	Fix typo.	Morgan Deters

2014-10-24	Minor parser performance fix.	Morgan Deters

2014-10-24	Add --user-pat=resort. Minor cleanup of options.	ajreynol

2014-10-23	Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.	Morgan Deters
	* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-10-23	Fixed inefficiency in bit-vector rewrite rule.	lianah

2014-10-21	Fixed bug 589	Tianyi Liang

2014-10-21	Fixed bug 590, added regression test	Clark Barrett

2014-10-20	Minor cleanup in datatypes.	ajreynol

2014-10-19	Finish sets type enumerator implementation.	Kshitij Bansal

2014-10-19	fix statistic in decision engine	Kshitij Bansal

2014-10-18	Fix assertion.	ajreynol

2014-10-18	Add dt lemma: zero size implies nullary constructor.	ajreynol