cvc5.git
6 years agoAdd regular expression elimination module (#2400)
Andrew Reynolds [Thu, 30 Aug 2018 16:57:58 +0000 (11:57 -0500)]
Add regular expression elimination module (#2400)

6 years agoRefactor MipLibTrick preprocessing pass. (#2359)
Mathias Preiner [Wed, 29 Aug 2018 21:38:33 +0000 (14:38 -0700)]
Refactor MipLibTrick preprocessing pass. (#2359)

6 years agoForcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
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)

6 years agofix bv total ops printing (#2365)
Haniel Barbosa [Wed, 29 Aug 2018 16:06:05 +0000 (11:06 -0500)]
fix bv total ops printing (#2365)

6 years ago Split term canonize utility to own file and document (#2398)
Andrew Reynolds [Tue, 28 Aug 2018 23:32:15 +0000 (18:32 -0500)]
 Split term canonize utility to own file and document (#2398)

6 years agoReorder circuit propagator class.
Aina Niemetz [Tue, 28 Aug 2018 17:03:13 +0000 (10:03 -0700)]
Reorder circuit propagator class.

6 years agoMove flag needsFinish from SMT engine to circuit propagator.
Aina Niemetz [Tue, 28 Aug 2018 16:53:58 +0000 (09:53 -0700)]
Move flag needsFinish from SMT engine to circuit propagator.

6 years ago Fix for get constraints method in fmf-fun (#2399)
Andrew Reynolds [Tue, 28 Aug 2018 22:09:01 +0000 (17:09 -0500)]
 Fix for get constraints method in fmf-fun (#2399)

6 years agoSolve equalities between Boolean variables in presolve. (#2390)
Andrew Reynolds [Tue, 28 Aug 2018 20:25:12 +0000 (15:25 -0500)]
Solve equalities between Boolean variables in presolve. (#2390)

6 years agoRemove throw specifiers in FP type checker (#2392)
Andres Noetzli [Tue, 28 Aug 2018 19:35:35 +0000 (12:35 -0700)]
Remove throw specifiers in FP type checker (#2392)

6 years agoRemove dead code in fp_converter (#2388)
Andres Noetzli [Tue, 28 Aug 2018 18:41:42 +0000 (11:41 -0700)]
Remove dead code in fp_converter (#2388)

This should fix Coverity issues 1473025 and 1459599.

6 years agoFix sort inference for quantified variables of interpreted types (#2393)
Andrew Reynolds [Tue, 28 Aug 2018 15:39:48 +0000 (10:39 -0500)]
Fix sort inference for quantified variables of interpreted types (#2393)

6 years ago Address more coverity warnings (#2394)
Andrew Reynolds [Tue, 28 Aug 2018 03:41:50 +0000 (22:41 -0500)]
 Address more coverity warnings (#2394)

6 years agoFix warning in sygus io. (#2391)
Andrew Reynolds [Tue, 28 Aug 2018 02:48:48 +0000 (21:48 -0500)]
Fix warning in sygus io. (#2391)

6 years agoRemove dead code in evaluator (#2389)
Andres Noetzli [Tue, 28 Aug 2018 01:59:59 +0000 (18:59 -0700)]
Remove dead code in evaluator (#2389)

This should fix Coverity issue 1470214.

6 years agoRefactor extended rewriter, move rewrites to aggressive (#2387)
Andrew Reynolds [Tue, 28 Aug 2018 01:08:01 +0000 (20:08 -0500)]
Refactor extended rewriter, move rewrites to aggressive (#2387)

This is work towards #2305.

With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.

6 years agoNew C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)
Aina Niemetz [Tue, 28 Aug 2018 00:28:08 +0000 (17:28 -0700)]
New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)

…underlying type.

6 years agoUse std:unique_ptr instead of raw pointers in theory/bv. (#2385)
Mathias Preiner [Mon, 27 Aug 2018 23:19:34 +0000 (16:19 -0700)]
Use std:unique_ptr instead of raw pointers in theory/bv. (#2385)

This should also fix CIDs 146568714656951465696, and 1465701.

6 years agoResolution proof: separate printing from proof (#1964)
Andres Noetzli [Mon, 27 Aug 2018 21:14:38 +0000 (14:14 -0700)]
Resolution proof: separate printing from proof (#1964)

Currently, we have an LFSCSatProof which inherits from TSatProof and
implements printing the proof. The seperation is not clean (e.g.
clauseName is used for printing only but is in TSatProof) and the
inheritance does not add any value while making dependencies more
confusing. The plan is that TSatProof becomes a self-contained part that
the MiniSat implementations generate and ProofManager prints out. This
commit is a first step in that direction. For SAT solvers with native
capabilities for producing proofs, we would simply implement a different
LFSC printer of their proof representation without changing the SAT
solver itself. The inheritance would make this awkward to deal with.

Additionally, the commit cleans up some unused functions and adjusts the
visibility of TSatProof methods and members.

6 years agoMake division chainable in the smt2 parser (#2367)
Andrew Reynolds [Mon, 27 Aug 2018 17:26:14 +0000 (12:26 -0500)]
Make division chainable in the smt2 parser (#2367)

6 years agoRemove Coverity build from Travis (#2373)
Andres Noetzli [Mon, 27 Aug 2018 16:13:52 +0000 (09:13 -0700)]
Remove Coverity build from Travis (#2373)

The Coverity build is now done as part of our nightlies and the Travis
Coverity build was timing out most of the time anyway, so this commit
removes it.

6 years agoUse uniform length limit for String constants (#2381)
Andres Noetzli [Sun, 26 Aug 2018 21:31:16 +0000 (14:31 -0700)]
Use uniform length limit for String constants (#2381)

6 years agoFix unsigned integer type issues in strings (#2380)
Andrew Reynolds [Sun, 26 Aug 2018 05:22:57 +0000 (00:22 -0500)]
Fix unsigned integer type issues in strings (#2380)

* Fix unsigned integer types in strings.

* Format

6 years agoRefactor unconstrained simplification pass (#2374)
Andres Noetzli [Sun, 26 Aug 2018 04:09:22 +0000 (21:09 -0700)]
Refactor unconstrained simplification pass (#2374)

6 years agoRefactor quantifier macros preprocessing pass (#1840)
yoni206 [Sat, 25 Aug 2018 21:31:32 +0000 (14:31 -0700)]
Refactor quantifier macros preprocessing pass (#1840)

Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`,
and added the necessary methods for inheritance from PreprocessingPass.

No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.

6 years agoRefactor nlExtPurify preprocessing pass (#1963)
Haniel Barbosa [Sat, 25 Aug 2018 01:19:14 +0000 (20:19 -0500)]
Refactor nlExtPurify preprocessing pass (#1963)

6 years agoClean up quantifiers engine initialization. (#2371)
Andrew Reynolds [Sat, 25 Aug 2018 00:40:36 +0000 (19:40 -0500)]
Clean up quantifiers engine initialization. (#2371)

6 years ago Fix more simple coverity warnings (#2372)
Andrew Reynolds [Fri, 24 Aug 2018 23:49:22 +0000 (18:49 -0500)]
 Fix more simple coverity warnings (#2372)

6 years ago Remove spurious disabling of cbqi-all (#2368)
Andrew Reynolds [Fri, 24 Aug 2018 20:16:44 +0000 (15:16 -0500)]
 Remove spurious disabling of cbqi-all (#2368)

6 years agoAdd tests that enumerate and verify rewrite rules (#2344)
Andres Noetzli [Fri, 24 Aug 2018 14:36:21 +0000 (07:36 -0700)]
Add tests that enumerate and verify rewrite rules (#2344)

6 years ago Do not print internally generated datatypes in external outputs with sygus (#2234)
Andrew Reynolds [Fri, 24 Aug 2018 01:34:40 +0000 (20:34 -0500)]
 Do not print internally generated datatypes in external outputs with sygus (#2234)

6 years agoNew C++ API: Add checks for kind arguments. (#2369)
Aina Niemetz [Fri, 24 Aug 2018 00:03:08 +0000 (17:03 -0700)]
New C++ API: Add checks for kind arguments. (#2369)

This should hopefully also take care of the open coverity issues for cvc4cpp.cpp.

6 years agoAdd missing overrides in unit tests (#2362)
Andres Noetzli [Thu, 23 Aug 2018 23:28:21 +0000 (16:28 -0700)]
Add missing overrides in unit tests (#2362)

6 years agoReplacing allocatedInCMM and d_noTrash with false everywhere in cdhashmap (#2355)
Tim King [Thu, 23 Aug 2018 22:24:47 +0000 (15:24 -0700)]
Replacing allocatedInCMM and d_noTrash with false everywhere in cdhashmap (#2355)

There do not appear to be any instances these can be positive.

6 years agoMakes the filename be set in the SMT engine by default (#2366)
Haniel Barbosa [Thu, 23 Aug 2018 21:09:16 +0000 (16:09 -0500)]
Makes the filename be set in the SMT engine by default (#2366)

6 years ago Fixing some coverity warnings (#2357)
Andrew Reynolds [Thu, 23 Aug 2018 19:59:20 +0000 (14:59 -0500)]
 Fixing some coverity warnings (#2357)

6 years agoFix regression requiring proof build. (#2364)
Andrew Reynolds [Thu, 23 Aug 2018 19:11:36 +0000 (14:11 -0500)]
Fix regression requiring proof build. (#2364)

6 years agoRefactor ITE simplification preprocessing pass. (#2360)
Aina Niemetz [Thu, 23 Aug 2018 18:05:38 +0000 (11:05 -0700)]
Refactor ITE simplification preprocessing pass. (#2360)

6 years agoUse "filename" instead of "name" in SmtEngine::setInfo() (#2361)
Andres Noetzli [Thu, 23 Aug 2018 17:10:48 +0000 (10:10 -0700)]
Use "filename" instead of "name" in SmtEngine::setInfo() (#2361)

6 years agoglobal-negate preprocessing pass (#2317)
yoni206 [Thu, 23 Aug 2018 04:13:46 +0000 (21:13 -0700)]
global-negate preprocessing pass (#2317)

6 years agoMore regressions that increase coverage (#2354)
Andrew Reynolds [Thu, 23 Aug 2018 01:47:27 +0000 (20:47 -0500)]
More regressions that increase coverage (#2354)

6 years ago More unused code elimination (#2358)
Andrew Reynolds [Wed, 22 Aug 2018 22:40:22 +0000 (17:40 -0500)]
 More unused code elimination (#2358)

6 years agoGenerating less consistency lemmas in bv-ackermann preprocessing pass (#2253)
yoni206 [Wed, 22 Aug 2018 21:36:13 +0000 (14:36 -0700)]
Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)

6 years agoWrapping TheorySetsPrivate in a unique_ptr. (#2356)
Tim King [Wed, 22 Aug 2018 20:09:39 +0000 (13:09 -0700)]
Wrapping TheorySetsPrivate in a unique_ptr. (#2356)

6 years agoFix option for real2int regression. (#2353)
Andrew Reynolds [Wed, 22 Aug 2018 17:39:22 +0000 (12:39 -0500)]
Fix option for real2int regression. (#2353)

6 years agoAdds regression test for automatic generation of SyGuS BV grammars (#2345)
Haniel Barbosa [Wed, 22 Aug 2018 17:18:14 +0000 (12:18 -0500)]
Adds regression test for automatic generation of SyGuS BV grammars (#2345)

6 years agoFix invalid iterator comparisons (#2349)
Andrew Reynolds [Wed, 22 Aug 2018 15:37:50 +0000 (10:37 -0500)]
Fix invalid iterator comparisons (#2349)

6 years ago Fix processing of nested Variable construct in sygus let bodies (#2351)
Andrew Reynolds [Wed, 22 Aug 2018 00:38:40 +0000 (19:38 -0500)]
 Fix processing of nested Variable construct in sygus let bodies (#2351)

6 years agoRemoving unused bool members in command.cpp. Also initializes a bool member. (#2321)
Tim King [Tue, 21 Aug 2018 22:25:00 +0000 (15:25 -0700)]
Removing unused bool members in command.cpp. Also initializes a bool member. (#2321)

6 years agoWarn and enable quantifiers when using sygus + logics with QF (#2352)
Andrew Reynolds [Tue, 21 Aug 2018 21:38:26 +0000 (16:38 -0500)]
Warn and enable quantifiers when using sygus + logics with QF (#2352)

6 years agoMakes the new row propagation system default (#2335)
Haniel Barbosa [Tue, 21 Aug 2018 21:14:55 +0000 (16:14 -0500)]
Makes the new row propagation system default (#2335)

6 years agoMove d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)
Mathias Preiner [Tue, 21 Aug 2018 20:33:01 +0000 (13:33 -0700)]
Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)

6 years agoAdd constexpr annotations to help coverity understand constant ... (#2314)
Tim King [Tue, 21 Aug 2018 19:58:05 +0000 (12:58 -0700)]
Add constexpr annotations to help coverity understand constant ... (#2314)

6 years agoUse cbqi-full for sygus (#2346)
Andrew Reynolds [Tue, 21 Aug 2018 17:10:38 +0000 (12:10 -0500)]
Use cbqi-full for sygus (#2346)

6 years agoRemove support for *.expect files in regressions (#2341)
Andres Noetzli [Tue, 21 Aug 2018 03:23:09 +0000 (20:23 -0700)]
Remove support for *.expect files in regressions (#2341)

Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).

6 years agoFix initialization of d_smt in ValidityChecker for changes from #2240. (#2343)
Aina Niemetz [Tue, 21 Aug 2018 02:13:49 +0000 (19:13 -0700)]
Fix initialization of d_smt in ValidityChecker for changes from #2240. (#2343)

6 years agoRemove disabled system test cvc3_george. (#2342)
Aina Niemetz [Tue, 21 Aug 2018 01:40:25 +0000 (18:40 -0700)]
Remove disabled system test cvc3_george. (#2342)

Disabled since 6 years, @mdeters commented when disabling it that it takes a very long time to build, see 868ee6d.

6 years agoMore unused code elimination (#2339)
Andrew Reynolds [Tue, 21 Aug 2018 00:22:21 +0000 (19:22 -0500)]
More unused code elimination (#2339)

6 years ago Remove support for prototype (non-sygus) synthesis (#2338)
Andrew Reynolds [Mon, 20 Aug 2018 23:40:40 +0000 (18:40 -0500)]
 Remove support for prototype (non-sygus) synthesis (#2338)

6 years agoAdd regressions that increase coverage (#2337)
Andrew Reynolds [Mon, 20 Aug 2018 23:05:43 +0000 (18:05 -0500)]
Add regressions that increase coverage (#2337)

6 years agoMinor improvements to the interface for sygus sampler (#2326)
Andrew Reynolds [Mon, 20 Aug 2018 21:29:30 +0000 (16:29 -0500)]
Minor improvements to the interface for sygus sampler (#2326)

6 years ago Make sygus inference a preprocessing pass (#2334)
Andrew Reynolds [Mon, 20 Aug 2018 17:21:37 +0000 (12:21 -0500)]
 Make sygus inference a preprocessing pass (#2334)

6 years agorun-regress script: Exit with exit code > 0 on failure. (#2336)
Aina Niemetz [Sat, 18 Aug 2018 07:03:47 +0000 (00:03 -0700)]
run-regress script: Exit with exit code > 0 on failure. (#2336)

This is in preparation for migration to cmake since ctest determines failure via exit code.

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.