cvc5.git
2012-11-09 Morgan DetersTheoryEngineModelBuilder::buildModel() is only called...
2012-11-09 Kshitij Bansalexport null nodes (fixes a bug in portfolio model stuff)
2012-11-09 Tim KingTest that breaks arithmetic model building due to diseq...
2012-11-09 Tim KingArithmetic problem that fails --check-models due incomp...
2012-11-09 Morgan DetersBug-fix for a crash involving improperly-thrown excepti...
2012-11-09 Morgan DetersIn non-linear logics, rewrite DIVISION, INTS_DIVISION...
2012-11-09 Morgan Detersanother DISTCLEANFILES entry, for proper "make distclea...
2012-11-09 Clark BarrettFix for another model assertion failure
2012-11-08 Tim KingTurns on TheoryUF when non-linear arithmetic is turned...
2012-11-08 Morgan Detersfix "make distcheck"
2012-11-08 Morgan DetersReview of trunk r4525 (TypeNode::getBaseType()):
2012-11-08 Tim KingImproved support for division by zero. This adds the...
2012-11-08 Morgan Detersexception fix
2012-11-08 Clark BarrettFixed two small bugs in model generation
2012-11-08 Clark BarrettAdded getBaseType - Morgan please check
2012-11-08 Andrew Reynoldsadded support for parametric datatypes in smt2 parser...
2012-11-07 Morgan Deters* Type ascription bug fixed (resolves bug 432), but...
2012-11-07 Tim KingFix to a bug in integer mod lemmas.
2012-11-06 Morgan Detersfix issue in compatibility layer that could segfault
2012-11-05 Tim KingFix to the context dependent static learning code.
2012-11-05 Morgan Detersfixes for replacement function library
2012-11-05 Morgan Detersfixes for mac os
2012-11-05 Morgan Detersfix for tarball building (fixes debian and distcheck...
2012-11-02 Andrew Reynoldsmore minor updates to inst gen and representative selec...
2012-10-31 Andrew Reynoldscleaning up some of the equality query stuff, implement...
2012-10-30 Dejan Jovanovićdelta of a model-building failure case
2012-10-29 Andrew Reynoldsmore updates and minor bug fixes for fmf/inst-gen quant...
2012-10-29 Clark BarrettTweak to options configuration for turning off minisat...
2012-10-29 Clark BarrettDisable minisat elimination when models are on
2012-10-29 Clark BarrettDisable some array optimizations when models are on
2012-10-29 Clark Barrettauflia directory missing from regression summary -...
2012-10-26 Morgan DetersFix to subrange type enumerator, and its unit test...
2012-10-26 Andrew Reynoldsbug fix for parametric datatypes, previously datatypes...
2012-10-26 Tim KingFix for bug 430. d_delta in PartialModel was never...
2012-10-26 Morgan Detersbuild options sources into distribution tarballs (in...
2012-10-26 Morgan Detersnew boost.m4 makes boost-thread require boost-system...
2012-10-26 Morgan Detersbetter parametric datatype arity checking; fixes bug 433
2012-10-26 Clark BarrettFixed a failing datatype regression with check-models
2012-10-26 ACSYStoday's build system fix: sometimes examples weren...
2012-10-26 Andrew Reynoldsfixed bug in datatypes decision procedure enforcing...
2012-10-26 Clark BarrettMore bug fixes and more checks for models
2012-10-25 ACSYSlast build system fix for now: fix some typos affecting Mac
2012-10-25 Morgan Detersextra quoting for special character
2012-10-25 ACSYSmore minor fixes to build system
2012-10-25 Morgan DetersOne of my changes to the build system yesterday broke...
2012-10-24 Andrew Reynoldsfixed assertion failures in efficient e-matching
2012-10-24 Morgan DetersIncludes many fixes to build system for Solaris (thanks...
2012-10-24 Tim KingUpdated the ArithStaticLearner to be user context depen...
2012-10-24 Tim KingFix for systems that do not have the MAP_FILE macro...
2012-10-24 Dejan Jovanovićfix for bug 429
2012-10-24 Dejan Jovanovićtwo smaller random pure LRA push-pop cases that fail
2012-10-24 Andrew Reynoldsefficient e-matching now specific to rewrite rules
2012-10-23 Andrew Reynoldsmore major cleanup of quantifiers code, separating...
2012-10-23 Andrew Reynoldsfixed problem with datatypes giving incorrect explanati...
2012-10-23 Clark BarrettMore debugging info, small changes to model builder
2012-10-23 Morgan Deterssome fixes for "make examples" and "make install-exampl...
2012-10-23 Clark BarrettAdded reads that were missing in collectModelInfo
2012-10-23 Liana Hadareanfixed TheoryBV collectModel info to check for shared...
2012-10-23 Tim KingThe contrib/get-antlr-3.4 script:
2012-10-23 Andrew Reynoldsmore updates to inst gen: fixed partial instantiations...
2012-10-22 Morgan Detersfix parser generation in distributed tarballs (should...
2012-10-22 Morgan Detersone more incorrect #line fixed
2012-10-22 Morgan Detersfix misleading comment in example
2012-10-22 Morgan Detersfix installation of certain header files
2012-10-22 Morgan Detersadd bug 425 models regression; fix mac-build execute...
2012-10-19 Tim KingFix for model building with shared terms for arithmetic.
2012-10-19 Kshitij BansalFix problem with incremental with portfolio. Fixes...
2012-10-19 Liana HadareanBV theory model fix
2012-10-19 Kshitij Bansal--fallback-sequential / --no-fallback-sequential option
2012-10-17 Andrew Reynoldsfirst working version of new inst-gen-style quantifier...
2012-10-16 Andrew Reynoldsmore cleanup of quantifiers code
2012-10-16 Andrew Reynoldsfirst draft of new inst gen method (still with bugs...
2012-10-14 Morgan Detersfix #line number warnings (sorry!)
2012-10-12 Clark BarrettAdded assertions and tracing code for collectModelInfo...
2012-10-12 Clark BarrettLatest changes to model code
2012-10-11 Morgan DetersFix bug 421, again, and add a second, independent test...
2012-10-11 Morgan Detersminor changes in wording for "cvc4 --version", and...
2012-10-11 Morgan DetersStandardizing copyright notice. Touches **ALL** source...
2012-10-11 Morgan DetersFix wording on GPL in legal notices; also remove an...
2012-10-11 Morgan Deterscompliance note
2012-10-10 Morgan DetersAbstract values for SMT-LIB.
2012-10-10 Andrew Reynoldscleanup up some static data members in the quantifiers...
2012-10-10 Dejan Jovanovićfixing the cvc bv parser and typechecker
2012-10-09 Kshitij Bansaltypo
2012-10-09 Kshitij Bansalbugfix: isQuantified, bugfix: flush
2012-10-09 Andrew Reynoldsfixed datatypes rewriter to detect clashes between...
2012-10-09 Morgan Deters* make Model class private (as discussed at meeting...
2012-10-09 Liana Hadareanfixed bv rewriter to evaluate bvurem over constants
2012-10-09 Clark BarrettMore fixes to model code
2012-10-09 Andrew Reynoldsmade datatypes rewrite incorrect selectors to ground...
2012-10-09 Morgan Detersusability: remove --no-interactive from --smtlib option
2012-10-09 Dejan Jovanovićfix for bug 415
2012-10-09 Morgan Deters* Add assertion in TheoryModel code to ensure we don...
2012-10-09 Morgan Detersfix beta reduction in both preRewrite() *and* postRewri...
2012-10-09 Morgan Deterssome documentation fixes
2012-10-09 Dejan Jovanovićadding mergePredicates method to the equality engine...
2012-10-08 Morgan Deters* Models' SubstitutionMaps are now attached to the...
2012-10-08 Liana Hadareanadded reduced bv model failing test case
2012-10-08 Clark BarrettFixed problem in assertEqualityEngine: predicates that...
2012-10-08 Morgan Deterssmall fix for compat JNI library installation
next