summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Collapse)Author
2015-09-05Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, ↵ajreynol
bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
2015-08-21Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. ↵ajreynol
Enable redundant ITE branch elimination in quantifiers rewriter.
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-04-07Removing the reference to THEORY_BOOL from the equality engine. This theoryDejan Jovanovic
id was used as an internal marker in a set of theories tagging reasons of a propagated disequalities. Replaced it with THEORY_LAST which is not completely kosher but is safe in the context being used.
2015-03-25change const are triggers from false to true in equality enginesKshitij Bansal
2015-03-14Patches for 32-bit ARMTianyi Liang
2015-01-16Minor: Ensure indexed terms are in EE. Add support for bv constants in ↵ajreynol
sygus parser.
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
trigger terms. I've disabled constants as triggers for all equality engines except for the shared terms engine where it is needed.
2014-12-12Add cvc parsing support for cardinality constraints. Bug fix for ↵ajreynol
enumerating elements to meet cardinality lower bounds.
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-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-19Making construction of trigger sets not use the global engine state.Dejan Jovanović
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-14Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.ajreynol
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not ↵ajreynol
assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
2014-09-24Refactor option for uf+cardinality constraints solver.ajreynol
2014-09-03check() optimizationKshitij Bansal
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
2014-08-04Some fixes to symmetry breaker (resolves bug 576).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-20UF kinds documentationMorgan Deters
2014-05-02Simplification of EqualityEngine::areDisequal. Comparison for production : ↵Andrew Reynolds
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5. Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
2014-04-29Fix compiler warning re: TheoryUF destructor.Morgan Deters
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵Andrew Reynolds
Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ↵Andrew Reynolds
by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.
2014-03-14Add ability to provide theory-specific proof rules to EqualityEngine, ↵Andrew Reynolds
extends enumeration of MergeReasonType. Add initial use in TheoryArrays.
2014-02-21Merge branch '1.3.x'Morgan Deters
2014-02-21No diamond-breaking under quantifiers (resolves bug #550).Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after ↵Morgan Deters
final options/logic are set.
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified ↵Andrew Reynolds
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
2014-01-07minor fix, bring back the assertion.Tianyi Liang
2014-01-07string contain changesTianyi Liang
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵Andrew Reynolds
inst gen-style MBQI.
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing ↵Andrew Reynolds
proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2013-11-19Bug fix for previous commitAndrew Reynolds
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-06Bug fixes for bounded integer quantification. Current best strategy is to ↵Andrew Reynolds
turn off MBQI. Disable relevant triggers by default.
2013-10-24Fix for bug515Clark Barrett
2013-10-03Added support for converting unsorted problems to multi-sorted problems via ↵Andrew Reynolds
sort inference and monotonicity. Minor cleanup.
2013-09-30Bug fixes and improvements for symmetry breaking, it now supports multiple ↵Andrew Reynolds
sorts. Working on monotonicity inference.
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements ↵Andrew Reynolds
to bounded integer quantifier instantiation.
2013-09-24Reduce compiler dependencies on substitutions.h,Clark Barrett
Some new functionality in substitutions.h/cpp
2013-09-23Revert Clark's last commit, at his request; there are some bugs.Morgan Deters
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
for faster compilation
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback