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

Age	Commit message (Collapse)	Author
2011-09-21	Java binding now working. Some interface types still need some work (e.g. ↵	Morgan Deters
	iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
2011-09-21	considerable bindings interface work, some improvements to build	Morgan Deters

2011-09-20	fix build	Morgan Deters

2011-09-20	Merge from "swig" branch: language binding for Java is compiling and ↵	Morgan Deters
	linking. Enable with --enable-language-bindings=java
2011-09-17	--show-debug-tags and --show-trace-tags now supported by Configuration API; ↵	Morgan Deters
	also, the information is only recompiled and relinked when it has changed, avoiding unnecessary relinking
2011-09-16	dump define-funs correctly with "--dump declarations", whether the function ↵	Morgan Deters
	is defined via API or through input language
2011-09-16	include example theory (former "UF-Tim") that's included in the dist but not ↵	Morgan Deters
	built for the library
2011-09-16	final(?) documentation fixes	Morgan Deters

2011-09-16	fix up more documentation	Morgan Deters

2011-09-16	some minor fixes to the cvc3 compatibility library and test case	Morgan Deters

2011-09-16	fix serious issue with copyright-updating script	Morgan Deters

2011-09-16	fix numerous documentation issues; doxygen complains much less, now	Morgan Deters

2011-09-16	fix an oversight in the language printers	Morgan Deters

2011-09-15	tim's fixes for context-dependent pre-registration	Dejan Jovanović

2011-09-15	adding --show-debug-tags to list all available debug tracing tags	Dejan Jovanović

2011-09-15	additional stuff for sharing,	Dejan Jovanović

2011-09-07	fixes for uf/equality engine from the quantifiers branch. mainly ↵	Dejan Jovanović
	backtracking issues.
2011-09-03	Disable a warning to address bug 277. (This doesn't really resolve the ↵	Morgan Deters
	issue, but the warning isn't dangerous here. See the bugzilla comments.)
2011-09-03	removing an assert i forgot to remove that andy found	Dejan Jovanović

2011-09-02	Merge from my post-smtcomp branch. Includes:	Morgan Deters
	Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02	Ensure that assignment gestures through CDMap iterators like:	Morgan Deters
	(*myCDMap.find(foo)).second = bar; fail with a compile-time error (rather than being silently ignored, like they had been). Resolves bug #276.
2011-09-02	Partial merge of integers work; this is simple B&B and some pseudoboolean	Morgan Deters
	infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-09-02	* Changing pre-registration to be context dependent -- it is called from the ↵	Dejan Jovanović
	SAT solver on every backtrack * Updated UF to handle the context dependent pre-registration * Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool
2011-08-30	Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK ↵	Dejan Jovanović
	will be reissued. Some unexpected slowdowns, but not too much.
2011-08-27	Removing Theory::registerTerm() as discussed in the meeting. Now ↵	Dejan Jovanović
	pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).
2011-08-24	Simplification of the preregister and register throught a NodeVisitor class. ↵	Dejan Jovanović
	The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.
2011-08-23	some uf cleanup	Dejan Jovanović

2011-08-17	new implementation of lemmas on demand	Dejan Jovanović
	comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
2011-07-12	fix bug 272, array unsoundness, and some array cleanup	Morgan Deters

2011-07-11	fixing out of place typename (error on g++ 4.4.3-4ubuntu5)	Morgan Deters

2011-07-11	Adding static_fact_manager	Clark Barrett

2011-07-11	Clark's work on array theory - can now solve all QF_AX problems	Clark Barrett

2011-07-11	fix some confusing debug output (bogus counter)	Morgan Deters

2011-07-11	if running in QF_AX, equalities over terms of uninterpreted sort go to ↵	Morgan Deters
	arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
2011-07-11	adding disequality propagation	Dejan Jovanović
	relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5
2011-07-11	merge from symmetry branch	Morgan Deters

2011-07-10	Reverting mistaken check-in	Clark Barrett

2011-07-10	changing the sat solver remove clauses constants	Dejan Jovanović
	with these we get closer to yices on uf and it seems better on lra vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471 vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576
2011-07-10	Fixed bug in default solve - wasn't returning when it was supposed to	Clark Barrett

2011-07-10	another typo	Dejan Jovanović

2011-07-10	yet another uf bug fix, hopefully the last	Dejan Jovanović

2011-07-10	another bugfix for uf	Dejan Jovanović

2011-07-09	some immediate bug fixes	Dejan Jovanović

2011-07-09	minor fixups	Morgan Deters

2011-07-09	surprize surprize	Dejan Jovanović

2011-07-07	removing duplicate clauses in ite cnf conversion	Dejan Jovanović

2011-07-06	Fixing two bugs:	Dejan Jovanović
	1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution 2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses
2011-07-05	updated preprocessing and rewriting input equalities into inequalities for LRA	Dejan Jovanović

2011-06-30	Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),	Morgan Deters
	when --strict-parsing is off (which it is by default). The danoint benchmarks have such monsters.
2011-06-30	Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to ↵	Tim King
	16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these.