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

Age	Commit message (Collapse)	Author
2012-05-27	Committing the work on equality engine, I need to see how it does on the ↵	Dejan Jovanović
	regressions. New additions: * areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later. * propagation of shared dis-equalities (not yet complete, once case missing) * changes to the theories that use it, authors should check up on the changes
2012-05-27	Another expensive function call in a Debug trace	Clark Barrett

2012-05-27	Another expensive function call in a Debug line	Clark Barrett

2012-05-25	init bug fix	Kshitij Bansal

2012-05-25	Checking in fix for bug 340 - somehow didn't get checked in earlier	Clark Barrett

2012-05-24	Separating the subtheory implementations in the bitvector theory.	Dejan Jovanović

2012-05-24	Significant changes to the internals of the equality engine. Equality is not ↵	Dejan Jovanović
	handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected.
2012-05-22	This commit merges in the branch arithmetic/cprop.	Tim King

2012-05-21	Updating equality manager to handle tagged trigger terms. Notifications are ↵	Dejan Jovanović
	pushed out for relationships between terms tagged with the same tag. No performance impact.
2012-05-21	main() no longer catches non-CVC4 exceptions. This means on memout and ↵	Morgan Deters
	other C++-level exceptions, we'll exit the C++ way rather than our custom way (so we don't get statistics etc.)
2012-05-19	Adding regress test for bug 341.	Tim King

2012-05-19	- The array type rules were fixed to use isSubtypeOf.	Tim King
	- The type of (kind::DIVISION x y) is RealType. - A reference to util/pseudoboolean.i was removed. - rec5.cvc is disabled for now. The type of 2 is Integer which is not a subtype of [0..11].
2012-05-18	This commit adds TypeNode::leastCommonTypeNode(). The special case for ↵	Tim King
	arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339
2012-05-18	This commit removes the dead psuedoboolean code.	Tim King

2012-05-18	Removing long unsigned operator+ from CDList's const_iterator.	Tim King

2012-05-18	removing failing regression	Dejan Jovanović

2012-05-17	This fixes a fascinating segfault. This is the sequence of events:	Tim King
	1) A restart occurs 2) A shared term is registered to arithmetic. 3) Arithmetic sets this up. 4) No new linear relations are added to arithmetic. 5) Eventually a restart occurs. 6) Arithmetic resets the tableau as it has not had a row added since the last restart. 7) A new variable is added. 8) This exceeds the size of the column vector of the saved tableau by exactly one. 9) segfault
2012-05-17	Fixing an issue with LogicInfo::isPure() that turned off simplification in ↵	Morgan Deters
	QF_UF and maybe others
2012-05-17	Fixed bug 338:	Liana Hadarean
	- fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants
2012-05-17	Adding failing regression for ite type computation.	Tim King

2012-05-17	Queueing up asserted literals in the proxy instead of sending them off to ↵	Dejan Jovanović
	the theory engine immediately. The queue is discharged just before a check().
2012-05-16	adding simple-minded handling of (dis-)equalities where constants are involved	Dejan Jovanović

2012-05-16	Fixing C compatibility library (it still had a reference to CONST_INTEGER).	Morgan Deters
	This hopefully fixes the Debian build.
2012-05-16	testcase for bug 337	Dejan Jovanović

2012-05-16	Changes to SAT solver:	Dejan Jovanović
	* allowing propagation of false literals (handles conflict) * allowing lemmas during BCP (bug 337) * UF does direct propagation, without checking for literal value anymore
2012-05-16	equality status for bitvectors can now look into the sat solver to check for ↵	Dejan Jovanović
	IN_MODEL status
2012-05-16	removing duplicate literals in explanations of propagations	Dejan Jovanović

2012-05-16	refactored TheoryBV bitblaster and equality engine into subtheories (similar ↵	Liana Hadarean
	to TheoryEngine
2012-05-15	fixed QF_BV performance problem due to using CDList instead of CDQueue	Liana Hadarean

2012-05-15	(no commit message)	Dejan Jovanović

2012-05-15	test cases	Dejan Jovanović

2012-05-15	Fix to shared terms visitor.	Tim King

2012-05-15	Implement TypeNode::isComparableTo() and add a unit test for it.	Morgan Deters

2012-05-15	Fixed several bugs in shared terms database	Clark Barrett

2012-05-15	This commit removes the CONST_INTEGER kind from nodes. This code comes from ↵	Tim King
	the branch arithmetic/remove_const_int.
2012-05-15	renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively	Liana Hadarean

2012-05-15	removing all extended commands (as inspired by the Z3 extended command set) ↵	Morgan Deters
	except for declare-datatypes
2012-05-15	Fix QF_AUFLIA (resolves bug #331).	Morgan Deters

2012-05-15	fixing warnings, grr	Dejan Jovanović

2012-05-15	several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify ↵	Liana Hadarean
	and now term notify handles boolean constants; fixed bug 328
2012-05-14	fixes for shared term registration. previously the type was not considered ↵	Dejan Jovanović
	when looking at theories of the term and for a term like read(a, f(x)) the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.
2012-05-14	Fixed assertion failures in array theory	Clark Barrett
	This fixes bugs 335 and 333.
2012-05-14	in debug builds, -d can be used for trace tags that aren't also debug tags	Morgan Deters

2012-05-14	fixing up preregistration again	Dejan Jovanović

2012-05-13	fixing build warnings	Dejan Jovanović

2012-05-11	fix regex in Debug_tags and Trace_tags generation for Mac OS	Morgan Deters

2012-05-11	fix typo in sed line	Morgan Deters

2012-05-11	output a warning message when a function type (or datatype, or array, etc.) ↵	Morgan Deters
	is created with a Boolean term inside it
2012-05-11	Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory	Clark Barrett

2012-05-11	Added some ITE rewrites,	Clark Barrett
	Added ITE simplifier - on by default only for QF_LIA benchmarks Fixed one bug in arrays Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()