Andrew Reynolds [Tue, 27 Nov 2018 16:56:27 +0000 (10:56 -0600)]
Lazy model construction in TheoryEngine (#2633)
Andres Noetzli [Tue, 27 Nov 2018 16:10:36 +0000 (08:10 -0800)]
Reduce lookahead when parsing string literals (#2721)
Alex Ozdemir [Tue, 27 Nov 2018 08:59:22 +0000 (00:59 -0800)]
LRA proof signature fixes and a first proof for linear polynomials (#2713)
* LRA proof signature fixes and a first proof
The existing LRA signature had a few problems (e.g. referencing symbols
that didn't exist, extra parentheses, etc). I patched it up and wrote an
first example LRA proof. load `th_lra_test.plf` last to run that test.
* Add dependency info to signatures
I chose to indicate shallow dependencies only.
Tom Smeding [Fri, 23 Nov 2018 07:31:21 +0000 (08:31 +0100)]
Use https for antlr3.org downloads (#2701)
This commit changes the two www,antlr3.org URL's in contrib/get-antlr-3.4 to use https instead of http, which is more secure.
Andres Noetzli [Thu, 22 Nov 2018 01:44:50 +0000 (17:44 -0800)]
Move ss-combine rewrite to extended rewriter (#2703)
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
Andres Noetzli [Thu, 22 Nov 2018 00:47:57 +0000 (16:47 -0800)]
Add rewrite for (str.substr s x y) --> "" (#2695)
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
Andrew Reynolds [Wed, 21 Nov 2018 23:07:17 +0000 (17:07 -0600)]
Cache evaluations for PBE (#2699)
Andrew Reynolds [Wed, 21 Nov 2018 22:24:16 +0000 (16:24 -0600)]
Quickly recognize when PBE conjectures are infeasible (#2718)
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
Martin [Wed, 21 Nov 2018 21:59:51 +0000 (21:59 +0000)]
Obvious rewrites to floating-point < and <=. (#2706)
Andrew Reynolds [Wed, 21 Nov 2018 20:44:44 +0000 (14:44 -0600)]
Support string replace all (#2704)
Andrew Reynolds [Wed, 21 Nov 2018 14:59:51 +0000 (08:59 -0600)]
Fix type enumerator for FP (#2717)
Andrew Reynolds [Tue, 20 Nov 2018 16:48:41 +0000 (10:48 -0600)]
Fix real2int regression. (#2716)
Alex Ozdemir [Tue, 20 Nov 2018 05:46:29 +0000 (21:46 -0800)]
Change lemma proof step storage & iterators (#2712)
Proof steps were in a std::list, which is a linked list, but really, we
only needed a stack, so I changed it to a vector, because LL's are
usually slower.
Also added an iterator for the proof steps, and << implementations
Andrew Reynolds [Tue, 20 Nov 2018 01:18:38 +0000 (19:18 -0600)]
Clausify context-dependent simplifications in ext theory (#2711)
Andrew Reynolds [Mon, 19 Nov 2018 23:29:44 +0000 (17:29 -0600)]
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Andrew Reynolds [Thu, 15 Nov 2018 22:40:37 +0000 (16:40 -0600)]
Expand definitions prior to model core computation (#2707)
Mathias Preiner [Wed, 14 Nov 2018 19:48:49 +0000 (11:48 -0800)]
cmake: Require boost 1.50.0 for examples. (#2710)
Mathias Preiner [Thu, 8 Nov 2018 19:10:16 +0000 (11:10 -0800)]
cmake: Add option to explicitely enable/disable static binaries. (#2698)
Andres Noetzli [Thu, 8 Nov 2018 01:04:52 +0000 (17:04 -0800)]
Evaluator: add support for str.code (#2696)
Haniel Barbosa [Wed, 7 Nov 2018 23:12:38 +0000 (17:12 -0600)]
Adding default SyGuS grammar construction for arrays (#2685)
Andres Noetzli [Wed, 7 Nov 2018 18:28:25 +0000 (10:28 -0800)]
Fix collectEmptyEqs in string rewriter (#2692)
Andrew Reynolds [Wed, 7 Nov 2018 16:52:51 +0000 (10:52 -0600)]
Fix for itos reduction (#2691)
Andrew Reynolds [Tue, 6 Nov 2018 23:28:41 +0000 (17:28 -0600)]
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Andrew Reynolds [Mon, 5 Nov 2018 22:50:48 +0000 (16:50 -0600)]
Change default sygus enumeration mode to auto (#2689)
Andrew Reynolds [Mon, 5 Nov 2018 22:16:31 +0000 (16:16 -0600)]
Fix coverity warnings in sygus enumerator (#2687)
Aina Niemetz [Mon, 5 Nov 2018 17:43:29 +0000 (09:43 -0800)]
New C++ API: Split unit tests. (#2688)
yoni206 [Mon, 5 Nov 2018 17:25:09 +0000 (09:25 -0800)]
Increasing coverage (#2683)
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
Andres Noetzli [Mon, 5 Nov 2018 17:01:03 +0000 (09:01 -0800)]
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
Andres Noetzli [Mon, 5 Nov 2018 16:42:21 +0000 (08:42 -0800)]
configure.sh: Fix option parsing to match --help (#2611)
Andrew Reynolds [Mon, 5 Nov 2018 15:25:33 +0000 (09:25 -0600)]
Allow partial models with optimized sygus enumeration (#2682)
Andrew Reynolds [Mon, 5 Nov 2018 00:06:29 +0000 (18:06 -0600)]
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Haniel Barbosa [Sat, 3 Nov 2018 14:48:31 +0000 (09:48 -0500)]
Refactor default grammars construction (#2681)
yoni206 [Fri, 2 Nov 2018 02:06:06 +0000 (19:06 -0700)]
fixes to regression docs (#2679)
Andrew Reynolds [Wed, 31 Oct 2018 21:25:37 +0000 (16:25 -0500)]
Add optimized sygus enumeration (#2677)
Andres Noetzli [Wed, 31 Oct 2018 14:23:09 +0000 (07:23 -0700)]
Record assumption info in AssertionPipeline (#2678)
Andrew Reynolds [Wed, 24 Oct 2018 20:20:18 +0000 (15:20 -0500)]
Minor improvement to sygus trace (#2675)
Andres Noetzli [Wed, 24 Oct 2018 04:43:28 +0000 (21:43 -0700)]
CMake: Set RPATH on installed binary (#2671)
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
Andrew Reynolds [Tue, 23 Oct 2018 00:26:10 +0000 (19:26 -0500)]
Do not use lazy trie for sygus-rr-verify (#2668)
makaimann [Mon, 22 Oct 2018 23:24:05 +0000 (16:24 -0700)]
Fail for SWIG 3.0.8 (#2656)
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
Andres Noetzli [Mon, 22 Oct 2018 23:07:26 +0000 (16:07 -0700)]
CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/
7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
Andres Noetzli [Mon, 22 Oct 2018 22:16:00 +0000 (15:16 -0700)]
Only build CryptoMiniSat library, no binary (#2657)
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
Andres Noetzli [Mon, 22 Oct 2018 16:12:47 +0000 (09:12 -0700)]
Recover from wrong use of get-info :reason-unknown (#2667)
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
Mathias Preiner [Sat, 20 Oct 2018 21:53:19 +0000 (14:53 -0700)]
Remove antlr_undefines.h. (#2664)
Is not required anymore since we don't use autotools anymore.
Andres Noetzli [Sat, 20 Oct 2018 14:20:12 +0000 (07:20 -0700)]
Add substr, contains and equality rewrites (#2665)
Andres Noetzli [Sat, 20 Oct 2018 14:02:16 +0000 (07:02 -0700)]
Disable dumping test for non-dumping builds (#2662)
Andres Noetzli [Sat, 20 Oct 2018 13:47:30 +0000 (06:47 -0700)]
Travis: run examples and avoid building them twice (#2663)
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
Aina Niemetz [Wed, 17 Oct 2018 21:26:32 +0000 (14:26 -0700)]
BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
Aina Niemetz [Wed, 17 Oct 2018 16:22:44 +0000 (09:22 -0700)]
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)
Andrew Reynolds [Sat, 20 Oct 2018 01:59:51 +0000 (20:59 -0500)]
Sygus streaming non-implied predicates (#2660)
Mathias Preiner [Fri, 19 Oct 2018 21:45:42 +0000 (14:45 -0700)]
Remove autotools build system. (#2639)
Andres Noetzli [Fri, 19 Oct 2018 17:15:33 +0000 (10:15 -0700)]
Fix util::Random for macOS builds (#2655)
Andres Noetzli [Fri, 19 Oct 2018 15:14:22 +0000 (08:14 -0700)]
Add helper to detect length one string terms (#2654)
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
Andres Noetzli [Fri, 19 Oct 2018 04:05:48 +0000 (21:05 -0700)]
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
Mathias Preiner [Fri, 19 Oct 2018 02:22:22 +0000 (19:22 -0700)]
cmake: Run regression level 2 for make check. (#2645)
Andrew Reynolds [Fri, 19 Oct 2018 00:37:11 +0000 (19:37 -0500)]
Non-implied mode for model cores (#2653)
Andrew Reynolds [Thu, 18 Oct 2018 17:51:42 +0000 (12:51 -0500)]
Non-contributing find replace rewrite (#2652)
Andrew Reynolds [Thu, 18 Oct 2018 16:58:51 +0000 (11:58 -0500)]
Improve reduction for str.to.int (#2636)
Haniel Barbosa [Thu, 18 Oct 2018 15:07:18 +0000 (10:07 -0500)]
Introducing internal commands for SyGuS commands (#2627)
Andrew Reynolds [Thu, 18 Oct 2018 12:37:43 +0000 (07:37 -0500)]
Constant length regular expression elimination (#2646)
Andres Noetzli [Thu, 18 Oct 2018 05:24:02 +0000 (22:24 -0700)]
Skip sygus-rr-synth-check regressions when ASAN on (#2651)
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
Andres Noetzli [Thu, 18 Oct 2018 04:21:00 +0000 (21:21 -0700)]
Show if ASAN build in --show-config (#2650)
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
Andrew Reynolds [Thu, 18 Oct 2018 03:09:45 +0000 (22:09 -0500)]
Sygus query generator (#2465)
Andrew Reynolds [Wed, 17 Oct 2018 16:14:49 +0000 (11:14 -0500)]
Fix context-dependent for positive contains reduction (#2644)
Aina Niemetz [Wed, 17 Oct 2018 00:48:58 +0000 (17:48 -0700)]
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
Mathias Preiner [Tue, 16 Oct 2018 19:24:12 +0000 (12:24 -0700)]
cmake: Add CxxTest include directory to unit test includes. (#2642)
Aina Niemetz [Tue, 16 Oct 2018 01:12:00 +0000 (18:12 -0700)]
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).
Aina Niemetz [Tue, 16 Oct 2018 00:10:47 +0000 (17:10 -0700)]
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
Aina Niemetz [Fri, 12 Oct 2018 21:21:35 +0000 (14:21 -0700)]
BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Aina Niemetz [Mon, 8 Oct 2018 17:35:21 +0000 (10:35 -0700)]
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
Andrew Reynolds [Tue, 16 Oct 2018 17:25:20 +0000 (12:25 -0500)]
Improve strings reductions including skolem caching for contains (#2641)
Andrew Reynolds [Tue, 16 Oct 2018 17:03:34 +0000 (12:03 -0500)]
Improve reduction for int.to.str (#2629)
Haniel Barbosa [Tue, 16 Oct 2018 07:39:03 +0000 (02:39 -0500)]
Option for shuffling condition pool in CegisUnif (#2587)
Mathias Preiner [Mon, 15 Oct 2018 23:46:17 +0000 (16:46 -0700)]
cmake: Generate git_versioninfo.cpp on build time. (#2640)
Andrew Reynolds [Mon, 15 Oct 2018 16:42:28 +0000 (11:42 -0500)]
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Andres Noetzli [Mon, 15 Oct 2018 15:39:02 +0000 (08:39 -0700)]
Add more (str.replace x y z) rewrites (#2628)
Andres Noetzli [Sun, 14 Oct 2018 01:48:36 +0000 (18:48 -0700)]
Fix fp-bool.sy grammar and require symfpu (#2631)
Andres Noetzli [Sat, 13 Oct 2018 02:35:01 +0000 (19:35 -0700)]
Reset input language for ExprMiner subsolver (#2624)
Andrew Reynolds [Fri, 12 Oct 2018 20:44:22 +0000 (15:44 -0500)]
Improvements to rewrite rules from inputs (#2625)
Andres Noetzli [Fri, 12 Oct 2018 07:21:51 +0000 (00:21 -0700)]
Add rewrites for str.replace in str.contains (#2623)
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
Andrew Reynolds [Fri, 12 Oct 2018 02:20:35 +0000 (21:20 -0500)]
Fix heuristic for string length approximation (#2622)
Andrew Reynolds [Fri, 12 Oct 2018 01:34:16 +0000 (20:34 -0500)]
Refactor printing of parameterized operators in smt2 (#2609)
Andres Noetzli [Thu, 11 Oct 2018 22:00:26 +0000 (15:00 -0700)]
Improve reasoning about empty strings in rewriter (#2615)
Andrew Reynolds [Thu, 11 Oct 2018 16:19:52 +0000 (11:19 -0500)]
Fix partial operator elimination in sygus grammar normalization (#2620)
Andrew Reynolds [Thu, 11 Oct 2018 05:31:57 +0000 (00:31 -0500)]
Fix string ext inference for rewrites that introduce negation (#2618)
Haniel Barbosa [Thu, 11 Oct 2018 04:30:58 +0000 (23:30 -0500)]
Fix default setting of CegisUnif options (#2605)
Mathias Preiner [Thu, 11 Oct 2018 03:48:44 +0000 (20:48 -0700)]
cmake: Use gcovr instead lcov for coverage report generation. (#2617)
Andres Noetzli [Thu, 11 Oct 2018 03:07:34 +0000 (20:07 -0700)]
Fix compiler warnings (#2602)
Andrew Reynolds [Thu, 11 Oct 2018 01:44:02 +0000 (20:44 -0500)]
Synthesize rewrite rules from inputs (#2608)
Andrew Reynolds [Wed, 10 Oct 2018 21:56:27 +0000 (16:56 -0500)]
Fix cegis so that evaluation unfolding is not interleaved. (#2614)
Andrew Reynolds [Wed, 10 Oct 2018 20:29:36 +0000 (15:29 -0500)]
Optimize regular expression elimination (#2612)
Andres Noetzli [Wed, 10 Oct 2018 19:30:06 +0000 (12:30 -0700)]
Add length-based rewrites for (str.substr _ _ _) (#2610)
Andrew Reynolds [Tue, 9 Oct 2018 21:54:58 +0000 (16:54 -0500)]
Support for basic actively-generated enumerators (#2606)
Aina Niemetz [Tue, 9 Oct 2018 17:36:40 +0000 (10:36 -0700)]
Random: support URNG interface (#2595)
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
Andrew Reynolds [Tue, 9 Oct 2018 16:51:06 +0000 (11:51 -0500)]
Allow multiple synthesis conjectures. (#2593)
Aina Niemetz [Tue, 9 Oct 2018 03:16:57 +0000 (20:16 -0700)]
Fix compiler warnings. (#2601)
Aina Niemetz [Tue, 9 Oct 2018 02:44:22 +0000 (19:44 -0700)]
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
Aina Niemetz [Tue, 9 Oct 2018 01:51:33 +0000 (18:51 -0700)]
BV inverter: Factor out util functions. (#2603)
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
Andrew Reynolds [Tue, 9 Oct 2018 01:03:39 +0000 (20:03 -0500)]
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Aina Niemetz [Tue, 9 Oct 2018 00:34:35 +0000 (17:34 -0700)]
Cmake: Fix ctest call for example/translator. (#2600)
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
Andrew Reynolds [Mon, 8 Oct 2018 23:28:30 +0000 (18:28 -0500)]
Address slow sygus regressions (#2598)