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
Tianyi Liang [Wed, 15 Jan 2014 23:20:27 +0000 (17:20 -0600)]
adds smt2 print for strings
Tianyi Liang [Wed, 15 Jan 2014 23:20:27 +0000 (17:20 -0600)]
adds smt2 print for strings
Andrew Reynolds [Wed, 15 Jan 2014 16:22:10 +0000 (10:22 -0600)]
Optimizations for quantifiers conflict find: better caching, process matching constraints eagerly.
Tianyi Liang [Fri, 10 Jan 2014 23:42:01 +0000 (17:42 -0600)]
normal form breaking
Tianyi Liang [Fri, 10 Jan 2014 19:26:56 +0000 (13:26 -0600)]
add repalce
Andrew Reynolds [Fri, 10 Jan 2014 16:50:56 +0000 (10:50 -0600)]
Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms.
Andrew Reynolds [Fri, 10 Jan 2014 08:04:51 +0000 (02:04 -0600)]
Add new method --quant-cf for finding conflicts eagerly for quantified formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
Tianyi Liang [Fri, 10 Jan 2014 00:23:15 +0000 (18:23 -0600)]
move new functions under exp options
Tianyi Liang [Thu, 9 Jan 2014 22:25:34 +0000 (16:25 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 9 Jan 2014 22:23:59 +0000 (16:23 -0600)]
add constant replace, indexof
Tianyi Liang [Thu, 9 Jan 2014 22:23:59 +0000 (16:23 -0600)]
add constant replace, indexof
Morgan Deters [Thu, 9 Jan 2014 21:48:32 +0000 (16:48 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 9 Jan 2014 21:48:21 +0000 (16:48 -0500)]
gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)
Tianyi Liang [Thu, 9 Jan 2014 19:24:27 +0000 (13:24 -0600)]
Another way to handle negative contain
Morgan Deters [Wed, 8 Jan 2014 20:32:59 +0000 (15:32 -0500)]
Merge branch '1.3.x'
Conflicts:
COPYING
NEWS
config/cvc4.m4
Morgan Deters [Wed, 8 Jan 2014 20:27:26 +0000 (15:27 -0500)]
Switch license default back to BSD, and add --best and --enable-gpl options.
Morgan Deters [Wed, 18 Dec 2013 02:13:12 +0000 (21:13 -0500)]
Cache apt packages on Travis.
Tianyi Liang [Wed, 8 Jan 2014 18:07:56 +0000 (12:07 -0600)]
clean some code
Morgan Deters [Wed, 8 Jan 2014 16:18:02 +0000 (11:18 -0500)]
Fix LogicInfo parsing for string logics
Morgan Deters [Wed, 8 Jan 2014 16:17:32 +0000 (11:17 -0500)]
Fix LogicInfo parsing for string logics
Tianyi Liang [Wed, 8 Jan 2014 02:04:27 +0000 (20:04 -0600)]
remove a warning in strings
Tianyi Liang [Wed, 8 Jan 2014 01:18:55 +0000 (19:18 -0600)]
minor fix, bring back the assertion.
Tianyi Liang [Wed, 8 Jan 2014 00:12:08 +0000 (18:12 -0600)]
string contain changes
Andrew Reynolds [Sat, 4 Jan 2014 04:36:55 +0000 (22:36 -0600)]
Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.
Andrew Reynolds [Fri, 3 Jan 2014 18:13:13 +0000 (12:13 -0600)]
Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
Morgan Deters [Thu, 2 Jan 2014 19:13:17 +0000 (14:13 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 2 Jan 2014 19:13:08 +0000 (14:13 -0500)]
Update copyright year.
Tianyi Liang [Fri, 27 Dec 2013 17:27:16 +0000 (11:27 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix
Morgan Deters [Fri, 27 Dec 2013 17:21:25 +0000 (12:21 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 27 Dec 2013 17:21:20 +0000 (12:21 -0500)]
Fix for ANTLR warning.
Tianyi Liang [Thu, 26 Dec 2013 23:18:26 +0000 (17:18 -0600)]
new functions in strings
Tianyi Liang [Thu, 26 Dec 2013 00:44:59 +0000 (18:44 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Wed, 25 Dec 2013 22:18:40 +0000 (17:18 -0500)]
fix for some nightly build failures
Morgan Deters [Tue, 24 Dec 2013 18:26:31 +0000 (13:26 -0500)]
Cleanup related to output language fix.
Morgan Deters [Tue, 24 Dec 2013 18:25:30 +0000 (13:25 -0500)]
Merge branch '1.3.x'
Conflicts:
NEWS
Morgan Deters [Tue, 24 Dec 2013 18:24:56 +0000 (13:24 -0500)]
Better automatic handling of output language setting.
Morgan Deters [Mon, 16 Dec 2013 14:49:05 +0000 (09:49 -0500)]
Better get-value parse error message for common user error.
Morgan Deters [Tue, 24 Dec 2013 17:45:13 +0000 (12:45 -0500)]
Minor code cleanup.
Morgan Deters [Tue, 24 Dec 2013 15:57:28 +0000 (10:57 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 3 Jun 2013 22:18:24 +0000 (18:18 -0400)]
Java datatype API fixups, datatype API examples
Morgan Deters [Mon, 23 Dec 2013 18:45:33 +0000 (13:45 -0500)]
cln now default w.r.t. build ID string
Morgan Deters [Mon, 5 Aug 2013 22:29:34 +0000 (18:29 -0400)]
Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
Morgan Deters [Sun, 22 Dec 2013 17:06:34 +0000 (12:06 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 19 Dec 2013 16:52:00 +0000 (11:52 -0500)]
Fix to interactive mode determination.