| 2012-06-16 |
Morgan Deters | updated build script for smt-comp submission
|
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | don't run rewriterules regressions by default; fixes...
|
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | some changes to make CVC4 work nicely with trace executor...
|
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | making --simplification=none the default for quantified...
|
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | The "no-tears-in-competition-mode" commit. Change...
|
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | bug 346 resolved
|
commit | commitdiff | tree |
| 2012-06-13 |
Morgan Deters | adding some regressions to the usual regressions runs...
|
commit | commitdiff | tree |
| 2012-06-13 |
Morgan Deters | revisions to the "make submission" target
|
commit | commitdiff | tree |
| 2012-06-13 |
Morgan Deters | Don't use the "inlined" feature of ANTLR 3.2, which...
|
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | Fix some compile warnings (but they never showed up...
|
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but...
|
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | minor cleanup, and replace a "private:" in equality...
|
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | fix a few compatibility bindings issues
|
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | fix ordering issue of --dump-to and --default-dag-thresh...
|
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | mark a quantifiers global var as "static" so we can...
|
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | distribute an .expect file. fixes a "make check" failure...
|
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch.
|
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | fix issue referred to in bug 352 regarding infinite...
|
commit | commitdiff | tree |
| 2012-06-09 |
Morgan Deters | Cleanup and comments for the dag-ifier. Also some...
|
commit | commitdiff | tree |
| 2012-06-09 |
Morgan Deters | Dagification of output expressions.
|
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | The option --arith-presolve-lemmas had previously been...
|
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | Extend Printer infrastructure also to the "Result"...
|
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | minor fixes, for Mac OS
|
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring...
|
commit | commitdiff | tree |
| 2012-06-07 |
Morgan Deters | LogicInfo locking implemented, and some initialization...
|
commit | commitdiff | tree |
| 2012-06-07 |
Morgan Deters | Adding EchoCommand and associated printer and parser...
|
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | removing std::cout from trunk
|
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | also remove now-incorrect comment from makefile
|
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | unconstrained regressions are now run with "make check...
|
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | Fixing numerous issues with tests and "make dist":
|
commit | commitdiff | tree |
| 2012-06-01 |
Morgan Deters | add a global user-context push/pop in smt engine, just...
|
commit | commitdiff | tree |
| 2012-05-31 |
Morgan Deters | svn:ignore a parallel-tests driver file that automake...
|
commit | commitdiff | tree |
| 2012-05-31 |
Morgan Deters | pass JAVA_CPPFLAGS properly
|
commit | commitdiff | tree |
| 2012-05-30 |
Morgan Deters | remove unused/broken check build target
|
commit | commitdiff | tree |
| 2012-05-29 |
Morgan Deters | removing now-unused TheoryEngine::setLogic() interface...
|
commit | commitdiff | tree |
| 2012-05-21 |
Morgan Deters | main() no longer catches non-CVC4 exceptions. This...
|
commit | commitdiff | tree |
| 2012-05-17 |
Morgan Deters | Fixing an issue with LogicInfo::isPure() that turned...
|
commit | commitdiff | tree |
| 2012-05-16 |
Morgan Deters | Fixing C compatibility library (it still had a reference...
|
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | Implement TypeNode::isComparableTo() and add a unit...
|
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | removing all extended commands (as inspired by the...
|
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | Fix QF_AUFLIA (resolves bug #331).
|
commit | commitdiff | tree |
| 2012-05-14 |
Morgan Deters | in debug builds, -d can be used for trace tags that...
|
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | fix regex in Debug_tags and Trace_tags generation for...
|
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | fix typo in sed line
|
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | output a warning message when a function type (or datatype...
|
commit | commitdiff | tree |
| 2012-05-09 |
Morgan Deters | fix an issue which breaks language bindings (so this...
|
commit | commitdiff | tree |
| 2012-05-09 |
Morgan Deters | --disable-tracing at configure time now disables Trace...
|
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | New LogicInfo functionality.
|
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | require boost library (but not the threading support...
|
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | undo, again
|
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to...
|
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | undo previous commit (as it will break a number of...
|
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to...
|
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | fix parser logic-handling oversights: QF_UFBV should...
|
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | break dependence on zlib-dev for now
|
commit | commitdiff | tree |
| 2012-04-13 |
Morgan Deters | Fix SExpr name qualification for swig, and #include...
|
commit | commitdiff | tree |
| 2012-04-12 |
Morgan Deters | svn ignore Makefile.in for aufbv regression directory
|
commit | commitdiff | tree |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch
|
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer.
|
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | fix distributed builds (and therefore the Debian nightly...
|
commit | commitdiff | tree |
| 2012-04-05 |
Morgan Deters | Support to test the "dumper" mechanism in regressions...
|
commit | commitdiff | tree |
| 2012-03-28 |
Morgan Deters | fix swig-ignored interface name; hopefully fixes Debian...
|
commit | commitdiff | tree |
| 2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks...
|
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | Some work on the dump infrastructure to support portfolio...
|
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | fix a "lost command" bug and associated memory leak...
|
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | Strengthen minisat assertion regarding t-propagations...
|
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | minor fixes: to "make dist" in build directories with...
|
commit | commitdiff | tree |
| 2012-03-08 |
Morgan Deters | fix "make dist"
|
commit | commitdiff | tree |
| 2012-03-07 |
Morgan Deters | fix some Java compatibility-layer interface problems...
|
commit | commitdiff | tree |
| 2012-03-03 |
Morgan Deters | Changing the dependency checking; GMP is required ...
|
commit | commitdiff | tree |
| 2012-03-02 |
Morgan Deters | committing the TNode/Node fix that was in the kind...
|
commit | commitdiff | tree |
| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minisat...
|
commit | commitdiff | tree |
| 2012-02-29 |
Morgan Deters | consistency in how the Dump output stream is used
|
commit | commitdiff | tree |
| 2012-02-28 |
Morgan Deters | fix theory "kinds" file documentation for allowed arity...
|
commit | commitdiff | tree |
| 2012-02-28 |
Morgan Deters | Replace the sequence of hardcoded addTheory() calls...
|
commit | commitdiff | tree |
| 2012-02-27 |
Morgan Deters | fixes to new-theory script; resolves bug #307
|
commit | commitdiff | tree |
| 2012-02-23 |
Morgan Deters | Added ability to set a "cvc4-specific logic" in standards...
|
commit | commitdiff | tree |
| 2012-02-23 |
Morgan Deters | pcvc4 only built if --with-portfolio given to the configure...
|
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | fixes to configure and boost.m4 to make certain boost...
|
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | another static library unavailability issue
|
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | make sure to clear out READLINE_LIBS if readline causes...
|
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | Added OutputChannel::propagateAsDecision() functionality...
|
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | Fixes to documentation / fixes for MacOS
|
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | add a "--with-portfolio" configure option that makes...
|
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | fix src/util/hash.h to specialize GNU's hash template...
|
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | language bindings fixes for yesterday's portfolio merge
|
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | don't require libboost_thread (its presence is detected...
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | fix sharing issue for portfolio (full lit-to-node map...
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | fix "make dist"
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | zlib not required; remove configure's dependency on it
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | portfolio merge
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | readline links in -ltermcap -ltinfo too (fixes breakage...
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | Added Theory::postsolve() infrastructure as Clark requested.
|
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | By default, ONLY enable symmetry breaker ONLY for QF_UF...
|
commit | commitdiff | tree |
| 2012-02-16 |
Morgan Deters | clarify wording in README, thanks for finding this...
|
commit | commitdiff | tree |
| 2012-02-13 |
Morgan Deters | proper handling of improper get-value
|
commit | commitdiff | tree |
| 2012-02-12 |
Morgan Deters | copyright year updated to 2012
|
commit | commitdiff | tree |
| 2012-02-12 |
Morgan Deters | separate new-theory components into a "theoryskel"...
|
commit | commitdiff | tree |
| 2012-02-11 |
Morgan Deters | ensure using bash for new-theory script
|
commit | commitdiff | tree |
| 2012-02-10 |
Morgan Deters | attempt at a fix for the local regression failure ...
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search