cvc5.git
10 years agoAdd ability to provide theory-specific proof rules to EqualityEngine, extends enumera...
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.

10 years agoAdd working example of LFSC proof with quantifiers. Update quantifiers signature...
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.

10 years agoWork on array pf signature, add working example. Add quantifiers proof signature...
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.

10 years agoMinor fixes post-merge of RR.
Andrew Reynolds [Wed, 12 Mar 2014 15:51:55 +0000 (10:51 -0500)]
Minor fixes post-merge of RR.

10 years agoFix LogicInfo unit test.
Morgan Deters [Wed, 12 Mar 2014 10:18:19 +0000 (06:18 -0400)]
Fix LogicInfo unit test.

10 years agoSome standardization of regression Makefiles that got out of sync. Fixes cases of...
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.

10 years agoDraft contrib/get-abc script for bitvectors libabc support.
Morgan Deters [Wed, 12 Mar 2014 01:32:49 +0000 (21:32 -0400)]
Draft contrib/get-abc script for bitvectors libabc support.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 11 Mar 2014 23:08:38 +0000 (19:08 -0400)]
Merge branch '1.3.x'

10 years agoFix for rewriterules build breakage.
Morgan Deters [Tue, 11 Mar 2014 22:47:18 +0000 (18:47 -0400)]
Fix for rewriterules build breakage.

10 years agoFix for random-seed option.
Morgan Deters [Tue, 11 Mar 2014 22:50:51 +0000 (18:50 -0400)]
Fix for random-seed option.

10 years agoFix for portfolio.
Morgan Deters [Tue, 11 Mar 2014 22:47:28 +0000 (18:47 -0400)]
Fix for portfolio.

10 years agoMinor cleanup.
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

10 years agoFix for (get-assignment), resolves bug 553.
Morgan Deters [Fri, 7 Mar 2014 20:42:29 +0000 (15:42 -0500)]
Fix for (get-assignment), resolves bug 553.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 11 Mar 2014 21:54:15 +0000 (17:54 -0400)]
Merge branch '1.3.x'

10 years agoFix some Win32 and SMT-LIB compliance bugs discovered by David Cok.
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.

10 years agoInitial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds...
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.

10 years agoadds intro vars length cache
Tianyi Liang [Mon, 10 Mar 2014 22:30:18 +0000 (17:30 -0500)]
adds intro vars length cache

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 10 Mar 2014 16:54:02 +0000 (11:54 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agominor change for strings-fmf
Tianyi Liang [Mon, 10 Mar 2014 16:53:12 +0000 (11:53 -0500)]
minor change for strings-fmf

10 years agominor change for strings-fmf
Tianyi Liang [Mon, 10 Mar 2014 16:53:12 +0000 (11:53 -0500)]
minor change for strings-fmf

10 years agoRe-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-ground...
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.

10 years agoMerge pull request #18 from timothy-king/master
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

10 years agoFixing name changes that cam in from the merge.
Tim King [Sat, 8 Mar 2014 19:42:35 +0000 (14:42 -0500)]
Fixing name changes that cam in from the merge.

10 years agoMerge remote-tracking branch 'CVC4root/master'
Tim King [Sat, 8 Mar 2014 19:27:40 +0000 (14:27 -0500)]
Merge remote-tracking branch 'CVC4root/master'

10 years agoRemove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies;...
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.

10 years agoFix run_regression on Mac.
Morgan Deters [Thu, 6 Mar 2014 21:53:16 +0000 (16:53 -0500)]
Fix run_regression on Mac.

10 years agoFix bug 554 (nominally).
Morgan Deters [Sat, 8 Mar 2014 04:47:56 +0000 (23:47 -0500)]
Fix bug 554 (nominally).

10 years agoFixing a SWIG problem for RationalFromDoubleException.
Tim King [Sat, 8 Mar 2014 00:45:37 +0000 (19:45 -0500)]
Fixing a SWIG problem for RationalFromDoubleException.

10 years agoMerging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master...
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.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 7 Mar 2014 21:04:09 +0000 (15:04 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoremove unrolling depth
Tianyi Liang [Fri, 7 Mar 2014 20:32:18 +0000 (14:32 -0600)]
remove unrolling depth

10 years agobring back D-Norm
Tianyi Liang [Fri, 7 Mar 2014 18:35:15 +0000 (12:35 -0600)]
bring back D-Norm

10 years agoFix strings-exp setting.
Morgan Deters [Thu, 6 Mar 2014 22:06:12 +0000 (17:06 -0500)]
Fix strings-exp setting.

10 years agoremove unrolling depth
Tianyi Liang [Fri, 7 Mar 2014 20:32:18 +0000 (14:32 -0600)]
remove unrolling depth

10 years agobring back D-Norm
Tianyi Liang [Fri, 7 Mar 2014 18:35:15 +0000 (12:35 -0600)]
bring back D-Norm

10 years agoFix strings-exp setting.
Morgan Deters [Thu, 6 Mar 2014 22:06:12 +0000 (17:06 -0500)]
Fix strings-exp setting.

10 years agoAdd swig renames for new Z3STR language.
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>
10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 7 Mar 2014 03:34:10 +0000 (21:34 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadds 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

10 years agoadds 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

10 years agoMerge pull request #14 from kbansal/sets-parserchanges
Kshitij Bansal [Wed, 5 Mar 2014 22:38:19 +0000 (17:38 -0500)]
Merge pull request #14 from kbansal/sets-parserchanges

Sets parserchanges

10 years agoArray smtlib compliance tests
Kshitij Bansal [Wed, 5 Mar 2014 19:48:08 +0000 (14:48 -0500)]
Array smtlib compliance tests

10 years agoRevert "fix naming conflicts in benchmarks"
Kshitij Bansal [Fri, 28 Feb 2014 15:19:26 +0000 (10:19 -0500)]
Revert "fix naming conflicts in benchmarks"

This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.

10 years agoDon't tokenize SET_THEORY operators in smt2 parser
Kshitij Bansal [Wed, 5 Mar 2014 03:16:21 +0000 (22:16 -0500)]
Don't tokenize SET_THEORY operators in smt2 parser

10 years agoImproving support for POW in arithmetic. Resolves bug 549.
Tim King [Wed, 5 Mar 2014 17:04:03 +0000 (12:04 -0500)]
Improving support for POW in arithmetic. Resolves bug 549.

10 years agoGuard java-specific swig code with SWIGJAVA.
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>
10 years agoDon't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves...
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).

10 years agoMore useful error message when someone tries mkExpr(VARIABLE).
Morgan Deters [Sat, 1 Mar 2014 18:27:20 +0000 (13:27 -0500)]
More useful error message when someone tries mkExpr(VARIABLE).

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sat, 1 Mar 2014 04:59:25 +0000 (22:59 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd re.nostr for the empty regular expression; add re.allchar for the regular express...
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

10 years agominor clean-up, bring back derivatives
Tianyi Liang [Fri, 28 Feb 2014 19:04:33 +0000 (13:04 -0600)]
minor clean-up, bring back derivatives

10 years agoa new regular expression engine for solving both positive and negative membership...
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

10 years agoadd re.nostr for the empty regular expression; add re.allchar for the regular express...
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

10 years agominor clean-up, bring back derivatives
Tianyi Liang [Fri, 28 Feb 2014 19:04:33 +0000 (13:04 -0600)]
minor clean-up, bring back derivatives

10 years agoa new regular expression engine for solving both positive and negative membership...
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

10 years agoMerge pull request #12 from kbansal/in-to-member
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

10 years agotheory/sets: cleanup
Kshitij Bansal [Fri, 28 Feb 2014 13:21:21 +0000 (08:21 -0500)]
theory/sets: cleanup

10 years agorename kind::IN to kind::MEMBER (fixes some windows build conflicts)
Kshitij Bansal [Fri, 28 Feb 2014 13:14:43 +0000 (08:14 -0500)]
rename kind::IN to kind::MEMBER (fixes some windows build conflicts)

10 years agoMerge pull request #11 from kbansal/improve-stats-every-query
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...

10 years ago--stats-every-query option: print increment in addition to cumulative value of each...
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)

10 years agoBug fix for QCF algorithm, was missing instantiations. Make prop-eq the default...
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.

10 years agosorry for the missing file
Tianyi Liang [Wed, 26 Feb 2014 20:37:59 +0000 (14:37 -0600)]
sorry for the missing file

10 years agobug fix (caused by merge), move cardinality option to expert option
Tianyi Liang [Wed, 26 Feb 2014 20:19:49 +0000 (14:19 -0600)]
bug fix (caused by merge), move cardinality option to expert option

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 26 Feb 2014 17:44:51 +0000 (11:44 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd a new file
Tianyi Liang [Wed, 26 Feb 2014 17:43:59 +0000 (11:43 -0600)]
add a new file

10 years agofor merging
Tianyi Liang [Wed, 26 Feb 2014 17:29:38 +0000 (11:29 -0600)]
for merging

10 years agosmt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc...
Tianyi Liang [Mon, 24 Feb 2014 20:45:06 +0000 (14:45 -0600)]
smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

10 years agofor merging
Tianyi Liang [Wed, 26 Feb 2014 17:29:38 +0000 (11:29 -0600)]
for merging

10 years agoMinor code clean up in parser.
Morgan Deters [Fri, 14 Feb 2014 23:28:02 +0000 (18:28 -0500)]
Minor code clean up in parser.

10 years agoNew translation work, support Z3-str-style string constraints.
Morgan Deters [Tue, 11 Feb 2014 02:05:16 +0000 (21:05 -0500)]
New translation work, support Z3-str-style string constraints.

10 years agoFix quotes in string constants.
Morgan Deters [Tue, 11 Feb 2014 02:04:58 +0000 (21:04 -0500)]
Fix quotes in string constants.

10 years agoAdd options --full-saturate-quant and --mbqi=trust. Other minor changes.
Andrew Reynolds [Tue, 25 Feb 2014 17:08:33 +0000 (11:08 -0600)]
Add options --full-saturate-quant and --mbqi=trust.  Other minor changes.

10 years agosmt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc...
Tianyi Liang [Mon, 24 Feb 2014 20:45:06 +0000 (14:45 -0600)]
smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

10 years agobug fix: strings preprocess for the orignal term, causing unknown in some cases
Tianyi Liang [Mon, 24 Feb 2014 17:36:23 +0000 (11:36 -0600)]
bug fix: strings preprocess for the orignal term, causing unknown in some cases

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 21 Feb 2014 23:16:38 +0000 (18:16 -0500)]
Merge branch '1.3.x'

10 years agoNo diamond-breaking under quantifiers (resolves bug #550).
Morgan Deters [Fri, 21 Feb 2014 22:15:43 +0000 (17:15 -0500)]
No diamond-breaking under quantifiers (resolves bug #550).

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 21 Feb 2014 21:20:35 +0000 (15:20 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoreorganize substr, fix some potential bugs, adds cache for preprocessing
Tianyi Liang [Fri, 21 Feb 2014 21:19:05 +0000 (15:19 -0600)]
reorganize substr, fix some potential bugs, adds cache for preprocessing

10 years agoreorganize substr, fix some potential bugs, adds cache for preprocessing
Tianyi Liang [Fri, 21 Feb 2014 21:19:05 +0000 (15:19 -0600)]
reorganize substr, fix some potential bugs, adds cache for preprocessing

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 21 Feb 2014 20:08:01 +0000 (15:08 -0500)]
Merge branch '1.3.x'

10 years agoFix two variants of Node::substitute().
Morgan Deters [Fri, 21 Feb 2014 19:45:52 +0000 (14:45 -0500)]
Fix two variants of Node::substitute().

Node::substitute() is overloaded.  One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted).  The others were
ignoring anything in function position.  Fixed.  Thanks to Wei Wang for
pointing this out.

10 years agoportfolio: fix export of emptyset
Kshitij Bansal [Fri, 21 Feb 2014 18:52:34 +0000 (13:52 -0500)]
portfolio: fix export of emptyset

10 years agoFix makefile dependence for system tests.
Morgan Deters [Fri, 21 Feb 2014 17:35:37 +0000 (12:35 -0500)]
Fix makefile dependence for system tests.

10 years agodisable test cvc3_main, attempt to fix dist_check
Kshitij Bansal [Fri, 21 Feb 2014 15:09:00 +0000 (10:09 -0500)]
disable test cvc3_main, attempt to fix dist_check

10 years agoMerge pull request #10 from kbansal/sets-for-merge
Kshitij Bansal [Fri, 21 Feb 2014 13:33:23 +0000 (08:33 -0500)]
Merge pull request #10 from kbansal/sets-for-merge

Sets for merge

10 years agooption to print stats after every satisfiability or validity query
Kshitij Bansal [Fri, 21 Feb 2014 09:06:40 +0000 (04:06 -0500)]
option to print stats after every satisfiability or validity query

10 years agoadd new theory (sets)
Kshitij Bansal [Mon, 9 Sep 2013 18:47:53 +0000 (14:47 -0400)]
add new theory (sets)

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

10 years agofix a -Wunused
Kshitij Bansal [Fri, 21 Feb 2014 09:58:31 +0000 (04:58 -0500)]
fix a -Wunused

10 years agofix makefile
Tianyi Liang [Fri, 21 Feb 2014 01:52:20 +0000 (19:52 -0600)]
fix makefile

10 years agoadd more tests, and define int.to.str(NEGATIVE)=""
Tianyi Liang [Fri, 21 Feb 2014 00:31:27 +0000 (18:31 -0600)]
add more tests, and define int.to.str(NEGATIVE)=""

10 years agoadd two cases to the regression test
Tianyi Liang [Thu, 20 Feb 2014 23:16:43 +0000 (17:16 -0600)]
add two cases to the regression test

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 20 Feb 2014 23:07:24 +0000 (17:07 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

10 years agohot fix for str2int/int2str
Tianyi Liang [Thu, 20 Feb 2014 22:07:23 +0000 (16:07 -0600)]
hot fix for str2int/int2str

10 years agoadd negative int2str
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str

10 years agoString parsing example in CVC parser
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 20 Feb 2014 23:03:24 +0000 (17:03 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

10 years agohot fix for str2int/int2str
Tianyi Liang [Thu, 20 Feb 2014 22:07:23 +0000 (16:07 -0600)]
hot fix for str2int/int2str

10 years agoadd negative int2str
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str

10 years agoString parsing example in CVC parser
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser

10 years agoFix ite and iff handling in QCF. Add option for heuristic instantiation in QCF ...
Andrew Reynolds [Thu, 20 Feb 2014 16:37:32 +0000 (10:37 -0600)]
Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF (not working yet).  Improve automatic option setting for quantifiers.