ajreynol [Tue, 1 Nov 2016 20:39:39 +0000 (15:39 -0500)]
Make tuple and record names unique. Do not print internal datatype declaration in cvc printer.
ajreynol [Tue, 1 Nov 2016 19:31:41 +0000 (14:31 -0500)]
Fix memory leak in TheorySetsRels. Minor cleanup.
ajreynol [Tue, 1 Nov 2016 19:23:30 +0000 (14:23 -0500)]
Revert change to Datatypes API to return vector of DatatypeTypes, as before. ASAN failures with datatypes should now be mostly fixed.
ajreynol [Tue, 1 Nov 2016 18:33:38 +0000 (13:33 -0500)]
Revert change to datatypes API for passing pointers, instead make deep copy during call to mkMutualDatatypes.
ajreynol [Tue, 1 Nov 2016 18:20:49 +0000 (13:20 -0500)]
Working memory leak free version, changes interface to pointers.
ajreynol [Mon, 31 Oct 2016 15:45:27 +0000 (10:45 -0500)]
Minor refactoring in preparation for datatypes node cycle breaking.
ajreynol [Fri, 28 Oct 2016 22:14:04 +0000 (17:14 -0500)]
Add get instantiations utilities to API.
Clark Barrett [Thu, 27 Oct 2016 17:11:22 +0000 (10:11 -0700)]
Merge pull request #99 from 4tXJ7f/fix_dist_build3
Fix typo in Makefile that makes distcheck fail
Andres Notzli [Wed, 26 Oct 2016 23:04:21 +0000 (16:04 -0700)]
Fix typo in Makefile that makes distcheck fail
ajreynol [Wed, 26 Oct 2016 22:10:28 +0000 (17:10 -0500)]
Enable bv2nat regressions
Andrew Reynolds [Wed, 26 Oct 2016 21:26:57 +0000 (16:26 -0500)]
Merge pull request #98 from 4tXJ7f/fix_dist_build
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
ajreynol [Wed, 26 Oct 2016 21:23:58 +0000 (16:23 -0500)]
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Andres Notzli [Mon, 24 Oct 2016 00:14:14 +0000 (17:14 -0700)]
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
This commit adds regress4 to the `test/regress/Makefile.am`.
ajreynol [Fri, 21 Oct 2016 19:21:05 +0000 (14:21 -0500)]
Fix/add missing makefiles.
ajreynol [Fri, 21 Oct 2016 19:01:17 +0000 (14:01 -0500)]
Move slow regress0 benchmarks to regress1, increment regress1 through regress3.
Tim King [Wed, 19 Oct 2016 16:40:12 +0000 (09:40 -0700)]
Merge pull request #97 from 4tXJ7f/fix_rewrite
Fix minor bug and typo in boolean rewriter
Andres Notzli [Wed, 19 Oct 2016 09:58:59 +0000 (02:58 -0700)]
Fix minor bug and typo in boolean rewriter
One of the rewrites in the boolean rewriter had the condition `n[0] ==
tt && n[0] == ff`, which could never be true. Another rewrite covers the
same case but returns a `REWRITE_AGAIN` instead of a `REWRITE_DONE`.
This commit also fixes a minor typo.
ajreynol [Thu, 13 Oct 2016 22:44:19 +0000 (17:44 -0500)]
Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.
Tim King [Thu, 13 Oct 2016 18:30:17 +0000 (11:30 -0700)]
Initializes RoundingMode::roundNearestTiesToAway to a distinct value.
Tim King [Thu, 13 Oct 2016 07:22:24 +0000 (00:22 -0700)]
Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"
This reverts commit
3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to
5f415d4585134612bc24e9a823289fee35541a01.
Paul Meng [Tue, 11 Oct 2016 18:54:20 +0000 (13:54 -0500)]
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Paul Meng [Tue, 11 Oct 2016 18:43:28 +0000 (13:43 -0500)]
- fixed a memory leak issue with context dependent data structure
- clean up
Tim King [Mon, 3 Oct 2016 05:01:27 +0000 (22:01 -0700)]
Adding initializers for structs internal to ite_utilities.
guykatzz [Thu, 6 Oct 2016 06:39:48 +0000 (23:39 -0700)]
Added an option that allow empty dependencies when attempting to minimize preprocessing holes
Tim King [Mon, 3 Oct 2016 04:20:09 +0000 (21:20 -0700)]
Removing the throw specifiers from theory_uf_type_rules.h.
Tim King [Mon, 3 Oct 2016 04:19:22 +0000 (21:19 -0700)]
Removing the throw specifiers from theory_fp_type_rules.h.
Tim King [Mon, 3 Oct 2016 04:17:50 +0000 (21:17 -0700)]
Removing the throw specifiers from theory_datatypes_type_rules.h.
Tim King [Mon, 3 Oct 2016 04:16:28 +0000 (21:16 -0700)]
Removing an unused member from TreeLog.
Tim King [Mon, 3 Oct 2016 04:15:01 +0000 (21:15 -0700)]
Removing the throw specifiers from theory_bv_type_rules.h.
Tim King [Mon, 3 Oct 2016 01:08:29 +0000 (18:08 -0700)]
Removing the throw specifiers from Cardinality.
Tim King [Sat, 1 Oct 2016 22:40:30 +0000 (15:40 -0700)]
Removing the throw specifiers from Result.
Tim King [Sat, 1 Oct 2016 22:12:20 +0000 (15:12 -0700)]
Merge pull request #93 from timothy-king/clang-format
Adding a clang format file for the project.
Tim King [Sat, 1 Oct 2016 21:06:20 +0000 (14:06 -0700)]
Removing the throw specifiers from SExpr.
Tim King [Sat, 1 Oct 2016 20:50:32 +0000 (13:50 -0700)]
Removing the throw specifiers from SubrangeBounds.
ajreynol [Sat, 1 Oct 2016 12:08:45 +0000 (07:08 -0500)]
Incorporate non-bv parts of ajr/bvExt branch
ajreynol [Thu, 29 Sep 2016 22:48:33 +0000 (17:48 -0500)]
Address some coverity warnings, add another stat.
ajreynol [Thu, 29 Sep 2016 21:01:34 +0000 (16:01 -0500)]
Minor cleanup and additions to quantifiers statistics.
Kshitij Bansal [Wed, 28 Sep 2016 16:03:08 +0000 (12:03 -0400)]
Fix the merge of kbansal/card branch (
2039eab).
A bug was introduced in the cleanup process as preparation for the merge
(theory_sets_private.cpp, lines 2502-2508 in this commit).
Tim King [Tue, 27 Sep 2016 16:20:11 +0000 (09:20 -0700)]
Removing an unused iterator.
Tim King [Tue, 27 Sep 2016 16:18:34 +0000 (09:18 -0700)]
Reverting part of the previous changes to unconstrained simplifier.
Tim King [Mon, 26 Sep 2016 04:34:40 +0000 (21:34 -0700)]
Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp.
Tim King [Mon, 26 Sep 2016 04:34:03 +0000 (21:34 -0700)]
Adding missing break statements.
Tim King [Mon, 26 Sep 2016 04:03:39 +0000 (21:03 -0700)]
Closing an open file descriptor in MemoryMapFile.
Tim King [Mon, 26 Sep 2016 03:53:23 +0000 (20:53 -0700)]
Freeing memory in error handling code for bounded_token_buffer.
Tim King [Mon, 26 Sep 2016 03:46:26 +0000 (20:46 -0700)]
Deleting the eager bitblasting solver if present in TheoryBV.
Tim King [Mon, 26 Sep 2016 03:44:09 +0000 (20:44 -0700)]
Adding a destructor to QuantAntiSkolem.
Tim King [Mon, 26 Sep 2016 03:28:30 +0000 (20:28 -0700)]
Adding a destructor to TermDb.
Tim King [Mon, 26 Sep 2016 03:28:08 +0000 (20:28 -0700)]
Adding a destructor to CegqiOutputSingleInv.
Tim King [Mon, 26 Sep 2016 02:43:11 +0000 (19:43 -0700)]
Deleting optional members of StrongSolverTheoryUF.
Tim King [Mon, 26 Sep 2016 01:32:40 +0000 (18:32 -0700)]
Disambiguating a vector insert warning coming from coverity scan.
Tim King [Mon, 26 Sep 2016 01:20:52 +0000 (18:20 -0700)]
Deleting a temporary in theory sets enumerator.
Tim King [Mon, 26 Sep 2016 01:10:23 +0000 (18:10 -0700)]
Deleting the intermediate command singleton.
Tim King [Mon, 26 Sep 2016 00:30:23 +0000 (17:30 -0700)]
Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.
Tim King [Sun, 25 Sep 2016 23:18:34 +0000 (16:18 -0700)]
Adding virtual destructors to several classes in expr.h .
Tim King [Sun, 25 Sep 2016 22:52:57 +0000 (15:52 -0700)]
Removing an unused iterator.
Tim King [Sun, 25 Sep 2016 22:49:52 +0000 (15:49 -0700)]
Fixing a potential use after free coming from a pop_back() call invalidating strictly earlier entries.
Tim King [Sun, 25 Sep 2016 22:18:31 +0000 (15:18 -0700)]
Integrating a working coverity_scan travis rule back into
Paul Meng [Fri, 23 Sep 2016 22:43:05 +0000 (17:43 -0500)]
fixed a few bugs
ajreynol [Wed, 21 Sep 2016 14:10:18 +0000 (09:10 -0500)]
Remove duplicate code from my last commit
Tim King [Wed, 21 Sep 2016 07:07:32 +0000 (00:07 -0700)]
Fixing an error in the previous travis commit.
Tim King [Wed, 21 Sep 2016 06:50:49 +0000 (23:50 -0700)]
Updating the travis file for coverity scan.
ajreynol [Tue, 20 Sep 2016 22:46:13 +0000 (17:46 -0500)]
Refactor, separate theory-specific counterexample-guided instantiation.
ajreynol [Tue, 20 Sep 2016 21:02:14 +0000 (16:02 -0500)]
More refactoring of cbqi. Add a few regressions. Add option for qcf.
Tim King [Mon, 19 Sep 2016 03:31:41 +0000 (20:31 -0700)]
Merge pull request #92 from timothy-king/travis-cpp11
Adding a gnu++11 rule to travis.
Tim King [Sun, 18 Sep 2016 22:50:46 +0000 (15:50 -0700)]
Adding a clang format file for the project.
Adds a single example of applying this clang-format.
Tim King [Wed, 31 Aug 2016 04:31:59 +0000 (21:31 -0700)]
Adding a gnu++11 rule to travis.
ajreynol [Sun, 18 Sep 2016 22:21:17 +0000 (17:21 -0500)]
Minor fix for strings
guykatzz [Sat, 17 Sep 2016 00:18:56 +0000 (17:18 -0700)]
In a ROW guard proof, if the transitivity proof does not have a disequality, we can deduce that it is a constant-disequality proof and process it accordingly
guykatzz [Sat, 17 Sep 2016 00:10:51 +0000 (17:10 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4
ajreynol [Sat, 17 Sep 2016 00:06:05 +0000 (19:06 -0500)]
Use matching heuristics for EPR instantiation.
Guy [Fri, 16 Sep 2016 23:26:30 +0000 (16:26 -0700)]
Handling a corner case where a ROW's guard is a constant disequality.
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
Guy [Fri, 16 Sep 2016 22:43:47 +0000 (15:43 -0700)]
Let arith_proof print its own terms
ajreynol [Fri, 16 Sep 2016 17:47:23 +0000 (12:47 -0500)]
More refactoring of cbqi, start developing new interface.
ajreynol [Thu, 15 Sep 2016 23:44:04 +0000 (18:44 -0500)]
Further refactor cbqi.
ajreynol [Thu, 15 Sep 2016 21:10:20 +0000 (16:10 -0500)]
Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.
ajreynol [Thu, 15 Sep 2016 19:04:50 +0000 (14:04 -0500)]
Make sep pto a trigger kind, track in equality engines and term database.
ajreynol [Thu, 15 Sep 2016 15:43:28 +0000 (10:43 -0500)]
Refactor setIncomplete in quantifiers.
ajreynol [Wed, 14 Sep 2016 21:41:27 +0000 (16:41 -0500)]
Support for unique variable generation in node manager.
ajreynol [Wed, 14 Sep 2016 15:42:39 +0000 (10:42 -0500)]
Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR
Paul Meng [Tue, 13 Sep 2016 21:11:16 +0000 (16:11 -0500)]
fixed type checking and computing for PRODUCT and JOIN
ajreynol [Tue, 13 Sep 2016 18:36:28 +0000 (13:36 -0500)]
Minor changes to sep logic, epr, quantifier splitting.
Paul Meng [Tue, 13 Sep 2016 16:05:25 +0000 (11:05 -0500)]
refactored the code, added more benchmarks and minor fixes
Paul Meng [Mon, 12 Sep 2016 21:46:39 +0000 (16:46 -0500)]
fixed capitalized "kind"
ajreynol [Mon, 12 Sep 2016 20:48:11 +0000 (15:48 -0500)]
Refactor prenex modes.
ajreynol [Mon, 12 Sep 2016 19:45:38 +0000 (14:45 -0500)]
Remove old implementation of cbqi
ajreynol [Mon, 12 Sep 2016 19:28:29 +0000 (14:28 -0500)]
Prefer non-cardinality constants in term models for sep logic.
ajreynol [Mon, 12 Sep 2016 18:43:02 +0000 (13:43 -0500)]
Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep.
ajreynol [Fri, 9 Sep 2016 20:01:20 +0000 (15:01 -0500)]
Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.
ajreynol [Fri, 9 Sep 2016 19:14:09 +0000 (14:14 -0500)]
Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
ajreynol [Thu, 8 Sep 2016 20:14:19 +0000 (15:14 -0500)]
Refactor seplog preprocess. Handle case where sep data type cannot be inferred.
ajreynol [Sat, 3 Sep 2016 22:40:18 +0000 (17:40 -0500)]
Miniscope top level conjunctions for prenex normal form, allow one level miniscoping in prenex normal form.
ajreynol [Sat, 3 Sep 2016 18:03:31 +0000 (13:03 -0500)]
Option for prenex normal form
Tim King [Fri, 2 Sep 2016 05:10:57 +0000 (22:10 -0700)]
Merge pull request #91 from timothy-king/no-throw
Relaxing the throw specifiers for the destructors for Node, TypeNode,…
ajreynol [Thu, 1 Sep 2016 21:35:06 +0000 (16:35 -0500)]
Fix boolean term issue in invariants from sygus. Minor default options changes for cbqi.
ajreynol [Thu, 1 Sep 2016 15:20:48 +0000 (10:20 -0500)]
Cleanup quantifier elimination in smt engine.
ajreynol [Wed, 31 Aug 2016 22:44:42 +0000 (17:44 -0500)]
Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
Tim King [Thu, 1 Sep 2016 08:28:02 +0000 (01:28 -0700)]
Relaxing the throw specifiers for the destructors for Node, TypeNode, the context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.
Tim King [Thu, 1 Sep 2016 06:06:39 +0000 (23:06 -0700)]
Removing the forward declaration of QuantInfo from rewrite_engine.h.
Tim King [Wed, 31 Aug 2016 22:59:26 +0000 (15:59 -0700)]
Cleaning up the dead FORIT macros.
Tim King [Wed, 31 Aug 2016 22:58:21 +0000 (15:58 -0700)]
Removing the usage of typeof from theory_sets_private.