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
Tianyi Liang [Thu, 20 Feb 2014 22:07:23 +0000 (16:07 -0600)]
hot fix for str2int/int2str
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser
Kshitij Bansal [Thu, 20 Feb 2014 13:57:39 +0000 (08:57 -0500)]
portfolio: add stat to track time spent waiting for interrupted threads to stop
Tim King [Wed, 19 Feb 2014 21:57:51 +0000 (16:57 -0500)]
Merge branch 'master' of github.com:CVC4/CVC4
Tianyi Liang [Wed, 19 Feb 2014 21:23:46 +0000 (15:23 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tim King [Wed, 19 Feb 2014 20:50:34 +0000 (15:50 -0500)]
Merge branch '1.3.x'
Tim King [Wed, 19 Feb 2014 20:50:07 +0000 (15:50 -0500)]
Stopping non-linear terms from entering the dio solver. Fixes bug 547.
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser
Tianyi Liang [Tue, 18 Feb 2014 17:22:46 +0000 (11:22 -0600)]
missed files for the latter commit
Tianyi Liang [Tue, 18 Feb 2014 17:08:20 +0000 (11:08 -0600)]
str.to.int(INVALID) = -1
Tianyi Liang [Tue, 18 Feb 2014 16:48:04 +0000 (10:48 -0600)]
switch to total function str.to.int: maps invalid and non-digit strings to 0
Tianyi Liang [Tue, 18 Feb 2014 03:09:33 +0000 (21:09 -0600)]
bring back the commits which is lost accidentally.
Tianyi Liang [Tue, 18 Feb 2014 01:59:03 +0000 (19:59 -0600)]
add str2int
Morgan Deters [Mon, 17 Feb 2014 21:19:32 +0000 (16:19 -0500)]
Fix for strings-exp: enable quantifiers
Morgan Deters [Mon, 17 Feb 2014 21:03:23 +0000 (16:03 -0500)]
Fix strings preprocessing for justification heuristic
Tianyi Liang [Mon, 17 Feb 2014 20:23:30 +0000 (14:23 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 17 Feb 2014 20:22:26 +0000 (14:22 -0600)]
type conversion
Tianyi Liang [Mon, 17 Feb 2014 20:22:26 +0000 (14:22 -0600)]
type conversion
Andrew Reynolds [Fri, 14 Feb 2014 21:44:21 +0000 (15:44 -0600)]
Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
Tianyi Liang [Fri, 14 Feb 2014 17:53:12 +0000 (11:53 -0600)]
partial function charat
Tianyi Liang [Fri, 14 Feb 2014 00:08:49 +0000 (18:08 -0600)]
fix expanding def
Tianyi Liang [Wed, 12 Feb 2014 22:10:07 +0000 (16:10 -0600)]
bug fix for reverse check
Tianyi Liang [Wed, 12 Feb 2014 04:50:08 +0000 (22:50 -0600)]
lexer fix: disable smt-lib conversion for string literals
Tianyi Liang [Wed, 12 Feb 2014 00:08:53 +0000 (18:08 -0600)]
minor fix for recognizing the tail backslash, still have smt-lib compliance issue.
Tianyi Liang [Tue, 11 Feb 2014 23:10:06 +0000 (17:10 -0600)]
resolve merge conflicts
Tianyi Liang [Tue, 11 Feb 2014 22:44:23 +0000 (16:44 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/theory/strings/theory_strings.cpp
Tianyi Liang [Tue, 11 Feb 2014 22:35:17 +0000 (16:35 -0600)]
escaped characters, having an issue with smt-lib defintion, further repair is needed.
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge
Tianyi Liang [Thu, 6 Feb 2014 17:22:43 +0000 (11:22 -0600)]
minor cleanup for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge
Tianyi Liang [Tue, 11 Feb 2014 22:35:17 +0000 (16:35 -0600)]
escaped characters, having an issue with smt-lib defintion, further repair is needed.
Morgan Deters [Tue, 11 Feb 2014 02:05:09 +0000 (21:05 -0500)]
Fix build (some nonexistent files listed in Makefile)
Andrew Reynolds [Sun, 9 Feb 2014 22:14:31 +0000 (16:14 -0600)]
More complete guess instantiation strategy, cvc4 now typically times out 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
Tianyi Liang [Thu, 6 Feb 2014 17:26:24 +0000 (11:26 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 6 Feb 2014 17:22:43 +0000 (11:22 -0600)]
minor cleanup for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge
Tianyi Liang [Thu, 6 Feb 2014 17:22:43 +0000 (11:22 -0600)]
minor cleanup for merge
Morgan Deters [Thu, 6 Feb 2014 16:13:24 +0000 (11:13 -0500)]
Minor fix for previous commit
Morgan Deters [Thu, 6 Feb 2014 16:07:34 +0000 (11:07 -0500)]
Oops.. premature push on lexer fix (remove debugging output)
Morgan Deters [Thu, 6 Feb 2014 16:05:07 +0000 (11:05 -0500)]
Fixes for escape-handling for string literals in SMT-LIBv2 lexer
Tianyi Liang [Wed, 5 Feb 2014 15:20:37 +0000 (09:20 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge
Andrew Reynolds [Wed, 5 Feb 2014 10:23:47 +0000 (04:23 -0600)]
Bug fix for theory strings related to old cycle detection code (was leading to bogus model). Minor cleanup of QCF.
Andrew Reynolds [Tue, 4 Feb 2014 16:03:25 +0000 (10:03 -0600)]
Do not use transitive closure module for cycle detection in datatypes (was bottleneck).
Andrew Reynolds [Tue, 4 Feb 2014 15:00:28 +0000 (09:00 -0600)]
Add variable ordering for QCF to accelerate matching procedure. Preparing for QCF_MC mode.
Andrew Reynolds [Mon, 3 Feb 2014 16:23:28 +0000 (10:23 -0600)]
Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain instantiation breadth-first.
Tianyi Liang [Fri, 31 Jan 2014 18:22:07 +0000 (12:22 -0600)]
Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib
Andrew Reynolds [Thu, 30 Jan 2014 22:13:17 +0000 (16:13 -0600)]
Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were added). Bug fix for QCF (was missing instantiations due to not using getRepresentative).
Tianyi Liang [Thu, 30 Jan 2014 22:30:21 +0000 (16:30 -0600)]
stats for eq/diseq splits
Tianyi Liang [Thu, 30 Jan 2014 21:26:50 +0000 (15:26 -0600)]
another name change
Tianyi Liang [Thu, 30 Jan 2014 21:18:09 +0000 (15:18 -0600)]
change string stats text names
Tianyi Liang [Thu, 30 Jan 2014 21:10:58 +0000 (15:10 -0600)]
adds stats
Tianyi Liang [Wed, 29 Jan 2014 18:05:02 +0000 (12:05 -0600)]
roll back to uf implementation for substr and charat
Tianyi Liang [Wed, 29 Jan 2014 16:32:17 +0000 (10:32 -0600)]
add prefixof, suffixof
Tianyi Liang [Tue, 28 Jan 2014 23:17:51 +0000 (17:17 -0600)]
merge internal and user of charat & substr into one
Andrew Reynolds [Tue, 28 Jan 2014 15:51:33 +0000 (09:51 -0600)]
More optimizations of quantifier instantiation data structures.
Morgan Deters [Mon, 27 Jan 2014 23:04:10 +0000 (18:04 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 27 Jan 2014 23:04:04 +0000 (18:04 -0500)]
URL update
Andrew Reynolds [Mon, 27 Jan 2014 14:34:52 +0000 (08:34 -0600)]
More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.
Andrew Reynolds [Sun, 26 Jan 2014 20:23:51 +0000 (14:23 -0600)]
More optimization of QCF. Fixed InstMatchTrie for caching instantiations. 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.
Tianyi Liang [Sat, 25 Jan 2014 18:49:19 +0000 (12:49 -0600)]
replace charat uf with internal one
Tianyi Liang [Sat, 25 Jan 2014 04:32:45 +0000 (22:32 -0600)]
minor fix, indexof rewriter opt
Tianyi Liang [Fri, 24 Jan 2014 23:50:47 +0000 (17:50 -0600)]
fix: indexof, replace rewriting
Tianyi Liang [Fri, 24 Jan 2014 21:40:34 +0000 (15:40 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 24 Jan 2014 21:39:13 +0000 (15:39 -0600)]
rev diseq
Tianyi Liang [Fri, 24 Jan 2014 20:22:37 +0000 (14:22 -0600)]
rev const split
Tianyi Liang [Fri, 24 Jan 2014 17:58:07 +0000 (11:58 -0600)]
optimize for the reverse direction
Tianyi Liang [Fri, 24 Jan 2014 21:39:13 +0000 (15:39 -0600)]
rev diseq
Tianyi Liang [Fri, 24 Jan 2014 20:22:37 +0000 (14:22 -0600)]
rev const split
Andrew Reynolds [Fri, 24 Jan 2014 19:58:52 +0000 (13:58 -0600)]
Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry approach. Minor change to quantifier macros. Add option --quant-cf-mode.
Tianyi Liang [Fri, 24 Jan 2014 17:58:07 +0000 (11:58 -0600)]
optimize for the reverse direction
Tianyi Liang [Thu, 23 Jan 2014 22:59:58 +0000 (16:59 -0600)]
fix: constants are inferred to be the same
Tianyi Liang [Thu, 23 Jan 2014 08:48:41 +0000 (02:48 -0600)]
minor fix
Tianyi Liang [Wed, 22 Jan 2014 20:08:47 +0000 (14:08 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Wed, 22 Jan 2014 20:08:04 +0000 (15:08 -0500)]
Some minor fixes to SmtEngine strings settings.
Tianyi Liang [Wed, 22 Jan 2014 20:07:10 +0000 (14:07 -0600)]
commented out all_supported in strings for now, it has a bug here.
Tianyi Liang [Wed, 22 Jan 2014 19:50:39 +0000 (13:50 -0600)]
solve string exp issue for regexp
Tianyi Liang [Wed, 22 Jan 2014 19:42:54 +0000 (13:42 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/smt/smt_engine.cpp
Tianyi Liang [Wed, 22 Jan 2014 19:40:54 +0000 (13:40 -0600)]
add warning for using strings in ALL_SUPPORTED
Tianyi Liang [Tue, 21 Jan 2014 19:40:00 +0000 (13:40 -0600)]
Smarter options, but still have a bug
Morgan Deters [Wed, 22 Jan 2014 15:06:04 +0000 (10:06 -0500)]
Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.
Tianyi Liang [Tue, 21 Jan 2014 19:40:00 +0000 (13:40 -0600)]
Smarter options, but still have a bug
Tianyi Liang [Tue, 21 Jan 2014 00:09:11 +0000 (18:09 -0600)]
improve string contains
Tianyi Liang [Mon, 20 Jan 2014 22:45:11 +0000 (16:45 -0600)]
improve string contains
Andrew Reynolds [Sat, 18 Jan 2014 18:13:47 +0000 (12:13 -0600)]
Fixed non-termination issue in bounded integers.
Andrew Reynolds [Sat, 18 Jan 2014 17:27:45 +0000 (11:27 -0600)]
Performance optimization for E-matching, working on using QCF module for propagations.
Tianyi Liang [Sat, 18 Jan 2014 17:11:03 +0000 (11:11 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 17 Jan 2014 23:56:08 +0000 (17:56 -0600)]
strings with new ideas
Morgan Deters [Sat, 18 Jan 2014 04:00:32 +0000 (23:00 -0500)]
Merge branch '1.3.x'
Morgan Deters [Sat, 18 Jan 2014 03:59:39 +0000 (22:59 -0500)]
Fix for quote-escaping in smt2 printer
Tianyi Liang [Fri, 17 Jan 2014 23:56:08 +0000 (17:56 -0600)]
strings with new ideas
Andrew Reynolds [Fri, 17 Jan 2014 15:57:12 +0000 (09:57 -0600)]
More optimizations for quantifiers conflict find. Add trust user patterns mode.
Kshitij Bansal [Fri, 17 Jan 2014 14:12:25 +0000 (09:12 -0500)]
Merge branch '1.3.x'
Kshitij Bansal [Fri, 17 Jan 2014 14:11:58 +0000 (09:11 -0500)]
enable search for html doc
Tianyi Liang [Thu, 16 Jan 2014 21:40:01 +0000 (15:40 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/printer/smt2/smt2_printer.cpp
Tianyi Liang [Thu, 16 Jan 2014 21:37:58 +0000 (15:37 -0600)]
adds partial functions
projects / cvc5.git / log