cvc5.git
6 years agoRemove support for flipDecision (#2319)
Andrew Reynolds [Fri, 17 Aug 2018 20:09:05 +0000 (15:09 -0500)]
Remove support for flipDecision (#2319)

6 years agoRemove miscellaneous unused code (#2333)
Andrew Reynolds [Fri, 17 Aug 2018 19:18:16 +0000 (14:18 -0500)]
Remove miscellaneous unused code (#2333)

6 years ago Add sygus stream regressions (#2330)
Andrew Reynolds [Fri, 17 Aug 2018 18:29:15 +0000 (13:29 -0500)]
 Add sygus stream regressions (#2330)

6 years agoSplit sygus grammar to its own ANTLR grammar (#2307)
Andrew Reynolds [Fri, 17 Aug 2018 17:37:19 +0000 (12:37 -0500)]
Split sygus grammar to its own ANTLR grammar (#2307)

6 years ago Fix spurious warning in sort inference (#2331)
Andrew Reynolds [Fri, 17 Aug 2018 17:08:48 +0000 (12:08 -0500)]
 Fix spurious warning in sort inference (#2331)

6 years ago Fix arithmetic division by zero in sygus repair constant module (#2329)
Andrew Reynolds [Fri, 17 Aug 2018 16:15:08 +0000 (11:15 -0500)]
 Fix arithmetic division by zero in sygus repair constant module (#2329)

6 years ago Eliminate partial operators in sygus grammar normalization (#2323)
Andrew Reynolds [Fri, 17 Aug 2018 07:48:22 +0000 (02:48 -0500)]
 Eliminate partial operators in sygus grammar normalization (#2323)

This corrects a bug that was introduced in #2266 (the hack removed there was necessary).

This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.

This also enables total semantics for BV div-by-zero for sygus.

6 years ago Initialize inputAssertions only when proofRecipe is non-null (#2325)
Tim King [Fri, 17 Aug 2018 06:48:17 +0000 (23:48 -0700)]
 Initialize inputAssertions only when proofRecipe is non-null (#2325)

Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... });

6 years agoRefactor eager atoms preprocessing pass. (#2318)
Mathias Preiner [Fri, 17 Aug 2018 06:07:49 +0000 (23:07 -0700)]
Refactor eager atoms preprocessing pass. (#2318)

6 years agocleaning unnecessary timers/dumps (#2327)
Haniel Barbosa [Fri, 17 Aug 2018 05:06:48 +0000 (00:06 -0500)]
cleaning unnecessary timers/dumps (#2327)

6 years agoAdding support for bitvector SyGuS problems without grammars (#2328)
Haniel Barbosa [Fri, 17 Aug 2018 04:01:05 +0000 (23:01 -0500)]
Adding support for bitvector SyGuS problems without grammars (#2328)

6 years agoMake quantifiers-preprocess preprocessing pass (#2322)
Caleb Donovick [Fri, 17 Aug 2018 03:16:00 +0000 (20:16 -0700)]
Make quantifiers-preprocess preprocessing pass (#2322)

6 years agoRemoving coverity warnings from theory_sep.cpp (#2320)
Tim King [Fri, 17 Aug 2018 02:37:38 +0000 (19:37 -0700)]
Removing coverity warnings from theory_sep.cpp (#2320)

6 years agoRefactor IteRemoval preprocessing pass (#1793)
Andres Noetzli [Fri, 17 Aug 2018 01:57:24 +0000 (18:57 -0700)]
Refactor IteRemoval preprocessing pass (#1793)

This commit refactors the IteRemoval pass to follow the new format.
In addition to moving the code, this entails the following changes:

- The timer for the ITE removal is now called differently (the default
  timer of PreprocessingPass is used) and measures just the
  preprocessing pass without applySubstitutions(). It also measures the
  time used by both invocations of the ITE removal pass.
- Debug output will be slightly different because we now just rely on
  the default functionality of PreprocessingPass.
- d_iteRemover is now passed into the PreprocessingPassContext.
- AssertionPipeline now owns the d_iteSkolemMap, which makes it
  accessible by preprocessing passes. The idea behind this is that the
  preprocessing passes collect information in AssertionPipeline and
  d_iteSkolemMap fits that pattern.

6 years agoMove node algorithms to separate file (#2311)
Andres Noetzli [Thu, 16 Aug 2018 23:46:05 +0000 (16:46 -0700)]
Move node algorithms to separate file (#2311)

6 years agoMinor fixes and improvement for sygus to builtin. (#2306)
Andrew Reynolds [Thu, 16 Aug 2018 21:57:50 +0000 (16:57 -0500)]
Minor fixes and improvement for sygus to builtin. (#2306)

6 years agoRefactor extended rewriter preprocessing pass (#2324)
Haniel Barbosa [Thu, 16 Aug 2018 21:15:07 +0000 (16:15 -0500)]
Refactor extended rewriter preprocessing pass (#2324)

6 years agoRefactor apply2const (#2316)
Haniel Barbosa [Thu, 16 Aug 2018 16:18:11 +0000 (11:18 -0500)]
Refactor apply2const (#2316)

6 years agoSwitching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315)
Tim King [Thu, 16 Aug 2018 01:09:45 +0000 (18:09 -0700)]
Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315)

6 years agoRemoving attribute cleanups. (#2300)
Tim King [Wed, 15 Aug 2018 22:49:15 +0000 (15:49 -0700)]
Removing attribute cleanups. (#2300)

* Removing attribute cleanups.

6 years agoAdd contrib/get-gmp script. (#2292)
Mathias Preiner [Wed, 15 Aug 2018 21:34:12 +0000 (14:34 -0700)]
Add contrib/get-gmp script. (#2292)

6 years agoRemove unused tuple classes (#2313)
Andres Noetzli [Wed, 15 Aug 2018 19:16:20 +0000 (12:16 -0700)]
Remove unused tuple classes (#2313)

Since we are using C++11, we can replace the triple and quad classes
with std::tuple.

6 years agoRemove unused class DynamicArray (#2312)
Andres Noetzli [Wed, 15 Aug 2018 18:46:31 +0000 (11:46 -0700)]
Remove unused class DynamicArray (#2312)

6 years agoMake sort inference a preprocessing pass (#2309)
Andrew Reynolds [Wed, 15 Aug 2018 18:02:46 +0000 (13:02 -0500)]
Make sort inference a preprocessing pass (#2309)

6 years agoFix dumping of get-unsat-assumptions (#2302)
Andres Noetzli [Wed, 15 Aug 2018 16:37:00 +0000 (09:37 -0700)]
Fix dumping of get-unsat-assumptions (#2302)

When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping
two `get-unsat-cores` commands. This commit splits
`SmtEngine::getUnsatCores()` into a part that does the dumping and an
internal part that actually gets the unsat core without dumping.
`SmtEngine::getUnsatAssumptions()` now calls the internal version to
avoid the redundant dumping of a `get-unsat-cores` command and changes
the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.

6 years agoRemove unused declaration (#2310)
Andres Noetzli [Wed, 15 Aug 2018 03:23:28 +0000 (20:23 -0700)]
Remove unused declaration (#2310)

6 years agoautotools: Remove personal builds, rename build 'default' to 'testing'. (#2303)
Aina Niemetz [Tue, 14 Aug 2018 15:24:33 +0000 (08:24 -0700)]
autotools: Remove personal builds, rename build 'default' to 'testing'. (#2303)

6 years agoFix get-unsat-assumptions output (#2301)
Andres Noetzli [Tue, 14 Aug 2018 01:03:54 +0000 (18:03 -0700)]
Fix get-unsat-assumptions output (#2301)

Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.

6 years agoRemoving support for T* and const T* attributes. (#2297)
Tim King [Mon, 13 Aug 2018 16:25:26 +0000 (09:25 -0700)]
Removing support for T* and const T* attributes. (#2297)

* Removing support for T* and const T* attributes. These are unused.

6 years agoMake attributes robust to static init orderings (#2295)
Andres Noetzli [Sat, 11 Aug 2018 18:13:17 +0000 (11:13 -0700)]
Make attributes robust to static init orderings (#2295)

@taking pointed out that part of the issue fixed in #2293 is also that
we should be more robust to different (de-)initialization orders. A
common, portable way to achieve this is to allocate the object in
question on the heap and make the pointer to it static [0]. This commit
fixes the variable in question.

I have tested this fix in ASAN (without using --no-static-init flag for
CxxTest) and it works.

[0] https://isocpp.org/wiki/faq/ctors#construct-on-first-use-v2

6 years agoFix portfolio command executor for changes from #2240. (#2294)
Aina Niemetz [Fri, 10 Aug 2018 23:45:27 +0000 (16:45 -0700)]
Fix portfolio command executor for changes from #2240. (#2294)

6 years agoDo not use static initialization in CxxTest runner (#2293)
Andres Noetzli [Fri, 10 Aug 2018 22:23:21 +0000 (15:23 -0700)]
Do not use static initialization in CxxTest runner (#2293)

The static initialization in the CxxTest runner was causing problems
when having `std::unique_ptr`s in test classes. When the ExprManager's
deconstructor is called, we count on certain static objects to be around
(e.g.
https://github.com/CVC4/CVC4/blob/0a02fd2b69c0c0f454fc33d8028b24f4fcf431de/src/expr/attribute_internals.h#L508).
If the ExprManager is (indirectly) owned by a `std::unique_ptr` in a
static class, however, there are no such guarantees as the destruction
order of static objects is not defined. This commit adds a flag for
CxxTest to not use static initialization in the test runner, which
solves the issue.  Additionally, the commit fixes a warning about a
missing virtual deconstructor in ParserBlack that came up after using
the new flags.

This fixes an issue reported in the nightly builds.

6 years ago Fix char overflow issues in regular expression solver (#2275)
Andrew Reynolds [Thu, 9 Aug 2018 20:11:27 +0000 (15:11 -0500)]
 Fix char overflow issues in regular expression solver (#2275)

6 years agoFix documentation of regression tests (#2290)
Andres Noetzli [Thu, 9 Aug 2018 18:43:00 +0000 (11:43 -0700)]
Fix documentation of regression tests (#2290)

6 years agoPlug solver API object into parser. (#2240)
Aina Niemetz [Thu, 9 Aug 2018 02:21:47 +0000 (19:21 -0700)]
Plug solver API object into parser. (#2240)

6 years agoFixing documentation nit from PR#2232. (#2289)
Tim King [Thu, 9 Aug 2018 00:44:00 +0000 (17:44 -0700)]
Fixing documentation nit from PR#2232. (#2289)

6 years ago Proposal for adding map utility functions to CVC4. (#2232)
Tim King [Wed, 8 Aug 2018 23:50:16 +0000 (16:50 -0700)]
 Proposal for adding map utility functions to CVC4. (#2232)

* Proposal for adding map utility functions to CVC4.

6 years agoDisable argument relevance for sygus by default (#2288)
Andrew Reynolds [Wed, 8 Aug 2018 22:09:18 +0000 (17:09 -0500)]
Disable argument relevance for sygus by default (#2288)

6 years agoAdd debug test for sygus subcall verify calls. (#2287)
Andrew Reynolds [Wed, 8 Aug 2018 20:57:45 +0000 (15:57 -0500)]
Add debug test for sygus subcall verify calls. (#2287)

6 years agoMove uf model code from uf to quantifiers (#2095)
Andrew Reynolds [Wed, 8 Aug 2018 18:09:19 +0000 (13:09 -0500)]
Move uf model code from uf to quantifiers (#2095)

6 years agoDo beta-reduction in expandDefinitions (#2286)
Andrew Reynolds [Wed, 8 Aug 2018 17:08:20 +0000 (12:08 -0500)]
Do beta-reduction in expandDefinitions (#2286)

6 years agoRequire Swig 3 (#2283)
Andres Noetzli [Wed, 8 Aug 2018 06:24:07 +0000 (23:24 -0700)]
Require Swig 3 (#2283)

Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h

6 years agoSimplify and improve the sygus parser (#2266)
Andrew Reynolds [Wed, 8 Aug 2018 05:51:13 +0000 (00:51 -0500)]
Simplify and improve the sygus parser (#2266)

Currently, there is code duplication for parsing constants in sygus grammars, e.g.:
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304

This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g.

As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants.

It also removes some unnecessary code for converting builtin kinds to their total versions.

This is work towards #2197.  We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols.

6 years agoDocument/refactor datatypes sygus simple symmetry breaking (#2233)
Andrew Reynolds [Wed, 8 Aug 2018 04:03:57 +0000 (23:03 -0500)]
Document/refactor datatypes sygus simple symmetry breaking (#2233)

6 years ago Fix simple reg exp consume rewrite (#2281)
Andrew Reynolds [Wed, 8 Aug 2018 03:06:19 +0000 (22:06 -0500)]
 Fix simple reg exp consume rewrite (#2281)

6 years agoDelete functions instead of using CVC4_UNDEFINED (#1794)
Andres Noetzli [Wed, 8 Aug 2018 00:26:58 +0000 (17:26 -0700)]
Delete functions instead of using CVC4_UNDEFINED (#1794)

C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.

6 years ago Wait to do sygus qe preprocess until full effort check (#2282)
Andrew Reynolds [Tue, 7 Aug 2018 22:57:39 +0000 (17:57 -0500)]
 Wait to do sygus qe preprocess until full effort check  (#2282)

6 years agoFix inference of pre and post conditions for non variable arguments. (#2237)
Andrew Reynolds [Tue, 7 Aug 2018 22:34:00 +0000 (17:34 -0500)]
Fix inference of pre and post conditions for non variable arguments. (#2237)

6 years agoMake output of flushInformation and safeFlushInformation consistent. (#2280)
Mathias Preiner [Tue, 7 Aug 2018 20:18:44 +0000 (13:18 -0700)]
Make output of flushInformation and safeFlushInformation consistent. (#2280)

6 years agoAdd rewrite for nested BITVECTOR_ITE that can be merged. (#2273)
Aina Niemetz [Tue, 7 Aug 2018 18:22:05 +0000 (11:22 -0700)]
Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273)

6 years agoMake flat form inferences optional in strings (#2277)
Andrew Reynolds [Tue, 7 Aug 2018 04:04:21 +0000 (23:04 -0500)]
Make flat form inferences optional in strings (#2277)

6 years agoAdd RegLan to smt2/sygus parsers. (#2276)
Andrew Reynolds [Tue, 7 Aug 2018 03:39:21 +0000 (22:39 -0500)]
Add RegLan to smt2/sygus parsers. (#2276)

6 years ago Move sygus quantifier elimination step for non-ground-single-invocation to sygus...
Andrew Reynolds [Tue, 7 Aug 2018 02:44:41 +0000 (21:44 -0500)]
 Move sygus quantifier elimination step for non-ground-single-invocation to sygus (#2269)

6 years agoRemove support for Enum sygus syntax. (#2264)
Andrew Reynolds [Tue, 7 Aug 2018 01:28:15 +0000 (20:28 -0500)]
Remove support for Enum sygus syntax. (#2264)

6 years agoFixes for sygus inference (#2238)
Andrew Reynolds [Mon, 6 Aug 2018 23:55:29 +0000 (18:55 -0500)]
Fixes for sygus inference (#2238)

This includes:
- Enabling sygus-specific options in SmtEngine::setDefaults,
- Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks),
- Treating free constants as functions to synthesize

6 years ago Fixes and improvements for single invocation inference (#2261)
Andrew Reynolds [Mon, 6 Aug 2018 22:33:23 +0000 (17:33 -0500)]
 Fixes and improvements for single invocation inference (#2261)

6 years agoFix degenerate case of sygus grammar construction for 0-argument Bools (#2260)
Andrew Reynolds [Mon, 6 Aug 2018 21:36:23 +0000 (16:36 -0500)]
Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260)

6 years ago Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)
Aina Niemetz [Sat, 4 Aug 2018 02:41:49 +0000 (19:41 -0700)]
 Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)

6 years agoAdd rewrite for BITVECTOR_ITE with const children. (#2271)
Aina Niemetz [Sat, 4 Aug 2018 01:09:07 +0000 (18:09 -0700)]
Add rewrite for BITVECTOR_ITE with const children. (#2271)

6 years agoAdd rewrite for BITVECTOR_ITE with term_then == term_else. (#2268)
Aina Niemetz [Fri, 3 Aug 2018 23:43:10 +0000 (16:43 -0700)]
Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268)

6 years agoEliminate option for sygus UF evaluation functions (#2262)
Andrew Reynolds [Fri, 3 Aug 2018 20:34:17 +0000 (15:34 -0500)]
Eliminate option for sygus UF evaluation functions (#2262)

6 years agoFix printing statistics in case of signals. (#2267)
Mathias Preiner [Fri, 3 Aug 2018 12:59:23 +0000 (05:59 -0700)]
Fix printing statistics in case of signals. (#2267)

6 years ago Add timer for BV inequality solver. (#2265)
Aina Niemetz [Fri, 3 Aug 2018 00:11:36 +0000 (17:11 -0700)]
 Add timer for BV inequality solver. (#2265)

6 years agoParse standard separation logic inputs (#2257)
Andrew Reynolds [Thu, 2 Aug 2018 22:17:09 +0000 (17:17 -0500)]
Parse standard separation logic inputs (#2257)

6 years agoImprove CEGQI heuristics involving equality and multiple instantiations (#2254)
Andrew Reynolds [Thu, 2 Aug 2018 20:29:45 +0000 (15:29 -0500)]
Improve CEGQI heuristics involving equality and multiple instantiations (#2254)

6 years agoFix candidate rewrite utilities for non-first-class types (#2256)
Andrew Reynolds [Thu, 2 Aug 2018 19:54:37 +0000 (14:54 -0500)]
Fix candidate rewrite utilities for non-first-class types (#2256)

6 years agoMake strings robust to regular expression variables. (#2255)
Andrew Reynolds [Thu, 2 Aug 2018 19:16:48 +0000 (14:16 -0500)]
Make strings robust to regular expression variables. (#2255)

The theory solver for strings does not support regular expression variables. With this PR, we properly throw an exception if it is given one.

However, the rewriter needs to handle regular expression variables (for various reasons: rewriting an expression before its asserted, sygus explanation generalization, etc.).  This corrects a few miscellaneous issues in the strings rewriter to make it sound for these cases.

It also corrects a seg fault in simpleRegexpConsume when testing memberships `(str.in.re "" R)`, where R is a *non-constant* regular expression (which will now be allowed if variables are allowed).

This is in preparation for adding `RegLan` as a token to the smt2/sygus parsers.

6 years agoAdd rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const condition/child. (#2259)
Aina Niemetz [Thu, 2 Aug 2018 18:52:32 +0000 (11:52 -0700)]
Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const condition/child. (#2259)

6 years ago Remove references to deprecated propagate as decision feature (#2258)
Andrew Reynolds [Thu, 2 Aug 2018 18:01:50 +0000 (13:01 -0500)]
 Remove references to deprecated propagate as decision feature (#2258)

6 years agoRemove Subversion build info (#2250)
Andres Noetzli [Thu, 2 Aug 2018 14:54:50 +0000 (07:54 -0700)]
Remove Subversion build info (#2250)

6 years agoFix API call for reg exp. (#2248)
Andrew Reynolds [Thu, 2 Aug 2018 04:24:53 +0000 (23:24 -0500)]
Fix API call for reg exp. (#2248)

6 years agoImprovements and fixes in cegqi arithmetic (#2247)
Andrew Reynolds [Thu, 2 Aug 2018 02:24:42 +0000 (21:24 -0500)]
Improvements and fixes in cegqi arithmetic (#2247)

This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.

It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.

This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.

6 years agoRemove outdated references to TLS (#2245)
Andres Noetzli [Thu, 2 Aug 2018 01:07:34 +0000 (18:07 -0700)]
Remove outdated references to TLS (#2245)

6 years agoFix issues with printing parametric datatypes in smt2 (#2213)
Andrew Reynolds [Thu, 2 Aug 2018 00:10:47 +0000 (19:10 -0500)]
Fix issues with printing parametric datatypes in smt2 (#2213)

6 years agoFix wrong evaluation of STRING_STOI (#2252)
Andres Noetzli [Wed, 1 Aug 2018 23:08:47 +0000 (16:08 -0700)]
Fix wrong evaluation of STRING_STOI (#2252)

6 years agoFix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)
Mathias Preiner [Wed, 1 Aug 2018 22:14:45 +0000 (15:14 -0700)]
Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)

6 years ago InteractiveShell: Remove redundant options argument. (#2244)
Aina Niemetz [Wed, 1 Aug 2018 19:08:02 +0000 (12:08 -0700)]
 InteractiveShell: Remove redundant options argument. (#2244)

6 years agoNew C++ API: Fixed ownership of options object. (#2243)
Aina Niemetz [Wed, 1 Aug 2018 18:36:30 +0000 (11:36 -0700)]
New C++ API: Fixed ownership of options object. (#2243)

6 years agoFix issues with bv2nat (#2219)
Andrew Reynolds [Wed, 1 Aug 2018 17:22:09 +0000 (12:22 -0500)]
Fix issues with bv2nat (#2219)

This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.

6 years ago Fix assertion in conjecture generator (#2246)
Andrew Reynolds [Wed, 1 Aug 2018 15:33:41 +0000 (10:33 -0500)]
 Fix assertion in conjecture generator (#2246)

Makes minor improvements and removes the need to have the assertion (which was incorrect).

This fixes the nightlies.

6 years agoMake conjecture generator's uf term enumeration safer (#2172)
Andrew Reynolds [Wed, 1 Aug 2018 07:31:49 +0000 (02:31 -0500)]
Make conjecture generator's uf term enumeration safer (#2172)

This ensures that the function getEnumerateUfTerm does not have out of bounds accesses. This is an alternative fix to the one brought up in #2158.

6 years agoMake candidate rewrite match filtering handle polymorphic operators properly (#2236)
Andrew Reynolds [Wed, 1 Aug 2018 06:31:14 +0000 (01:31 -0500)]
Make candidate rewrite match filtering handle polymorphic operators properly (#2236)

Currently, the discrimination tree index used for candidate rewrite rule filtering based on matching does not properly distinguish polymorphic operators, which leads to type errors. This makes the index handle them correctly.

Fixes #1923.

6 years agoImprovements and tests for the API around separation logic (#2229)
ayveejay [Wed, 1 Aug 2018 02:25:51 +0000 (03:25 +0100)]
Improvements and tests for the API around separation logic (#2229)

- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to
  obtain the separation logic heap/nil (validate_exception())
- Introduces a system test demonstrating how to use the separation logic theory, and then how
  to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters())
- Refactors the original getters to avoid duplicate code
- Add a check as part of the getters to ensure that THEORY_SEP is in use

6 years agoRemove hasAssertions() method from eager BV solver. (#2239)
Mathias Preiner [Wed, 1 Aug 2018 00:51:15 +0000 (17:51 -0700)]
Remove hasAssertions() method from eager BV solver. (#2239)

6 years agoFix option handler for lazy/bv-sat-solver combinations. (#2225)
Mathias Preiner [Tue, 31 Jul 2018 18:25:27 +0000 (11:25 -0700)]
Fix option handler for lazy/bv-sat-solver combinations. (#2225)

Further, unifies all *limitHandler and *limitPerHandler to limitHandler.

6 years agoAdd support for incremental eager bit-blasting. (#1838)
Mathias Preiner [Mon, 30 Jul 2018 22:24:55 +0000 (15:24 -0700)]
Add support for incremental eager bit-blasting. (#1838)

Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.

6 years agoFix several spelling errors (#2231)
FabianWolff [Mon, 30 Jul 2018 16:28:11 +0000 (18:28 +0200)]
Fix several spelling errors (#2231)

6 years agoStoring a std::pair<Key,Data> on CDOhash_map.
Tim King [Mon, 30 Jul 2018 02:02:44 +0000 (19:02 -0700)]
Storing a std::pair<Key,Data> on CDOhash_map.

Changing the return type of CDHashMap::iterator* to return a reference. Requires performance testing.

6 years agoRequire argument description for non-{bool,void} options. (#2228)
Mathias Preiner [Fri, 27 Jul 2018 21:54:06 +0000 (14:54 -0700)]
Require argument description for non-{bool,void} options. (#2228)

Not adding the argument description for non-{bool,void} options is now an error.

Further, adds missing argument descriptions.

6 years agoFix issues related to cxxtest in configure.ac (#2226)
Andres Noetzli [Fri, 27 Jul 2018 20:22:49 +0000 (13:22 -0700)]
Fix issues related to cxxtest in configure.ac (#2226)

Fixes #2188. There were two issues related to cxxtest in configure.ac:

- `AC_PATH_PROGS` was used wrong (the third argument is a value to
  assign to the first argument and cannot be used for arbitrary
  commands)
- The `test` command always executes both sides of an "and" (`-a`), so
  `basename` was called without arguments when `CXXTESTGEN` was empty

This commit fixes both issues.

6 years agoMake Python a required CVC4 dependency. (#2227)
Mathias Preiner [Fri, 27 Jul 2018 19:50:47 +0000 (12:50 -0700)]
Make Python a required CVC4 dependency. (#2227)

Python is required for generating the options code. The dependency is now
required. Now autoconf searches for a Python version >= 2.7 and sets the
corresponding environment variables. mkoptions.py is now called with $(PYTHON).

This fixes the broken competition and windows nightly builds.

6 years agoFix for candidate rewrite rule filtering. (#2220)
Andrew Reynolds [Fri, 27 Jul 2018 15:56:01 +0000 (10:56 -0500)]
Fix for candidate rewrite rule filtering. (#2220)

6 years ago Make check-synth robust for assertions that are not the synth conjecture (#2217)
Andrew Reynolds [Fri, 27 Jul 2018 15:19:13 +0000 (10:19 -0500)]
 Make check-synth robust for assertions that are not the synth conjecture (#2217)

6 years agoFix Node::hasFreeVar for function variables (#2216)
Andrew Reynolds [Fri, 27 Jul 2018 07:03:56 +0000 (02:03 -0500)]
Fix Node::hasFreeVar for function variables (#2216)

A Node has free variables if its operator has free variables.

6 years agoFix CryptoMiniSat config to allow system versions. (#2223)
Mathias Preiner [Fri, 27 Jul 2018 02:56:44 +0000 (19:56 -0700)]
Fix CryptoMiniSat config to allow system versions. (#2223)

6 years agoNew C++ API: Enable examples. (#2222)
Aina Niemetz [Thu, 26 Jul 2018 23:37:26 +0000 (16:37 -0700)]
New C++ API: Enable examples. (#2222)

6 years agoRemoving unused CDTrailHashmap. (#2221)
Tim King [Thu, 26 Jul 2018 23:02:33 +0000 (16:02 -0700)]
Removing unused CDTrailHashmap. (#2221)

6 years agoDisabling bvLazyRewriteExtf in the right place (#2214)
yoni206 [Thu, 26 Jul 2018 22:16:04 +0000 (15:16 -0700)]
Disabling bvLazyRewriteExtf in the right place (#2214)

6 years agoChanging CDInsertHashMap to store <const Key, const Data> pairs. This is in preparati...
Tim King [Thu, 26 Jul 2018 20:55:53 +0000 (13:55 -0700)]
Changing CDInsertHashMap to store <const Key, const Data> pairs. This is in preparation for adding map utility functions. (#2209)

6 years agoChanging the arithmetic static learner to use CDHashMap. This is 2/3 PRs for deprecat...
Tim King [Thu, 26 Jul 2018 20:13:43 +0000 (13:13 -0700)]
Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for deprecating CDTrailHashMap. (#2207)