cvc5.git
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 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 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 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.

7 years agoEnable non-linear solve by default, update regressions.
ajreynol [Wed, 28 Jun 2017 18:37:18 +0000 (13:37 -0500)]
Enable non-linear solve by default, update regressions.

7 years agoFix assertion failure due to missing clause id (#180)
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`.

7 years agoFix unsat cores script for SMT-COMP (#179)
Andres Nötzli [Thu, 22 Jun 2017 00:17:36 +0000 (17:17 -0700)]
Fix unsat cores script for SMT-COMP (#179)

7 years agoMerge pull request #175 from CVC4/fix_uninit
Andrew Reynolds [Wed, 21 Jun 2017 20:50:04 +0000 (15:50 -0500)]
Merge pull request #175 from CVC4/fix_uninit

Fix uninitialized value

7 years agoProperly handle subtypes in smt2 printer.
ajreynol [Wed, 21 Jun 2017 19:21:45 +0000 (14:21 -0500)]
Properly handle subtypes in smt2 printer.

7 years agoAdd run script for unsat cores track at SMT-COMP (#177)
Andres Nötzli [Wed, 21 Jun 2017 16:25:11 +0000 (09:25 -0700)]
Add run script for unsat cores track at SMT-COMP (#177)

Note: this was a last minute effort, so we do not use the portfolio build for
this track. This part for example:

https://github.com/CVC4/CVC4/blob/d43e5fb294d89ba69f7d2607a12c8700b7ec9345/src/main/command_executor_portfolio.cpp#L351-L355

Would have to change before we can enable use the portfolio build for unsat
cores in a competition build.

7 years agoMerge pull request #176 from CVC4/smtcomp2017
Andrew Reynolds [Wed, 21 Jun 2017 16:15:06 +0000 (11:15 -0500)]
Merge pull request #176 from CVC4/smtcomp2017

Better configuration for QF_NRA

7 years agoUpdate casc and sygus comp scripts.
ajreynol [Wed, 21 Jun 2017 15:24:11 +0000 (10:24 -0500)]
Update casc and sygus comp scripts.

7 years agoCheck for sigaltstack in configure (#172)
Clément Pit-Claudel [Wed, 21 Jun 2017 14:35:36 +0000 (10:35 -0400)]
Check for sigaltstack in configure (#172)

7 years agoFix SIGILL handler
Andres Noetzli [Tue, 20 Jun 2017 19:50:40 +0000 (12:50 -0700)]
Fix SIGILL handler

As pointed out by @cpitclaudel in pull request #172, we are using the same
handler for SIGSEGV and SIGILL and ill_handler() is unused. This commit changes
the SIGILL handler to ill_handler().

7 years agoBetter configuration for QF_NRA
Andres Noetzli [Mon, 19 Jun 2017 06:51:27 +0000 (23:51 -0700)]
Better configuration for QF_NRA

7 years agoFix assertion
ajreynol [Sun, 18 Jun 2017 14:09:16 +0000 (09:09 -0500)]
Fix assertion

7 years agoMinor change to ensureTheoryAtoms for bug 828.
ajreynol [Sun, 18 Jun 2017 13:54:36 +0000 (08:54 -0500)]
Minor change to ensureTheoryAtoms for bug 828.

7 years agoChange language in competition script to smt2.6 (#171)
Andres Nötzli [Sat, 17 Jun 2017 03:07:17 +0000 (20:07 -0700)]
Change language in competition script to smt2.6 (#171)

* Change language in competition script to smt2.6

The benchmark scrambler for the application track cuts out
the :smt-lib-version command, so this commit sets it
manually to 2.6 (all benchmarks in SMT-COMP use the 2.6
standard) instead of 2.0. I have not seen any failures due
to that but might as well be prudent.

* Change language in competition script to smt2.6

The benchmark scrambler (at least for the application
track) cuts out the :smt-lib-version command, so this
commit sets it manually to 2.6 (all benchmarks in SMT-COMP
use the 2.6 standard) instead of 2.0. I have not seen any
failures due to that but might as well be prudent.

7 years agoFix stream parsing
Andres Nötzli [Sat, 17 Jun 2017 00:42:22 +0000 (17:42 -0700)]
Fix stream parsing

This commit fixes bug 811. Bug 811 was caused because tokens were referring to
a buffer that was reallocated and thus the pointers were not valid anymore.

Background:
The buffered input stream avoids copying the whole input stream before handing
it to ANTLR (in contrast to the non-buffered input stream that first copies
everything into a buffer). This enables interactivity (e.g. with kind2) and may
save memory.
CVC4 uses it when reading from stdin in competition mode for the application
track (the incremental benchmarks) and in non-competition mode. To set the
CVC4_SMTCOMP_APPLICATION_TRACK flag, the {C,CXX}FLAGS have to be modified at
configure time.

Solution:
This commit fixes the issue by changing how a stream gets buffered. Instead of
storing the stream into a single buffer, CVC4 now stores each line in a
separate buffer, making sure that they do not have to move, keeping tokens
valid. The commit adds the LineBuffer class for managing those buffers. It
further modifies CVC4's LA and consume functions to use line number and
position within a line to index into the line buffer. This allows us to use the
standard mark()/etc. functions because they automatically store and
restore that state. The solution also (arguably) simplifies the code.

Disadvantages:
Tokens split across lines would cause problems (seems reasonable to me). One
allocation per line.

Alternatives considered:
Pull request 162 by Tim was a first attempt to solve the problem. The issues
with this solution are: memory usage (old versions of the buffer do not get
deleted), tokens split across buffers would be problematic, and
mark()/rewind()/etc. would have to be overwritten for the approach to work.
I had a partially working fix that used indexes into the stream instead of
pointers to memory. The solution stored the content of the stream into a
segmented buffer (lines were not guaranteed to be consecutive in memory. This
approach was working for basic use cases but had the following issues: ugly
casting (the solution requires casting the index to a pointer and storing it in
the input stream's nextChar because that's where ANTLR is taking the location
information from when creating a token), more modifications (not only would
this solution require overwriting more functions of the input stream such as
substr, it also requires changes to the use of GETCHARINDEX() in the Smt2
parser and AntlrInput::tokenText() for example), more complex code.

7 years agoMerge pull request #170 from CVC4/fix_2_6_parser3
Clark Barrett [Fri, 16 Jun 2017 19:46:47 +0000 (12:46 -0700)]
Merge pull request #170 from CVC4/fix_2_6_parser3

Parse 'is', 'match' differently for non-DT input

7 years agoFix segfault by making unit conflict CDMaybe
Andres Nötzli [Fri, 16 Jun 2017 18:16:04 +0000 (11:16 -0700)]
Fix segfault by making unit conflict CDMaybe

This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.

7 years agoParse 'is', 'match' differently for non-DT input
Andres Noetzli [Fri, 16 Jun 2017 15:47:35 +0000 (08:47 -0700)]
Parse 'is', 'match' differently for non-DT input

In SMT 2.6, Datatypes are being introduced and they come
with testers (indexed identifier of the form (_ is c)) and
match expressions. This lead to failures in UFIDL
benchmarks in SMT-LIB because they declare the function
'is'. This commit changes the parser s.t. it does not
consider 'is' and 'match' special tokens unless the theory
of datatypes is enabled.

7 years agoFix for bug 639.
Clark Barrett [Fri, 16 Jun 2017 00:11:22 +0000 (17:11 -0700)]
Fix for bug 639.

7 years agoMake comp script more robust
Andres Noetzli [Thu, 15 Jun 2017 21:11:29 +0000 (14:11 -0700)]
Make comp script more robust

In certain cases, the trace executor inserts empty lines, which threw off
our competition script. This commit adds code to ignores empty lines.

7 years agoFix for issue related to cbqi + E-matching.
ajreynol [Thu, 15 Jun 2017 17:47:43 +0000 (12:47 -0500)]
Fix for issue related to cbqi + E-matching.

7 years agoAdd regression.
ajreynol [Thu, 15 Jun 2017 16:34:15 +0000 (11:34 -0500)]
Add regression.

7 years agoFix relevant domain for datatypes, fixes bug 824.
ajreynol [Thu, 15 Jun 2017 15:49:51 +0000 (10:49 -0500)]
Fix relevant domain for datatypes, fixes bug 824.

7 years agoEnsure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for...
ajreynol [Thu, 15 Jun 2017 15:31:58 +0000 (10:31 -0500)]
Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.

7 years agoMerge pull request #167 from CVC4/fix_div
Clark Barrett [Thu, 15 Jun 2017 02:56:56 +0000 (19:56 -0700)]
Merge pull request #167 from CVC4/fix_div

Remove UdivSelf rewrite, add UdivZero rewrite

7 years agoRemove UdivSelf rewrite, add UdivZero rewrite
Andres Noetzli [Wed, 14 Jun 2017 22:53:51 +0000 (15:53 -0700)]
Remove UdivSelf rewrite, add UdivZero rewrite

This fixes bug 820. The issue was that (a udiv a) got rewriten to 1, which is
not correct when a is 0 (the result is all ones in that case). Even with the
--bv-div-zero-const flag disabled, the UdivSelf rewrite was incorrect because
it was applied to BITVECTOR_UDIV_TOTAL, which is "defined to be the all-ones
bit pattern, if divisor is 0" according to src/theory/bv/kinds . The commit
adds instead an optimization that returns all ones if the divisor of a
BITVECTOR_UDIV_TOTAL is zero.

7 years agoFix uninitialized value
Andres Noetzli [Wed, 14 Jun 2017 09:40:17 +0000 (02:40 -0700)]
Fix uninitialized value

7 years agoFix compile error
Clark Barrett [Sun, 4 Jun 2017 05:19:01 +0000 (22:19 -0700)]
Fix compile error

7 years agoMinor to smt comp script.
ajreynol [Sat, 3 Jun 2017 18:27:52 +0000 (13:27 -0500)]
Minor to smt comp script.

7 years agoFix regression.
ajreynol [Fri, 2 Jun 2017 20:58:02 +0000 (15:58 -0500)]
Fix regression.

7 years agoIncorporate datatypes into smt comp script, add regression.
ajreynol [Fri, 2 Jun 2017 20:54:14 +0000 (15:54 -0500)]
Incorporate datatypes into smt comp script, add regression.

7 years agoMinor optimizations related to cbqi.
ajreynol [Thu, 1 Jun 2017 17:38:33 +0000 (12:38 -0500)]
Minor optimizations related to cbqi.