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

Age	Commit message (Collapse)	Author
2016-04-20	add utils class for relational theory	PaulMeng

2016-04-19	Refactored code	PaulMeng

2016-04-15	change transitive closure operator name to TCLOUSRE	PaulMeng

2016-04-14	- Implement constant rewriter for relational operators for model generation	PaulMeng
	- fixed a few bugs
2016-04-12	fixed explanation for transitive closure inferences	PaulMeng

2016-04-07	implement standard effort support for product	PaulMeng

2016-04-07	- added standard effort for transpose	PaulMeng
	- implement transitive closure rule for concrete input
2016-03-23	added typing rule for transitive closure	PaulMeng

2016-03-22	minor fix	PaulMeng

2016-03-21	minor fix	PaulMeng

2016-03-11	minor fix	PaulMeng

2016-03-10	minor fix	PaulMeng

2016-03-10	fixed the transpose-occur rule	PaulMeng

2016-03-08	make skolems and tuple reduction terms as shared terms	PaulMeng
	- added more benchmarks for pressure and theory combination tests - fixed find terms method in trie data structure - use a separate membership map to store positive membership terms
2016-03-07	modified CVC4 native language parser to accept 1-tuple declaration:	PaulMeng
	TUPLE(1) - fixed the tuple element selection for product-split and join-split rules
2016-03-04	refactored the code	PaulMeng
	- send out facts as lemmas - fixed the non-termination problem caused by sending facts as lemmas - unfolded symbolic tuples by adding equality lemmas
2016-03-01	small fixes for eq rep names	PaulMeng

2016-03-01	small fix for naming	PaulMeng

2016-03-01	fixed product rules	PaulMeng

2016-02-29	adapted the solver to accept sets of built-in types (int, string, real)	PaulMeng
	use dummy lemmas to find tuple elements equality
2016-02-29	Added more benchmarks	PaulMeng
	Fixed the problem that duplicates and split facts were sent as lemmas causing nontermination Fixed the computation of join and product relations without simplication
2016-02-28	implemented a basic solving procedure for finite relations (only for	PaulMeng
	join, product, transpose operators)
2016-02-17	added rules for join and transpose operators	PaulMeng
	added more benchmarks
2016-02-15	Merge remote-tracking branch 'origin/master'	PaulMeng

2016-02-15	extended smt parser for the finite relations	PaulMeng
	fixed typing rules for relational terms added a benchmark example for the theory of finite relations
2016-02-15	Minor change to last commit	ajreynol

2016-02-15	Eliminate most of the internal representation infrastructure for tuples and ↵	ajreynol
	records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
2016-02-11	More aggressive conditional rewriting for quantified formulas. Bug fix set ↵	ajreynol
	incomplete for fmc.
2016-02-10	Fix model postprocessor for tuples, add regression.	ajreynol

2016-02-09	Fix regression, minor change to output.	ajreynol

2016-02-09	- extend cvc4 frontend parser to accept relational operators (product,	PaulMeng
	join, transpose, transitive closure) - added a finite relations module to collect all relational terms in EE
2016-02-09	Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing ↵	ajreynol
	to quantifier instantiations.
2016-02-08	Updates related to finite model finding and (co)datatypes. Bug fix ↵	ajreynol
	enumerator and codatatype rewriter, further simplify fmc.
2016-02-05	Changing the way the equality engine explains disequalities.	guykatzz
	The explanation for a != b is now: 1. a == find(a) 2. ( find(a) == find(b) ) == false 3. find(b) == b This simplifies the creation of transitivity proofs for disequalities.
2016-02-05	Add two optimizations for datatypes, currently disabled. Bug fix rewriter ↵	ajreynol
	for selectors applied to codatatype values.
2016-02-04	Fixed two more memory leaks in array_info.cpp	Clark Barrett

2016-02-03	Added --omit-dont-cares option which doesn't print model values for	Clark Barrett
	variables known to be don't-cares.
2016-02-02	Moving dump., command., model., and ite_removal. from smt_util/ to smt/. ↵	Tim King
	Breaking an edge between the sat solver and command.h.
2016-02-01	Removing the CVC4_PUBLIC attribute from the forward declaration of Record in ↵	Tim King
	type.h.
2016-02-01	Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build ↵	Tim King
	process.
2016-02-01	Generalizing lib/strtok_r.c so that it can always be compiled.	Tim King

2016-02-01	Generalizing the implementation of lib/clock_gettime.c so that it can always ↵	Tim King
	be compiled.
2016-02-01	Fixing a potentially malformed template expansion when Dump() is disabled.	Tim King

2016-02-01	Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.	Tim King

2016-02-01	Adding an virtual destructor to OstreamUpdate.	Tim King

2016-02-01	Making the ManagedOstream::defaultSource() a const function.	Tim King

2016-02-01	Adding a destructor to ProofOutputChannel.	Tim King

2016-02-01	Fixing white spaces in sat_proof.h.	Tim King

2016-02-01	Making the references to std more explicit in didyoumean.cpp.	Tim King

2016-02-01	Fixing a memory leak in array info.	Tim King