| 2012-10-29 |
Clark Barrett | Disable some array optimizations when models are on |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | auflia directory missing from regression summary -... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | Fix to subrange type enumerator, and its unit test... |
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | bug fix for parametric datatypes, previously datatypes... |
commit | commitdiff | tree |
| 2012-10-26 |
Tim King | Fix for bug 430. d_delta in PartialModel was never... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | build options sources into distribution tarballs (in... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | new boost.m4 makes boost-thread require boost-system... |
commit | commitdiff | tree |
| 2012-10-26 |
Morgan Deters | better parametric datatype arity checking; fixes bug 433 |
commit | commitdiff | tree |
| 2012-10-26 |
Clark Barrett | Fixed a failing datatype regression with check-models |
commit | commitdiff | tree |
| 2012-10-26 |
ACSYS | today's build system fix: sometimes examples weren... |
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | fixed bug in datatypes decision procedure enforcing... |
commit | commitdiff | tree |
| 2012-10-26 |
Clark Barrett | More bug fixes and more checks for models |
commit | commitdiff | tree |
| 2012-10-25 |
ACSYS | last build system fix for now: fix some typos affecting Mac |
commit | commitdiff | tree |
| 2012-10-25 |
Morgan Deters | extra quoting for special character |
commit | commitdiff | tree |
| 2012-10-25 |
ACSYS | more minor fixes to build system |
commit | commitdiff | tree |
| 2012-10-25 |
Morgan Deters | One of my changes to the build system yesterday broke... |
commit | commitdiff | tree |
| 2012-10-24 |
Andrew Reynolds | fixed assertion failures in efficient e-matching |
commit | commitdiff | tree |
| 2012-10-24 |
Morgan Deters | Includes many fixes to build system for Solaris (thanks... |
commit | commitdiff | tree |
| 2012-10-24 |
Tim King | Updated the ArithStaticLearner to be user context depen... |
commit | commitdiff | tree |
| 2012-10-24 |
Tim King | Fix for systems that do not have the MAP_FILE macro... |
commit | commitdiff | tree |
| 2012-10-24 |
Dejan Jovanović | fix for bug 429 |
commit | commitdiff | tree |
| 2012-10-24 |
Dejan Jovanović | two smaller random pure LRA push-pop cases that fail |
commit | commitdiff | tree |
| 2012-10-24 |
Andrew Reynolds | efficient e-matching now specific to rewrite rules |
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | more major cleanup of quantifiers code, separating... |
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | fixed problem with datatypes giving incorrect explanati... |
commit | commitdiff | tree |
| 2012-10-23 |
Clark Barrett | More debugging info, small changes to model builder |
commit | commitdiff | tree |
| 2012-10-23 |
Morgan Deters | some fixes for "make examples" and "make install-exampl... |
commit | commitdiff | tree |
| 2012-10-23 |
Clark Barrett | Added reads that were missing in collectModelInfo |
commit | commitdiff | tree |
| 2012-10-23 |
Liana Hadarean | fixed TheoryBV collectModel info to check for shared... |
commit | commitdiff | tree |
| 2012-10-23 |
Tim King | The contrib/get-antlr-3.4 script: |
commit | commitdiff | tree |
| 2012-10-23 |
Andrew Reynolds | more updates to inst gen: fixed partial instantiations... |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | fix parser generation in distributed tarballs (should... |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | one more incorrect #line fixed |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | fix misleading comment in example |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | fix installation of certain header files |
commit | commitdiff | tree |
| 2012-10-22 |
Morgan Deters | add bug 425 models regression; fix mac-build execute... |
commit | commitdiff | tree |
| 2012-10-19 |
Tim King | Fix for model building with shared terms for arithmetic. |
commit | commitdiff | tree |
| 2012-10-19 |
Kshitij Bansal | Fix problem with incremental with portfolio. Fixes... |
commit | commitdiff | tree |
| 2012-10-19 |
Liana Hadarean | BV theory model fix |
commit | commitdiff | tree |
| 2012-10-19 |
Kshitij Bansal | --fallback-sequential / --no-fallback-sequential option |
commit | commitdiff | tree |
| 2012-10-17 |
Andrew Reynolds | first working version of new inst-gen-style quantifier... |
commit | commitdiff | tree |
| 2012-10-16 |
Andrew Reynolds | more cleanup of quantifiers code |
commit | commitdiff | tree |
| 2012-10-16 |
Andrew Reynolds | first draft of new inst gen method (still with bugs... |
commit | commitdiff | tree |
| 2012-10-14 |
Morgan Deters | fix #line number warnings (sorry!) |
commit | commitdiff | tree |
| 2012-10-12 |
Clark Barrett | Added assertions and tracing code for collectModelInfo... |
commit | commitdiff | tree |
| 2012-10-12 |
Clark Barrett | Latest changes to model code |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | Fix bug 421, again, and add a second, independent test... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | minor changes in wording for "cvc4 --version", and... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | Fix wording on GPL in legal notices; also remove an... |
commit | commitdiff | tree |
| 2012-10-11 |
Morgan Deters | compliance note |
commit | commitdiff | tree |
| 2012-10-10 |
Morgan Deters | Abstract values for SMT-LIB. |
commit | commitdiff | tree |
| 2012-10-10 |
Andrew Reynolds | cleanup up some static data members in the quantifiers... |
commit | commitdiff | tree |
| 2012-10-10 |
Dejan Jovanović | fixing the cvc bv parser and typechecker |
commit | commitdiff | tree |
| 2012-10-09 |
Kshitij Bansal | typo |
commit | commitdiff | tree |
| 2012-10-09 |
Kshitij Bansal | bugfix: isQuantified, bugfix: flush |
commit | commitdiff | tree |
| 2012-10-09 |
Andrew Reynolds | fixed datatypes rewriter to detect clashes between... |
commit | commitdiff | tree |
| 2012-10-09 |
Morgan Deters | * make Model class private (as discussed at meeting... |
commit | commitdiff | tree |
| 2012-10-09 |
Liana Hadarean | fixed bv rewriter to evaluate bvurem over constants |
commit | commitdiff | tree |
| 2012-10-09 |
Clark Barrett | More fixes to model code |
commit | commitdiff | tree |
| 2012-10-09 |
Andrew Reynolds | made datatypes rewrite incorrect selectors to ground... |
commit | commitdiff | tree |
| 2012-10-09 |
Morgan Deters | usability: remove --no-interactive from --smtlib option |
commit | commitdiff | tree |
| 2012-10-09 |
Dejan Jovanović | fix for bug 415 |
commit | commitdiff | tree |
| 2012-10-09 |
Morgan Deters | * Add assertion in TheoryModel code to ensure we don... |
commit | commitdiff | tree |
| 2012-10-09 |
Morgan Deters | fix beta reduction in both preRewrite() *and* postRewri... |
commit | commitdiff | tree |
| 2012-10-09 |
Morgan Deters | some documentation fixes |
commit | commitdiff | tree |
| 2012-10-09 |
Dejan Jovanović | adding mergePredicates method to the equality engine... |
commit | commitdiff | tree |
| 2012-10-08 |
Morgan Deters | * Models' SubstitutionMaps are now attached to the... |
commit | commitdiff | tree |
| 2012-10-08 |
Liana Hadarean | added reduced bv model failing test case |
commit | commitdiff | tree |
| 2012-10-08 |
Clark Barrett | Fixed problem in assertEqualityEngine: predicates that... |
commit | commitdiff | tree |
| 2012-10-08 |
Morgan Deters | small fix for compat JNI library installation |
commit | commitdiff | tree |
| 2012-10-08 |
Morgan Deters | fix SMT-LIBv2 compliance mode for bitvectors (was compl... |
commit | commitdiff | tree |
| 2012-10-06 |
Morgan Deters | turn off cudd by default in configure script |
commit | commitdiff | tree |
| 2012-10-06 |
Morgan Deters | * more complete support for --dump assertions:{pre... |
commit | commitdiff | tree |
| 2012-10-06 |
Morgan Deters | * Clean up some options documentation |
commit | commitdiff | tree |
| 2012-10-06 |
Morgan Deters | * Some documentation about building compatibility and... |
commit | commitdiff | tree |
| 2012-10-06 |
Morgan Deters | * Include a few bug testcases for resolved bugs. |
commit | commitdiff | tree |
| 2012-10-06 |
Morgan Deters | * Fix some regressions' expected outputs. |
commit | commitdiff | tree |
| 2012-10-05 |
Morgan Deters | fix \file |
commit | commitdiff | tree |
| 2012-10-05 |
Morgan Deters | Bug-related: |
commit | commitdiff | tree |
| 2012-10-05 |
Dejan Jovanović | BoolExpr removed and replaced with Expr |
commit | commitdiff | tree |
| 2012-10-04 |
Morgan Deters | disable model-generation by default in cvc3 compatibili... |
commit | commitdiff | tree |
| 2012-10-04 |
Clark Barrett | Implemented array type enumerator, more fixes for models |
commit | commitdiff | tree |
| 2012-10-04 |
Morgan Deters | IllegalArgumentException in java needs to be named... |
commit | commitdiff | tree |
| 2012-10-03 |
Andrew Reynolds | minor fix for mbqi in finite model finding |
commit | commitdiff | tree |
| 2012-10-03 |
Liana Hadarean | implemented collectModelInfo for TheoryBV |
commit | commitdiff | tree |
| 2012-10-03 |
Morgan Deters | updates to contrib scripts to match docs |
commit | commitdiff | tree |
| 2012-10-03 |
Morgan Deters | better documentation, allow examples to be installed... |
commit | commitdiff | tree |
| 2012-10-03 |
Clark Barrett | New model code, mostly workin |
commit | commitdiff | tree |
| 2012-10-03 |
Morgan Deters | new README and INSTALL files |
commit | commitdiff | tree |
| 2012-10-03 |
Liana Hadarean | added support for interrupting TheoryBV |
commit | commitdiff | tree |
| 2012-10-03 |
Kshitij Bansal | --wait-to-join / --no-wait-to-join option |
commit | commitdiff | tree |
| 2012-10-03 |
Dejan Jovanović | adding ::getBooleanVariables to the PropEngine |
commit | commitdiff | tree |
| 2012-10-02 |
Morgan Deters | * re-enable some Z3 extended commands: |
commit | commitdiff | tree |
| 2012-10-02 |
Morgan Deters | workaround for a nasty CLN bug |
commit | commitdiff | tree |
| 2012-10-01 |
Kshitij Bansal | "Fix" (disable) portfolio when using quantifiers |
commit | commitdiff | tree |
| 2012-10-01 |
Morgan Deters | make sure to mark LogicInfo as CVC4_PUBLIC |
commit | commitdiff | tree |
| 2012-10-01 |
Morgan Deters | fix for dejan: term ITEs now dumped correctly |
commit | commitdiff | tree |
| 2012-10-01 |
Andrew Reynolds | initial draft of skolemization during pre-processing... |
commit | commitdiff | tree |
| 2012-09-30 |
Morgan Deters | minor changes to arithmetic assertions involving nonlin... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog