cvc5.git
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
2012-10-08 Morgan Detersfix SMT-LIBv2 compliance mode for bitvectors (was compl...
2012-10-06 Morgan Detersturn off cudd by default in configure script
2012-10-06 Morgan Deters* more complete support for --dump assertions:{pre...
2012-10-06 Morgan Deters* Clean up some options documentation
2012-10-06 Morgan Deters* Some documentation about building compatibility and...
2012-10-06 Morgan Deters* Include a few bug testcases for resolved bugs.
2012-10-06 Morgan Deters* Fix some regressions' expected outputs.
2012-10-05 Morgan Detersfix \file
2012-10-05 Morgan DetersBug-related:
2012-10-05 Dejan JovanovićBoolExpr removed and replaced with Expr
2012-10-04 Morgan Detersdisable model-generation by default in cvc3 compatibili...
2012-10-04 Clark BarrettImplemented array type enumerator, more fixes for models
2012-10-04 Morgan DetersIllegalArgumentException in java needs to be named...
2012-10-03 Andrew Reynoldsminor fix for mbqi in finite model finding
2012-10-03 Liana Hadareanimplemented collectModelInfo for TheoryBV
2012-10-03 Morgan Detersupdates to contrib scripts to match docs
2012-10-03 Morgan Detersbetter documentation, allow examples to be installed...
2012-10-03 Clark BarrettNew model code, mostly workin
2012-10-03 Morgan Detersnew README and INSTALL files
2012-10-03 Liana Hadareanadded support for interrupting TheoryBV
2012-10-03 Kshitij Bansal--wait-to-join / --no-wait-to-join option
2012-10-03 Dejan Jovanovićadding ::getBooleanVariables to the PropEngine
2012-10-02 Morgan Deters* re-enable some Z3 extended commands:
2012-10-02 Morgan Detersworkaround for a nasty CLN bug
2012-10-01 Kshitij Bansal"Fix" (disable) portfolio when using quantifiers
2012-10-01 Morgan Detersmake sure to mark LogicInfo as CVC4_PUBLIC
next