Tianyi Liang [Thu, 27 Mar 2014 21:54:46 +0000 (16:54 -0500)]
adds new feature: re.loop
Tianyi Liang [Wed, 26 Mar 2014 22:31:23 +0000 (17:31 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 26 Mar 2014 22:30:30 +0000 (17:30 -0500)]
deriv symbolic regexp
Tianyi Liang [Tue, 25 Mar 2014 06:08:29 +0000 (01:08 -0500)]
adds intersection
Tianyi Liang [Wed, 26 Mar 2014 22:30:30 +0000 (17:30 -0500)]
deriv symbolic regexp
Tim King [Wed, 26 Mar 2014 20:56:13 +0000 (16:56 -0400)]
Merging in a fix from 1.3.x.
Fixes an idempotency issue for non-linear multiplication with integer and real variables.
Conflicts:
src/theory/arith/normal_form.cpp
Tianyi Liang [Tue, 25 Mar 2014 06:08:29 +0000 (01:08 -0500)]
adds intersection
Kshitij Bansal [Fri, 21 Mar 2014 02:57:20 +0000 (22:57 -0400)]
Merge pull request #22 from kbansal/sets-model
Sets model
Kshitij Bansal [Thu, 20 Mar 2014 23:27:21 +0000 (19:27 -0400)]
cleanup
Kshitij Bansal [Thu, 20 Mar 2014 06:01:24 +0000 (02:01 -0400)]
fix for sets/mar2014/..317minimized..
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().
Kshitij Bansal [Mon, 17 Mar 2014 22:01:10 +0000 (18:01 -0400)]
Fix for registration issues of term appearing in a shared lemma
(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)
Kshitij Bansal [Fri, 14 Mar 2014 02:27:22 +0000 (22:27 -0400)]
rewriter fix, weaken an assertion
Kshitij Bansal [Fri, 14 Mar 2014 02:17:02 +0000 (22:17 -0400)]
constant normal form and rewrite
Kshitij Bansal [Thu, 13 Mar 2014 23:33:11 +0000 (19:33 -0400)]
fix a sharing issues with sets
Kshitij Bansal [Wed, 12 Mar 2014 18:43:37 +0000 (14:43 -0400)]
push subtyping for sets to the element type
for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real
Kshitij Bansal [Wed, 12 Mar 2014 03:47:33 +0000 (23:47 -0400)]
enable check-models for sets/ regressions
Kshitij Bansal [Mon, 10 Mar 2014 23:02:32 +0000 (19:02 -0400)]
work on set model
Kshitij Bansal [Wed, 12 Mar 2014 17:53:22 +0000 (13:53 -0400)]
testlemma regressions
Andrew Reynolds [Thu, 20 Mar 2014 21:10:04 +0000 (16:10 -0500)]
Minor fix for CBQI, ignore inst constant nodes.
Morgan Deters [Wed, 19 Mar 2014 21:30:59 +0000 (17:30 -0400)]
Fix documentation for Theory::preRegisterTerm().
Martin Brain [Tue, 11 Mar 2014 00:03:41 +0000 (00:03 +0000)]
Refactor the theory specific parts of definition expansion into the theory solvers.
In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Morgan Deters [Wed, 19 Mar 2014 20:32:05 +0000 (16:32 -0400)]
Set dumping options from (set-option..) and API more directly.
Morgan Deters [Wed, 19 Mar 2014 17:58:59 +0000 (13:58 -0400)]
Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.
Morgan Deters [Sat, 15 Mar 2014 21:41:27 +0000 (17:41 -0400)]
Move the translator binary from src/main to examples, no longer built by default.
Morgan Deters [Sat, 15 Mar 2014 21:38:07 +0000 (17:38 -0400)]
Appease compilers from latest XCode release (v5.1).
Morgan Deters [Sat, 15 Mar 2014 21:29:09 +0000 (17:29 -0400)]
Minor usability fixes related to SMT-LIB compliance.
Morgan Deters [Wed, 19 Mar 2014 14:34:41 +0000 (10:34 -0400)]
Fix proof signatures makefile
Morgan Deters [Fri, 14 Mar 2014 20:10:37 +0000 (16:10 -0400)]
Minor documentation fixups.
Andrew Reynolds [Wed, 19 Mar 2014 14:03:18 +0000 (09:03 -0500)]
Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan (problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof.
Tianyi Liang [Mon, 17 Mar 2014 18:22:21 +0000 (13:22 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 17 Mar 2014 18:17:12 +0000 (13:17 -0500)]
hot fix for pre-reg term caching in strings
Tianyi Liang [Mon, 17 Mar 2014 18:17:12 +0000 (13:17 -0500)]
hot fix for pre-reg term caching in strings
Morgan Deters [Fri, 14 Mar 2014 19:21:24 +0000 (15:21 -0400)]
SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). Thanks to David Cok for the bug report.
Morgan Deters [Thu, 13 Mar 2014 17:00:07 +0000 (13:00 -0400)]
dos2unix on the proof signatures, and fix the makefile.
Andrew Reynolds [Fri, 14 Mar 2014 16:50:28 +0000 (11:50 -0500)]
Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType. Add initial use in TheoryArrays.
Andrew Reynolds [Thu, 13 Mar 2014 14:58:07 +0000 (09:58 -0500)]
Add working example of LFSC proof with quantifiers. Update quantifiers signature to avoid dependent types in side condition.
Andrew Reynolds [Wed, 12 Mar 2014 19:25:25 +0000 (14:25 -0500)]
Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
Andrew Reynolds [Wed, 12 Mar 2014 15:51:55 +0000 (10:51 -0500)]
Minor fixes post-merge of RR.
Morgan Deters [Wed, 12 Mar 2014 10:18:19 +0000 (06:18 -0400)]
Fix LogicInfo unit test.
Morgan Deters [Wed, 12 Mar 2014 09:26:19 +0000 (05:26 -0400)]
Some standardization of regression Makefiles that got out of sync. Fixes cases of nonterminating rewrite-rules regressions.
Morgan Deters [Wed, 12 Mar 2014 01:32:49 +0000 (21:32 -0400)]
Draft contrib/get-abc script for bitvectors libabc support.
Morgan Deters [Tue, 11 Mar 2014 23:08:38 +0000 (19:08 -0400)]
Merge branch '1.3.x'
Morgan Deters [Tue, 11 Mar 2014 22:47:18 +0000 (18:47 -0400)]
Fix for rewriterules build breakage.
Morgan Deters [Tue, 11 Mar 2014 22:50:51 +0000 (18:50 -0400)]
Fix for random-seed option.
Morgan Deters [Tue, 11 Mar 2014 22:47:28 +0000 (18:47 -0400)]
Fix for portfolio.
Morgan Deters [Sat, 8 Mar 2014 06:38:25 +0000 (01:38 -0500)]
Minor cleanup.
* Reenable parts of bvsimple test
* Fix typo in #endif comment
Morgan Deters [Fri, 7 Mar 2014 20:42:29 +0000 (15:42 -0500)]
Fix for (get-assignment), resolves bug 553.
Morgan Deters [Tue, 11 Mar 2014 21:54:15 +0000 (17:54 -0400)]
Merge branch '1.3.x'
Morgan Deters [Tue, 11 Mar 2014 19:07:38 +0000 (15:07 -0400)]
Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.
Andrew Reynolds [Thu, 20 Feb 2014 15:45:46 +0000 (09:45 -0600)]
Initial refactor of rewrite rules, make theory_rewriterules empty theory. 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.
Tianyi Liang [Mon, 10 Mar 2014 22:30:18 +0000 (17:30 -0500)]
adds intro vars length cache
Tianyi Liang [Mon, 10 Mar 2014 16:54:02 +0000 (11:54 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 10 Mar 2014 16:53:12 +0000 (11:53 -0500)]
minor change for strings-fmf
Tianyi Liang [Mon, 10 Mar 2014 16:53:12 +0000 (11:53 -0500)]
minor change for strings-fmf
Morgan Deters [Sat, 8 Mar 2014 20:33:46 +0000 (15:33 -0500)]
Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-ground ITEs also.
Tim King [Sat, 8 Mar 2014 19:44:56 +0000 (14:44 -0500)]
Merge pull request #18 from timothy-king/master
Merging in the glpk changes
Tim King [Sat, 8 Mar 2014 19:42:35 +0000 (14:42 -0500)]
Fixing name changes that cam in from the merge.
Tim King [Sat, 8 Mar 2014 19:27:40 +0000 (14:27 -0500)]
Merge remote-tracking branch 'CVC4root/master'
Morgan Deters [Fri, 7 Mar 2014 15:24:04 +0000 (10:24 -0500)]
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
Morgan Deters [Thu, 6 Mar 2014 21:53:16 +0000 (16:53 -0500)]
Fix run_regression on Mac.
Morgan Deters [Sat, 8 Mar 2014 04:47:56 +0000 (23:47 -0500)]
Fix bug 554 (nominally).
Tim King [Sat, 8 Mar 2014 00:45:37 +0000 (19:45 -0500)]
Fixing a SWIG problem for RationalFromDoubleException.
Tim King [Fri, 7 Mar 2014 23:00:37 +0000 (18:00 -0500)]
Merging a squash of the branch timothy-king/CVC4/glpknecfix
c95bf7d4f1 into 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.
Tianyi Liang [Fri, 7 Mar 2014 21:04:09 +0000 (15:04 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 7 Mar 2014 20:32:18 +0000 (14:32 -0600)]
remove unrolling depth
Tianyi Liang [Fri, 7 Mar 2014 18:35:15 +0000 (12:35 -0600)]
bring back D-Norm
Morgan Deters [Thu, 6 Mar 2014 22:06:12 +0000 (17:06 -0500)]
Fix strings-exp setting.
Tianyi Liang [Fri, 7 Mar 2014 20:32:18 +0000 (14:32 -0600)]
remove unrolling depth
Tianyi Liang [Fri, 7 Mar 2014 18:35:15 +0000 (12:35 -0600)]
bring back D-Norm
Morgan Deters [Thu, 6 Mar 2014 22:06:12 +0000 (17:06 -0500)]
Fix strings-exp setting.
Thomas Hunger [Thu, 6 Mar 2014 22:37:34 +0000 (22:37 +0000)]
Add swig renames for new Z3STR language.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Tianyi Liang [Fri, 7 Mar 2014 03:34:10 +0000 (21:34 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 7 Mar 2014 03:27:37 +0000 (21:27 -0600)]
adds incremental for strings; clean-up codes
Tianyi Liang [Fri, 7 Mar 2014 03:27:37 +0000 (21:27 -0600)]
adds incremental for strings; clean-up codes
Kshitij Bansal [Wed, 5 Mar 2014 22:38:19 +0000 (17:38 -0500)]
Merge pull request #14 from kbansal/sets-parserchanges
Sets parserchanges
Kshitij Bansal [Wed, 5 Mar 2014 19:48:08 +0000 (14:48 -0500)]
Array smtlib compliance tests
Kshitij Bansal [Fri, 28 Feb 2014 15:19:26 +0000 (10:19 -0500)]
Revert "fix naming conflicts in benchmarks"
This reverts commit
4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
Kshitij Bansal [Wed, 5 Mar 2014 03:16:21 +0000 (22:16 -0500)]
Don't tokenize SET_THEORY operators in smt2 parser
Tim King [Wed, 5 Mar 2014 17:04:03 +0000 (12:04 -0500)]
Improving support for POW in arithmetic. Resolves bug 549.
Thomas Hunger [Sun, 2 Mar 2014 16:01:37 +0000 (16:01 +0000)]
Guard java-specific swig code with SWIGJAVA.
Without this building just the python bindings will fail.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Morgan Deters [Mon, 17 Feb 2014 23:59:39 +0000 (18:59 -0500)]
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
Morgan Deters [Sat, 1 Mar 2014 18:27:20 +0000 (13:27 -0500)]
More useful error message when someone tries mkExpr(VARIABLE).
Tianyi Liang [Sat, 1 Mar 2014 04:59:25 +0000 (22:59 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sat, 1 Mar 2014 04:56:45 +0000 (22:56 -0600)]
add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors
Tianyi Liang [Fri, 28 Feb 2014 19:04:33 +0000 (13:04 -0600)]
minor clean-up, bring back derivatives
Tianyi Liang [Fri, 28 Feb 2014 17:05:09 +0000 (11:05 -0600)]
a new regular expression engine for solving both positive and negative membership constraints
Tianyi Liang [Sat, 1 Mar 2014 04:56:45 +0000 (22:56 -0600)]
add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors
Tianyi Liang [Fri, 28 Feb 2014 19:04:33 +0000 (13:04 -0600)]
minor clean-up, bring back derivatives
Tianyi Liang [Fri, 28 Feb 2014 17:05:09 +0000 (11:05 -0600)]
a new regular expression engine for solving both positive and negative membership constraints
Kshitij Bansal [Fri, 28 Feb 2014 14:50:47 +0000 (09:50 -0500)]
Merge pull request #12 from kbansal/in-to-member
rename the kind IN to MEMBER
Kshitij Bansal [Fri, 28 Feb 2014 13:21:21 +0000 (08:21 -0500)]
theory/sets: cleanup
Kshitij Bansal [Fri, 28 Feb 2014 13:14:43 +0000 (08:14 -0500)]
rename kind::IN to kind::MEMBER (fixes some windows build conflicts)
Kshitij Bansal [Fri, 28 Feb 2014 02:36:32 +0000 (21:36 -0500)]
Merge pull request #11 from kbansal/improve-stats-every-query
--stats-every-query option: print increment in addition to cumulative va...
Kshitij Bansal [Thu, 27 Feb 2014 21:43:48 +0000 (16:43 -0500)]
--stats-every-query option: print increment in addition to cumulative value of each stat
the increment is printed in parantheses at the end, e.g.
sat::decisions, 100 (50)
Andrew Reynolds [Thu, 27 Feb 2014 14:34:59 +0000 (08:34 -0600)]
Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the default QCF setting. Bug fix to prevent non-ground terms from entering relevant domains.
Tianyi Liang [Wed, 26 Feb 2014 20:37:59 +0000 (14:37 -0600)]
sorry for the missing file
Tianyi Liang [Wed, 26 Feb 2014 20:19:49 +0000 (14:19 -0600)]
bug fix (caused by merge), move cardinality option to expert option
Tianyi Liang [Wed, 26 Feb 2014 17:44:51 +0000 (11:44 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 26 Feb 2014 17:43:59 +0000 (11:43 -0600)]
add a new file
Tianyi Liang [Wed, 26 Feb 2014 17:29:38 +0000 (11:29 -0600)]
for merging