| Age | Commit message (Collapse) | Author |
|---|
|
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
|
|
This changes our implementation of GetModelCommand so that we use the API to print the model.
It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.
It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.
This eliminates the last call to getSmtEngine() from the command layer.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
|
|
|
|
Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used.
|
|
This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.
This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.
This is one of the last remaining steps for migrating the parser to the new API.
The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.
|
|
This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.
Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
|
|
This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
|
|
This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary.
Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only.
This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR modifies the printers to use Result::Sat, "internal" version of BenchmarkStatus, for printing benchmark status commands.
|
|
This PR is a step towards the migration of Commands to the public API. Node versions of some Commands are introduced for internal use (as necessary). The DumpManager is refactored to make use of those commands.
|
|
This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.
|
|
|
|
Fixes https://github.com/CVC4/cvc4-wishues/issues/9.
When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed.
This change adds begin and end markers as the example below:
```
MODEL BEGIN
x : INT = -3;
y : INT = 0;
z : INT = 0;
MODEL END;
```
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. no decimals used for rational literals
2. queries/check-sats wrapped with PUSH/POP
|
|
|
|
|
|
|
|
|
|
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
|
|
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.
|
|
language
all theory writers should take a look a what's being printed, to ensure all cases are covered
|
|
* 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.)
|
