Tim King [Tue, 28 Mar 2017 05:15:23 +0000 (22:15 -0700)]
Minor cleanups to ExtTheory.
Tim King [Tue, 28 Mar 2017 03:59:48 +0000 (20:59 -0700)]
Removing the friend class modifier from ExtTheory to Theory.
Clark Barrett [Mon, 27 Mar 2017 20:20:27 +0000 (13:20 -0700)]
Merge pull request #137 from 4tXJ7f/throw_quals
Remove throw qualifiers in type enumerators
Tim King [Mon, 27 Mar 2017 19:26:14 +0000 (12:26 -0700)]
Making the ExtTheory object a private member of Theory.
Tim King [Mon, 27 Mar 2017 17:24:13 +0000 (10:24 -0700)]
Making ppNotifyAssertions take a const vector.
Tim King [Mon, 27 Mar 2017 17:02:11 +0000 (10:02 -0700)]
Moving the CareGraph into its own file.
Tim King [Mon, 27 Mar 2017 16:40:30 +0000 (09:40 -0700)]
Moving the theory::Assertion struct into its own file.
Andres Notzli [Mon, 27 Mar 2017 09:40:45 +0000 (11:40 +0200)]
Tim King [Mon, 27 Mar 2017 04:59:36 +0000 (21:59 -0700)]
Alphabetizing libcvc4_la_SOURCES.
ajreynol [Fri, 24 Mar 2017 14:56:12 +0000 (09:56 -0500)]
Add some regressions. Minor.
ajreynol [Fri, 24 Mar 2017 14:37:13 +0000 (09:37 -0500)]
Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
Clark Barrett [Thu, 23 Mar 2017 22:15:56 +0000 (15:15 -0700)]
Fixing warning message.
guykatzz [Thu, 23 Mar 2017 21:13:46 +0000 (14:13 -0700)]
support incremental unsat cores
ajreynol [Wed, 22 Mar 2017 16:15:19 +0000 (11:15 -0500)]
Fix more cases of rewritten explanations in strings for bug 784. Minor.
ajreynol [Wed, 22 Mar 2017 15:58:03 +0000 (10:58 -0500)]
Minor fix for bounded integers.
ajreynol [Wed, 22 Mar 2017 13:52:42 +0000 (08:52 -0500)]
Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.
ajreynol [Tue, 21 Mar 2017 21:39:25 +0000 (16:39 -0500)]
Improve computeCareGraph functions to check shared term equality status once per equivalence class pair.
Andrew Reynolds [Mon, 20 Mar 2017 20:42:16 +0000 (15:42 -0500)]
Merge pull request #135 from PaulMeng/master
fixed cvc4 parser for set complement
Paul Meng [Mon, 20 Mar 2017 18:49:31 +0000 (13:49 -0500)]
fixed cvc4 parser for set complement
Clark Barrett [Sat, 18 Mar 2017 23:20:56 +0000 (16:20 -0700)]
Fix for bug 707.
Clark Barrett [Sat, 18 Mar 2017 20:46:37 +0000 (13:46 -0700)]
Fix to help with bug 717
guykatzz [Fri, 17 Mar 2017 21:11:41 +0000 (14:11 -0700)]
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
Tim King [Thu, 16 Mar 2017 21:06:17 +0000 (14:06 -0700)]
Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.
ajreynol [Thu, 16 Mar 2017 19:19:58 +0000 (14:19 -0500)]
More fixes, features to examples.
ajreynol [Thu, 16 Mar 2017 19:05:23 +0000 (14:05 -0500)]
Minor fixes, always expand applications of lambdas at preprocess.
ajreynol [Thu, 16 Mar 2017 18:24:31 +0000 (13:24 -0500)]
Support for SMT LIB 2.6 syntax declare-datatype and match.
ajreynol [Thu, 16 Mar 2017 16:37:53 +0000 (11:37 -0500)]
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
ajreynol [Wed, 15 Mar 2017 21:28:55 +0000 (16:28 -0500)]
Fix regress1 Makefile for rewriterules, fixes bug 783.
Clark Barrett [Wed, 15 Mar 2017 21:00:17 +0000 (14:00 -0700)]
Merge pull request #134 from 4tXJ7f/fix_host
Fix win-build script to use MinGW-w64 by default
ajreynol [Wed, 15 Mar 2017 18:11:08 +0000 (13:11 -0500)]
Allow 0 argument recursive functions. Fixes bug 782.
Andres Notzli [Wed, 15 Mar 2017 08:25:39 +0000 (01:25 -0700)]
Fix win-build script to use MinGW-w64 by default
Previous changes to the win-build script left the script in an
inconsistent state: the script was updated to refer to MinGW-w64 but the
default host was still referring to MinGW.
guykatzz [Tue, 14 Mar 2017 19:52:42 +0000 (12:52 -0700)]
Merge pull request #133 from 4tXJ7f/fix_uninitialized
Fix uninitialized variable
Andres Notzli [Tue, 14 Mar 2017 18:32:26 +0000 (11:32 -0700)]
fix uninitialized variable
Clark Barrett [Tue, 14 Mar 2017 17:40:26 +0000 (10:40 -0700)]
Merge pull request #132 from 4tXJ7f/fix_mingw64
Fix MinGW-w64 build
ajreynol [Fri, 10 Mar 2017 22:36:10 +0000 (16:36 -0600)]
Minor fix for cbqi-all.
guykatzz [Thu, 9 Mar 2017 22:46:33 +0000 (14:46 -0800)]
bug fix
guykatzz [Thu, 9 Mar 2017 20:13:12 +0000 (12:13 -0800)]
better proof support for bools and formulas
Andres Notzli [Wed, 8 Mar 2017 10:50:56 +0000 (02:50 -0800)]
Fix MinGW-w64 build
This commit fixes configure.ac to try to get clock_gettime() from
pthread. Without it, clock_gettime() is detected as missing at
configuration time for MinGW-w64 but exists at compile time, which
causes conflicts. Additionally, this commit updates the helper script
for Windows to use MinGW-w64 by default instead of MinGW.
ajreynol [Tue, 7 Mar 2017 17:17:34 +0000 (11:17 -0600)]
More fixes for printing/parsing sets, fix kind name.
ajreynol [Tue, 7 Mar 2017 15:11:33 +0000 (09:11 -0600)]
Fix cvc parser for set compliment.
ajreynol [Mon, 6 Mar 2017 16:18:17 +0000 (10:18 -0600)]
Do not eagerly construct explanations in relation solver.
ajreynol [Mon, 6 Mar 2017 15:39:03 +0000 (09:39 -0600)]
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Clark Barrett [Mon, 6 Mar 2017 08:25:26 +0000 (00:25 -0800)]
Adding support for bool-to-bv
Squashed commit of the following:
commit
5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Mar 6 00:16:16 2017 -0800
Remove IFF case
commit
2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date: Mon Feb 20 12:37:06 2017 -0800
proof support for bvcomp
commit
d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 21:09:04 2017 -0800
Added missing cases to operator<< for bv rewrite rules.
commit
0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 11:43:51 2017 -0800
Added rewrite rules for new bitvector kinds.
commit
3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Feb 13 14:41:49 2017 -0800
First draft of bool-to-bv pass.
ajreynol [Fri, 3 Mar 2017 22:17:24 +0000 (16:17 -0600)]
Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.
ajreynol [Fri, 3 Mar 2017 16:33:03 +0000 (10:33 -0600)]
Another minor fix for sets related to sharing + finite element types.
ajreynol [Thu, 2 Mar 2017 22:40:39 +0000 (16:40 -0600)]
Fixes related to sets.
ajreynol [Thu, 2 Mar 2017 21:24:07 +0000 (15:24 -0600)]
Minor cleanup and reorganization related to last commit.
ajreynol [Thu, 2 Mar 2017 20:45:21 +0000 (14:45 -0600)]
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
ajreynol [Thu, 16 Feb 2017 22:19:51 +0000 (16:19 -0600)]
Minor fixes for relations, quantifiers dsplit.
ajreynol [Thu, 16 Feb 2017 19:26:10 +0000 (13:26 -0600)]
Fixes for sets+rels check. Minor.
ajreynol [Wed, 15 Feb 2017 17:26:56 +0000 (11:26 -0600)]
Minimization modes for fmf bound.
ajreynol [Tue, 7 Feb 2017 19:26:57 +0000 (13:26 -0600)]
Generalize finite bound inference to unifiable variables in set membership literals.
ajreynol [Mon, 30 Jan 2017 17:20:29 +0000 (11:20 -0600)]
Fix regexp cache issue in strings, add regression.
Andres Noetzli [Wed, 4 Jan 2017 17:20:34 +0000 (09:20 -0800)]
Fix non-idempotent rewrite in Array rewriter
This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.
Andrew Reynolds [Wed, 18 Jan 2017 19:32:55 +0000 (13:32 -0600)]
Merge pull request #128 from 4tXJ7f/fix_lfsc_perf
[LFSC] Fix performance issues, more determinism
ajreynol [Wed, 18 Jan 2017 18:39:24 +0000 (12:39 -0600)]
Minor fix in relations.
Andres Notzli [Tue, 10 Jan 2017 22:23:22 +0000 (01:23 +0300)]
[LFSC] Fix performance issues, more determinism
For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.
Clark Barrett [Sat, 14 Jan 2017 05:23:42 +0000 (21:23 -0800)]
Fix call to SExpr constructor for greater portability.
Clark Barrett [Sat, 14 Jan 2017 04:18:16 +0000 (20:18 -0800)]
Merge pull request #130 from chadbrewbaker/master
Fixing memory leak
ajreynol [Fri, 13 Jan 2017 15:40:15 +0000 (09:40 -0600)]
Do not rewrite explanations in strings.
Clark Barrett [Wed, 11 Jan 2017 22:20:22 +0000 (14:20 -0800)]
Merge pull request #129 from timothy-king/regression-scrubber
Adding regression test scrubbing.
Clark Barrett [Wed, 11 Jan 2017 22:03:11 +0000 (14:03 -0800)]
Merge pull request #131 from makaimann/fix_702
Proposed fix for bug 702
makaimann [Wed, 11 Jan 2017 21:47:06 +0000 (13:47 -0800)]
Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind BUILTIN before passing to prefixPrintGetValue()
ajreynol [Wed, 11 Jan 2017 20:34:18 +0000 (14:34 -0600)]
Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.
Clark Barrett [Wed, 11 Jan 2017 19:03:22 +0000 (11:03 -0800)]
Merge pull request #127 from cristian-mattarei/issue_679
Bug 679 fix
Chad Brewbaker [Wed, 11 Jan 2017 02:59:20 +0000 (20:59 -0600)]
revert
Chad Brewbaker [Wed, 11 Jan 2017 02:51:24 +0000 (20:51 -0600)]
Quashing memory leak
Tim King [Wed, 11 Jan 2017 01:51:14 +0000 (17:51 -0800)]
Adding regression test scrubbing.
Cristian Mattarei [Mon, 9 Jan 2017 03:00:09 +0000 (19:00 -0800)]
With reference to Bug 679, this commit integrates part of the patch proposed, and it fixes the correct float parsing of an std::istringstream.
The compilation issue in Bug 679 does not apply anymore with gcc6.3.1
Chad Brewbaker [Sat, 7 Jan 2017 04:56:07 +0000 (22:56 -0600)]
quashing debug memory leak
ajreynol [Fri, 6 Jan 2017 19:27:18 +0000 (13:27 -0600)]
Minor fix for sets.
Tim King [Thu, 5 Jan 2017 23:07:33 +0000 (15:07 -0800)]
Disabling a regression test that assumes CVC4 is configured with proofs on. Modifying the travis rules so there are instances with proofs disabled.
ajreynol [Wed, 4 Jan 2017 21:28:24 +0000 (15:28 -0600)]
Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes.
Tim King [Wed, 4 Jan 2017 21:36:30 +0000 (13:36 -0800)]
Marking regression test files as non-executable.
Tim King [Wed, 4 Jan 2017 21:00:25 +0000 (13:00 -0800)]
Marking the proof signature files as non-executable.
Tim King [Wed, 4 Jan 2017 20:59:16 +0000 (12:59 -0800)]
Setting the executable bit for the newer run scripts in contrib.
Tim King [Wed, 4 Jan 2017 20:57:55 +0000 (12:57 -0800)]
Reverting two files encoding with DOS linebreaks back into using unix linebreaks.
Andrew Reynolds [Wed, 4 Jan 2017 18:21:52 +0000 (12:21 -0600)]
Merge pull request #122 from 4tXJ7f/fix_lfsc_str
[LFSC] Minor fixes/improvements
guykatzz [Wed, 4 Jan 2017 18:18:36 +0000 (10:18 -0800)]
Merge pull request #120 from 4tXJ7f/fix_f_pp_holes
Fix dependency tracing for fewerPreprocessingHoles
Andrew Reynolds [Wed, 4 Jan 2017 17:47:52 +0000 (11:47 -0600)]
Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks
[LFSC] Fix memory leaks when creating CExprs
Tim King [Thu, 29 Dec 2016 23:43:04 +0000 (15:43 -0800)]
Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.
Tim King [Thu, 29 Dec 2016 22:42:59 +0000 (14:42 -0800)]
Eliminating a signed vs. unsigned comparison.
Tim King [Thu, 29 Dec 2016 22:36:36 +0000 (14:36 -0800)]
Changing getTearDownIncremental() to return the type of options::tearDownIncremental.
Tim King [Thu, 29 Dec 2016 22:36:00 +0000 (14:36 -0800)]
Adding a destructor to InstantiationNotify.
Tim King [Thu, 29 Dec 2016 22:35:02 +0000 (14:35 -0800)]
Adding a destructor to RepBoundExt.
Tim King [Thu, 29 Dec 2016 22:34:29 +0000 (14:34 -0800)]
Reordering sep and sets in Makefile.theories.
Andres Notzli [Thu, 22 Dec 2016 12:45:29 +0000 (04:45 -0800)]
[LFSC] Minor fixes/improvements
- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions
Andres Notzli [Thu, 22 Dec 2016 04:03:29 +0000 (20:03 -0800)]
[LFSC] Fix memory leaks when creating CExprs
In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).
Andres Notzli [Thu, 15 Dec 2016 05:20:17 +0000 (21:20 -0800)]
Fix dependency tracing for fewerPreprocessingHoles
Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed. Additionally, it fixes
a similar issue in the theory engine.
NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.
Clark Barrett [Wed, 14 Dec 2016 21:45:54 +0000 (13:45 -0800)]
Merge pull request #119 from 4tXJ7f/smt_v2_5
Switch from SMT-LIB v2.0 to v2.5 for smt2 files
Andres Notzli [Wed, 14 Dec 2016 19:33:08 +0000 (11:33 -0800)]
Switch from SMT-LIB v2.0 to v2.5 for smt2 files
As mentioned in bug 741, CVC4 was parsing `.smt2` files using the
SMT-LIB v2.0 standard by default. This commit switches to v2.5.
Clark Barrett [Wed, 14 Dec 2016 19:12:58 +0000 (11:12 -0800)]
Made tear-down-incremental more like it used to be: when tear-down value
is 1, it does not automatically enable incremental mode.
Andrew Reynolds [Tue, 13 Dec 2016 21:20:58 +0000 (15:20 -0600)]
Merge pull request #118 from 4tXJ7f/fix_emp
Fix split-find-unsat-w-emp test
Clark Barrett [Mon, 12 Dec 2016 17:38:53 +0000 (09:38 -0800)]
Merge pull request #117 from 4tXJ7f/fix_order
Fix initialization order
Andres Notzli [Mon, 12 Dec 2016 09:55:36 +0000 (01:55 -0800)]
Fix split-find-unsat-w-emp test
Commit
2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the
split-find-unsat-w-emp test, this commit fixes that.
Clark Barrett [Mon, 12 Dec 2016 02:21:52 +0000 (18:21 -0800)]
Merge branch 'master' into fix_order
Clark Barrett [Mon, 12 Dec 2016 02:18:44 +0000 (18:18 -0800)]
Merge pull request #116 from 4tXJ7f/fix_mult
Fix (inactive) `MultSlice` rewrite
Tim King [Fri, 9 Dec 2016 22:28:23 +0000 (14:28 -0800)]
Fixing a use after free bug in Polynomial::denominatorLCM.
Andres Notzli [Thu, 8 Dec 2016 02:05:54 +0000 (18:05 -0800)]
Fix initialization order
This commit addresses the following warning:
```
warning: field 'd_negOne' will be initialized after field 'd_pivots'
[-Wreorder]
```
Andres Notzli [Thu, 8 Dec 2016 22:21:28 +0000 (14:21 -0800)]
Fix (inactive) `MultSlice` rewrite
The `MultSlice` rewrite was previously accepting multiplications of
three and more variables even though it was designed for multiplications
of two variables only. Fortunately, the rewrite was not actively used in
the bitvector solver. This commit strengthens the condition in
`applies()` and adds a unit test that checks that x * y * z and x * y do
not get rewritten to the same term.