cvc5.git
10 years agoSupport E-matching/QCF for Set operators.
ajreynol [Tue, 3 Jun 2014 12:01:01 +0000 (14:01 +0200)]
Support E-matching/QCF for Set operators.

10 years agoFix for Windows builds (rlimit doesn't exist on Windows).
Morgan Deters [Sun, 1 Jun 2014 17:21:05 +0000 (13:21 -0400)]
Fix for Windows builds (rlimit doesn't exist on Windows).

10 years agoMore make rules
Morgan Deters [Fri, 30 May 2014 23:31:12 +0000 (19:31 -0400)]
More make rules

10 years agoOne final bit (I hope) of make magic
Morgan Deters [Fri, 30 May 2014 22:01:47 +0000 (18:01 -0400)]
One final bit (I hope) of make magic

10 years agoMore make rules
Morgan Deters [Fri, 30 May 2014 21:58:48 +0000 (17:58 -0400)]
More make rules

10 years agoBug fix for string-opt2 (copied from Tianyi's branch).
Morgan Deters [Fri, 30 May 2014 21:07:38 +0000 (17:07 -0400)]
Bug fix for string-opt2 (copied from Tianyi's branch).

10 years agoUpdate submission make rules.
Morgan Deters [Fri, 30 May 2014 19:41:20 +0000 (15:41 -0400)]
Update submission make rules.

10 years agoChange SMT COMP script to use external timeouts.
ajreynol [Fri, 30 May 2014 19:30:23 +0000 (21:30 +0200)]
Change SMT COMP script to use external timeouts.

10 years agoRun script updates: no --stats, also application-track version.
Morgan Deters [Fri, 30 May 2014 19:00:38 +0000 (15:00 -0400)]
Run script updates: no --stats, also application-track version.

10 years agorun script fix
Kshitij Bansal [Fri, 30 May 2014 18:38:05 +0000 (14:38 -0400)]
run script fix

10 years agoImprove --dt-stc-ind for multi-variable datatype properties.
ajreynol [Fri, 30 May 2014 13:48:53 +0000 (15:48 +0200)]
Improve --dt-stc-ind for multi-variable datatype properties.

10 years agoFixes for --inst-max-level
ajreynol [Fri, 30 May 2014 10:17:05 +0000 (12:17 +0200)]
Fixes for --inst-max-level

10 years agoFix personal.mk for some make targets.
Morgan Deters [Fri, 30 May 2014 04:11:44 +0000 (00:11 -0400)]
Fix personal.mk for some make targets.

10 years agoMinor changes to script. Disable cbqi sat.
ajreynol [Wed, 28 May 2014 21:32:59 +0000 (23:32 +0200)]
Minor changes to script.  Disable cbqi sat.

10 years agoAdd option to avoid dumping partial models/proofs.
Andrew Reynolds [Wed, 28 May 2014 07:28:39 +0000 (02:28 -0500)]
Add option to avoid dumping partial models/proofs.

10 years agoSome fixes to GC order in Java.
Morgan Deters [Wed, 28 May 2014 03:35:40 +0000 (23:35 -0400)]
Some fixes to GC order in Java.

10 years agoMerge pull request #27 from kbansal/statistics
Kshitij Bansal [Tue, 27 May 2014 21:51:07 +0000 (17:51 -0400)]
Merge pull request #27 from kbansal/statistics

update stats_black

10 years agoupdate stats_black
Kshitij Bansal [Tue, 27 May 2014 20:16:55 +0000 (16:16 -0400)]
update stats_black

10 years agoNew --tear-down-incremental mode, useful for debugging and performance profiling.
Morgan Deters [Tue, 5 Mar 2013 00:58:15 +0000 (19:58 -0500)]
New --tear-down-incremental mode, useful for debugging and performance profiling.

10 years agofix timespec printing
Kshitij Bansal [Tue, 27 May 2014 18:46:11 +0000 (14:46 -0400)]
fix timespec printing

sorry prvs fix added some unrelated code

10 years agoRevert "timespec printing bug"
Kshitij Bansal [Tue, 27 May 2014 18:43:46 +0000 (14:43 -0400)]
Revert "timespec printing bug"

This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.

10 years agotimespec printing bug
Kshitij Bansal [Tue, 27 May 2014 18:41:47 +0000 (14:41 -0400)]
timespec printing bug

10 years agoFix typo in Java destruction code; should fix some recent bug reports of crashes...
Morgan Deters [Tue, 27 May 2014 04:07:17 +0000 (00:07 -0400)]
Fix typo in Java destruction code; should fix some recent bug reports of crashes in Java.

10 years agoImproved type-checking for tuple and record selects.
Morgan Deters [Tue, 27 May 2014 04:06:42 +0000 (00:06 -0400)]
Improved type-checking for tuple and record selects.

10 years agoFix bug 567
Kshitij Bansal [Tue, 27 May 2014 00:22:55 +0000 (20:22 -0400)]
Fix bug 567

This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083.
The backing Node didn't always exist because of the changes.

10 years agoFixing Tim's subtype/solving bug for arrays
Clark Barrett [Mon, 26 May 2014 19:30:13 +0000 (12:30 -0700)]
Fixing Tim's subtype/solving bug for arrays

10 years agoSeparating an implicit inclusion of smt_engine.h from theory.h.
Tim King [Mon, 26 May 2014 15:44:38 +0000 (11:44 -0400)]
Separating an implicit inclusion of smt_engine.h from theory.h.

10 years agoFixing a soundness bug due to the default implmentation of Theory::ppAssert() not...
Tim King [Mon, 26 May 2014 14:12:19 +0000 (10:12 -0400)]
Fixing a soundness bug due to the default implmentation of Theory::ppAssert() not respecting subtyping.

10 years agoImprove quantifier instantiation: always use original terms when matching (was missin...
Andrew Reynolds [Sun, 25 May 2014 14:18:42 +0000 (09:18 -0500)]
Improve quantifier instantiation: always use original terms when matching (was missing for simple triggers).   Minor updates to scripts.

10 years agoSome cleanup, fix warnings raised by Debian packager.
Morgan Deters [Sun, 25 May 2014 00:16:46 +0000 (20:16 -0400)]
Some cleanup, fix warnings raised by Debian packager.

10 years agoFix bug in E-matching Real/Int terms.
Andrew Reynolds [Fri, 23 May 2014 21:59:48 +0000 (16:59 -0500)]
Fix bug in E-matching Real/Int terms.

10 years agoSafer swig-wrapping for unsigned long long in Java, which will throw an exception...
Morgan Deters [Wed, 21 May 2014 17:55:13 +0000 (13:55 -0400)]
Safer swig-wrapping for unsigned long long in Java, which will throw an exception if the argument is out of bounds for unsigned long long.  Thanks to Steve Siegel for the report.

10 years agoFix compiler warning (missing virtual dtor)
Morgan Deters [Fri, 16 May 2014 03:33:55 +0000 (23:33 -0400)]
Fix compiler warning (missing virtual dtor)

10 years agoMore documentation fixes. Apologies for multiple commits.
Tim King [Mon, 19 May 2014 19:14:54 +0000 (15:14 -0400)]
More documentation fixes. Apologies for multiple commits.

10 years agoFixing documentation for glpk configuration.
Tim King [Mon, 19 May 2014 19:12:54 +0000 (15:12 -0400)]
Fixing documentation for glpk configuration.

10 years agominor fix for string equality engine assertion.
Tianyi Liang [Mon, 19 May 2014 02:06:29 +0000 (21:06 -0500)]
minor fix for string equality engine assertion.

10 years agoMerge pull request #26 from kbansal/sets
Kshitij Bansal [Sat, 17 May 2014 06:43:55 +0000 (02:43 -0400)]
Merge pull request #26 from kbansal/sets

Sets

10 years agolfsc_checker: fix some warnings reported by _both_ gcc and clang
Kshitij Bansal [Fri, 16 May 2014 22:38:22 +0000 (18:38 -0400)]
lfsc_checker: fix some warnings reported by _both_ gcc and clang

10 years agosets: fix a bug in model building, another in handling set of sets
Kshitij Bansal [Fri, 16 May 2014 22:18:35 +0000 (18:18 -0400)]
sets: fix a bug in model building, another in handling set of sets

10 years agominor improvements (fixes) to did-you-mean suggestions
Kshitij Bansal [Fri, 16 May 2014 17:41:31 +0000 (13:41 -0400)]
minor improvements (fixes) to did-you-mean suggestions

10 years agoMinor fixes. Add SMTCOMP 2014 script.
Andrew Reynolds [Thu, 15 May 2014 17:51:35 +0000 (12:51 -0500)]
Minor fixes.  Add SMTCOMP 2014 script.

10 years agoFinish --dump-instantiations option. Update scripts.
Andrew Reynolds [Wed, 14 May 2014 19:46:53 +0000 (14:46 -0500)]
Finish --dump-instantiations option.  Update scripts.

10 years agoReject native extended ASCII characters. It requires user to use escaped sequence...
Tianyi Liang [Tue, 13 May 2014 20:22:38 +0000 (15:22 -0500)]
Reject native extended ASCII characters. It requires user to use escaped sequence for an extended ASCII character.

10 years agoReject un-escaped extended ASCII characters
Tianyi Liang [Tue, 13 May 2014 16:16:06 +0000 (11:16 -0500)]
Reject un-escaped extended ASCII characters

10 years agoAdd lazy strategy for bounded integers to avoid non-terminating unsat cases. Add...
ajreynol [Tue, 13 May 2014 15:18:18 +0000 (17:18 +0200)]
Add lazy strategy for bounded integers to avoid non-terminating unsat cases.  Add regressions.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 13 May 2014 02:03:25 +0000 (21:03 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoFix a bug in the IndexOf function.
Tianyi Liang [Tue, 13 May 2014 02:02:24 +0000 (21:02 -0500)]
Fix a bug in the IndexOf function.

10 years agoFix a bug in the IndexOf function.
Tianyi Liang [Tue, 13 May 2014 02:02:24 +0000 (21:02 -0500)]
Fix a bug in the IndexOf function.

10 years agoMinor updates/fix to --cbqi-recurse
Andrew Reynolds [Mon, 12 May 2014 19:15:40 +0000 (14:15 -0500)]
Minor updates/fix to --cbqi-recurse

10 years agoMerge remote-tracking branch 'timothy-king/master'
Tim King [Mon, 12 May 2014 17:10:16 +0000 (13:10 -0400)]
Merge remote-tracking branch 'timothy-king/master'

10 years agoMerging in additional glpk options and statistics from CAV submission.
Tim King [Mon, 12 May 2014 17:08:53 +0000 (13:08 -0400)]
Merging in additional glpk options and statistics from CAV submission.

10 years agoAdd a benchmark that detects a bug in parsing. Thank Vijay for his bug report.
Tianyi Liang [Mon, 12 May 2014 16:10:06 +0000 (11:10 -0500)]
Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 12 May 2014 03:14:46 +0000 (22:14 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoReplace lemma sending with EQ assertions. Fix a typo in hex_to_int function.
Tianyi Liang [Mon, 12 May 2014 03:13:17 +0000 (22:13 -0500)]
Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.

10 years agoReplace lemma sending with EQ assertions. Fix a typo in hex_to_int function.
Tianyi Liang [Mon, 12 May 2014 03:13:17 +0000 (22:13 -0500)]
Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.

10 years agoMore preparation for CASC proofs. Minor fix for sort inference (rewrite new assertio...
Andrew Reynolds [Sun, 11 May 2014 19:36:50 +0000 (14:36 -0500)]
More preparation for CASC proofs.  Minor fix for sort inference (rewrite new assertions).  Bug fix for ambqi : simplify correctly for multi-sorted case.  Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

10 years agoBug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, minor...
Andrew Reynolds [Sat, 10 May 2014 20:14:34 +0000 (15:14 -0500)]
Bug fixes to CBQI.  Add first draft of CASC j7 TFF script.  Add regression, minor changes.

10 years agoFix for example installation.
Morgan Deters [Fri, 9 May 2014 15:11:31 +0000 (11:11 -0400)]
Fix for example installation.

10 years agoInitial draft of run scripts for CASC j7
Andrew Reynolds [Fri, 9 May 2014 21:53:57 +0000 (16:53 -0500)]
Initial draft of run scripts for CASC j7

10 years agoAdd variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Andrew Reynolds [Fri, 9 May 2014 11:51:43 +0000 (06:51 -0500)]
Add variable ordering to ambqi.  Bug fix to macros. More preparation for CASC proofs.

10 years agoMajor simplifications to macros module.
ajreynol [Thu, 8 May 2014 16:18:53 +0000 (18:18 +0200)]
Major simplifications to macros module.

10 years agoFixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes...
Andrew Reynolds [Thu, 8 May 2014 13:13:05 +0000 (08:13 -0500)]
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers.  Minor fixes to ambqi.  Preparation for CASC proof output.  Add NNF option.

10 years agoBasic optimizations for ambqi : only normalize UF applied to variables, direct handli...
Andrew Reynolds [Thu, 8 May 2014 07:18:54 +0000 (02:18 -0500)]
Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT

10 years agoAdding encoding of sha1 collision for the hashing example
Dejan Jovanovic [Thu, 8 May 2014 06:26:42 +0000 (23:26 -0700)]
Adding encoding of sha1 collision for the hashing example

10 years agopatch to the last commit: add a single character case
Tianyi Liang [Thu, 8 May 2014 00:32:03 +0000 (19:32 -0500)]
patch to the last commit: add a single character case

10 years agofix a bug in contain
Tianyi Liang [Wed, 7 May 2014 20:49:09 +0000 (15:49 -0500)]
fix a bug in contain

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 7 May 2014 19:45:57 +0000 (14:45 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd splits
Tianyi Liang [Wed, 7 May 2014 19:43:42 +0000 (14:43 -0500)]
add splits

10 years agoadd splits
Tianyi Liang [Wed, 7 May 2014 19:43:42 +0000 (14:43 -0500)]
add splits

10 years agoFixes to ambqi, now solution-sound.
Andrew Reynolds [Wed, 7 May 2014 18:36:58 +0000 (13:36 -0500)]
Fixes to ambqi, now solution-sound.

10 years agoFirst draft of ambqi_builder (new implementation of MBQI based on disjoint sets).
Andrew Reynolds [Tue, 6 May 2014 13:19:04 +0000 (08:19 -0500)]
First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).

10 years agofix a bug in replace and contains
Tianyi Liang [Tue, 6 May 2014 01:17:31 +0000 (20:17 -0500)]
fix a bug in replace and contains

10 years agoadd constant regular expression check for intersection.
Tianyi Liang [Mon, 5 May 2014 23:01:14 +0000 (18:01 -0500)]
add constant regular expression check for intersection.

10 years agoImproving documentation for glpk-cut-log switch.
Tim King [Mon, 5 May 2014 21:20:38 +0000 (17:20 -0400)]
Improving documentation for glpk-cut-log switch.

10 years agoValuation::entailmentCheck() proxy for TheoryEngine version. Signature and contract...
Morgan Deters [Mon, 5 May 2014 18:10:10 +0000 (14:10 -0400)]
Valuation::entailmentCheck() proxy for TheoryEngine version.  Signature and contract is the same as for TheoryEngine version.

10 years agoFix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.
Morgan Deters [Fri, 2 May 2014 23:22:26 +0000 (19:22 -0400)]
Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.

10 years agoSimplification of EqualityEngine::areDisequal. Comparison for production : http...
Andrew Reynolds [Fri, 2 May 2014 21:25:56 +0000 (16:25 -0500)]
Simplification of EqualityEngine::areDisequal.  Comparison for production : 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.

10 years agoFix assertion from previous commit.
ajreynol [Fri, 2 May 2014 12:45:09 +0000 (14:45 +0200)]
Fix assertion from previous commit.

10 years agoAdd option --dt-stc-ind for strengthening skolemization. Refactor skolemization.
Andrew Reynolds [Fri, 2 May 2014 12:11:08 +0000 (07:11 -0500)]
Add option --dt-stc-ind for strengthening skolemization.  Refactor skolemization.

10 years agoMore minor optimizations for datatypes.
ajreynol [Fri, 2 May 2014 08:57:51 +0000 (10:57 +0200)]
More minor optimizations for datatypes.

10 years agoMinor optimizations to datatypes, revert to checkClash not mod eq. Minor clean up.
ajreynol [Thu, 1 May 2014 11:28:56 +0000 (13:28 +0200)]
Minor optimizations to datatypes, revert to checkClash not mod eq.  Minor clean up.

10 years agoMerge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Thu, 1 May 2014 04:04:21 +0000 (00:04 -0400)]
Merge remote-tracking branch 'upstream/master' into sets

10 years agodecision engine: cache start index for and/or nodes
Kshitij Bansal [Wed, 30 Apr 2014 20:09:32 +0000 (16:09 -0400)]
decision engine: cache start index for and/or nodes

This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.

This was triggerred by a benchmark sent by andy/viktor.

performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex

10 years agoT-entailment work, and QCF (quant conflict find) work that uses it.
Tim King [Wed, 30 Apr 2014 21:28:00 +0000 (17:28 -0400)]
T-entailment work, and QCF (quant conflict find) work that uses it.

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>
10 years agoFix warnings, cleanup in strings typechecker.
Morgan Deters [Wed, 30 Apr 2014 01:57:16 +0000 (21:57 -0400)]
Fix warnings, cleanup in strings typechecker.

10 years agoFix compiler warning re: TheoryUF destructor.
Morgan Deters [Wed, 30 Apr 2014 01:48:49 +0000 (21:48 -0400)]
Fix compiler warning re: TheoryUF destructor.

10 years agoFix simplify output for SMT2 printer.
Morgan Deters [Wed, 30 Apr 2014 01:28:25 +0000 (21:28 -0400)]
Fix simplify output for SMT2 printer.

10 years agoFix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.
Morgan Deters [Tue, 29 Apr 2014 22:04:38 +0000 (18:04 -0400)]
Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.

10 years agoMostly resolves bug #561 memory leaks, and more.
Morgan Deters [Tue, 29 Apr 2014 23:51:29 +0000 (19:51 -0400)]
Mostly resolves bug #561 memory leaks, and more.

10 years agoFix for --force-logic to extend its reach to the parser.
Morgan Deters [Tue, 29 Apr 2014 21:57:17 +0000 (17:57 -0400)]
Fix for --force-logic to extend its reach to the parser.

10 years agofixed couple of more warnings
Kshitij Bansal [Tue, 29 Apr 2014 23:38:29 +0000 (19:38 -0400)]
fixed couple of more warnings

10 years agofix was compiler warning in antlr_input, crashing test case with the old fix
Kshitij Bansal [Tue, 29 Apr 2014 23:07:20 +0000 (19:07 -0400)]
fix was compiler warning in antlr_input, crashing test case with the old fix

10 years agoRevert a compiler warning fix from ea6a5a6.
Morgan Deters [Tue, 29 Apr 2014 22:14:34 +0000 (18:14 -0400)]
Revert a compiler warning fix from ea6a5a6.

10 years agofix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr
Tianyi Liang [Tue, 29 Apr 2014 21:54:26 +0000 (16:54 -0500)]
fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr

10 years agoadd leading zeros support for str.to.int
Tianyi Liang [Tue, 29 Apr 2014 20:32:38 +0000 (15:32 -0500)]
add leading zeros support for str.to.int

10 years agoSignificantly improve performance for producing datatypes models.
ajreynol [Tue, 29 Apr 2014 13:39:11 +0000 (15:39 +0200)]
Significantly improve performance for producing datatypes models.

10 years agoMerge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Mon, 28 Apr 2014 23:11:59 +0000 (19:11 -0400)]
Merge remote-tracking branch 'upstream/master' into sets

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 28 Apr 2014 22:38:56 +0000 (17:38 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd strings-opt2 for regular splitting
Tianyi Liang [Mon, 28 Apr 2014 21:29:27 +0000 (16:29 -0500)]
add strings-opt2 for regular splitting

10 years agocleanup
Kshitij Bansal [Mon, 28 Apr 2014 22:18:24 +0000 (18:18 -0400)]
cleanup