Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-08-24 | fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on ↵ | Morgan Deters | |
active theories; resolves bug 380 | |||
2012-08-24 | fix warning in arrays rewriter | Morgan Deters | |
2012-08-24 | fix get-value output in a couple ways; this fixes bug #378 | Morgan Deters | |
2012-08-23 | attribute stuff for Clark's array constants | Morgan Deters | |
2012-08-23 | Array constant coding done except for the attributes needed | Clark Barrett | |
2012-08-22 | Cap finite cardinalities at 2^64, as discussed in the meeting last week. | Morgan Deters | |
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. | |||
2012-08-22 | fix some build dependencies in options-building; should fix a strange bug ↵ | Morgan Deters | |
Andy saw when adding options & re-making, which was caused by sources not being properly recompiled when they should be | |||
2012-08-22 | More progress on array constants. | Clark Barrett | |
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. | |||
2012-08-21 | add some incremental in-tree regressions | Morgan Deters | |
2012-08-21 | rewriterules: fix a correction bug with --simplification=batch | François Bobot | |
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. | |||
2012-08-20 | remove duplicate function TheoryEngine::getTheory(TheoryId). It was a ↵ | Morgan Deters | |
duplicate of TheoryEngine::theoryOf(TheoryId) | |||
2012-08-20 | minor cleanup | Morgan Deters | |
2012-08-20 | fixes for java bindings | Morgan Deters | |
2012-08-19 | 1. Fix for inst_match.cpp to allow compilation on fedora | Clark Barrett | |
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 | |||
2012-08-16 | The SmtEngine now ensures that setLogicInternal() is called even if there is ↵ | Morgan Deters | |
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). | |||
2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters | |
* 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 | |||
2012-08-16 | ArrayStoreAll should (for now) only allow constant expressions, as it is ↵ | Morgan Deters | |
itself a CONSTANT. | |||
2012-08-16 | fix exceptions and mkConst() in java binding | Morgan Deters | |
2012-08-16 | some fixes for language bindings | Morgan Deters | |
2012-08-14 | Fixes to integer wrapper classes: | Morgan Deters | |
* 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) | |||
2012-08-14 | Implements TheoryArith::collectModelInfo(). The current implementation is ↵ | Tim King | |
quite basic. This may need to be revisited. | |||
2012-08-14 | Adds substituteDelta() to DeltaRational which given a value for delta ↵ | Tim King | |
returns the corresponding rational value. | |||
2012-08-14 | Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers. | Tim King | |
2012-08-14 | Switched a number of EqClassIterator operations to const as well as the ↵ | Tim King | |
internal EqualityEngine pointer. | |||
2012-08-13 | fix integer parsing error.. thanks dejan for the report. this indicates ↵ | Morgan Deters | |
that we have a problem with our Integer class though; it appears to behave differently for GMP and CLN | |||
2012-08-13 | Make a few functions in TheoryEngine (like theoryOf()) const. | Morgan Deters | |
2012-08-13 | Minor cleanup. No performance difference expected. | Morgan Deters | |
2012-08-09 | minor isConst()-related fixes to printing; also add some debugging stuff to ↵ | Morgan Deters | |
see how isConst() operates: use -d isConst | |||
2012-08-08 | Fix --no-checking option. | Morgan Deters | |
2012-08-08 | Public interface review items: | Morgan Deters | |
* don't document internal-only stuff (like DefaultCleanup for CDLists) * NoSuchFunctionException -> TypeCheckingException | |||
2012-08-07 | small fixes | Dejan Jovanović | |
2012-08-07 | some fixes to command and declaration tab-completion in interactive shell | Morgan Deters | |
2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters | |
* rename DeclarationScope to SymbolTable * rename all HashStrategy -> HashFunction (which we often have anyways) * remove CDCircList (no one is currently using it) | |||
2012-08-07 | Fix SmtEngine::setInfo() handling for certain keys. This fixes the ↵ | Morgan Deters | |
"unsupported" message we see in QF_SAT nightly regressions. | |||
2012-08-06 | Support setting :regular-output-channel and :diagnostic-output-channel. | Morgan Deters | |
Also some cleanup of option-related exceptions infrastructure. | |||
2012-08-06 | removing the sat solver inmterface from being public | Dejan Jovanović | |
2012-08-06 | Cleanup of some command stuff, fixes broken Java build. | Morgan Deters | |
2012-08-06 | fix constant printing for datatypes | Dejan Jovanović | |
2012-08-04 | isConst() rule for datatypes | Morgan Deters | |
2012-08-03 | the array-store "construle" for isConst | Morgan Deters | |
2012-08-03 | Comparisons for LogicInfos, and associated tests | Morgan Deters | |
2012-08-03 | ArrayStoreAll infrastructure | Morgan Deters | |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use ↵ | Morgan Deters | |
isConst() and isVar() as appropriate) also some base infrastructure for the new ::isConst(). | |||
2012-08-03 | fix for proofs-enabled builds | Morgan Deters | |
2012-08-03 | better parser makefile fix | Morgan Deters | |
2012-08-02 | fixes to paths in parser makefiles; if you've noticed strange SMT2 parser ↵ | Morgan Deters | |
behavior the last couple days, this should fix it | |||
2012-08-02 | array-store-all class | Morgan Deters | |
2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ↵ | Morgan Deters | |
after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message | |||
2012-08-01 | a couple fixes to SmtEngine::setOption(). thanks Andy for the report! | Morgan Deters | |
2012-08-01 | fixes to some *clean targets | Morgan Deters | |