Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-12-06 | Fix dt.size care graph. | ajreynol | |
2014-12-04 | Relaxed the constant requirement for regular expression loop; | Tianyi Liang | |
Added "ignoring negative membership" option (fragment checking is not provided, and users must make sure the constraint is in the fragment; otherwise, the solution may not be correct). | |||
2014-12-04 | clean up and improve intersection | Tianyi Liang | |
2014-12-04 | Fix valgrind-flagged error about uninitialized value. | Morgan Deters | |
2014-12-04 | Fix segfault in lambdas when constructed via API. | Morgan Deters | |
2014-12-03 | Fix UnsatCore in language bindings. | Morgan Deters | |
2014-12-03 | Floating point infrastructure. | Martin Brain | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-12-03 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Kshitij Bansal | |
2014-12-03 | Revert "Disable constants sharing in eq engine, disable hack in theory engine." | Kshitij Bansal | |
This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba. In particular, it DOES NOT revert "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine." which is part of the same commit. | |||
2014-12-02 | disable inter cache | Tianyi Liang | |
2014-11-28 | Synchronize conjecture generation with E-matching. Minor fix to ↵ | ajreynol | |
--full-saturate-quant. | |||
2014-11-26 | add intersection rewriting | Tianyi Liang | |
2014-11-26 | add more regexp rewriting | Tianyi Liang | |
2014-11-26 | add more functions for regular expressions | Tianyi Liang | |
2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support ↵ | ajreynol | |
inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers. | |||
2014-11-22 | added number of resource units used as a stat | lianah | |
2014-11-21 | Throw error when pattern is not list of terms. | ajreynol | |
2014-11-21 | Change default option to --inst-when=full-last-call (interleave ↵ | ajreynol | |
instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs. | |||
2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. ↵ | ajreynol | |
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine. | |||
2014-11-20 | Fix #lines in template. | Morgan Deters | |
2014-11-19 | Making construction of trigger sets not use the global engine state. | Dejan Jovanović | |
2014-11-19 | Distribute UnsafeInterruptException interface file for SWIG. | Morgan Deters | |
2014-11-18 | Merge pull request #70 from kbansal/sets-for-merge-squashed | Kshitij Bansal | |
Set Constant's normal form and other short fixes | |||
2014-11-18 | Set Constant's normal form and other short fixes | Kshitij Bansal | |
Other short fixes: * use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT * theoryof-mode fix in smt_engine.cpp * hack in TheoryModel::getModelValue [TODO: notify Clark/Andy] * Lemma generation when it rewrites to true/false fix * TermInfoManager::addTerm(..) fix * Move SUBSET rewrite to preRewrite * On preRegister, queue up propagation to be done upfront ** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code. * TheorySetsProperties::getCardinality(..) fix Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing! | |||
2014-11-18 | clear model cache in BVQuickCheck clearSolver() (fixes bug 587) | Liana Hadarean | |
2014-11-18 | All Minisat solve calls now return lbool (fixes bug 599) | lianah | |
2014-11-18 | Compute model basis only for fmf. Add another co-datatype regression. | ajreynol | |
2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ↵ | ajreynol | |
how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist. | |||
2014-11-17 | added command line option for extractArith bv rewrite | lianah | |
2014-11-17 | Short-circuit in TheoryArithPrivate::check(), care of Tim. | Morgan Deters | |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters | |
2014-11-17 | Resource-limiting work. | Liana Hadarean | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where ↵ | ajreynol | |
equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup. | |||
2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol | |
2014-11-13 | Merge pull request #69 from mdeters/bug594 | Morgan Deters | |
Fix memory leak in CDHashMap<> with Node keys (resolves bug 594). | |||
2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol | |
2014-11-13 | More preparation for filtering relevant terms in TermDb. | ajreynol | |
2014-11-12 | Possible fix for bug594 | Morgan Deters | |
2014-11-12 | BV inequality graph TNode fix. | Morgan Deters | |
2014-11-12 | Fix BV inequality solver caching. | Morgan Deters | |
2014-11-12 | Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5. | Morgan Deters | |
2014-11-11 | Minor cleanup. | Morgan Deters | |
2014-11-11 | Merge pull request #64 from mdeters/theorysets-hashset-iteration | Kshitij Bansal | |
Update TheorySets to use CDHashSet<>::key_begin() / key_end(). | |||
2014-11-11 | Work on synchronizing decision=justification and E-matching. | ajreynol | |
2014-11-10 | Merge pull request #63 from mdeters/theorystrings-hashset-iteration | Tianyi Liang | |
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end(). | |||
2014-11-10 | Bug 593 fix: if the type is finite, it is now considered for detecting ↵ | Dejan Jovanović | |
theories of nested terms. | |||
2014-11-10 | Do not eliminate variables only occurring in patterns. Minor improvements ↵ | ajreynol | |
to sort inference. Remove unused code. | |||
2014-11-09 | Merge branch '1.4.x' | Morgan Deters | |
2014-11-09 | Update TheorySets to use CDHashSet<>::key_begin() / key_end(). | Morgan Deters | |
2014-11-09 | Update TheoryStrings to use CDHashSet<>::key_begin() / key_end(). | Morgan Deters | |