Tianyi Liang [Wed, 7 Jan 2015 16:02:01 +0000 (10:02 -0600)]
added initial AX rules;
fixed a bug for empty string in regex
ajreynol [Sun, 28 Dec 2014 04:42:28 +0000 (05:42 +0100)]
Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter
Dejan Jovanovic [Sat, 27 Dec 2014 03:15:13 +0000 (19:15 -0800)]
Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.
Tianyi Liang [Mon, 22 Dec 2014 22:24:08 +0000 (16:24 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 22 Dec 2014 22:22:42 +0000 (16:22 -0600)]
bug fix for constant regular expression model building
Tianyi Liang [Mon, 22 Dec 2014 22:22:42 +0000 (16:22 -0600)]
bug fix for constant regular expression model building
ajreynol [Mon, 22 Dec 2014 22:21:40 +0000 (23:21 +0100)]
Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.
ajreynol [Sun, 21 Dec 2014 23:49:27 +0000 (00:49 +0100)]
Add misc trigger options.
Morgan Deters [Tue, 16 Dec 2014 23:04:47 +0000 (18:04 -0500)]
Fix oversight in dumping assertions in preprocessing.
ajreynol [Fri, 12 Dec 2014 11:03:26 +0000 (12:03 +0100)]
Add cvc parsing support for cardinality constraints. Bug fix for enumerating elements to meet cardinality lower bounds.
Morgan Deters [Thu, 11 Dec 2014 22:04:29 +0000 (17:04 -0500)]
Minor fixes to language bindings. (Resolves #607.)
ajreynol [Thu, 11 Dec 2014 13:09:54 +0000 (14:09 +0100)]
Option to enable/disable cyclicity check in datatypes.
Tianyi Liang [Thu, 11 Dec 2014 02:59:32 +0000 (20:59 -0600)]
bug fix, thanks to Guy's example.
Morgan Deters [Tue, 9 Dec 2014 23:48:55 +0000 (18:48 -0500)]
Better error description (related to bug 605).
Morgan Deters [Tue, 9 Dec 2014 23:48:43 +0000 (18:48 -0500)]
Cleanup.
Tianyi Liang [Sat, 6 Dec 2014 21:28:52 +0000 (15:28 -0600)]
Added string constant in java api example.
Tianyi Liang [Sat, 6 Dec 2014 19:26:39 +0000 (13:26 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sat, 6 Dec 2014 19:24:01 +0000 (13:24 -0600)]
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
Tianyi Liang [Sat, 6 Dec 2014 19:24:01 +0000 (13:24 -0600)]
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
ajreynol [Sat, 6 Dec 2014 00:26:44 +0000 (01:26 +0100)]
Fix dt.size care graph.
Tianyi Liang [Fri, 5 Dec 2014 00:17:55 +0000 (18:17 -0600)]
Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).
Tianyi Liang [Thu, 4 Dec 2014 22:13:41 +0000 (16:13 -0600)]
clean up and improve intersection
Morgan Deters [Thu, 4 Dec 2014 06:40:21 +0000 (01:40 -0500)]
Fix valgrind-flagged error about uninitialized value.
Morgan Deters [Thu, 4 Dec 2014 06:39:53 +0000 (01:39 -0500)]
Fix segfault in lambdas when constructed via API.
Morgan Deters [Thu, 4 Dec 2014 02:58:50 +0000 (21:58 -0500)]
Fix UnsatCore in language bindings.
Martin Brain [Thu, 4 Dec 2014 02:29:43 +0000 (21:29 -0500)]
Floating point infrastructure.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Kshitij Bansal [Wed, 3 Dec 2014 17:09:14 +0000 (12:09 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Wed, 3 Dec 2014 16:38:36 +0000 (11:38 -0500)]
Revert "Disable constants sharing in eq engine, disable hack in theory engine."
This partially reverts commit
f70804a7159390fcb01d8c1ec208fbfd8e544fba.
In particular, it DOES NOT revert
"Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine."
which is part of the same commit.
Tianyi Liang [Wed, 3 Dec 2014 05:44:26 +0000 (23:44 -0600)]
disable inter cache
ajreynol [Fri, 28 Nov 2014 15:27:19 +0000 (16:27 +0100)]
Synchronize conjecture generation with E-matching. Minor fix to --full-saturate-quant.
Tianyi Liang [Thu, 27 Nov 2014 04:09:38 +0000 (22:09 -0600)]
add intersection rewriting
Tianyi Liang [Thu, 27 Nov 2014 01:34:37 +0000 (19:34 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 27 Nov 2014 01:32:32 +0000 (19:32 -0600)]
add more regexp rewriting
Tianyi Liang [Thu, 27 Nov 2014 00:11:35 +0000 (18:11 -0600)]
add more functions for regular expressions
Tianyi Liang [Thu, 27 Nov 2014 01:32:32 +0000 (19:32 -0600)]
add more regexp rewriting
Tianyi Liang [Thu, 27 Nov 2014 00:11:35 +0000 (18:11 -0600)]
add more functions for regular expressions
ajreynol [Tue, 25 Nov 2014 15:15:10 +0000 (16:15 +0100)]
Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.
lianah [Sat, 22 Nov 2014 18:11:19 +0000 (10:11 -0800)]
added number of resource units used as a stat
ajreynol [Fri, 21 Nov 2014 09:48:17 +0000 (10:48 +0100)]
Throw error when pattern is not list of terms.
ajreynol [Fri, 21 Nov 2014 08:42:07 +0000 (09:42 +0100)]
Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
ajreynol [Thu, 20 Nov 2014 09:56:20 +0000 (10:56 +0100)]
Disable constants sharing in eq engine, disable hack in theory engine. Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
Morgan Deters [Thu, 20 Nov 2014 05:30:33 +0000 (00:30 -0500)]
Fix #lines in template.
Dejan Jovanović [Thu, 20 Nov 2014 03:42:31 +0000 (22:42 -0500)]
Making construction of trigger sets not use the global engine state.
Morgan Deters [Wed, 19 Nov 2014 15:27:59 +0000 (10:27 -0500)]
Distribute UnsafeInterruptException interface file for SWIG.
Kshitij Bansal [Wed, 19 Nov 2014 02:50:33 +0000 (21:50 -0500)]
Merge pull request #70 from kbansal/sets-for-merge-squashed
Set Constant's normal form and other short fixes
Kshitij Bansal [Mon, 10 Nov 2014 18:11:20 +0000 (13:11 -0500)]
Set Constant's normal form and other short fixes
Other short fixes:
* use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT
* theoryof-mode fix in smt_engine.cpp
* hack in TheoryModel::getModelValue [TODO: notify Clark/Andy]
* Lemma generation when it rewrites to true/false fix
* TermInfoManager::addTerm(..) fix
* Move SUBSET rewrite to preRewrite
* On preRegister, queue up propagation to be done upfront
** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code.
* TheorySetsProperties::getCardinality(..) fix
Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!
Liana Hadarean [Tue, 18 Nov 2014 22:58:34 +0000 (14:58 -0800)]
clear model cache in BVQuickCheck clearSolver() (fixes bug 587)
lianah [Tue, 18 Nov 2014 19:35:02 +0000 (14:35 -0500)]
All Minisat solve calls now return lbool (fixes bug 599)
ajreynol [Tue, 18 Nov 2014 17:44:48 +0000 (18:44 +0100)]
Compute model basis only for fmf. Add another co-datatype regression.
ajreynol [Tue, 18 Nov 2014 16:39:05 +0000 (17:39 +0100)]
Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
lianah [Mon, 17 Nov 2014 23:40:26 +0000 (18:40 -0500)]
added command line option for extractArith bv rewrite
Morgan Deters [Mon, 17 Nov 2014 14:33:55 +0000 (09:33 -0500)]
Short-circuit in TheoryArithPrivate::check(), care of Tim.
Morgan Deters [Thu, 13 Nov 2014 00:42:23 +0000 (19:42 -0500)]
New, uniform checkTime statistic for all theories (as discussed in meeting).
Liana Hadarean [Mon, 17 Nov 2014 20:26:42 +0000 (15:26 -0500)]
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
ajreynol [Sun, 16 Nov 2014 15:38:50 +0000 (16:38 +0100)]
Add term db mode. Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup.
ajreynol [Fri, 14 Nov 2014 11:25:07 +0000 (12:25 +0100)]
Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.
Clark Barrett [Thu, 13 Nov 2014 23:13:49 +0000 (15:13 -0800)]
Minor changes to AUTHORS and COPYING
Morgan Deters [Thu, 13 Nov 2014 22:02:24 +0000 (17:02 -0500)]
Minor adjustments to wording.
Morgan Deters [Thu, 13 Nov 2014 21:37:19 +0000 (16:37 -0500)]
Copyright text fixes.
Morgan Deters [Thu, 13 Nov 2014 18:35:46 +0000 (13:35 -0500)]
Merge pull request #69 from mdeters/bug594
Fix memory leak in CDHashMap<> with Node keys (resolves bug 594).
ajreynol [Thu, 13 Nov 2014 11:17:46 +0000 (12:17 +0100)]
Remove two obsolete versions of MBQI.
ajreynol [Thu, 13 Nov 2014 09:43:57 +0000 (10:43 +0100)]
More preparation for filtering relevant terms in TermDb.
Morgan Deters [Tue, 11 Nov 2014 21:21:37 +0000 (16:21 -0500)]
Possible fix for bug594
Morgan Deters [Thu, 13 Nov 2014 04:26:16 +0000 (23:26 -0500)]
Merge pull request #65 from mdeters/bv-ineq-cachefix
Fix BV inequality solver caching, and TNode fix.
Morgan Deters [Wed, 12 Nov 2014 17:31:00 +0000 (12:31 -0500)]
BV inequality graph TNode fix.
Morgan Deters [Wed, 12 Nov 2014 12:46:02 +0000 (07:46 -0500)]
Fix BV inequality solver caching.
Morgan Deters [Wed, 12 Nov 2014 13:29:00 +0000 (08:29 -0500)]
Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.
Morgan Deters [Mon, 10 Nov 2014 14:34:32 +0000 (09:34 -0500)]
Minor cleanup.
Kshitij Bansal [Tue, 11 Nov 2014 19:01:47 +0000 (14:01 -0500)]
Merge pull request #64 from mdeters/theorysets-hashset-iteration
Update TheorySets to use CDHashSet<>::key_begin() / key_end().
ajreynol [Tue, 11 Nov 2014 10:38:35 +0000 (11:38 +0100)]
Work on synchronizing decision=justification and E-matching.
Tianyi Liang [Mon, 10 Nov 2014 19:48:17 +0000 (13:48 -0600)]
Merge pull request #63 from mdeters/theorystrings-hashset-iteration
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().
Dejan Jovanović [Fri, 7 Nov 2014 17:31:26 +0000 (12:31 -0500)]
Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.
ajreynol [Mon, 10 Nov 2014 14:53:51 +0000 (15:53 +0100)]
Do not eliminate variables only occurring in patterns. Minor improvements to sort inference. Remove unused code.
Morgan Deters [Mon, 10 Nov 2014 00:02:42 +0000 (19:02 -0500)]
Merge branch '1.4.x'
Morgan Deters [Sun, 9 Nov 2014 23:20:28 +0000 (18:20 -0500)]
Update TheorySets to use CDHashSet<>::key_begin() / key_end().
Morgan Deters [Sun, 9 Nov 2014 23:20:32 +0000 (18:20 -0500)]
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().
Morgan Deters [Sat, 8 Nov 2014 20:13:24 +0000 (15:13 -0500)]
Work around an apparent bug in libc++ that was causing crashes on Mac..
Morgan Deters [Sun, 9 Nov 2014 23:20:04 +0000 (18:20 -0500)]
Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac).
Morgan Deters [Sun, 9 Nov 2014 23:53:11 +0000 (18:53 -0500)]
Increase stack size when running regressions (fixes some regression crashes on Mac).
ajreynol [Sun, 9 Nov 2014 11:17:55 +0000 (12:17 +0100)]
Fix dt shared terms issue, reenable regression.
ajreynol [Sat, 8 Nov 2014 16:42:50 +0000 (17:42 +0100)]
Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug484, enable parsing_ringer.
Morgan Deters [Sat, 8 Nov 2014 15:52:22 +0000 (10:52 -0500)]
Merge pull request #62 from mdeters/bv-cleanup
Remove some unused variables.
Morgan Deters [Sat, 8 Nov 2014 01:43:53 +0000 (20:43 -0500)]
Remove some unused variables.
Clark Barrett [Sat, 8 Nov 2014 00:40:54 +0000 (16:40 -0800)]
Fixed bug in model builder with subtypes
Morgan Deters [Fri, 7 Nov 2014 23:59:36 +0000 (18:59 -0500)]
Remove some dead code.
Morgan Deters [Fri, 7 Nov 2014 22:55:30 +0000 (17:55 -0500)]
Fix a memory leak in SatSolverRegistry (re: bug #594).
Morgan Deters [Fri, 7 Nov 2014 22:24:35 +0000 (17:24 -0500)]
Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).
Morgan Deters [Fri, 7 Nov 2014 21:59:09 +0000 (16:59 -0500)]
Merge branch '1.4.x'
Conflicts:
src/smt/model_postprocessor.cpp
test/regress/regress0/Makefile.am
Morgan Deters [Fri, 7 Nov 2014 21:57:58 +0000 (16:57 -0500)]
Fix missing case in Boolean terms rewriting. (Resolves bug #596.)
Morgan Deters [Fri, 7 Nov 2014 21:51:26 +0000 (16:51 -0500)]
Merge branch '1.4.x'
Conflicts:
src/smt/model_postprocessor.cpp
Morgan Deters [Fri, 7 Nov 2014 21:16:57 +0000 (16:16 -0500)]
Corrected fix for missing case in model postprocessor (resolves bug #595).
ajreynol [Fri, 7 Nov 2014 16:38:53 +0000 (17:38 +0100)]
Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.
Morgan Deters [Fri, 7 Nov 2014 15:16:00 +0000 (10:16 -0500)]
Revert "Fix missing case in model postprocessor (resolves bug #595)."
This reverts commit
61042cf551b19d06673be2b069bacc7cb1cd775a.
Morgan Deters [Fri, 7 Nov 2014 15:15:41 +0000 (10:15 -0500)]
Revert "Fix missing case in model postprocessor (resolves bug #595)."
This reverts commit
61042cf551b19d06673be2b069bacc7cb1cd775a.
Conflicts:
test/regress/regress0/Makefile.am
Morgan Deters [Mon, 27 Oct 2014 23:29:22 +0000 (19:29 -0400)]
Update competition build rules.
Morgan Deters [Fri, 7 Nov 2014 14:24:15 +0000 (09:24 -0500)]
Merge branch '1.4.x'
Conflicts:
test/regress/regress0/Makefile.am
Morgan Deters [Fri, 7 Nov 2014 14:22:11 +0000 (09:22 -0500)]
Fix missing case in model postprocessor (resolves bug #595).
ajreynol [Fri, 7 Nov 2014 10:37:43 +0000 (11:37 +0100)]
Properly distinguish which EQC to assign values in datatypes, use assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
ajreynol [Thu, 6 Nov 2014 13:05:08 +0000 (14:05 +0100)]
Minor fix for getInstCons
ajreynol [Thu, 6 Nov 2014 10:41:35 +0000 (11:41 +0100)]
Reenable regression. Add (for now, disabled) changes to datatypes theory combination. Relax communication of dt facts.