summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Collapse)Author
2014-04-09inputs to trigger bugKshitij Bansal
2014-04-06Reduced example from pcc's bug report.Tim King
2014-04-06Merge pull request #21 from pcc/ite-fixTim King
Fix for ite of >=64bit wide bitvectors with unconstrained condition.
2014-04-03Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis ↵Morgan Deters
Deligiannis and Jeroen Ketema for discovering this issue.
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-28add construles, type_rules rm redundant, kinds cleanupKshitij Bansal
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-20Merge pull request #22 from kbansal/sets-modelKshitij Bansal
Sets model
2014-03-20cleanupKshitij Bansal
2014-03-20fix for sets/mar2014/..317minimized..Kshitij Bansal
Observed behavior: --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) with different set of elements in the model for representative and the node itself. Issue: The trouble with data structure being mainted to ensure that things for which lemmas have been generated are not generated again. This data structure (d_pendingEverInserted) needs to be user context dependent. The bug was in the sequence of steps from requesting that a lemma be generated to when it actually was. Sequence was: addToPending (and also adds to pending ever inserted) -> isComplete (might remove things from pending if requirment met in other ways) -> getLemma (actually generated the lemma, if requirement not already met) Resolution: adding terms to d_pendingEverInserted was moved from addToPending() to getLemma().
2014-03-20Fix for registration issues of term appearing in a shared lemmaKshitij Bansal
(brought to attention by lianah -- fix currently just adapted using arrays -- this is to remind me to raise why do we even have this isPreregistered bussiness)
2014-03-20fix a sharing issues with setsKshitij Bansal
2014-03-20enable check-models for sets/ regressionsKshitij Bansal
2014-03-20testlemma regressionsKshitij Bansal
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-16Fix for ite of >=64bit wide bitvectors with unconstrained condition.Peter Collingbourne
2014-03-12Work on array pf signature, add working example. Add quantifiers proof ↵Andrew Reynolds
signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes ↵Morgan Deters
cases of nonterminating rewrite-rules regressions.
2014-03-11Minor cleanup.Morgan Deters
* Reenable parts of bvsimple test * Fix typo in #endif comment
2014-03-11Fix for (get-assignment), resolves bug 553.Morgan Deters
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵Andrew Reynolds
Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge.
2014-03-08Merge remote-tracking branch 'CVC4root/master'Tim King
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵Morgan Deters
bodies; fix bug 551, improper ITE removal under quantifiers.
2014-03-07Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into ↵Tim King
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
2014-03-05Array smtlib compliance testsKshitij Bansal
2014-03-05Revert "fix naming conflicts in benchmarks"Kshitij Bansal
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
2014-03-05Don't tokenize SET_THEORY operators in smt2 parserKshitij Bansal
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-02-28a new regular expression engine for solving both positive and negative ↵Tianyi Liang
membership constraints
2014-02-26sorry for the missing fileTianyi Liang
2014-02-26bug fix (caused by merge), move cardinality option to expert optionTianyi Liang
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-20fix makefileTianyi Liang
2014-02-20add more tests, and define int.to.str(NEGATIVE)=""Tianyi Liang
2014-02-20add two cases to the regression testTianyi Liang
2014-02-19Merge branch '1.3.x'Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
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-28merge internal and user of charat & substr into oneTianyi Liang
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.
2014-01-18strings with new ideasTianyi Liang
2014-01-16adds partial functionsTianyi Liang
2013-12-26new functions in stringsTianyi Liang
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-12-16Fix for bug 544.Morgan Deters
2013-12-13cleanupMorgan Deters
2013-12-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-05disable substring in default modeTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback