Pat Hawks [Thu, 24 Aug 2017 22:31:09 +0000 (17:31 -0500)]
Test Java API on CI
Andres Noetzli [Thu, 24 Aug 2017 17:08:39 +0000 (10:08 -0700)]
Add include to fix build
Andrew Reynolds [Thu, 24 Aug 2017 12:09:43 +0000 (14:09 +0200)]
Merge pull request #191 from timothy-king/cleanup-regexp
Cleaning up the CVC4::String class.
Andres Noetzli [Wed, 23 Aug 2017 18:13:07 +0000 (11:13 -0700)]
Fix typos
Tim King [Wed, 23 Aug 2017 22:49:32 +0000 (15:49 -0700)]
Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)
Aina Niemetz [Tue, 22 Aug 2017 01:33:29 +0000 (18:33 -0700)]
Cleanup: use Assert rather than C assert. (#1052)
Clark Barrett [Tue, 22 Aug 2017 00:30:45 +0000 (17:30 -0700)]
Updated NYU -> Stanford
Mathias Preiner [Mon, 21 Aug 2017 17:06:02 +0000 (10:06 -0700)]
Change Bugzilla urls to Github issues.
Andres Noetzli [Thu, 17 Aug 2017 15:51:51 +0000 (08:51 -0700)]
Remove unused SubrangeBound(s) classes (#221)
As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
ajreynol [Thu, 17 Aug 2017 09:53:11 +0000 (11:53 +0200)]
Add mbqi interleave option, change option fs-inst to fs-interleave.
Andres Noetzli [Tue, 15 Aug 2017 05:46:48 +0000 (22:46 -0700)]
Minimize includes in expr.h: remove dups, iostream (#219)
Andres Noetzli [Tue, 15 Aug 2017 03:10:55 +0000 (20:10 -0700)]
Move function definitions from metakind.h to cpp (#218)
Andres Noetzli [Tue, 15 Aug 2017 01:34:18 +0000 (18:34 -0700)]
Move function definitions from kind.h to kind.cpp (#217)
Andres Noetzli [Mon, 14 Aug 2017 22:32:23 +0000 (15:32 -0700)]
Move function defns from smt_engine_scope.h to cpp (#216)
Additionally, this commit removes unnecessary includes, adds includes to
smt_engine.h in files that require it and removes s_smtEngine_current from
smt_engine_scope.h.
Mathias Preiner [Mon, 14 Aug 2017 18:27:53 +0000 (11:27 -0700)]
Use antlr-3.4 directory if already present in CVC4 root directory (#213)
* Find antlr-3.4 directory if installed via contrib/get-antlr-3.4.
Aina Niemetz [Mon, 14 Aug 2017 16:56:00 +0000 (09:56 -0700)]
Merge pull request #214 from CVC4/fix_warn_nonlinear
Fix compiler warnings in theory/arith/nonlinear_extension.cpp
Mark Laws [Mon, 14 Aug 2017 16:44:54 +0000 (01:44 +0900)]
Build and test suite fixes for Windows (#186)
- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows
Aina Niemetz [Sat, 12 Aug 2017 06:00:08 +0000 (23:00 -0700)]
Fix compiler warnings in theory/arith/nonlinear_extension.cpp
ajreynol [Thu, 10 Aug 2017 11:08:46 +0000 (06:08 -0500)]
Maintain frontier for tangent planes.
Andres Noetzli [Thu, 10 Aug 2017 23:55:55 +0000 (16:55 -0700)]
Fix line numbers in options_template
Mathias Preiner [Wed, 9 Aug 2017 23:44:05 +0000 (16:44 -0700)]
Fix compiler warning in src/context/context.h.
Aina Niemetz [Wed, 9 Aug 2017 23:33:23 +0000 (16:33 -0700)]
Fix help message for disable-unit-testing in configure.ac (don't -> do not)
Previous help message broke syntax highlighting in vim.
Mathias Preiner [Wed, 9 Aug 2017 22:47:27 +0000 (15:47 -0700)]
Remove AigBitblaster implementation if ABC is not compiled (#212)
* Guard use of AigBitblaster with CVC4_USE_ABC.
This removes the Unreachable() implementation of AigBitblaster in case CVC4 is
not compiled with ABC support.
Aina Niemetz [Wed, 9 Aug 2017 22:27:33 +0000 (15:27 -0700)]
Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
Andres Noetzli [Tue, 8 Aug 2017 01:16:02 +0000 (18:16 -0700)]
Fix compiler warning in sat_proof_implementation
ajreynol [Tue, 8 Aug 2017 07:40:00 +0000 (02:40 -0500)]
Use cache for datatypes cycle check, add regression.
Andrew Reynolds [Tue, 8 Aug 2017 07:05:11 +0000 (09:05 +0200)]
Merge pull request #211 from CVC4/fix_warn_sygus
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp
Andres Noetzli [Tue, 8 Aug 2017 01:35:30 +0000 (18:35 -0700)]
Optionally split regression tests into test groups (#207)
To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.
Aina Niemetz [Tue, 8 Aug 2017 00:05:47 +0000 (17:05 -0700)]
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp
ajreynol [Mon, 7 Aug 2017 10:00:43 +0000 (05:00 -0500)]
Change sygus output for failed reconstruction case.
ajreynol [Mon, 7 Aug 2017 08:14:07 +0000 (03:14 -0500)]
Make quantifier elimination more robust to preprocessing.
Aina Niemetz [Sat, 5 Aug 2017 00:40:47 +0000 (17:40 -0700)]
Reorganized bitvector.h
Aina Niemetz [Fri, 4 Aug 2017 17:28:29 +0000 (10:28 -0700)]
Fix comments
Aina Niemetz [Fri, 4 Aug 2017 17:28:16 +0000 (10:28 -0700)]
Fix typos in comments
ajreynol [Fri, 4 Aug 2017 14:51:35 +0000 (16:51 +0200)]
Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.
Mathias Preiner [Wed, 2 Aug 2017 23:18:53 +0000 (16:18 -0700)]
Disable debug symbols for production builds.
ajreynol [Mon, 31 Jul 2017 08:20:17 +0000 (03:20 -0500)]
Minor improvement for enumerative instantiation.
Andres Noetzli [Sun, 30 Jul 2017 17:38:06 +0000 (10:38 -0700)]
Fix memory leak in symbol table (#209)
Commit
4cab39bd4f166716cd3d357a175c346afb838137 moved d_exprMap, d_typeMap,
and d_functions into SymbolTable::Implementation but did not move the deletion
of those objects from SymbolTable to the SymbolTable::Implementation
desconstructor, resulting in a memory leak. This commit fixes the issue.
Andres Noetzli [Sun, 30 Jul 2017 01:06:30 +0000 (18:06 -0700)]
Change remaining hash_set -> unordered_set (#208)
The nightly competition build has been failing due to a remaining use of
hash_set in approx_simplex.cpp. This commit changes the remaining uses
of hash_set to unordered_set.
The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC
required changing the configure.ac for LFSC to require C++11 support to
make sure that it can be compiled independently from the rest of CVC4 (some
of our Travis tests do that as well). To have the macros for these additional
checks available, the commit adds a symlink to the files in config that contain
the macros). I did not find a way to add macros from a parent's folder that
did not break `make distcheck
ajreynol [Sat, 29 Jul 2017 09:33:27 +0000 (04:33 -0500)]
Add support for charat in native language, minor cleanup.
ajreynol [Fri, 28 Jul 2017 12:57:42 +0000 (07:57 -0500)]
Fix cache issues for cyclic string equations.
Andres Noetzli [Thu, 27 Jul 2017 00:05:12 +0000 (17:05 -0700)]
-Og for non-opt build, parallel pcvc4 check (#206)
-Og enables optimizations that do not interfere with debugging. This is the new
default for debug builds if the compiler supports the flag. This commit also
enables parallel checking for the portfolio build on Travis.
Mathias Preiner [Wed, 26 Jul 2017 15:24:02 +0000 (08:24 -0700)]
Use TEST_CPPFLAGS/TEST_CXXFLAGS to add path to CxxTest headers in configure.ac. (#200)
CxxTest headers were included in test/unit/Makefile.am as -I@CXXTEST@. However, in configure.ac if CXXTEST was not set by the user, it was initially set to `dirname "$CXXTESTGEN"` while determining the path to the header files. If CXXTESTGEN pointed to /usr/bin and if the headers were found in /usr/include, CXXTEST was not reset, which led to CXXTEST being replaced by /usr/bin in test/unit/Makefile.am. As a consequence, the locale binary in /usr/bin got included instead of the locale header file.
Tim King [Sun, 23 Jul 2017 08:01:25 +0000 (01:01 -0700)]
Disabling compiling unit tests with coverity scan for now.
Tim King [Sun, 23 Jul 2017 03:02:44 +0000 (20:02 -0700)]
Deprecating the unused convenience_node_builders.h (#203)
Tim King [Sun, 23 Jul 2017 02:56:49 +0000 (19:56 -0700)]
Consolidating the opaque pointers in SymbolTable. (#204)
* Consolidating the opaque pointers in SymbolTable. This removes details about the implementation from a public header.
* Removing the guard for SymbolTable for the move constructor.
Tim King [Fri, 21 Jul 2017 01:00:11 +0000 (18:00 -0700)]
Merge branch 'master' into cleanup-regexp
Tim King [Fri, 21 Jul 2017 00:04:30 +0000 (17:04 -0700)]
Moving from the gnu extensions for hash maps to the c++11 hash maps
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
ajreynol [Thu, 20 Jul 2017 08:35:38 +0000 (10:35 +0200)]
Fix a few bugs related to sygus.
Tim King [Fri, 14 Jul 2017 23:56:11 +0000 (16:56 -0700)]
Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing it as well.
Andres Noetzli [Wed, 19 Jul 2017 19:59:36 +0000 (15:59 -0400)]
Fix simple_vc_compat_cxx example (#202)
The CVC3 compatibility layer was broken because it was setting
simplification mode to SIMPLIFICATION_MODE_INCREMENTAL, which
is not supported anymore since commit
2dbe1f150d30f0fb0c8522f891104270ce09db4c . This commit changes
the compatibility layer to not set the option anymore.
This addresses bug 833, which had been reported on the cvc-bugs mailing list.
Tim King [Fri, 14 Jul 2017 22:18:23 +0000 (15:18 -0700)]
Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap garbage.
Tim King [Mon, 17 Jul 2017 18:04:24 +0000 (11:04 -0700)]
Fixing the order of the comparison operation.
Tim King [Mon, 17 Jul 2017 17:51:09 +0000 (10:51 -0700)]
Merge branch 'master' into cleanup-regexp
Andres Noetzli [Mon, 17 Jul 2017 12:07:59 +0000 (08:07 -0400)]
Use is_sorted, merge, copy from std (#199)
Previously, we were checking whether we should use is_sorted
from std or __gnu_cxx. With C++11, std::is_sorted is
guaranteed to exist. This commit changes
arith/normal_form.{h,cpp} to always use std::is_sorted and
also removes the custom implementations for merge and copy by
using the std implementations instead.
Andres Noetzli [Mon, 17 Jul 2017 05:18:10 +0000 (01:18 -0400)]
Remove PtrCloser (#198)
With C++11, we don't need PtrCloser anymore because we can
just use std::unique_ptr.
Tim King [Mon, 17 Jul 2017 05:13:10 +0000 (22:13 -0700)]
Moving to static_assert now that c++11 is available.
Andres Noetzli [Sun, 16 Jul 2017 16:22:32 +0000 (12:22 -0400)]
Use CXXFLAGS when compiling parsers (#197)
ANTLR generates C files that we compile with the C++ compiler.
To do so, we set CC=CXX in the `Makefile.am`s of the parsers.
Previously, we did not copy the CXXFLAGS to the CFLAGS, which
could result in problems, e.g. when using -std=gnu++11 in the
CXXFLAGS, compiling the parsers would fail if they used C++11
features (configure.ac usually modifies CXX to include the
-std=gnu++11 flag but if it is included in CXXFLAGS, the CXX
is not changed).
Andres Noetzli [Sat, 15 Jul 2017 20:20:01 +0000 (16:20 -0400)]
Fix warning about unknown escape sequence (#196)
Andres Noetzli [Sat, 15 Jul 2017 02:37:27 +0000 (22:37 -0400)]
Disable separate gnu++11 tests on Travis (#193)
Given that we are now always compiling with gnu++11, we don't need
separate tests anymore.
Tim King [Fri, 14 Jul 2017 01:16:59 +0000 (18:16 -0700)]
Removing BOOST_FOREACH usage.
Tim King [Fri, 14 Jul 2017 00:35:00 +0000 (17:35 -0700)]
Cleaning up the CVC4::String class.
Aina Niemetz [Thu, 13 Jul 2017 21:41:35 +0000 (14:41 -0700)]
Merge pull request #188 from aniemetz/cx11
autoconf: make -std=gnu++11 mandatory
Aina Niemetz [Thu, 13 Jul 2017 19:36:38 +0000 (12:36 -0700)]
autoconf: make -std=gnu++11 mandatory
ajreynol [Wed, 12 Jul 2017 16:44:11 +0000 (11:44 -0500)]
Fix unit tests for subranges. Fix destructors for context objs in unit tests.
ajreynol [Wed, 12 Jul 2017 14:34:14 +0000 (09:34 -0500)]
Fix .i files from last commit.
ajreynol [Wed, 12 Jul 2017 13:35:03 +0000 (08:35 -0500)]
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Mathias Preiner [Tue, 11 Jul 2017 18:55:54 +0000 (11:55 -0700)]
Remove trailing slashes from directories if specified via command line.
ajreynol [Mon, 10 Jul 2017 22:40:56 +0000 (17:40 -0500)]
Do not exit when value/model/unsat-core/proof is requested at wrong time, for bug 831.
ajreynol [Mon, 10 Jul 2017 21:52:10 +0000 (16:52 -0500)]
Add nl regression.
ajreynol [Mon, 10 Jul 2017 21:22:19 +0000 (16:22 -0500)]
Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
ajreynol [Mon, 10 Jul 2017 19:35:47 +0000 (14:35 -0500)]
Separate sygus term utilities to new file, minor cleanup from last commit.
ajreynol [Mon, 10 Jul 2017 19:06:52 +0000 (14:06 -0500)]
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
Mathias Preiner [Mon, 10 Jul 2017 18:44:36 +0000 (11:44 -0700)]
Prerelease versioning for master.
Mathias Preiner [Mon, 10 Jul 2017 17:26:01 +0000 (10:26 -0700)]
Cutting release 1.5.
Mathias Preiner [Sat, 8 Jul 2017 00:43:07 +0000 (17:43 -0700)]
Disable tarball signing for now.
Mathias Preiner [Sat, 8 Jul 2017 00:11:07 +0000 (17:11 -0700)]
Merge branch 'master' of github.com:CVC4/CVC4
Mathias Preiner [Fri, 7 Jul 2017 23:38:42 +0000 (16:38 -0700)]
Update copyright year and refer to authors URL.
Andres Noetzli [Fri, 7 Jul 2017 22:25:04 +0000 (15:25 -0700)]
Remove unused stacking_vector class (#185)
Andres Noetzli [Fri, 7 Jul 2017 22:21:12 +0000 (15:21 -0700)]
Avoid invoking copy constructor when safe printing (#184)
When CVC4 gets interrupted, we use async-signal safe printing functions
to print statistics. Unfortunately, the code for that was invoking copy
constructors, which is problematic due to memory allocation; for example
with statistics such as ReferenceStat<std::string>. This commit adds a
getDataRef() method for statistics that returns a const reference to the
object being printed such that the copy constructor is not called. Note:
modifying getData() was unfortunately not an option because in the case
of TimerStat, we can't return a reference to an object on the stack. We
could remove the const modifier on getData() and use d_data to store the
information but then we would have to remove it on
safeFlushInformation() and potentially other methods as well, which
seems like a worse solution.
Mathias Preiner [Fri, 7 Jul 2017 21:57:36 +0000 (14:57 -0700)]
Update copyright headers.
Mathias Preiner [Fri, 7 Jul 2017 21:56:20 +0000 (14:56 -0700)]
Update files that are part of the CVC4 license, exclude minisat files.
Mathias Preiner [Fri, 7 Jul 2017 21:45:27 +0000 (14:45 -0700)]
Use consistent author names for the copyright headers.
Mathias Preiner [Fri, 7 Jul 2017 18:54:58 +0000 (11:54 -0700)]
Use new copyright header format.
Mathias Preiner [Fri, 7 Jul 2017 16:40:08 +0000 (09:40 -0700)]
Escape left brace in regex in update-copyright script.
Mathias Preiner [Thu, 6 Jul 2017 23:24:41 +0000 (16:24 -0700)]
Fix passing antlr arguments to configure in contrib/cut-release
Also fixes passing of makeargs.
Aina Niemetz [Thu, 6 Jul 2017 22:43:06 +0000 (15:43 -0700)]
cut-release: git co -> git checkout
Aina Niemetz [Thu, 6 Jul 2017 21:30:52 +0000 (14:30 -0700)]
cut-release: option handling, get-antlr
+ easier-to-maintain option handling
+ new option for compiling release with local antlr
ajreynol [Wed, 5 Jul 2017 21:55:20 +0000 (16:55 -0500)]
Fix for logic info, update regressions. Update casc tfa script.
Mathias Preiner [Wed, 5 Jul 2017 21:26:06 +0000 (14:26 -0700)]
updated INSTALL for version 1.5
ajreynol [Wed, 5 Jul 2017 21:07:04 +0000 (16:07 -0500)]
Update unit test, news.
ajreynol [Wed, 5 Jul 2017 20:01:23 +0000 (15:01 -0500)]
Non-linear supported in ALL logics. Minor fixes for set logic with sygus.
Andres Nötzli [Tue, 4 Jul 2017 05:56:10 +0000 (22:56 -0700)]
Update README for 1.5 release (#182)
Clark Barrett [Fri, 30 Jun 2017 22:20:38 +0000 (15:20 -0700)]
Updates to AUTHORS and THANKS for 1.5 (mostly done by Tim).
Clark Barrett [Fri, 30 Jun 2017 21:30:45 +0000 (14:30 -0700)]
Updated NEWS, README, RELEASE-NOTES.
Andres Nötzli [Fri, 30 Jun 2017 18:39:17 +0000 (11:39 -0700)]
Fix use-after-free with unsat cores/proofs (#174)
In TSatProof<Solver>::finalizeProof(), we got a clause from the clause
allocator, called resolveUnit() and then size() on the clause. The problem is
that resolveUnit() can reallocate memory (and there is even a comment warning
about that in finalizeProof()), which invalidates the clause. This commit gets
the clause again from the clause allocator before calling size().
ajreynol [Fri, 30 Jun 2017 14:02:51 +0000 (09:02 -0500)]
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
ajreynol [Wed, 28 Jun 2017 18:37:18 +0000 (13:37 -0500)]
Enable non-linear solve by default, update regressions.
Andres Nötzli [Fri, 23 Jun 2017 06:56:45 +0000 (23:56 -0700)]
Fix assertion failure due to missing clause id (#180)
This commit fixes bug 821. As written in the description of the bug, the issue
is that `id` is not being set on one of the paths in addClause(), specifically
in the case where all but one literal are assigned false and the remaining
literal is assigned true. In that case, we are not actually adding anything and
set the `id` to `ClauseIdUndef`.
Andres Nötzli [Thu, 22 Jun 2017 00:17:36 +0000 (17:17 -0700)]
Fix unsat cores script for SMT-COMP (#179)