cvc5.git
2010-06-03 Tim KingFixes 2 issues with assignments. The first is construct...
2010-06-03 Tim KingAdds toString to DeltaRational
2010-06-03 Tim KingFixes a bug where registration occurs before preregistr...
2010-06-03 Christopher... Changing ANTLR3 detection in configure (Fixes #147)
2010-06-03 Morgan Deters* Added NodeBuilder<>::getChild() to make interface...
2010-06-03 Morgan Detersresolving bug 139: metaKindOf() warnings still exist...
2010-06-02 Morgan Detersadded a handful of debugTagIsOn("context") checks to...
2010-06-02 Morgan Detersmore VERBOSE test failures
2010-06-01 Christopher... Fixing test failures in production build
2010-06-01 Tim KingThis commit adds a debugTagIsOn() guard around some...
2010-06-01 Tim KingThis commit is a fix for a bug in removeITEs(). The...
2010-06-01 Christopher... Adding SMT v2 parsing support for: QF_IDL, QF_NIA,...
2010-06-01 Christopher... Checking for executable permission on antlr3 script
2010-06-01 Tim KingFixed a bug in partial_model.cpp where the data was...
2010-06-01 Christopher... Fixing failing test in r521
2010-06-01 Dejan JovanovićIn order for splitting on demand to be able to retract...
2010-05-31 Christopher... First draft implementation of mkAssociative
2010-05-29 Tim KingAdding a couple of example from fuzzsmt to regress1.
2010-05-29 Tim KingCouple of fixes to theory arith. pivotAndUpdate now...
2010-05-29 Tim KingAfter blasting the disjuncts, TheoryEngine rewrite...
2010-05-28 Tim KingThis update enables TheoryArith to accept assertions...
2010-05-28 Tim KingBug fixes for combining coefficients of rewritten nodes.
2010-05-28 Tim KingAdded printModel() to src/theory/arith/partial_model...
2010-05-28 Tim KingA few changes to the organization of TheoryEngine rewri...
2010-05-28 Tim KingMoving the ITE removal from CnfStream to TheoryEngine...
2010-05-27 Morgan Detersfix bug #134: infinite deallocation loop
2010-05-27 Morgan Deterssmall cosmetic change to tests summary output
2010-05-27 Morgan DetersRemove isAtomic() as per 4/27/2010 meeting. Add commen...
2010-05-27 Morgan Detersfix compiler comparison-signedness warnings
2010-05-27 Tim KingReverting this file to not include any comments. (Morga...
2010-05-27 Morgan Detersadded the ability to add custom expected stdout, stderr...
2010-05-27 Tim KingPreregistration has been turned on. Highly experimental...
2010-05-27 Morgan DetersUse the newer automake test driver "parallel-tests...
2010-05-27 Christopher... Adding debug assertions on most TNode operations
2010-05-27 Christopher... Adding NodeManager::prepareToBeDestroyed() (Fixes:...
2010-05-27 Christopher... Adding .cvc4_config to .gitignore
2010-05-27 Morgan Detersfix bug #111: errors in building lcov-all
2010-05-27 Morgan Detersfix bug 120; competition mode regression failures for...
2010-05-26 Tim King . '+Outstanding case split in theory arith'
2010-05-26 Christopher... Adding CnfStreamBlack tests for all Boolean connectives
2010-05-26 Christopher... Fixing test failures in CnfStreamBlack (it was the...
2010-05-26 Christopher... Adding documentation to my-configure
2010-05-26 Christopher... Fixing my-configure
2010-05-26 Christopher... Adding contrib/my-configure
2010-05-26 Christopher... Adding CnfStream unit tests
2010-05-26 Morgan DetersCDMap<> and CDOmap<> fixes to resolve bug 123
2010-05-26 Tim KingFix for bug 131. Added some additional debugging assert...
2010-05-26 Morgan DetersCDMap: fix bug 130
2010-05-26 Christopher... Prevent lexer errors being raised if a parser error...
2010-05-25 Tim KingAdded Rational constructors that only take a numerator...
2010-05-25 Dejan JovanovićSome initial changes to allow for lemmas on demand.
2010-05-21 Tim KingSmall fixes to TheoryArith. Added a hack to make Integ...
2010-05-20 Tim KingAdded the division symbol to the parser, and minimal...
2010-05-19 Tim KingSignificant revision to theory/arith. The new draft...
2010-05-14 Christopher... Adding debugging code in PropEngine/CnfStream
2010-05-14 Christopher... Adding ITE tests
2010-05-14 Christopher... Adding rudimentary ITE handling in CnfStream
2010-05-14 Christopher... Virtualizing interface between CnfStream and SatSolver
2010-05-13 Christopher... Minor refactorings to PropEngine, SatSolver
2010-05-13 Christopher... Minor refactorings and corrections to comments
2010-05-12 Christopher... Adding ParserBuilder, reducing visibility of Parser...
2010-05-12 Christopher... true and false are only defined if the core theory...
2010-05-12 Christopher... Refactoring parser tests
2010-05-12 Christopher... Adding class Smt2 to handle declaration of logic and...
2010-05-07 Christopher... Tightening lexer rules for numerals in SMT v2
2010-05-07 Morgan Detersmake CVC4::Rational public (fixes broken build)
2010-05-06 Christopher... Adding --strict-parsing option
2010-05-06 Christopher... Adding AntlrInput::tokenTextSubstr
2010-05-06 Christopher... Adding tests for Rational::fromDecimal
2010-05-06 Christopher... Adding tests for Integer::pow
2010-05-06 Christopher... Adding bit-vector constants in SMT2
2010-05-06 Christopher... Implementing Rational::fromDecimal and adding support...
2010-05-06 Dejan Jovanovićfixing the nightly failure. TypeCheckingException is...
2010-05-05 Dejan Jovanovićchanging the interface to bit-vector constant constructor
2010-05-05 Dejan Jovanovićbit-vector constant constructor from string
2010-05-05 Dejan Jovanovićbug fixes for types, old unit tests for types work now
2010-05-04 Christopher... Adding simple SMT2 parser tests
2010-05-04 Christopher... Disabling semantic checks in competition mode.
2010-05-04 Christopher... Minor change to SMT v2 grammar
2010-05-04 Christopher... Adding general support for SMT2 set-info command
2010-05-04 Christopher... Handling SMT 2.0 symbols and info flags
2010-05-04 Dejan JovanovićType-checking classes and hooks (not tested yet).
2010-05-03 Morgan Detersmore reasonable smt 2.0 benchmark test
2010-05-03 Morgan Detersmain driver supports .smt2 input, added an smt2 regress...
2010-05-03 Morgan Deterstheory detection fixes; fixes build breakage when you...
2010-05-03 Christopher... Small mistake in previous commit
2010-05-03 Christopher... Importing ANTLR3 lexer nextToken function to avoid...
2010-05-02 Dejan Jovanovićsmt parser for bit-vectors
2010-05-01 Dejan JovanovićFix for the last night's build errors (type that broke...
2010-05-01 Christopher... Adding missed antlr_input files
2010-05-01 Christopher... Fixing private/public header warnings in parser library
2010-05-01 Christopher... Adding comments to bounded token files
2010-04-30 Dejan JovanovićFix for bug 115, mapping was going in the wrong direction.
2010-04-29 Dejan JovanovićAdded the capability to construct expressions by passin...
2010-04-29 Christopher... (Not) Handling parameterized sorts in SMT v2
2010-04-29 Christopher... Minor fix to SMT v2 parser tests
2010-04-29 Christopher... First draft implementation of SMT v2 parser
2010-04-28 Christopher... SMT parser has to map 'Real' to RealType
2010-04-28 Tim KingMerging the arithmetic theory draft (lra-init) back...
2010-04-28 Dejan Jovanovićadding integer and real types to the public interface
next