cvc5.git
7 years agoTravis: Package instead of download for cxxtest (#1055)
Andres Noetzli [Mon, 28 Aug 2017 17:22:31 +0000 (10:22 -0700)]
Travis: Package instead of download for cxxtest (#1055)

Before this commit, we were downloading cxxtest from Sourceforge. This commit
instead installs the Ubuntu package, which is easier and more reliable. Instead
of adding the package to the list of packages for Coverity and the common list
of packages, this commit changes the Coverity package list to just refer to the
common list of packages.

7 years agoMove LFSC checker out of the CVC repository. (#222)
Aina Niemetz [Fri, 25 Aug 2017 22:39:16 +0000 (15:39 -0700)]
Move LFSC checker out of the CVC repository. (#222)

LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we

+ Add --with-lfsc and --with-lfsc-directory as configure options.
   In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
   LFSC is disabled.

+ Disable proof checking if CVC4_USE_LFSC is not defined.
   Configuring the build with --check-proofs but without --with-lfsc results in an error.

+ Do not call LFSC's cleanup function (but we should in the future).
   LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
   Disabled call to lfscc_cleanup until the problem in lfscc is fixed.

+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
   anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
   before calling make check on the temp build (the build of the unpacked distribution tar ball).

7 years agoAdded missing includes (algorithm).
Aina Niemetz [Fri, 25 Aug 2017 20:29:04 +0000 (13:29 -0700)]
Added missing includes (algorithm).

Algorithm was previously removed from src/util/regexp.h which broke
compilation on some platforms.

7 years agoTest Java API on CI
Pat Hawks [Thu, 24 Aug 2017 22:31:09 +0000 (17:31 -0500)]
Test Java API on CI

7 years agoAdd include to fix build
Andres Noetzli [Thu, 24 Aug 2017 17:08:39 +0000 (10:08 -0700)]
Add include to fix build

7 years agoMerge pull request #191 from timothy-king/cleanup-regexp
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.

7 years agoFix typos
Andres Noetzli [Wed, 23 Aug 2017 18:13:07 +0000 (11:13 -0700)]
Fix typos

7 years agoRemoving TODO for 'Optimize via the iterator'. Not a priority. (#1051)
Tim King [Wed, 23 Aug 2017 22:49:32 +0000 (15:49 -0700)]
Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)

7 years agoCleanup: use Assert rather than C assert. (#1052)
Aina Niemetz [Tue, 22 Aug 2017 01:33:29 +0000 (18:33 -0700)]
Cleanup: use Assert rather than C assert. (#1052)

7 years agoUpdated NYU -> Stanford
Clark Barrett [Tue, 22 Aug 2017 00:30:45 +0000 (17:30 -0700)]
Updated NYU -> Stanford

7 years agoChange Bugzilla urls to Github issues.
Mathias Preiner [Mon, 21 Aug 2017 17:06:02 +0000 (10:06 -0700)]
Change Bugzilla urls to Github issues.

7 years agoRemove unused SubrangeBound(s) classes (#221)
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.

7 years agoAdd mbqi interleave option, change option fs-inst to fs-interleave.
ajreynol [Thu, 17 Aug 2017 09:53:11 +0000 (11:53 +0200)]
Add mbqi interleave option, change option fs-inst to fs-interleave.

7 years agoMinimize includes in expr.h: remove dups, iostream (#219)
Andres Noetzli [Tue, 15 Aug 2017 05:46:48 +0000 (22:46 -0700)]
Minimize includes in expr.h: remove dups, iostream (#219)

7 years agoMove function definitions from metakind.h to cpp (#218)
Andres Noetzli [Tue, 15 Aug 2017 03:10:55 +0000 (20:10 -0700)]
Move function definitions from metakind.h to cpp (#218)

7 years agoMove function definitions from kind.h to kind.cpp (#217)
Andres Noetzli [Tue, 15 Aug 2017 01:34:18 +0000 (18:34 -0700)]
Move function definitions from kind.h to kind.cpp (#217)

7 years agoMove function defns from smt_engine_scope.h to cpp (#216)
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.

7 years agoUse antlr-3.4 directory if already present in CVC4 root directory (#213)
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.

7 years agoMerge pull request #214 from CVC4/fix_warn_nonlinear
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

7 years agoBuild and test suite fixes for Windows (#186)
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

7 years agoFix compiler warnings in theory/arith/nonlinear_extension.cpp
Aina Niemetz [Sat, 12 Aug 2017 06:00:08 +0000 (23:00 -0700)]
Fix compiler warnings in theory/arith/nonlinear_extension.cpp

7 years agoMaintain frontier for tangent planes.
ajreynol [Thu, 10 Aug 2017 11:08:46 +0000 (06:08 -0500)]
Maintain frontier for tangent planes.

7 years agoFix line numbers in options_template
Andres Noetzli [Thu, 10 Aug 2017 23:55:55 +0000 (16:55 -0700)]
Fix line numbers in options_template

7 years agoFix compiler warning in src/context/context.h.
Mathias Preiner [Wed, 9 Aug 2017 23:44:05 +0000 (16:44 -0700)]
Fix compiler warning in src/context/context.h.

7 years agoFix help message for disable-unit-testing in configure.ac (don't -> do not)
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.

7 years agoRemove AigBitblaster implementation if ABC is not compiled (#212)
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.

7 years agoFix Assertion (compiler warning) in theory/bv/theory_bv.cpp
Aina Niemetz [Wed, 9 Aug 2017 22:27:33 +0000 (15:27 -0700)]
Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp

7 years agoFix compiler warning in sat_proof_implementation
Andres Noetzli [Tue, 8 Aug 2017 01:16:02 +0000 (18:16 -0700)]
Fix compiler warning in sat_proof_implementation

7 years agoUse cache for datatypes cycle check, add regression.
ajreynol [Tue, 8 Aug 2017 07:40:00 +0000 (02:40 -0500)]
Use cache for datatypes cycle check, add regression.

7 years agoMerge pull request #211 from CVC4/fix_warn_sygus
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

7 years agoOptionally split regression tests into test groups (#207)
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.

7 years agoFix compiler warning in theory/quantifiers/term_database_sygus.cpp
Aina Niemetz [Tue, 8 Aug 2017 00:05:47 +0000 (17:05 -0700)]
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp

7 years agoChange sygus output for failed reconstruction case.
ajreynol [Mon, 7 Aug 2017 10:00:43 +0000 (05:00 -0500)]
Change sygus output for failed reconstruction case.

7 years agoMake quantifier elimination more robust to preprocessing.
ajreynol [Mon, 7 Aug 2017 08:14:07 +0000 (03:14 -0500)]
Make quantifier elimination more robust to preprocessing.

7 years agoReorganized bitvector.h
Aina Niemetz [Sat, 5 Aug 2017 00:40:47 +0000 (17:40 -0700)]
Reorganized bitvector.h

7 years agoFix comments
Aina Niemetz [Fri, 4 Aug 2017 17:28:29 +0000 (10:28 -0700)]
Fix comments

7 years agoFix typos in comments
Aina Niemetz [Fri, 4 Aug 2017 17:28:16 +0000 (10:28 -0700)]
Fix typos in comments

7 years agoSet default language to smt lib 2.6 (including as a base language for sygus), update...
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.

7 years agoDisable debug symbols for production builds.
Mathias Preiner [Wed, 2 Aug 2017 23:18:53 +0000 (16:18 -0700)]
Disable debug symbols for production builds.

7 years agoMinor improvement for enumerative instantiation.
ajreynol [Mon, 31 Jul 2017 08:20:17 +0000 (03:20 -0500)]
Minor improvement for enumerative instantiation.

7 years agoFix memory leak in symbol table (#209)
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.

7 years agoChange remaining hash_set -> unordered_set (#208)
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

7 years agoAdd support for charat in native language, minor cleanup.
ajreynol [Sat, 29 Jul 2017 09:33:27 +0000 (04:33 -0500)]
Add support for charat in native language, minor cleanup.

7 years agoFix cache issues for cyclic string equations.
ajreynol [Fri, 28 Jul 2017 12:57:42 +0000 (07:57 -0500)]
Fix cache issues for cyclic string equations.

7 years ago-Og for non-opt build, parallel pcvc4 check (#206)
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.

7 years agoUse TEST_CPPFLAGS/TEST_CXXFLAGS to add path to CxxTest headers in configure.ac. ...
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.

7 years agoDisabling compiling unit tests with coverity scan for now.
Tim King [Sun, 23 Jul 2017 08:01:25 +0000 (01:01 -0700)]
Disabling compiling unit tests with coverity scan for now.

7 years agoDeprecating the unused convenience_node_builders.h (#203)
Tim King [Sun, 23 Jul 2017 03:02:44 +0000 (20:02 -0700)]
Deprecating the unused convenience_node_builders.h (#203)

7 years agoConsolidating the opaque pointers in SymbolTable. (#204)
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.

7 years agoMerge branch 'master' into cleanup-regexp
Tim King [Fri, 21 Jul 2017 01:00:11 +0000 (18:00 -0700)]
Merge branch 'master' into cleanup-regexp

7 years agoMoving from the gnu extensions for hash maps to the c++11 hash maps
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.

7 years agoFix a few bugs related to sygus.
ajreynol [Thu, 20 Jul 2017 08:35:38 +0000 (10:35 +0200)]
Fix a few bugs related to sygus.

7 years agoRemoving the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing...
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.

7 years agoFix simple_vc_compat_cxx example (#202)
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.

7 years agoAdding a garbage list that get collected during the ~Scope. Removing the CDHashMap...
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.

7 years agoFixing the order of the comparison operation.
Tim King [Mon, 17 Jul 2017 18:04:24 +0000 (11:04 -0700)]
Fixing the order of the comparison operation.

7 years agoMerge branch 'master' into cleanup-regexp
Tim King [Mon, 17 Jul 2017 17:51:09 +0000 (10:51 -0700)]
Merge branch 'master' into cleanup-regexp

7 years agoUse is_sorted, merge, copy from std (#199)
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.

7 years agoRemove PtrCloser (#198)
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.

7 years agoMoving to static_assert now that c++11 is available.
Tim King [Mon, 17 Jul 2017 05:13:10 +0000 (22:13 -0700)]
Moving to static_assert now that c++11 is available.

7 years agoUse CXXFLAGS when compiling parsers (#197)
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).

7 years agoFix warning about unknown escape sequence (#196)
Andres Noetzli [Sat, 15 Jul 2017 20:20:01 +0000 (16:20 -0400)]
Fix warning about unknown escape sequence (#196)

7 years agoDisable separate gnu++11 tests on Travis (#193)
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.

7 years agoRemoving BOOST_FOREACH usage.
Tim King [Fri, 14 Jul 2017 01:16:59 +0000 (18:16 -0700)]
Removing BOOST_FOREACH usage.

7 years agoCleaning up the CVC4::String class.
Tim King [Fri, 14 Jul 2017 00:35:00 +0000 (17:35 -0700)]
Cleaning up the CVC4::String class.

7 years agoMerge pull request #188 from aniemetz/cx11
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

7 years agoautoconf: make -std=gnu++11 mandatory
Aina Niemetz [Thu, 13 Jul 2017 19:36:38 +0000 (12:36 -0700)]
autoconf: make -std=gnu++11 mandatory

7 years agoFix unit tests for subranges. Fix destructors for context objs in unit tests.
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.

7 years agoFix .i files from last commit.
ajreynol [Wed, 12 Jul 2017 14:34:14 +0000 (09:34 -0500)]
Fix .i files from last commit.

7 years agoMake type rules more strict for operators whose type rules involve subtypes. Disable...
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).

7 years agoRemove trailing slashes from directories if specified via command line.
Mathias Preiner [Tue, 11 Jul 2017 18:55:54 +0000 (11:55 -0700)]
Remove trailing slashes from directories if specified via command line.

7 years agoDo not exit when value/model/unsat-core/proof is requested at wrong time, for bug...
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.

7 years agoAdd nl regression.
ajreynol [Mon, 10 Jul 2017 21:52:10 +0000 (16:52 -0500)]
Add nl regression.

7 years agoMerge ntExt branch. Adds support for transcendental functions. Refactoring of non...
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.

7 years agoSeparate sygus term utilities to new file, minor cleanup from last commit.
ajreynol [Mon, 10 Jul 2017 19:35:47 +0000 (14:35 -0500)]
Separate sygus term utilities to new file, minor cleanup from last commit.

7 years agoMerge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision...
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.

7 years agoPrerelease versioning for master.
Mathias Preiner [Mon, 10 Jul 2017 18:44:36 +0000 (11:44 -0700)]
Prerelease versioning for master.

7 years agoCutting release 1.5.
Mathias Preiner [Mon, 10 Jul 2017 17:26:01 +0000 (10:26 -0700)]
Cutting release 1.5.

7 years agoDisable tarball signing for now.
Mathias Preiner [Sat, 8 Jul 2017 00:43:07 +0000 (17:43 -0700)]
Disable tarball signing for now.

7 years agoMerge branch 'master' of github.com:CVC4/CVC4
Mathias Preiner [Sat, 8 Jul 2017 00:11:07 +0000 (17:11 -0700)]
Merge branch 'master' of github.com:CVC4/CVC4

7 years agoUpdate copyright year and refer to authors URL.
Mathias Preiner [Fri, 7 Jul 2017 23:38:42 +0000 (16:38 -0700)]
Update copyright year and refer to authors URL.

7 years agoRemove unused stacking_vector class (#185)
Andres Noetzli [Fri, 7 Jul 2017 22:25:04 +0000 (15:25 -0700)]
Remove unused stacking_vector class (#185)

7 years agoAvoid invoking copy constructor when safe printing (#184)
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.

7 years agoUpdate copyright headers.
Mathias Preiner [Fri, 7 Jul 2017 21:57:36 +0000 (14:57 -0700)]
Update copyright headers.

7 years agoUpdate files that are part of the CVC4 license, exclude minisat files.
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.

7 years agoUse consistent author names for the copyright headers.
Mathias Preiner [Fri, 7 Jul 2017 21:45:27 +0000 (14:45 -0700)]
Use consistent author names for the copyright headers.

7 years agoUse new copyright header format.
Mathias Preiner [Fri, 7 Jul 2017 18:54:58 +0000 (11:54 -0700)]
Use new copyright header format.

7 years agoEscape left brace in regex in update-copyright script.
Mathias Preiner [Fri, 7 Jul 2017 16:40:08 +0000 (09:40 -0700)]
Escape left brace in regex in update-copyright script.

7 years agoFix passing antlr arguments to configure in contrib/cut-release
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.

7 years agocut-release: git co -> git checkout
Aina Niemetz [Thu, 6 Jul 2017 22:43:06 +0000 (15:43 -0700)]
cut-release: git co -> git checkout

7 years agocut-release: option handling, get-antlr
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

7 years agoFix for logic info, update regressions. Update casc tfa script.
ajreynol [Wed, 5 Jul 2017 21:55:20 +0000 (16:55 -0500)]
Fix for logic info, update regressions. Update casc tfa script.

7 years agoupdated INSTALL for version 1.5
Mathias Preiner [Wed, 5 Jul 2017 21:26:06 +0000 (14:26 -0700)]
updated INSTALL for version 1.5

7 years agoUpdate unit test, news.
ajreynol [Wed, 5 Jul 2017 21:07:04 +0000 (16:07 -0500)]
Update unit test, news.

7 years agoNon-linear supported in ALL logics. Minor fixes for set logic with sygus.
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.

7 years agoUpdate README for 1.5 release (#182)
Andres Nötzli [Tue, 4 Jul 2017 05:56:10 +0000 (22:56 -0700)]
Update README for 1.5 release (#182)

7 years agoUpdates to AUTHORS and THANKS for 1.5 (mostly done by Tim).
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).

7 years agoUpdated NEWS, README, RELEASE-NOTES.
Clark Barrett [Fri, 30 Jun 2017 21:30:45 +0000 (14:30 -0700)]
Updated NEWS, README, RELEASE-NOTES.

7 years agoFix use-after-free with unsat cores/proofs (#174)
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().

7 years agoMinor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp...
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.