| Age | Commit message (Collapse) | Author |
|---|
|
documentation, etc.).
* Remove sat_module.cpp, which was no longer used (was previously refactored?)
|
|
* Fix "make distclean." This should fix the "local regressions fail"
that caused documentation, debian, and "distcheck" nightly build targets
to fail.
* "make clean" now removes some options stuff that previously required a
"make distclean."
* Cosmetic and portability adjustments.
|
|
|
|
the new CVC3-compatibility-API system test to fail)
|
|
should work now
|
|
numerous bugfixes, and the cvc3 system test is enabled.
|
|
|
|
loudly about invalid reads and writes, and (2) apparently causing problems deleting the decision engine (which is now being properly deleted)
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
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
|
|
|
|
|
|
|
|
|
|
Replace all cardinality comparison functions <=, ==, !=, >=, <, >, with a single compare() function that can return UNKNOWN in the case of unknown (or large-finite and thus not *precisely* known) cardinalities.
|
|
Andy saw when adding options & re-making, which was caused by sources not being properly recompiled when they should be
|
|
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)
|
|
CVC4 differ in the answer), so it doesn't really test anything
|
|
|
|
|
|
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).
|
|
"Possible soundness problem somewhere in the solver
(assertion failure in DE)"
|
|
* 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
|
|
itself a CONSTANT.
|
|
|
|
|
|
* more uniform interface between the CLN and GMP wrappers
* support base inference (base == 0) on parsing strings with the CLN wrapper; this was a difference from the GMP wrapper (resolves bug #372)
|
|
quite basic. This may need to be revisited.
|
|
returns the corresponding rational value.
|
|
|
|
internal EqualityEngine pointer.
|
|
that we have a problem with our Integer class though; it appears to behave differently for GMP and CLN
|
|
|
|
|
|
see how isConst() operates: use -d isConst
|
|
|
|
* don't document internal-only stuff (like DefaultCleanup for CDLists)
* NoSuchFunctionException -> TypeCheckingException
|
|
|
|
|
|
* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)
|
