summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2012-08-16ArrayStoreAll should (for now) only allow constant expressions, as it is itse...Morgan Deters
2012-08-16fix exceptions and mkConst() in java bindingMorgan Deters
2012-08-16some fixes for language bindingsMorgan Deters
2012-08-14Fixes to integer wrapper classes:Morgan Deters
2012-08-14Implements TheoryArith::collectModelInfo(). The current implementation is qu...Tim King
2012-08-14Adds substituteDelta() to DeltaRational which given a value for delta returns...Tim King
2012-08-14Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.Tim King
2012-08-14Switched a number of EqClassIterator operations to const as well as the inter...Tim King
2012-08-13fix integer parsing error.. thanks dejan for the report. this indicates that...Morgan Deters
2012-08-13Make a few functions in TheoryEngine (like theoryOf()) const.Morgan Deters
2012-08-13Minor cleanup. No performance difference expected.Morgan Deters
2012-08-09minor isConst()-related fixes to printing; also add some debugging stuff to s...Morgan Deters
2012-08-08Fix --no-checking option.Morgan Deters
2012-08-08Public interface review items:Morgan Deters
2012-08-07small fixesDejan Jovanović
2012-08-07some fixes to command and declaration tab-completion in interactive shellMorgan Deters
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
2012-08-07Fix SmtEngine::setInfo() handling for certain keys. This fixes the "unsuppor...Morgan Deters
2012-08-06Support setting :regular-output-channel and :diagnostic-output-channel.Morgan Deters
2012-08-06removing the sat solver inmterface from being publicDejan Jovanović
2012-08-06Cleanup of some command stuff, fixes broken Java build.Morgan Deters
2012-08-06fix constant printing for datatypesDejan Jovanović
2012-08-04isConst() rule for datatypesMorgan Deters
2012-08-03the array-store "construle" for isConstMorgan Deters
2012-08-03Comparisons for LogicInfos, and associated testsMorgan Deters
2012-08-03ArrayStoreAll infrastructureMorgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-08-03fix for proofs-enabled buildsMorgan Deters
2012-08-03better parser makefile fixMorgan Deters
2012-08-02fixes to paths in parser makefiles; if you've noticed strange SMT2 parser beh...Morgan Deters
2012-08-02array-store-all classMorgan Deters
2012-08-01add isFinished() to type enumerators (so we don't rely on exception-throwing ...Morgan Deters
2012-08-01a couple fixes to SmtEngine::setOption(). thanks Andy for the report!Morgan Deters
2012-08-01fixes to some *clean targetsMorgan Deters
2012-08-01fix for the SmtEngine::beforeSearch() option predicateMorgan Deters
2012-08-01some fixes for Mac OSMorgan Deters
2012-07-31fixes for portfolioMorgan Deters
2012-07-31Moving some instantiation-related stuff from src/theory to src/theory/quantif...Morgan Deters
2012-07-31fix some file documentationMorgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27Minor cleanup after today's commits:Morgan Deters
2012-07-27removing unecessary filesAndrew Reynolds
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to mod...Andrew Reynolds
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-26Datatype enumerator work. This version is not a "fair" enumerator, but I got...Morgan Deters
2012-07-18more compliance fixes for SMT-LIBv2Morgan Deters
2012-07-18small change to model-generation function, after discussion w/ AndyMorgan Deters
2012-07-18removing an obsolete assertion in model-generation framework, per Andy's requestMorgan Deters
2012-07-18removing output operator for SExprTypes, which is never used (and SExprTypes ...Morgan Deters
2012-07-17SMT-LIBv2 compliance updates:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback