Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-04-07 | Removing the reference to THEORY_BOOL from the equality engine. This theory | Dejan 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-25 | change const are triggers from false to true in equality engines | Kshitij Bansal | |
2015-03-14 | Patches for 32-bit ARM | Tianyi Liang | |
2015-01-16 | Minor: Ensure indexed terms are in EE. Add support for bv constants in ↵ | ajreynol | |
sygus parser. | |||
2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan 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-12 | Add cvc parsing support for cardinality constraints. Bug fix for ↵ | ajreynol | |
enumerating elements to meet cardinality lower bounds. | |||
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-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-19 | Making construction of trigger sets not use the global engine state. | Dejan Jovanović | |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters | |
2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol | |
2014-11-05 | More 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-24 | Refactor option for uf+cardinality constraints solver. | ajreynol | |
2014-09-03 | check() optimization | Kshitij Bansal | |
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization | |||
2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters | |
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-06-20 | UF kinds documentation | Morgan Deters | |
2014-05-02 | Simplification 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-29 | Fix compiler warning re: TheoryUF destructor. | Morgan Deters | |
2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters | |
2014-04-10 | Add 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-09 | Handle 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-14 | Add ability to provide theory-specific proof rules to EqualityEngine, ↵ | Andrew Reynolds | |
extends enumeration of MergeReasonType. Add initial use in TheoryArrays. | |||
2014-02-21 | Merge branch '1.3.x' | Morgan Deters | |
2014-02-21 | No diamond-breaking under quantifiers (resolves bug #550). | Morgan Deters | |
2014-02-21 | add 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-22 | Delay QuantifiersEngine and UF strong solver initialization until after ↵ | Morgan Deters | |
final options/logic are set. | |||
2014-01-10 | Add 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-07 | minor fix, bring back the assertion. | Tianyi Liang | |
2014-01-07 | string contain changes | Tianyi Liang | |
2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵ | Andrew Reynolds | |
inst gen-style MBQI. | |||
2014-01-03 | Added 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-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters | |
2013-11-27 | General pre-release cleanup commit | Morgan 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-19 | Bug fix for previous commit | Andrew Reynolds | |
2013-11-19 | Add fair strategy for finite model finding multiple sorts --uf-ss-fair. | Andrew Reynolds | |
2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters | |
2013-11-06 | Bug fixes for bounded integer quantification. Current best strategy is to ↵ | Andrew Reynolds | |
turn off MBQI. Disable relevant triggers by default. | |||
2013-10-24 | Fix for bug515 | Clark Barrett | |
2013-10-03 | Added support for converting unsorted problems to multi-sorted problems via ↵ | Andrew Reynolds | |
sort inference and monotonicity. Minor cleanup. | |||
2013-09-30 | Bug fixes and improvements for symmetry breaking, it now supports multiple ↵ | Andrew Reynolds | |
sorts. Working on monotonicity inference. | |||
2013-09-27 | Add new symmetry breaking technique for finite model finding. Improvements ↵ | Andrew Reynolds | |
to bounded integer quantifier instantiation. | |||
2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett | |
Some new functionality in substitutions.h/cpp | |||
2013-09-23 | Revert Clark's last commit, at his request; there are some bugs. | Morgan Deters | |
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0. | |||
2013-09-23 | Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h | Clark Barrett | |
for faster compilation | |||
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters | |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters | |
2013-07-19 | possible fix for bug 521 | Dejan Jovanovic | |
2013-07-16 | "Tabular"-style function definitions in models with ↵ | Morgan Deters | |
--no-condense-function-values | |||
2013-07-02 | Make uf strong solver user-context dependent, fixes bug 522. | Andrew Reynolds | |