summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers
AgeCommit message (Collapse)Author
2016-03-18Limit duplicate propagating instances to avoid exponential behavior in ↵ajreynol
QuantConflictFind.
2016-03-12Add options related to interleaving quantifiers and theory combination, ↵ajreynol
changes default behavior.
2016-03-02Work towards complete instantiation for datatypes.ajreynol
2016-03-01Shorter explanations for strings based on tracking which parts of normal ↵ajreynol
forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
2016-02-18Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug ↵ajreynol
fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.
2016-02-11More aggressive conditional rewriting for quantified formulas. Bug fix set ↵ajreynol
incomplete for fmc.
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix ↵ajreynol
enumerator and codatatype rewriter, further simplify fmc.
2015-11-11Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to ↵ajreynol
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-11-05Merging the google branch back into master.Tim King
2015-11-05Fixes some initialization and desctruction problems in quantifiers. Also ↵Tim King
restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
2015-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-26Extend counterexample-guided instantiation to extended theory of Int/Real, ↵ajreynol
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
2015-10-22Enable counterexample-guided quantifier instantiation by default for ↵ajreynol
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
2015-09-24Counterexample-guided instantiation for datatypes. Make sygus parsing more ↵ajreynol
liberal.
2015-08-27Modify slow regressions.ajreynol
2015-08-24Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ↵ajreynol
symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
2015-08-21Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. ↵ajreynol
Enable redundant ITE branch elimination in quantifiers rewriter.
2015-08-19Implementation of model-based projection in cbqi, cleanup, add regressions.ajreynol
2015-08-12Improvements to --macros-quant. Enable --clause-split by default. Bug fix ↵ajreynol
for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
2015-07-30Implement virtual term substitution for non-nested quantifiers. Fix ↵ajreynol
soundness bug in strings related to explaining length terms.
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
(mostly whitespace differences).
2015-04-21Fix file permissionsClark Barrett
2015-03-23Parsing support for define-fun-rec/define-funs-rec.ajreynol
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-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-09-17Fix soundness bug for quantifier macros involving Int/Real.ajreynol
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵ajreynol
Add regressions.
2014-05-10Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, ↵Andrew Reynolds
minor changes.
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
This commit includes work from the past month on the T-entailment check infrastructure (due to Tim), an entailment check for arithmetic (also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds). Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
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-03-05Revert "fix naming conflicts in benchmarks"Kshitij Bansal
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
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-02-10Fix build (some nonexistent files listed in Makefile)Morgan Deters
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out ↵Andrew Reynolds
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
2014-01-26More optimization of QCF. Fixed InstMatchTrie for caching instantiations. ↵Andrew Reynolds
Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Move some regress benchmarks around that took too long, other test cleanup.Morgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed ↵Andrew Reynolds
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-09-18SMT-LIBv2 compliance regarding outputting "unknown".Morgan Deters
Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-31merge from fmf-devel branch. more updates to models: now with ↵Andrew Reynolds
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions ↵Morgan Deters
should work now
2012-08-27* Reversing commit r4258 (which disabled failing regressions). Fixed the ↵Morgan Deters
problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381. * Added LAMBDA kind and type rule, and Node::isClosure(). (this commit was certified error- and warning-free by the test-and-commit script.)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback