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

Age	Commit message (Collapse)	Author
2015-02-26	Robust strategy for single invocation LIA synthesis conjectures. Add ↵	ajreynol
	regressions.
2015-02-13	Handle recursive singleton case for codatatypes, add regression. Simplify ↵	ajreynol
	implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
2015-02-05	Minor clean up	Tianyi Liang

2015-02-05	Improved string performance, thanks to Peter's benchmarks.	Tianyi Liang

2015-01-20	Mark datatypes as sygus. Add option to normalize sygus terms in search. ↵	ajreynol
	Add sygus regressions.
2015-01-19	Adding tests for get-value output for arithmetic.	Tim King
	Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.
2015-01-14	sygus input language and benchmark	Morgan Deters

2015-01-11	adjusted to both v2.0 and v2.5 string literals	Tianyi Liang

2015-01-09	blocked unprintable characters in string literals;	Tianyi Liang
	disabled string literal test case for smtlib v2.5
2015-01-07	bug fix, thanks to Pierre's report	Tianyi Liang

2014-12-28	Disable prenex by default when using fmf bound int, minor improvement to ↵	ajreynol
	datatypes rewriter
2014-12-04	Relaxed the constant requirement for regular expression loop;	Tianyi Liang
	Added "ignoring negative membership" option (fragment checking is not provided, and users must make sure the constraint is in the fragment; otherwise, the solution may not be correct).
2014-11-26	add intersection rewriting	Tianyi Liang

2014-11-21	Throw error when pattern is not list of terms.	ajreynol

2014-11-21	Change default option to --inst-when=full-last-call (interleave ↵	ajreynol
	instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
2014-11-20	Disable constants sharing in eq engine, disable hack in theory engine. ↵	ajreynol
	Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
2014-11-18	Compute model basis only for fmf. Add another co-datatype regression.	ajreynol

2014-11-18	Add local theory extensions instantiation strategy (incomplete). Refactor ↵	ajreynol
	how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
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-09	Merge branch '1.4.x'	Morgan Deters

2014-11-09	Increase stack size when running regressions (fixes some regression crashes ↵	Morgan Deters
	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	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	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	Reenable regression. Add (for now, disabled) changes to datatypes theory ↵	ajreynol
	combination. Relax communication of dt facts.
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	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-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-22	Fix bug590 regression distcheck failure from last night.	Morgan Deters

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

2014-10-10	Merge remote-tracking branch 'origin/1.4.x'	Kshitij Bansal

2014-10-10	Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵	Kshitij Bansal
	Rabitti for the report.
2014-10-06	Merge branch '1.4.x'	Morgan Deters

2014-10-06	Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.	Morgan Deters

2014-10-06	Merge branch '1.4.x'	Morgan Deters

2014-10-06	fix for bug586	Kshitij Bansal

2014-10-06	Extended parsing testcase, with constant arrays and RESET.	Morgan Deters

2014-10-06	Merge branch '1.4.x'	Morgan Deters
	Conflicts: test/regress/regress0/arrays/Makefile.am
2014-10-06	Fix native language parsing of chained-store expressions (resolves bug 585). ↵	Morgan Deters
	Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.
2014-10-04	Enable some old bug testcases that (maybe?) never got added.	Morgan Deters