| 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 |
| 2012-09-30 |
Morgan Deters | minor fixes to pickler (hopefully fixes Debian build... |
commit | commitdiff | tree |
| 2012-09-30 |
Morgan Deters | release notes |
commit | commitdiff | tree |
| 2012-09-29 |
Tim King | Calling the setIncompleteness() flag on all full checks... |
commit | commitdiff | tree |
| 2012-09-29 |
Morgan Deters | Fix a few segfaults in driver. |
commit | commitdiff | tree |
| 2012-09-29 |
Morgan Deters | draft RELEASE-NOTES file, and minor release stuff |
commit | commitdiff | tree |
| 2012-09-29 |
Morgan Deters | fixes to "make distclean" and C compatibility bindings... |
commit | commitdiff | tree |
| 2012-09-29 |
Morgan Deters | fixes to "make distclean" and C compatibility bindings... |
commit | commitdiff | tree |
| 2012-09-29 |
Tim King | This commit add interpretation by lemma for INTS_DIVISI... |
commit | commitdiff | tree |
| 2012-09-28 |
Kshitij Bansal | Some fixes to portfolio |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | fix distribution of cvc4_assert.i |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | fixes for compatibility (i.e., CVC3) Java bindings |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert... |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | some fixes to build system |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | fix production-build linking error |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | Public interface review items: |
commit | commitdiff | tree |
| 2012-09-28 |
Morgan Deters | * fix compatibility library naming for SMT-LIBv1 |
commit | commitdiff | tree |
| 2012-09-27 |
Morgan Deters | * Rename SMT parts (printer, parser) to SMT1 |
commit | commitdiff | tree |
| 2012-09-27 |
Morgan Deters | finally, a portable solution |
commit | commitdiff | tree |
| 2012-09-27 |
Morgan Deters | fix for non-Mac |
commit | commitdiff | tree |
| 2012-09-27 |
Morgan Deters | speed up mkoptions script (esp. on Macs) |
commit | commitdiff | tree |
| 2012-09-27 |
Morgan Deters | better progress indicator for mkoptions |
commit | commitdiff | tree |
| 2012-09-26 |
Morgan Deters | disable building of cvc3_george system-test object... |
commit | commitdiff | tree |
| 2012-09-26 |
Morgan Deters | Finish off SEXPR kind work. |
commit | commitdiff | tree |
| 2012-09-26 |
Andrew Reynolds | updates to model generation : do not modify equality... |
commit | commitdiff | tree |
| 2012-09-26 |
Morgan Deters | Fix a handful of things for Mac, and Java bindings. |
commit | commitdiff | tree |
| 2012-09-26 |
Morgan Deters | bug #398 test (bug was resolved last night), and a... |
commit | commitdiff | tree |
| 2012-09-26 |
Morgan Deters | Fix type checking for define-funs (resolves bug 398). |
commit | commitdiff | tree |
| 2012-09-26 |
Morgan Deters | The Tuesday Afternoon Catch-All Commit (TACAC): |
commit | commitdiff | tree |
| 2012-09-25 |
Morgan Deters | fix |
commit | commitdiff | tree |
| 2012-09-25 |
Morgan Deters | fix some Mac issues |
commit | commitdiff | tree |
| 2012-09-25 |
Morgan Deters | some buggy examples for incrementality, and make bug326... |
commit | commitdiff | tree |
| 2012-09-24 |
Dejan Jovanović | some api changes |
commit | commitdiff | tree |
| 2012-09-24 |
Morgan Deters | Fix the memout issue seen in recent nightly regressions... |
commit | commitdiff | tree |
| 2012-09-22 |
Morgan Deters | Separate public-facing and internal-facing interfaces... |
commit | commitdiff | tree |
| 2012-09-22 |
Dejan Jovanović | another fix for the equality class iterator |
commit | commitdiff | tree |
| 2012-09-21 |
Morgan Deters | Fixes for datatype dumping and printing. Add a new... |
commit | commitdiff | tree |
| 2012-09-21 |
Morgan Deters | SMT-LIBv2 compliance updates: |
commit | commitdiff | tree |
| 2012-09-21 |
Morgan Deters | better verbosity support (so it's sensible when the... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog