| Age | Commit message (Collapse) | Author |
|---|
|
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default
Also:
* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
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.)
|
|
some internal nodes in eq engine were treated as constants incorrectly
|
|
if this does what you want it to do.
|
|
|
|
fixes bug 382.
|
|
bodies, do not dag-ify model output
|
|
To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.
By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems:
make regress CVC4_REGRESSION_ARGS=--check-models
To see it work, use -v in addition to --check-models.
There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.
--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).
Also:
* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
|
|
|
|
Node version of getValue() in TheoryModel.
|
|
|
|
dead code. (Nobody internally made minus nodes.)
|
|
|
|
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
|
|
documentation, etc.).
* Remove sat_module.cpp, which was no longer used (was previously refactored?)
|
|
numerous bugfixes, and the cvc3 system test is enabled.
|
|
problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381.
* Added LAMBDA kind and type rule, and Node::isClosure().
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
|
|
this fixes at least one known bug where quantifiers could be asserted in quantifier-free logics, with incorrect results.
|
|
active theories; resolves bug 380
|
|
|
|
|
|
|
|
|
|
Here's a fun way to give yourself a week-long headache: try to figure out how
to write efficient code to normalize array constants.
It's mostly there now - just need to figure out how to use type enumerators and
update once the new cardinality stuff is in place.
|
|
|
|
Rewriterules used ppAssert to obtain early the rewriterules in order
to use them in ppRewrite. But all the simplifications (ex. f x = b :
[f x/b]) are not done at that point. Since --simplification=batch
remove the equality (unlike =incremental), for
reachability_bbttf_eT_arrays.smt2 the answer was sat instead of
unsat (thx Andy).
Partial fix: don't take the rewriterules during ppAssert. That changes
nothing since early rewrite was already disabled. But the complete
fix (when early rewrite will be enabled again) will need to take the
rewriterules more than once.
|
|
duplicate of TheoryEngine::theoryOf(TheoryId)
|
|
|
|
2. Initial implementation of computeIsConst for arrays - still needs
additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL
|
|
no explicit setLogic(). This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses. setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.
This means that the CVC language can now take advantage of statistics.
Also added the ability to set the logic from CVC presentation language via (e.g.)
OPTION "logic" "QF_UFLIA";
Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality. Kshitij may have a fix (I warned him about this commit).
|
|
* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups
|
|
quite basic. This may need to be revisited.
|
|
returns the corresponding rational value.
|
|
|
|
internal EqualityEngine pointer.
|
|
|
|
|
|
* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)
|
|
|
|
|
|
|
|
|
|
isConst() and isVar() as appropriate)
also some base infrastructure for the new ::isConst().
|
|
after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message
|
|
|
