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

Age	Commit message (Collapse)	Author
2015-11-05	Merging the google branch back into master.	Tim King

2015-11-05	Fixes some initialization and desctruction problems in quantifiers. Also ↵	Tim King
	restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
2015-11-05	This commit slightly generalizes the scripts for generating the _tags files.	Tim King

2015-11-04	Better combination of UF with cbqi, refactor quantifiers intialization.	ajreynol

2015-11-03	Fixing typo.	Tim King

2015-11-03	Adding a test to ensure the <build>/src/theory directory is available to the ↵	Tim King
	scripts in src/Makefile.am. This should fix a bug in building the debian packages.
2015-10-31	Improvements to handling of mixed Int/Real quantifiers.	ajreynol

2015-10-29	Removes an extra dollar sign from src/options/mktagheaders. The extra dollar ↵	Tim King
	sign came in as a copy paste from a Makefile. This was not proper bash.
2015-10-27	Adding the new mkdirs script to EXTRA_DIST. This should fix the failing ↵	Tim King
	nightly distcheck.
2015-10-26	This commit fixes a bug related to a public header depending on a compiler ↵	Tim King
	flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information.
2015-10-26	This commit removes using absolute paths in the generation of the .subdirs ↵	Tim King
	file. This also rearranges generation of the file so that one .subdirs file is generated once per Makefile.am file. This keeps using relative paths clean.
2015-10-26	This commit moves the scripts for building the Debug_tags, Traces_tags, ↵	Tim King
	Debug_tags.h and Trace_tags.h out of options/Makefile.am and into seperate scripts. This also enables these files always being created.
2015-10-26	This fixes a one definition rule violation for reduceDB_lt in Solver.cc in ↵	Tim King
	minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *.
2015-10-26	Promote InstStrategyCbqi to quantifier module. Cleanup unused code.	ajreynol

2015-10-26	Extend counterexample-guided instantiation to extended theory of Int/Real, ↵	ajreynol
	mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
2015-10-24	Fixes related to string contains.	ajreynol

2015-10-23	This removes a bug for reading data that has been popped from the back of a ↵	Tim King
	vector using a stale reference in the unconstrained simplifier.
2015-10-23	Specify that the default initialization must always be done for ↵	Tim King
	CDOhash_map's data field. Without doing this, there exists a loop where uninitialized data can be read. This can happen if T is a type like bool. The trace goes: CDOhash_map::set(data) calls ContextObj::make_current(). Now (d_pScope->isCurrent()) is false. So ContextObj::make_current() calls ContextObj::update(). ContextObj::update() calls CDOhash_map::save(). CDOhash_map::save() calls return new(pCMM) CDOhash_map(*this) which calls the copy constructor which reads the data using d_data(other.d_data).
2015-10-23	Switching Options::current() to return a pointer. This helps avoid undefined ↵	Tim King
	behavior due to dereferencing a null pointer in the future.
2015-10-23	This patch slightly generalizes how the std::isfinite function in <cmath> is ↵	Tim King
	referred.
2015-10-22	Enable counterexample-guided quantifier instantiation by default for ↵	ajreynol
	quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
2015-10-21	Minor refactoring in strings related to length.	ajreynol

2015-10-20	Refactor strings, remove old cycle checks in normalize eqc.	ajreynol

2015-10-20	Clean up explanations involving string length. Add regression.	ajreynol

2015-10-19	Improve stratification of strings extended function reductions, add ↵	ajreynol
	regressions. Eliminate preprocess for regexp.
2015-10-19	Improve regexp rewriter, simplify regexp preprocess, add basic trans closure ↵	ajreynol
	for string contains, refactoring.
2015-10-18	Fix for no condense func values.	ajreynol

2015-10-16	Add option to interleave enumerative instantiation with other strategies.	ajreynol

2015-10-16	Throw error for recursively defined types involving Boolean.	ajreynol

2015-10-16	Fix for codatatype constant rewrite, add regression.	ajreynol

2015-10-15	Fix congruence check in strings, fixes bug 686.	ajreynol

2015-10-15	Change semantics of str.substr to allow endpoint out of bounds, and return ↵	ajreynol
	empty string for error conditions. Improve rewriter for str.substr.
2015-10-15	Decompose string contains, minor refactoring.	ajreynol

2015-10-13	remove options infrastructure code which depended on undefined behavior	Kshitij Bansal
	appears to be source of crashes on mac
2015-10-11	fix regression tests, support fallback mode for proofs	Kshitij Bansal

2015-10-11	Fix strings preprocessing + incremental, fixes bug 682. Add initial ↵	ajreynol
	infrastructure for str.contains inferences.
2015-10-08	Minor improvements to strings. Refactor rewriter. Enable fairness for ↵	ajreynol
	multiple sorts in UF finite model finding by default.
2015-10-07	Disabled donePPSimpITE when unsat-cores are enabled (fixes bug648)	Liana Hadarean

2015-10-07	Minor improvements, add endpoint eq inference to strings.	ajreynol

2015-10-06	More improvements to strings rewriter for regexps, contains, indexof, ↵	ajreynol
	replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.
2015-10-02	Fixes related to explanations for cycles, sym inferences. Minor fixes and ↵	ajreynol
	improvements.
2015-10-02	Improvements to rewriter for regexp, contains, indexof. Improvements and ↵	ajreynol
	fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.
2015-10-01	Evaluate extended operators on partially concrete arguments. More aggressive ↵	ajreynol
	rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms.
2015-10-01	More improvements to strings. More aggressive inference of constant eqc, ↵	ajreynol
	reductions based on congruence, precheck for cycles.
2015-09-30	Refactor strings, bug fix inferences vs lemmas.	ajreynol

2015-09-29	Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add ↵	ajreynol
	regressions.
2015-09-28	Improve quantifiers engine wrt incremental presolve. Add regressions.	ajreynol

2015-09-28	Minor fix	ajreynol

2015-09-28	Minor fixes to strings, add regressions.	ajreynol

2015-09-28	Fix bug for trivial extf inferences in strings. Improve caching for splits ↵	ajreynol
	in strings. Other improvements.