summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-12-06Fix dt.size care graph.ajreynol
2014-12-04Relaxed 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-04clean up and improve intersectionTianyi Liang
2014-12-04Fix valgrind-flagged error about uninitialized value.Morgan Deters
2014-12-04Fix segfault in lambdas when constructed via API.Morgan Deters
2014-12-03Fix UnsatCore in language bindings.Morgan Deters
2014-12-03Floating point infrastructure.Martin Brain
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-12-03Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2014-12-03Revert "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-02disable inter cacheTianyi Liang
2014-11-28Synchronize conjecture generation with E-matching. Minor fix to ↵ajreynol
--full-saturate-quant.
2014-11-26add intersection rewritingTianyi Liang
2014-11-26add more regexp rewritingTianyi Liang
2014-11-26add more functions for regular expressionsTianyi Liang
2014-11-25Fix 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-22added number of resource units used as a statlianah
2014-11-21Throw error when pattern is not list of terms.ajreynol
2014-11-21Change 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-20Disable 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-20Fix #lines in template.Morgan Deters
2014-11-19Making construction of trigger sets not use the global engine state.Dejan Jovanović
2014-11-19Distribute UnsafeInterruptException interface file for SWIG.Morgan Deters
2014-11-18Merge pull request #70 from kbansal/sets-for-merge-squashedKshitij Bansal
Set Constant's normal form and other short fixes
2014-11-18Set Constant's normal form and other short fixesKshitij 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-18clear model cache in BVQuickCheck clearSolver() (fixes bug 587)Liana Hadarean
2014-11-18All Minisat solve calls now return lbool (fixes bug 599)lianah
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-18Add 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-17added command line option for extractArith bv rewritelianah
2014-11-17Short-circuit in TheoryArithPrivate::check(), care of Tim.Morgan Deters
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-17Resource-limiting work.Liana Hadarean
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-16Add 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-14Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.ajreynol
2014-11-13Merge pull request #69 from mdeters/bug594Morgan Deters
Fix memory leak in CDHashMap<> with Node keys (resolves bug 594).
2014-11-13Remove two obsolete versions of MBQI.ajreynol
2014-11-13More preparation for filtering relevant terms in TermDb.ajreynol
2014-11-12Possible fix for bug594Morgan Deters
2014-11-12BV inequality graph TNode fix.Morgan Deters
2014-11-12Fix BV inequality solver caching.Morgan Deters
2014-11-12Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.Morgan Deters
2014-11-11Minor cleanup.Morgan Deters
2014-11-11Merge pull request #64 from mdeters/theorysets-hashset-iterationKshitij Bansal
Update TheorySets to use CDHashSet<>::key_begin() / key_end().
2014-11-11Work on synchronizing decision=justification and E-matching.ajreynol
2014-11-10Merge pull request #63 from mdeters/theorystrings-hashset-iterationTianyi Liang
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().
2014-11-10Bug 593 fix: if the type is finite, it is now considered for detecting ↵Dejan Jovanović
theories of nested terms.
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements ↵ajreynol
to sort inference. Remove unused code.
2014-11-09Merge branch '1.4.x'Morgan Deters
2014-11-09Update TheorySets to use CDHashSet<>::key_begin() / key_end().Morgan Deters
2014-11-09Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback