Aina Niemetz [Wed, 15 Aug 2018 23:47:00 +0000 (16:47 -0700)]
cmake: Added support for coverage and profiling.
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).
Mathias Preiner [Wed, 15 Aug 2018 19:53:43 +0000 (12:53 -0700)]
cmake: Add module finder for readline.
Mathias Preiner [Wed, 15 Aug 2018 00:43:17 +0000 (17:43 -0700)]
cmake: Generate token headers.
Aina Niemetz [Wed, 15 Aug 2018 01:18:04 +0000 (18:18 -0700)]
cmake: Added licensing options and warnings/errors.
Mathias Preiner [Wed, 15 Aug 2018 00:32:26 +0000 (17:32 -0700)]
cmake: Cleanup CMakeLists.txt files, remove SHARED.
Aina Niemetz [Tue, 14 Aug 2018 20:22:15 +0000 (13:22 -0700)]
cmake: Add build configurations.
Aina Niemetz [Mon, 13 Aug 2018 22:22:07 +0000 (15:22 -0700)]
cmake: Fixed compiler flag macros.
Mathias Preiner [Tue, 14 Aug 2018 00:49:47 +0000 (17:49 -0700)]
cmake: Add module finder for LFSC.
Mathias Preiner [Tue, 14 Aug 2018 00:37:24 +0000 (17:37 -0700)]
cmake: Add module finder for CaDiCaL.
Mathias Preiner [Tue, 14 Aug 2018 00:21:13 +0000 (17:21 -0700)]
cmake: Add module finder for CryptoMiniSat.
Mathias Preiner [Mon, 13 Aug 2018 22:24:46 +0000 (15:24 -0700)]
cmake: Add module finder for SymFPU.
Mathias Preiner [Mon, 13 Aug 2018 21:03:54 +0000 (14:03 -0700)]
cmake: Add module finder for CLN.
Mathias Preiner [Mon, 13 Aug 2018 16:06:33 +0000 (09:06 -0700)]
cmake: Add libsignatures for proofs.
Mathias Preiner [Mon, 13 Aug 2018 16:06:11 +0000 (09:06 -0700)]
cmake: Remove unused CMakeLists.txt
Aina Niemetz [Mon, 13 Aug 2018 17:52:00 +0000 (10:52 -0700)]
cmake: Generate cvc4autoconfig.h (options currently statically set).
Aina Niemetz [Mon, 13 Aug 2018 17:50:24 +0000 (10:50 -0700)]
cmake: Added missing dependency for src/util
Mathias Preiner [Fri, 10 Aug 2018 23:19:43 +0000 (16:19 -0700)]
cmake: Working build infrastructure.
TODO: cvc4autoconfig.h
Mathias Preiner [Fri, 10 Aug 2018 23:10:23 +0000 (16:10 -0700)]
cmake: Antlr parser generation done.
Aina Niemetz [Sat, 11 Aug 2018 00:57:15 +0000 (17:57 -0700)]
cmake: Generate trace and debug tags
Aina Niemetz [Sat, 16 Jun 2018 02:33:04 +0000 (19:33 -0700)]
cmake: .cpp generation done, .h generation not yet complete
Aina Niemetz [Mon, 11 Sep 2017 22:49:22 +0000 (15:49 -0700)]
cmake: Added initial build infrastructure.
Andrew Reynolds [Wed, 19 Sep 2018 16:17:27 +0000 (11:17 -0500)]
Decision strategy: incorporate arrays. (#2495)
Andres Noetzli [Wed, 19 Sep 2018 15:16:46 +0000 (08:16 -0700)]
Add rewrites for str.contains + str.replace/substr (#2496)
Andrew Reynolds [Wed, 19 Sep 2018 02:26:28 +0000 (21:26 -0500)]
Decision strategy: incorporate separation logic. (#2494)
Andrew Reynolds [Wed, 19 Sep 2018 01:54:13 +0000 (20:54 -0500)]
Add two rewrites for string contains character (#2492)
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.
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)
Andres Noetzli [Tue, 18 Sep 2018 23:01:13 +0000 (16:01 -0700)]
Fix issue with str.idof in evaluator (#2493)
Andrew Reynolds [Tue, 18 Sep 2018 21:56:24 +0000 (16:56 -0500)]
Decision strategy: incorporate strings fmf. (#2485)
Andrew Reynolds [Tue, 18 Sep 2018 20:38:44 +0000 (15:38 -0500)]
More aggressive caching of string skolems. (#2491)
Andrew Reynolds [Tue, 18 Sep 2018 15:26:36 +0000 (10:26 -0500)]
Move and rename sygus solver classes (#2488)
Haniel Barbosa [Tue, 18 Sep 2018 13:07:21 +0000 (08:07 -0500)]
fix assertion error (#2487)
Andrew Reynolds [Tue, 18 Sep 2018 01:36:36 +0000 (20:36 -0500)]
Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)
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.
Andrew Reynolds [Mon, 17 Sep 2018 23:49:08 +0000 (18:49 -0500)]
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
Andrew Reynolds [Mon, 17 Sep 2018 22:32:02 +0000 (17:32 -0500)]
Decision strategy: incorporate cegis unif (#2482)
Andrew Reynolds [Mon, 17 Sep 2018 21:50:19 +0000 (16:50 -0500)]
Decision strategy: incorporate bounded integers (#2481)
Andrew Reynolds [Mon, 17 Sep 2018 21:26:00 +0000 (16:26 -0500)]
Decision strategy: incorporate datatypes sygus solver. (#2479)
Andrew Reynolds [Mon, 17 Sep 2018 20:40:28 +0000 (15:40 -0500)]
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
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.
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.
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
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.
Andrew Reynolds [Mon, 17 Sep 2018 16:40:16 +0000 (11:40 -0500)]
Decision strategy: incorporate UF with cardinality constraints (#2476)
Andrew Reynolds [Mon, 17 Sep 2018 14:27:03 +0000 (09:27 -0500)]
Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)
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.
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.
Andrew Reynolds [Fri, 14 Sep 2018 02:48:25 +0000 (21:48 -0500)]
Generalize CandidateRewriteDatabase to ExprMiner (#2340)
Mathias Preiner [Thu, 13 Sep 2018 22:17:39 +0000 (15:17 -0700)]
Fix #include for minisat headers in bvminisat. (#2463)
Haniel Barbosa [Thu, 13 Sep 2018 20:06:50 +0000 (15:06 -0500)]
Uses information gain heuristic for building better solutions from DTs (#2451)
Andrew Reynolds [Thu, 13 Sep 2018 17:18:12 +0000 (12:18 -0500)]
Simplify storing of transcendental function applications that occur in assertions (#2458)
Andrew Reynolds [Thu, 13 Sep 2018 13:01:30 +0000 (08:01 -0500)]
Decision strategy: incorporate CEGQI (#2460)
Aina Niemetz [Wed, 12 Sep 2018 23:41:18 +0000 (16:41 -0700)]
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Aina Niemetz [Wed, 12 Sep 2018 22:50:44 +0000 (15:50 -0700)]
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)
Andrew Reynolds [Wed, 12 Sep 2018 18:18:13 +0000 (13:18 -0500)]
Initial infrastructure for theory decision manager (#2447)
Andrew Reynolds [Wed, 12 Sep 2018 02:15:28 +0000 (21:15 -0500)]
Fix for when strings process loop is disabled. (#2456)
Aina Niemetz [Tue, 11 Sep 2018 23:26:16 +0000 (16:26 -0700)]
Fixe compiler warning in line_buffer.cpp. (#2453)
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.
yoni206 [Tue, 11 Sep 2018 16:30:35 +0000 (09:30 -0700)]
Avoid calling size() every iteration (#2450)
Andrew Reynolds [Tue, 11 Sep 2018 04:31:29 +0000 (23:31 -0500)]
Fix global negate (#2449)
Haniel Barbosa [Tue, 11 Sep 2018 03:20:42 +0000 (22:20 -0500)]
fix (#2446)
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.
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.
Aina Niemetz [Tue, 11 Sep 2018 00:16:28 +0000 (17:16 -0700)]
Refactor non-clausal simplify preprocessing pass. (#2425)
Andrew Reynolds [Mon, 10 Sep 2018 20:52:05 +0000 (15:52 -0500)]
Squash implementation of counterexample-guided instantiation (#2423)
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)
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.
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().
Andrew Reynolds [Fri, 7 Sep 2018 15:42:41 +0000 (10:42 -0500)]
Make isClosedEnumerable a member of TypeNode (#2434)
Andrew Reynolds [Thu, 6 Sep 2018 20:48:58 +0000 (15:48 -0500)]
Further simplify and fix initialization of ce guided instantiation (#2437)
Andrew Reynolds [Thu, 6 Sep 2018 16:33:33 +0000 (11:33 -0500)]
Refactor and document quantifiers variable elimination and conditional splitting (#2424)
Andrew Reynolds [Thu, 6 Sep 2018 13:14:08 +0000 (08:14 -0500)]
Minor improvements to interface for rep set. (#2435)
Andrew Reynolds [Wed, 5 Sep 2018 22:36:00 +0000 (17:36 -0500)]
More extended rewrites for strings equality (#2431)
Andrew Reynolds [Wed, 5 Sep 2018 22:03:17 +0000 (17:03 -0500)]
Eliminate select over store in quantifier bodies (#2433)
Mathias Preiner [Wed, 5 Sep 2018 21:31:11 +0000 (14:31 -0700)]
Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
Andrew Reynolds [Wed, 5 Sep 2018 20:40:26 +0000 (15:40 -0500)]
Remove printing support for sygus enumeration types (#2430)
Andrew Reynolds [Wed, 5 Sep 2018 17:41:47 +0000 (12:41 -0500)]
Finer-grained inference of substitutions in incremental mode (#2403)
Andres Noetzli [Wed, 5 Sep 2018 14:49:59 +0000 (07:49 -0700)]
Add regex grammar to rewriter verification tests (#2426)
Andrew Reynolds [Wed, 5 Sep 2018 14:14:14 +0000 (09:14 -0500)]
Extended rewriter for string equalities (#2427)
Mathias Preiner [Wed, 5 Sep 2018 03:40:32 +0000 (20:40 -0700)]
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
Andrew Reynolds [Tue, 4 Sep 2018 23:35:54 +0000 (18:35 -0500)]
Remove redundant strings rewrite. (#2422)
str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since
re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )
This PR removes the above rewrite, which was implemented incorrectly and was dead code.
Andres Noetzli [Tue, 4 Sep 2018 22:34:43 +0000 (15:34 -0700)]
Update INSTALL instructions (#2420)
Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.
Andres Noetzli [Tue, 4 Sep 2018 21:59:19 +0000 (14:59 -0700)]
Remove CVC3 compatibility layer (#2418)
Andres Noetzli [Tue, 4 Sep 2018 21:12:52 +0000 (14:12 -0700)]
Remove unused options file (#2413)
Andrew Reynolds [Tue, 4 Sep 2018 20:18:12 +0000 (15:18 -0500)]
Minor improvements to theory model builder interface. (#2408)
Andrew Reynolds [Tue, 4 Sep 2018 19:34:21 +0000 (14:34 -0500)]
Make quantifiers strategies exit immediately when in conflict (#2099)
Aina Niemetz [Tue, 4 Sep 2018 18:35:50 +0000 (11:35 -0700)]
Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)
Aina Niemetz [Tue, 4 Sep 2018 17:51:41 +0000 (10:51 -0700)]
Fix merge mishap of #2359.
Andrew Reynolds [Tue, 4 Sep 2018 16:43:39 +0000 (11:43 -0500)]
Refactor ceg conjecture initialization (#2411)
Haniel Barbosa [Fri, 31 Aug 2018 23:10:57 +0000 (18:10 -0500)]
Allows SAT checks of repair const to have different options (#2412)
Andrew Reynolds [Fri, 31 Aug 2018 22:22:04 +0000 (17:22 -0500)]
Refactor and document alpha equivalence. (#2402)
Haniel Barbosa [Fri, 31 Aug 2018 20:08:40 +0000 (15:08 -0500)]
Fix export of bound variables (#2409)
Mathias Preiner [Thu, 30 Aug 2018 22:49:45 +0000 (15:49 -0700)]
Refactor theory preprocess into preprocessing pass. (#2395)
Andres Noetzli [Thu, 30 Aug 2018 17:22:47 +0000 (10:22 -0700)]
Use useBland option in FCSimplexDecisionProcedure (#2405)
Andrew Reynolds [Thu, 30 Aug 2018 16:57:58 +0000 (11:57 -0500)]
Add regular expression elimination module (#2400)
Mathias Preiner [Wed, 29 Aug 2018 21:38:33 +0000 (14:38 -0700)]
Refactor MipLibTrick preprocessing pass. (#2359)
Tim King [Wed, 29 Aug 2018 17:27:57 +0000 (10:27 -0700)]
Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
Haniel Barbosa [Wed, 29 Aug 2018 16:06:05 +0000 (11:06 -0500)]
fix bv total ops printing (#2365)
Andrew Reynolds [Tue, 28 Aug 2018 23:32:15 +0000 (18:32 -0500)]
Split term canonize utility to own file and document (#2398)