| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* ITE removal fixed to be context-dependent (on UserContext).
Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
(partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
was labeled sat); re-enable it for "make regress"
Also:
* --check-model doesn't fail if quantified assertions don't simplify away.
* fix some examples, and the Java system test, for the disappearance of the
BoolExpr class
* add copy constructor to array type enumerator (the type enumerator
framework requires copy ctors, and the automatically-generated copy ctor
was copying pointers that were then deleted, leaving dangling pointers in
the copy and causing segfaults)
* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
you to dump before/after a particular preprocessing pass. E.g.,
--dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
"--dump=assertions" by itself is after all preprocessing, just before CNF
conversion.
* minor fixes to dumping output
* include Model in language bindings
Minor refactoring/misc:
* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
(e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications
|
|
|
|
meeting last week. The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.
The way to create a skolem is now:
nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")
The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name). Without a "$$", a "_$$"
is automatically appended to the given name.
The second argument is the type.
The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.
An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name). Look at the documentation for details on these.
In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment. This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.
Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit. Some remains to be cleaned up.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
|
|
* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
(there were some minor differences from the spec)
|
|
By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.
If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.
|
|
different output languages can write "sat", "unsat", etc., in different ways. No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.
|
|
* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.
Also:
Stop #defining NULL ((void*) 0). This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea. In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type. We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.
New exception-free Command architecture. Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error. This is much more consistent now. Each Command invocation
results in a CommandStatus. The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.) All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.
Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess. In the future we might put other
options into a compliance mode, or we might choose to make it the
default.
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
|
|
|
|
implemented. This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0. Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder. (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)
|
