cvc5.git
6 years agocmake: Add library versioning for libcvc4.so.
Mathias Preiner [Thu, 6 Sep 2018 16:18:07 +0000 (09:18 -0700)]
cmake: Add library versioning for libcvc4.so.

6 years agocmake: Rebase with current master, add new tests/source files.
Mathias Preiner [Wed, 5 Sep 2018 21:00:52 +0000 (14:00 -0700)]
cmake: Rebase with current master, add new tests/source files.

6 years agocmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.
Mathias Preiner [Tue, 4 Sep 2018 18:40:46 +0000 (11:40 -0700)]
cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.

6 years agocmake: Use target specific includes for libcvc4.
Mathias Preiner [Fri, 31 Aug 2018 16:11:23 +0000 (09:11 -0700)]
cmake: Use target specific includes for libcvc4.

Further, print definitions added with add_definitions(...).

6 years agocmake: Add missing dependency.
Mathias Preiner [Fri, 31 Aug 2018 16:10:50 +0000 (09:10 -0700)]
cmake: Add missing dependency.

6 years agocmake: Add support for building static binaries/libraries.
Mathias Preiner [Wed, 29 Aug 2018 17:26:10 +0000 (10:26 -0700)]
cmake: Add support for building static binaries/libraries.

6 years agocmake: Add options for specifying install directories for dependencies.
Mathias Preiner [Wed, 29 Aug 2018 15:20:31 +0000 (08:20 -0700)]
cmake: Add options for specifying install directories for dependencies.

6 years agocmake: Add module finder for GLPK-cut-log.
Mathias Preiner [Sat, 25 Aug 2018 06:14:32 +0000 (23:14 -0700)]
cmake: Add module finder for GLPK-cut-log.

6 years agocmake: Add module finder for ABC.
Mathias Preiner [Sat, 25 Aug 2018 02:27:37 +0000 (19:27 -0700)]
cmake: Add module finder for ABC.

6 years agocmake: Compile Java tests and add to ctest if Java bindings are enabled.
Mathias Preiner [Fri, 24 Aug 2018 22:11:03 +0000 (15:11 -0700)]
cmake: Compile Java tests and add to ctest if Java bindings are enabled.

6 years agocmake: Add SWIG support + Python and Java bindings.
Mathias Preiner [Fri, 24 Aug 2018 19:52:49 +0000 (12:52 -0700)]
cmake: Add SWIG support + Python and Java bindings.

6 years agocmake: Add dependencies for test targets and support for make coverage.
Aina Niemetz [Wed, 22 Aug 2018 15:46:50 +0000 (08:46 -0700)]
cmake: Add dependencies for test targets and support for make coverage.

6 years agocmake: Various portfolio/default option fixes.
Mathias Preiner [Tue, 21 Aug 2018 02:39:32 +0000 (19:39 -0700)]
cmake: Various portfolio/default option fixes.

6 years agocmake: Enable parallel execution for test targets regress, units, systemtests.
Aina Niemetz [Tue, 21 Aug 2018 01:40:27 +0000 (18:40 -0700)]
cmake: Enable parallel execution for test targets regress, units, systemtests.

6 years agocmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.
Aina Niemetz [Tue, 21 Aug 2018 01:39:10 +0000 (18:39 -0700)]
cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.

6 years agocmake: Added system tests and target make systemtests.
Aina Niemetz [Tue, 21 Aug 2018 00:26:56 +0000 (17:26 -0700)]
cmake: Added system tests and target make systemtests.

6 years agocmake: Added regression tests and target make regress.
Aina Niemetz [Sat, 18 Aug 2018 01:25:27 +0000 (18:25 -0700)]
cmake: Added regression tests and target make regress.

6 years agocmake: Add portfolio support.
Mathias Preiner [Sat, 18 Aug 2018 01:11:26 +0000 (18:11 -0700)]
cmake: Add portfolio support.

6 years agocmake: Add ASAN support.
Mathias Preiner [Fri, 17 Aug 2018 23:59:09 +0000 (16:59 -0700)]
cmake: Add ASAN support.

6 years agocmake: Enable shared by default.
Mathias Preiner [Fri, 17 Aug 2018 23:58:27 +0000 (16:58 -0700)]
cmake: Enable shared by default.

Further, force shared builds in case of unit tests.

6 years agocmake: Disable W-suggest-override for unit tests.
Mathias Preiner [Fri, 17 Aug 2018 23:57:20 +0000 (16:57 -0700)]
cmake: Disable W-suggest-override for unit tests.

6 years agocmake: Add target units.
Aina Niemetz [Fri, 17 Aug 2018 18:37:27 +0000 (11:37 -0700)]
cmake: Add target units.

6 years agocmake: Removed obsolete CMakeLists file in test.
Aina Niemetz [Fri, 17 Aug 2018 18:12:57 +0000 (11:12 -0700)]
cmake: Removed obsolete CMakeLists file in test.

6 years agocmake: Add support for CxxTest.
Aina Niemetz [Fri, 17 Aug 2018 01:56:03 +0000 (18:56 -0700)]
cmake: Add support for CxxTest.

6 years agocmake: Filter through and disable unused HAVE_* variables from autotools.
Aina Niemetz [Thu, 16 Aug 2018 22:55:25 +0000 (15:55 -0700)]
cmake: Filter through and disable unused HAVE_* variables from autotools.

6 years agocmake: Do not set global output directories for binaries and libraries.
Mathias Preiner [Fri, 17 Aug 2018 01:07:59 +0000 (18:07 -0700)]
cmake: Do not set global output directories for binaries and libraries.

6 years agocmake: Fix some includes.
Mathias Preiner [Fri, 17 Aug 2018 00:57:55 +0000 (17:57 -0700)]
cmake: Fix some includes.

6 years agocmake: Added support for coverage and profiling.
Aina Niemetz [Wed, 15 Aug 2018 23:47:00 +0000 (16:47 -0700)]
cmake: Added support for coverage and profiling.

6 years agocmake: Added 3-valued option handling (to enable detection of user-set options).
Aina Niemetz [Wed, 15 Aug 2018 21:00:33 +0000 (14:00 -0700)]
cmake: Added 3-valued option handling (to enable detection of user-set options).

6 years agocmake: Add module finder for readline.
Mathias Preiner [Wed, 15 Aug 2018 19:53:43 +0000 (12:53 -0700)]
cmake: Add module finder for readline.

6 years agocmake: Generate token headers.
Mathias Preiner [Wed, 15 Aug 2018 00:43:17 +0000 (17:43 -0700)]
cmake: Generate token headers.

6 years agocmake: Added licensing options and warnings/errors.
Aina Niemetz [Wed, 15 Aug 2018 01:18:04 +0000 (18:18 -0700)]
cmake: Added licensing options and warnings/errors.

6 years agocmake: Cleanup CMakeLists.txt files, remove SHARED.
Mathias Preiner [Wed, 15 Aug 2018 00:32:26 +0000 (17:32 -0700)]
cmake: Cleanup CMakeLists.txt files, remove SHARED.

6 years agocmake: Add build configurations.
Aina Niemetz [Tue, 14 Aug 2018 20:22:15 +0000 (13:22 -0700)]
cmake: Add build configurations.

6 years agocmake: Fixed compiler flag macros.
Aina Niemetz [Mon, 13 Aug 2018 22:22:07 +0000 (15:22 -0700)]
cmake: Fixed compiler flag macros.

6 years agocmake: Add module finder for LFSC.
Mathias Preiner [Tue, 14 Aug 2018 00:49:47 +0000 (17:49 -0700)]
cmake: Add module finder for LFSC.

6 years agocmake: Add module finder for CaDiCaL.
Mathias Preiner [Tue, 14 Aug 2018 00:37:24 +0000 (17:37 -0700)]
cmake: Add module finder for CaDiCaL.

6 years agocmake: Add module finder for CryptoMiniSat.
Mathias Preiner [Tue, 14 Aug 2018 00:21:13 +0000 (17:21 -0700)]
cmake: Add module finder for CryptoMiniSat.

6 years agocmake: Add module finder for SymFPU.
Mathias Preiner [Mon, 13 Aug 2018 22:24:46 +0000 (15:24 -0700)]
cmake: Add module finder for SymFPU.

6 years agocmake: Add module finder for CLN.
Mathias Preiner [Mon, 13 Aug 2018 21:03:54 +0000 (14:03 -0700)]
cmake: Add module finder for CLN.

6 years agocmake: Add libsignatures for proofs.
Mathias Preiner [Mon, 13 Aug 2018 16:06:33 +0000 (09:06 -0700)]
cmake: Add libsignatures for proofs.

6 years agocmake: Remove unused CMakeLists.txt
Mathias Preiner [Mon, 13 Aug 2018 16:06:11 +0000 (09:06 -0700)]
cmake: Remove unused CMakeLists.txt

6 years agocmake: Generate cvc4autoconfig.h (options currently statically set).
Aina Niemetz [Mon, 13 Aug 2018 17:52:00 +0000 (10:52 -0700)]
cmake: Generate cvc4autoconfig.h (options currently statically set).

6 years agocmake: Added missing dependency for src/util
Aina Niemetz [Mon, 13 Aug 2018 17:50:24 +0000 (10:50 -0700)]
cmake: Added missing dependency for src/util

6 years agocmake: Working build infrastructure.
Mathias Preiner [Fri, 10 Aug 2018 23:19:43 +0000 (16:19 -0700)]
cmake: Working build infrastructure.

TODO: cvc4autoconfig.h

6 years agocmake: Antlr parser generation done.
Mathias Preiner [Fri, 10 Aug 2018 23:10:23 +0000 (16:10 -0700)]
cmake: Antlr parser generation done.

6 years agocmake: Generate trace and debug tags
Aina Niemetz [Sat, 11 Aug 2018 00:57:15 +0000 (17:57 -0700)]
cmake: Generate trace and debug tags

6 years agocmake: .cpp generation done, .h generation not yet complete
Aina Niemetz [Sat, 16 Jun 2018 02:33:04 +0000 (19:33 -0700)]
cmake: .cpp generation done, .h generation not yet complete

6 years agocmake: Added initial build infrastructure.
Aina Niemetz [Mon, 11 Sep 2017 22:49:22 +0000 (15:49 -0700)]
cmake: Added initial build infrastructure.

6 years agoDecision strategy: incorporate arrays. (#2495)
Andrew Reynolds [Wed, 19 Sep 2018 16:17:27 +0000 (11:17 -0500)]
Decision strategy: incorporate arrays. (#2495)

6 years agoAdd rewrites for str.contains + str.replace/substr (#2496)
Andres Noetzli [Wed, 19 Sep 2018 15:16:46 +0000 (08:16 -0700)]
Add rewrites for str.contains + str.replace/substr (#2496)

6 years agoDecision strategy: incorporate separation logic. (#2494)
Andrew Reynolds [Wed, 19 Sep 2018 02:26:28 +0000 (21:26 -0500)]
Decision strategy: incorporate separation logic. (#2494)

6 years agoAdd two rewrites for string contains character (#2492)
Andrew Reynolds [Wed, 19 Sep 2018 01:54:13 +0000 (20:54 -0500)]
Add two rewrites for string contains character (#2492)

6 years ago Refactor strings extended functions inferences (#2480)
Andrew Reynolds [Wed, 19 Sep 2018 01:10:59 +0000 (20:10 -0500)]
 Refactor strings extended functions inferences (#2480)

This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.

This is in preparation for working on solving equations and further inferences in this style.

6 years agoNew C++ API: Introduce new macro and exception for API checks. (#2486)
Aina Niemetz [Wed, 19 Sep 2018 00:22:30 +0000 (17:22 -0700)]
New C++ API: Introduce new macro and exception for API checks. (#2486)

6 years agoFix issue with str.idof in evaluator (#2493)
Andres Noetzli [Tue, 18 Sep 2018 23:01:13 +0000 (16:01 -0700)]
Fix issue with str.idof in evaluator (#2493)

6 years agoDecision strategy: incorporate strings fmf. (#2485)
Andrew Reynolds [Tue, 18 Sep 2018 21:56:24 +0000 (16:56 -0500)]
Decision strategy: incorporate strings fmf. (#2485)

6 years agoMore aggressive caching of string skolems. (#2491)
Andrew Reynolds [Tue, 18 Sep 2018 20:38:44 +0000 (15:38 -0500)]
More aggressive caching of string skolems. (#2491)

6 years agoMove and rename sygus solver classes (#2488)
Andrew Reynolds [Tue, 18 Sep 2018 15:26:36 +0000 (10:26 -0500)]
Move and rename sygus solver classes (#2488)

6 years agofix assertion error (#2487)
Haniel Barbosa [Tue, 18 Sep 2018 13:07:21 +0000 (08:07 -0500)]
fix assertion error (#2487)

6 years agoClean remaining references to getNextDecisionRequest in quantifiers. (#2484)
Andrew Reynolds [Tue, 18 Sep 2018 01:36:36 +0000 (20:36 -0500)]
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)

6 years agoImprovements and fixes for symmetry detection and breaking (#2459)
Andrew Reynolds [Tue, 18 Sep 2018 00:51:06 +0000 (19:51 -0500)]
Improvements and fixes for symmetry detection and breaking (#2459)

This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.

6 years agoMove inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Andrew Reynolds [Mon, 17 Sep 2018 23:49:08 +0000 (18:49 -0500)]
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)

6 years agoDecision strategy: incorporate cegis unif (#2482)
Andrew Reynolds [Mon, 17 Sep 2018 22:32:02 +0000 (17:32 -0500)]
Decision strategy: incorporate cegis unif (#2482)

6 years ago Decision strategy: incorporate bounded integers (#2481)
Andrew Reynolds [Mon, 17 Sep 2018 21:50:19 +0000 (16:50 -0500)]
 Decision strategy: incorporate bounded integers (#2481)

6 years agoDecision strategy: incorporate datatypes sygus solver. (#2479)
Andrew Reynolds [Mon, 17 Sep 2018 21:26:00 +0000 (16:26 -0500)]
Decision strategy: incorporate datatypes sygus solver. (#2479)

6 years agoMore aggressive skolem caching for strings, document and clean preprocessor (#2478)
Andrew Reynolds [Mon, 17 Sep 2018 20:40:28 +0000 (15:40 -0500)]
More aggressive skolem caching for strings, document and clean preprocessor (#2478)

6 years agoMake strings model construction robust to lengths that are not propagated equal ...
Andrew Reynolds [Mon, 17 Sep 2018 19:38:07 +0000 (14:38 -0500)]
Make strings model construction robust to lengths that are not propagated equal (#2444)

This fixes #2429.

This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value.  See explanation in comment.

We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms.  I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.

Regardless, the strings model construction should be robust to handle this case, which this PR does.

6 years agoFollow redirects with cURL in contrib/get* scripts (#2471)
Andres Noetzli [Mon, 17 Sep 2018 19:16:07 +0000 (12:16 -0700)]
Follow redirects with cURL in contrib/get* scripts (#2471)

On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.

6 years agoRemove broken dumping support from portfolio build (#2470)
Andres Noetzli [Mon, 17 Sep 2018 17:57:19 +0000 (10:57 -0700)]
Remove broken dumping support from portfolio build (#2470)

Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:

- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.

This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously.  Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).

[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117

6 years agoRemove unnecessary tracing from preprocessing (#2472)
Andres Noetzli [Mon, 17 Sep 2018 17:16:59 +0000 (10:16 -0700)]
Remove unnecessary tracing from preprocessing (#2472)

With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.

6 years agoDecision strategy: incorporate UF with cardinality constraints (#2476)
Andrew Reynolds [Mon, 17 Sep 2018 16:40:16 +0000 (11:40 -0500)]
Decision strategy: incorporate UF with cardinality constraints (#2476)

6 years agoDecision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
Andrew Reynolds [Mon, 17 Sep 2018 14:27:03 +0000 (09:27 -0500)]
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)

6 years agoRefactor how assertions are added to decision engine (#2396)
Andres Noetzli [Sat, 15 Sep 2018 05:15:37 +0000 (22:15 -0700)]
Refactor how assertions are added to decision engine (#2396)

Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.

6 years agoAdd Skolem cache for strings, refactor length registration (#2457)
Andrew Reynolds [Fri, 14 Sep 2018 19:57:35 +0000 (14:57 -0500)]
Add Skolem cache for strings, refactor length registration (#2457)

This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).

It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.

6 years agoGeneralize CandidateRewriteDatabase to ExprMiner (#2340)
Andrew Reynolds [Fri, 14 Sep 2018 02:48:25 +0000 (21:48 -0500)]
Generalize CandidateRewriteDatabase to ExprMiner (#2340)

6 years agoFix #include for minisat headers in bvminisat. (#2463)
Mathias Preiner [Thu, 13 Sep 2018 22:17:39 +0000 (15:17 -0700)]
Fix #include for minisat headers in bvminisat. (#2463)

6 years agoUses information gain heuristic for building better solutions from DTs (#2451)
Haniel Barbosa [Thu, 13 Sep 2018 20:06:50 +0000 (15:06 -0500)]
Uses information gain heuristic for building better solutions from DTs (#2451)

6 years agoSimplify storing of transcendental function applications that occur in assertions...
Andrew Reynolds [Thu, 13 Sep 2018 17:18:12 +0000 (12:18 -0500)]
Simplify storing of transcendental function applications that occur in assertions (#2458)

6 years ago Decision strategy: incorporate CEGQI (#2460)
Andrew Reynolds [Thu, 13 Sep 2018 13:01:30 +0000 (08:01 -0500)]
 Decision strategy: incorporate CEGQI (#2460)

6 years agoNew C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Aina Niemetz [Wed, 12 Sep 2018 23:41:18 +0000 (16:41 -0700)]
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)

6 years agoExamples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Aina Niemetz [Wed, 12 Sep 2018 22:50:44 +0000 (15:50 -0700)]
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)

6 years ago Initial infrastructure for theory decision manager (#2447)
Andrew Reynolds [Wed, 12 Sep 2018 18:18:13 +0000 (13:18 -0500)]
 Initial infrastructure for theory decision manager (#2447)

6 years agoFix for when strings process loop is disabled. (#2456)
Andrew Reynolds [Wed, 12 Sep 2018 02:15:28 +0000 (21:15 -0500)]
Fix for when strings process loop is disabled. (#2456)

6 years agoFixe compiler warning in line_buffer.cpp. (#2453)
Aina Niemetz [Tue, 11 Sep 2018 23:26:16 +0000 (16:26 -0700)]
Fixe compiler warning in line_buffer.cpp. (#2453)

6 years agoSupport model cores via option --produce-model-cores. (#2407)
Andrew Reynolds [Tue, 11 Sep 2018 18:08:00 +0000 (13:08 -0500)]
Support model cores via option --produce-model-cores. (#2407)

This adds support for model cores, fixes #1233.

It includes some minor cleanup and additions to utility functions.

6 years agoAvoid calling size() every iteration (#2450)
yoni206 [Tue, 11 Sep 2018 16:30:35 +0000 (09:30 -0700)]
Avoid calling size() every iteration (#2450)

6 years agoFix global negate (#2449)
Andrew Reynolds [Tue, 11 Sep 2018 04:31:29 +0000 (23:31 -0500)]
Fix global negate (#2449)

6 years agofix (#2446)
Haniel Barbosa [Tue, 11 Sep 2018 03:20:42 +0000 (22:20 -0500)]
fix (#2446)

6 years agoSet NodeManager to nullptr when exporting vars (#2445)
Andres Noetzli [Tue, 11 Sep 2018 02:27:05 +0000 (19:27 -0700)]
Set NodeManager to nullptr when  exporting vars (#2445)

PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.

6 years agoUsing a single condition enumerator in sygus-unif (#2440)
Haniel Barbosa [Tue, 11 Sep 2018 01:51:03 +0000 (20:51 -0500)]
Using a single condition enumerator in sygus-unif (#2440)

This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).

In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:

- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.

A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.

There is also small improvements for trace messages.

6 years agoRefactor non-clausal simplify preprocessing pass. (#2425)
Aina Niemetz [Tue, 11 Sep 2018 00:16:28 +0000 (17:16 -0700)]
Refactor non-clausal simplify preprocessing pass. (#2425)

6 years agoSquash implementation of counterexample-guided instantiation (#2423)
Andrew Reynolds [Mon, 10 Sep 2018 20:52:05 +0000 (15:52 -0500)]
Squash implementation of counterexample-guided instantiation (#2423)

6 years agoAdd (str.replace (str.replace y w y) y z) rewrite (#2441)
Andres Noetzli [Mon, 10 Sep 2018 13:54:11 +0000 (06:54 -0700)]
Add (str.replace (str.replace y w y) y z) rewrite (#2441)

6 years agoReplace boost::integer_traits with std::numeric_limits. (#2439)
Mathias Preiner [Fri, 7 Sep 2018 19:31:20 +0000 (12:31 -0700)]
Replace boost::integer_traits with std::numeric_limits. (#2439)

Further, remove redundant gmp.h include in options_handler.cpp.

6 years agoRemove clock_gettime() replacement for macOS. (#2436)
Mathias Preiner [Fri, 7 Sep 2018 17:20:06 +0000 (10:20 -0700)]
Remove clock_gettime() replacement for macOS. (#2436)

Not needed anymore since macOS 10.12 introduced clock_gettime().

6 years ago Make isClosedEnumerable a member of TypeNode (#2434)
Andrew Reynolds [Fri, 7 Sep 2018 15:42:41 +0000 (10:42 -0500)]
 Make isClosedEnumerable a member of TypeNode (#2434)

6 years ago Further simplify and fix initialization of ce guided instantiation (#2437)
Andrew Reynolds [Thu, 6 Sep 2018 20:48:58 +0000 (15:48 -0500)]
 Further simplify and fix initialization of ce guided instantiation (#2437)

6 years agoRefactor and document quantifiers variable elimination and conditional splitting...
Andrew Reynolds [Thu, 6 Sep 2018 16:33:33 +0000 (11:33 -0500)]
Refactor and document quantifiers variable elimination and conditional splitting (#2424)

6 years agoMinor improvements to interface for rep set. (#2435)
Andrew Reynolds [Thu, 6 Sep 2018 13:14:08 +0000 (08:14 -0500)]
Minor improvements to interface for rep set. (#2435)