Kshitij Bansal [Thu, 17 Oct 2013 18:03:25 +0000 (14:03 -0400)]
minor fix to last commit (gitignore)
Kshitij Bansal [Thu, 17 Oct 2013 18:02:27 +0000 (14:02 -0400)]
.gitignore personal configuration files
Tianyi Liang [Wed, 16 Oct 2013 18:24:56 +0000 (13:24 -0500)]
adds fmf for strings
Tianyi Liang [Wed, 16 Oct 2013 15:16:59 +0000 (10:16 -0500)]
renames for strings fmf
Tianyi Liang [Wed, 16 Oct 2013 14:37:17 +0000 (09:37 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 15 Oct 2013 22:23:51 +0000 (17:23 -0500)]
bug fix in strings : change from assert to alwaysassert
Tianyi Liang [Tue, 15 Oct 2013 19:23:08 +0000 (14:23 -0500)]
removes some junks
Andrew Reynolds [Tue, 15 Oct 2013 19:23:20 +0000 (14:23 -0500)]
performance optimizations for quantifier instantiation
Tianyi Liang [Tue, 15 Oct 2013 22:23:51 +0000 (17:23 -0500)]
bug fix in strings : change from assert to alwaysassert
Andrew Reynolds [Tue, 15 Oct 2013 19:23:20 +0000 (14:23 -0500)]
performance optimizations for quantifier instantiation
Tianyi Liang [Tue, 15 Oct 2013 19:23:08 +0000 (14:23 -0500)]
removes some junks
Tianyi Liang [Tue, 15 Oct 2013 18:16:03 +0000 (13:16 -0500)]
bug fix: string cache cleaning
Tianyi Liang [Mon, 14 Oct 2013 21:39:13 +0000 (16:39 -0500)]
add another regexp test
Tianyi Liang [Mon, 14 Oct 2013 21:27:33 +0000 (16:27 -0500)]
Adds Regular Expression support.
Tianyi Liang [Fri, 11 Oct 2013 21:54:22 +0000 (16:54 -0500)]
Adds regular expression support, it is actually CFL because of variables.
Tianyi Liang [Fri, 11 Oct 2013 08:34:04 +0000 (03:34 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 11 Oct 2013 08:32:33 +0000 (03:32 -0500)]
add constant membership
Tianyi Liang [Thu, 10 Oct 2013 17:06:25 +0000 (12:06 -0500)]
adds native regexp.
Tianyi Liang [Fri, 11 Oct 2013 08:32:33 +0000 (03:32 -0500)]
add constant membership
Andrew Reynolds [Thu, 10 Oct 2013 17:36:24 +0000 (12:36 -0500)]
Minor bug fix to datatypes.
Tianyi Liang [Thu, 10 Oct 2013 17:07:40 +0000 (12:07 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 10 Oct 2013 17:06:25 +0000 (12:06 -0500)]
adds native regexp.
Tianyi Liang [Thu, 10 Oct 2013 17:06:25 +0000 (12:06 -0500)]
adds native regexp.
Andrew Reynolds [Wed, 9 Oct 2013 17:26:11 +0000 (12:26 -0500)]
More improvements to datatypes, eager selector collapsing, improved collect model info. Also fix bug in model post-processor.
Andrew Reynolds [Tue, 8 Oct 2013 14:01:13 +0000 (09:01 -0500)]
Optimizations for datatypes theory. There seems to be a bug in trans_closure, currently implemented a work around.
Andrew Reynolds [Mon, 7 Oct 2013 15:02:57 +0000 (10:02 -0500)]
Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
Tianyi Liang [Thu, 3 Oct 2013 16:17:12 +0000 (11:17 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Andrew Reynolds [Thu, 3 Oct 2013 14:52:24 +0000 (09:52 -0500)]
Adding example proof signatures for LFSC.
Andrew Reynolds [Wed, 2 Oct 2013 19:22:36 +0000 (14:22 -0500)]
Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity. Minor cleanup.
Tianyi Liang [Thu, 3 Oct 2013 15:53:46 +0000 (10:53 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/theory/strings/theory_strings.cpp
Tianyi Liang [Thu, 3 Oct 2013 15:48:25 +0000 (10:48 -0500)]
adds some fixes. it solves kaluza problems
Andrew Reynolds [Thu, 3 Oct 2013 14:52:24 +0000 (09:52 -0500)]
Adding example proof signatures for LFSC.
Andrew Reynolds [Wed, 2 Oct 2013 19:22:36 +0000 (14:22 -0500)]
Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity. Minor cleanup.
Tianyi Liang [Wed, 2 Oct 2013 01:03:30 +0000 (20:03 -0500)]
adds partial function substr. the use of this function should be guarded, especially for disequalities
Tianyi Liang [Wed, 2 Oct 2013 01:03:30 +0000 (20:03 -0500)]
adds partial function substr. the use of this function should be guarded, especially for disequalities
Andrew Reynolds [Tue, 1 Oct 2013 16:05:23 +0000 (11:05 -0500)]
Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535
Tianyi Liang [Tue, 1 Oct 2013 04:29:57 +0000 (23:29 -0500)]
replace with a new method for disequality, move to QF_S
Tianyi Liang [Mon, 30 Sep 2013 20:51:25 +0000 (15:51 -0500)]
add x=y
Tianyi Liang [Mon, 30 Sep 2013 16:43:20 +0000 (11:43 -0500)]
fixed a loop bug
Andrew Reynolds [Mon, 30 Sep 2013 15:14:32 +0000 (10:14 -0500)]
Bug fixes and improvements for symmetry breaking, it now supports multiple sorts. Working on monotonicity inference.
Morgan Deters [Fri, 27 Sep 2013 22:42:13 +0000 (18:42 -0400)]
Some fixes to recent strings commits.
Morgan Deters [Fri, 27 Sep 2013 21:52:51 +0000 (17:52 -0400)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Sep 2013 21:46:33 +0000 (16:46 -0500)]
adds communication with arith engine
Andrew Reynolds [Fri, 27 Sep 2013 14:27:19 +0000 (09:27 -0500)]
Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.
Tianyi Liang [Fri, 27 Sep 2013 14:26:57 +0000 (09:26 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Sep 2013 14:24:42 +0000 (09:24 -0500)]
removes unsound cases, adds unrolling
Tianyi Liang [Wed, 25 Sep 2013 18:23:23 +0000 (13:23 -0500)]
fix the infinite issue
Tianyi Liang [Wed, 25 Sep 2013 18:00:13 +0000 (13:00 -0500)]
for morgan to see the regression problems
Tianyi Liang [Tue, 24 Sep 2013 19:17:36 +0000 (14:17 -0500)]
fix loop detection for multi-vars
Tianyi Liang [Mon, 23 Sep 2013 23:21:58 +0000 (18:21 -0500)]
optimizing model generation for strings
Tianyi Liang [Mon, 23 Sep 2013 21:54:32 +0000 (16:54 -0500)]
adds model generation for strings, and a hacked way in arith engine for models
Tianyi Liang [Fri, 27 Sep 2013 14:24:42 +0000 (09:24 -0500)]
removes unsound cases, adds unrolling
Tianyi Liang [Wed, 25 Sep 2013 18:23:23 +0000 (13:23 -0500)]
fix the infinite issue
Tianyi Liang [Wed, 25 Sep 2013 18:00:13 +0000 (13:00 -0500)]
for morgan to see the regression problems
Clark Barrett [Tue, 24 Sep 2013 23:56:06 +0000 (16:56 -0700)]
Reduce compiler dependencies on substitutions.h,
Some new functionality in substitutions.h/cpp
Clark Barrett [Tue, 24 Sep 2013 23:25:53 +0000 (16:25 -0700)]
Better fix for bug 528
Tianyi Liang [Tue, 24 Sep 2013 19:17:36 +0000 (14:17 -0500)]
fix loop detection for multi-vars
Tianyi Liang [Mon, 23 Sep 2013 23:21:58 +0000 (18:21 -0500)]
optimizing model generation for strings
Tianyi Liang [Mon, 23 Sep 2013 21:54:32 +0000 (16:54 -0500)]
adds model generation for strings, and a hacked way in arith engine for models
Morgan Deters [Mon, 23 Sep 2013 23:56:01 +0000 (19:56 -0400)]
Revert Clark's last commit, at his request; there are some bugs.
This reverts commit
9775bced75843c6f01e9524c2d0e7021535e3ec0.
Clark Barrett [Mon, 23 Sep 2013 21:33:53 +0000 (14:33 -0700)]
Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h
for faster compilation
Clark Barrett [Thu, 19 Sep 2013 21:29:29 +0000 (14:29 -0700)]
Fix for bug 528
Morgan Deters [Thu, 5 Sep 2013 13:14:39 +0000 (09:14 -0400)]
Support a personal build configuration and make rules.
Morgan Deters [Wed, 18 Sep 2013 20:53:18 +0000 (16:53 -0400)]
Support for bv2nat/int2bv in parser and BV rewriter.
Morgan Deters [Tue, 17 Sep 2013 21:21:26 +0000 (17:21 -0400)]
Fixes to theoryof-mode; no longer static in Theory class.
Morgan Deters [Sat, 14 Sep 2013 23:41:53 +0000 (19:41 -0400)]
Fix (extraneous) command dumping.
Andrew Reynolds [Fri, 13 Sep 2013 16:23:30 +0000 (11:23 -0500)]
Change default option of simple ite lifting within quantifier bodies. add some debug messages.
Morgan Deters [Fri, 16 Aug 2013 21:07:22 +0000 (17:07 -0400)]
Fix sat_proof "parentheses into the void" after conferring with Liana.
Morgan Deters [Fri, 16 Aug 2013 19:04:14 +0000 (15:04 -0400)]
Move some regress benchmarks around that took too long, other test cleanup.
Morgan Deters [Fri, 16 Aug 2013 19:15:03 +0000 (15:15 -0400)]
Documentation fixes, some code typo fixes, file perms, other minor things.
Kshitij Bansal [Fri, 13 Sep 2013 20:08:56 +0000 (16:08 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Thu, 12 Sep 2013 18:44:49 +0000 (14:44 -0400)]
fix bug 534: portfolio define-fun duplicate model
Tianyi Liang [Wed, 11 Sep 2013 15:23:19 +0000 (11:23 -0400)]
Theory of strings.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Andrew Reynolds [Mon, 9 Sep 2013 23:40:45 +0000 (18:40 -0500)]
Another minor fix for datatypes to repair my previous commit.
Morgan Deters [Mon, 19 Aug 2013 22:15:21 +0000 (18:15 -0400)]
Add support for check-sat with argument.
Morgan Deters [Fri, 6 Sep 2013 00:59:18 +0000 (20:59 -0400)]
Fix declare-datatypes dumping bug (bug 385).
Morgan Deters [Thu, 5 Sep 2013 00:29:24 +0000 (20:29 -0400)]
Support per-command verbosity settings.
Morgan Deters [Wed, 4 Sep 2013 23:55:16 +0000 (19:55 -0400)]
Support empty (and 1-ary) tuples and records.
Morgan Deters [Mon, 9 Sep 2013 19:27:22 +0000 (15:27 -0400)]
Fix some line-numbering in auto-generated metakind.h. Thanks to Martin Brain for reporting this.
Morgan Deters [Mon, 9 Sep 2013 19:26:50 +0000 (15:26 -0400)]
Fix portfolio on bug411.smt2. (get-model command should only go to last winner)
Morgan Deters [Mon, 9 Sep 2013 18:41:21 +0000 (14:41 -0400)]
Ensure no cost for datatypes debugging when not tracing it.
Andrew Reynolds [Sat, 7 Sep 2013 02:34:44 +0000 (21:34 -0500)]
Fix datatypes for bug 503
Morgan Deters [Thu, 5 Sep 2013 19:43:47 +0000 (15:43 -0400)]
Fix FLOOR and DISTINCT in CVC language parser.
Morgan Deters [Thu, 5 Sep 2013 14:47:07 +0000 (10:47 -0400)]
Fix lambda handling in CVC parser
Morgan Deters [Fri, 16 Aug 2013 23:41:36 +0000 (19:41 -0400)]
Permit setOption(decision-mode)
Morgan Deters [Thu, 5 Sep 2013 13:37:01 +0000 (09:37 -0400)]
Fix bugs/issues with missed-t-prop dump output
Morgan Deters [Fri, 23 Aug 2013 20:01:13 +0000 (16:01 -0400)]
Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer
Morgan Deters [Sat, 31 Aug 2013 01:00:56 +0000 (21:00 -0400)]
Add ability to mkConst(TupleSelect) and friends in language bindings
Kshitij Bansal [Mon, 26 Aug 2013 23:48:10 +0000 (19:48 -0400)]
Merge branch '1.2.x'
Kshitij Bansal [Mon, 26 Aug 2013 22:56:39 +0000 (18:56 -0400)]
bug 374 fix: assert litVal=desiredVal only for leaf nodes
Kshitij Bansal [Mon, 26 Aug 2013 22:54:42 +0000 (18:54 -0400)]
Bug 374 benchmarks
Morgan Deters [Tue, 20 Aug 2013 20:32:31 +0000 (16:32 -0400)]
Change recursive expandDefinitions() to an interative worklist-based one; we were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
Morgan Deters [Tue, 13 Aug 2013 15:59:26 +0000 (11:59 -0400)]
--segv-nospin is now default.
Morgan Deters [Tue, 13 Aug 2013 21:58:30 +0000 (17:58 -0400)]
Minor cleanup.
Andrew Reynolds [Tue, 13 Aug 2013 21:10:41 +0000 (16:10 -0500)]
Minor fixes for --fmf-fmc for quantifiers containing datatypes
Andrew Reynolds [Mon, 22 Jul 2013 22:59:47 +0000 (17:59 -0500)]
initial modifications for per-ic cbqi
Morgan Deters [Fri, 9 Aug 2013 13:56:50 +0000 (09:56 -0400)]
Clean up "make install"-produced intermediate files (resolves bug 526)
Morgan Deters [Thu, 8 Aug 2013 23:29:50 +0000 (19:29 -0400)]
Fix a serious bug in the preprocessor; problem inputs reported by Pantazis Deligiannis.
Morgan Deters [Thu, 8 Aug 2013 16:23:59 +0000 (12:23 -0400)]
Parameterized, uninterpreted sorts need no Boolean-term conversion
Morgan Deters [Tue, 30 Jul 2013 16:37:04 +0000 (12:37 -0400)]
Minor fixes to build system.