cvc5.git
5 years agoFix issue related to enum in cegqi (#3267)
Andrew Reynolds [Tue, 10 Sep 2019 22:06:30 +0000 (17:06 -0500)]
Fix issue related to enum in cegqi (#3267)

5 years agoFix issue in cegqi related to enum (#3265)
Andrew Reynolds [Mon, 9 Sep 2019 17:47:23 +0000 (12:47 -0500)]
Fix issue in cegqi related to enum (#3265)

5 years agoRemove portfolio (#3236)
Andrew Reynolds [Sat, 7 Sep 2019 01:52:16 +0000 (20:52 -0500)]
Remove portfolio (#3236)

5 years agoRemove parsing/printing of meta-info command. (#3260)
Mathias Preiner [Fri, 6 Sep 2019 23:42:44 +0000 (16:42 -0700)]
Remove parsing/printing of meta-info command. (#3260)

5 years agoRemove SMT1 parser. (#3228)
Mathias Preiner [Fri, 6 Sep 2019 22:28:07 +0000 (15:28 -0700)]
Remove SMT1 parser. (#3228)

This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).

Fixes #2948 and fixes #1313.

5 years agoMake CEGQI term type to enum (#3256)
Andrew Reynolds [Fri, 6 Sep 2019 16:46:21 +0000 (11:46 -0500)]
Make CEGQI term type to enum (#3256)

5 years ago Model API for domain elements (#3243)
Andrew Reynolds [Fri, 6 Sep 2019 02:40:50 +0000 (21:40 -0500)]
 Model API for domain elements (#3243)

5 years agoExplicitly pass current sygus solution to exclude (#3209)
Andrew Reynolds [Thu, 5 Sep 2019 02:58:33 +0000 (21:58 -0500)]
Explicitly pass current sygus solution to exclude (#3209)

5 years agoRefactoring CEGQI interface (#3239)
Andrew Reynolds [Thu, 5 Sep 2019 00:58:51 +0000 (19:58 -0500)]
Refactoring CEGQI interface (#3239)

5 years agoTowards incremental SyGuS in SMT engine (#3195)
Andrew Reynolds [Wed, 4 Sep 2019 21:45:08 +0000 (16:45 -0500)]
Towards incremental SyGuS in SMT engine (#3195)

5 years agoMore details in substitution function documentation (#3244)
yoni206 [Wed, 4 Sep 2019 20:52:43 +0000 (13:52 -0700)]
More details in substitution function documentation (#3244)

5 years agoMove getCounterexampleLiteral out of term utilities (#3238)
Andrew Reynolds [Wed, 4 Sep 2019 19:45:21 +0000 (14:45 -0500)]
Move getCounterexampleLiteral out of term utilities (#3238)

5 years agoFix DAGification for printer. (#3233)
Mathias Preiner [Wed, 4 Sep 2019 18:13:18 +0000 (11:13 -0700)]
Fix DAGification for printer. (#3233)

5 years ago Fixes related to destructing null (#3231)
Andrew Reynolds [Wed, 4 Sep 2019 17:51:02 +0000 (12:51 -0500)]
 Fixes related to destructing null (#3231)

5 years agoRemove duplicate regression tests. (#3227)
Mathias Preiner [Wed, 4 Sep 2019 17:06:56 +0000 (10:06 -0700)]
Remove duplicate regression tests. (#3227)

5 years agoFix out-of-bounds access in regexp inclusion test (#3242)
Andres Noetzli [Fri, 30 Aug 2019 16:14:28 +0000 (09:14 -0700)]
Fix out-of-bounds access in regexp inclusion test (#3242)

If `re.*(re.allchar)` was at the end of a regular expression
concatenation, the regular expression inclusion test could cause
out-of-bound accesses. For `re.*(re.allchar)`, we were blindly adding
the index after it to the set of indices being considered. Later in the
loop, we were assuming that all the indices are smaller than the number
of components in the concatenation, thus leading to out-of-bound
accesses. This commit adds a check before adding the index to the set of
indices.

Signed-off-by: Andres Noetzli <andres.noetzli@gmail.com>
5 years agoUndo unintential change to FindCxxTest (#3240)
Andrew Reynolds [Fri, 30 Aug 2019 15:37:36 +0000 (10:37 -0500)]
Undo unintential change to FindCxxTest (#3240)

5 years agoBetter heuristic for str.code/re.range (#3220)
Andres Noetzli [Fri, 30 Aug 2019 04:15:33 +0000 (21:15 -0700)]
Better heuristic for str.code/re.range (#3220)

To make sure that our `str.code` function is injectve (except for -1 in
the codomain), we send the inference that `str.code(x) == -1 v
str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms.
Because of the order of disjuncts, `str.code(x) != str.code(y)` was
usually assigned true. This in turn lead to a difficult problem for the
arithmetic engine if there were more `str.code` applications than the
size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i
<= 10, then the arithmetic engine had a difficult time finding a
conflict. This PR improves the heuristic by setting the phase of
`str.code(x) != str.code(y)` to false, so we prefer to keep the
`str.code` values equal instead of trying to make them different.

This change is also reflected in the models produced for inputs
involving `str.code`: Previously, we were producing models with
different values for the `str.code` whereas now the models are much more
uniform.

The PR adds two regressions, one testing `str.code` performance directly
and one testing it for `str.code` terms generated by `re.range`.

Signed-off-by: Andres Noetzli <anoetzli@amazon.com>
5 years agoInfer conflicts based on regular expression inclusion (#3234)
Andres Noetzli [Fri, 30 Aug 2019 02:38:17 +0000 (19:38 -0700)]
Infer conflicts based on regular expression inclusion (#3234)

We have a conflict if we have `str.in.re(x, R1)` and `~str.in.re(x, R2)`
and `R2` includes `R1` because there is no possible value for `x` that
satisfies both memberships. This commit adds code to detect regular
expression inclusion for a small fragment of regular expressions: string
literals with single char (`re.allchar`) and multichar wildcards
(`re.*(re.allchar)`).

Signed-off-by: Andres Noetzli <anoetzli@amazon.com>
5 years agoRemoving comments related to issues (#3232)
Andrew Reynolds [Wed, 28 Aug 2019 23:18:52 +0000 (18:18 -0500)]
Removing comments related to issues (#3232)

5 years agoFixes for get-abduct (#3229)
Andrew Reynolds [Wed, 28 Aug 2019 02:07:13 +0000 (21:07 -0500)]
Fixes for get-abduct (#3229)

5 years agoMake contrib/get-* more robust. (#3198)
Mathias Preiner [Mon, 26 Aug 2019 22:38:04 +0000 (15:38 -0700)]
Make contrib/get-* more robust. (#3198)

We use the command which to determine if a command is available on the system. However, which is not installed on all platforms by default (e.g. CentOS). command is a shell builtin that can be used for the same purpose.

5 years agoRemove unnecessary code from Cvc.g (#3213)
Andrew Reynolds [Mon, 26 Aug 2019 18:28:37 +0000 (13:28 -0500)]
Remove unnecessary code from Cvc.g (#3213)

5 years agofix misuse of iterator with a different container (#3214)
Piotr Trojanek [Sat, 24 Aug 2019 17:48:44 +0000 (19:48 +0200)]
fix misuse of iterator with a different container (#3214)

5 years agofix mismatch between "delete" and "new []" (#2795)
Piotr Trojanek [Sat, 24 Aug 2019 16:36:31 +0000 (18:36 +0200)]
fix mismatch between "delete" and "new []" (#2795)

5 years ago Infer emptiness instead of splitting when a string equality rewrites to a constant...
Andrew Reynolds [Fri, 23 Aug 2019 22:27:05 +0000 (17:27 -0500)]
 Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)

5 years ago Fixes for sygus regressions (#3219)
Andrew Reynolds [Fri, 23 Aug 2019 21:59:41 +0000 (16:59 -0500)]
 Fixes for sygus regressions (#3219)

5 years agoDocument transition inference utility (#3207)
Andrew Reynolds [Fri, 23 Aug 2019 19:44:14 +0000 (14:44 -0500)]
Document transition inference utility (#3207)

5 years agoExclude redundant lemmas when tracking inst lemmas. (#3210)
Andrew Reynolds [Fri, 23 Aug 2019 19:00:53 +0000 (14:00 -0500)]
Exclude redundant lemmas when tracking inst lemmas. (#3210)

5 years agoUpdate dynamic splitting strategy for quantifiers (#3162)
Andrew Reynolds [Fri, 23 Aug 2019 18:00:43 +0000 (13:00 -0500)]
Update dynamic splitting strategy for quantifiers (#3162)

5 years agoFix argument in nonlinear extension. (#3216)
Andrew Reynolds [Fri, 23 Aug 2019 15:44:29 +0000 (10:44 -0500)]
Fix argument in nonlinear extension. (#3216)

5 years agoMinor update to term util (#3208)
Andrew Reynolds [Fri, 23 Aug 2019 15:15:43 +0000 (10:15 -0500)]
Minor update to term util (#3208)

5 years ago Pass synthesis conjecture to sygus modules (#3212)
Andrew Reynolds [Fri, 23 Aug 2019 14:31:21 +0000 (09:31 -0500)]
 Pass synthesis conjecture to sygus modules (#3212)

5 years ago Local substitutions for context-depdendent simplification in strings (#3204)
Andrew Reynolds [Thu, 22 Aug 2019 14:55:31 +0000 (09:55 -0500)]
 Local substitutions for context-depdendent simplification in strings (#3204)

5 years agoFixes for sygus inference on quantifier free problems (#3202)
Andrew Reynolds [Tue, 20 Aug 2019 22:18:02 +0000 (17:18 -0500)]
Fixes for sygus inference on quantifier free problems (#3202)

5 years agoNew C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming. (...
Aina Niemetz [Mon, 19 Aug 2019 22:10:04 +0000 (15:10 -0700)]
New C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming. (#3197)

5 years agoContext-independent regular expression unfolding (#3168)
Andrew Reynolds [Sun, 18 Aug 2019 12:32:40 +0000 (07:32 -0500)]
Context-independent regular expression unfolding (#3168)

5 years ago Cleaning make bound var in smt2 parser (#3192)
Andrew Reynolds [Sun, 18 Aug 2019 01:15:07 +0000 (20:15 -0500)]
 Cleaning make bound var in smt2 parser (#3192)

5 years agoMove quantifiers relevance module inside E-matching module (#3186)
Andrew Reynolds [Sat, 17 Aug 2019 18:50:31 +0000 (13:50 -0500)]
Move quantifiers relevance module inside E-matching module (#3186)

5 years agoMark symbols introduced by named attributes as defined. (#3190)
Andrew Reynolds [Sat, 17 Aug 2019 15:53:51 +0000 (10:53 -0500)]
Mark symbols introduced by named attributes as defined. (#3190)

5 years ago Fix for when to apply single invocation techniques (#3193)
Andrew Reynolds [Thu, 15 Aug 2019 15:00:51 +0000 (10:00 -0500)]
 Fix for when to apply single invocation techniques (#3193)

5 years agocmake: Use ExactVersion instead of SameMinorVersion. (#3191)
Mathias Preiner [Thu, 15 Aug 2019 12:35:38 +0000 (05:35 -0700)]
cmake: Use ExactVersion instead of SameMinorVersion. (#3191)

5 years agoRemove option --continued-execution. (#3189)
Mathias Preiner [Wed, 14 Aug 2019 20:12:19 +0000 (13:12 -0700)]
Remove option --continued-execution. (#3189)

5 years ago Update to standard implementation of getting free variables (#3175)
Andrew Reynolds [Wed, 14 Aug 2019 19:07:18 +0000 (14:07 -0500)]
 Update to standard implementation of getting free variables (#3175)

5 years agoCall separate SMT engine for single invocation sygus (#3151)
Andrew Reynolds [Wed, 14 Aug 2019 18:23:07 +0000 (13:23 -0500)]
Call separate SMT engine for single invocation sygus (#3151)

5 years agocmake: Export CVC4 library interface. (#3179)
Mathias Preiner [Wed, 14 Aug 2019 17:56:26 +0000 (10:56 -0700)]
cmake: Export CVC4 library interface. (#3179)

5 years agoEnable Clang-Format for Java (#3064)
Andres Noetzli [Wed, 14 Aug 2019 17:03:21 +0000 (10:03 -0700)]
Enable Clang-Format for Java (#3064)

5 years agoMinor cleaning of sygus term database (#3159)
Andrew Reynolds [Wed, 14 Aug 2019 16:17:09 +0000 (11:17 -0500)]
Minor cleaning of sygus term database (#3159)

5 years agoFix issue related to higher-order purification in term database (#3157)
Andrew Reynolds [Wed, 14 Aug 2019 15:37:03 +0000 (10:37 -0500)]
Fix issue related to higher-order purification in term database (#3157)

5 years agoSmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)
Aina Niemetz [Wed, 14 Aug 2019 01:20:59 +0000 (18:20 -0700)]
SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)

5 years agoNew C++ API: Add checks and tests for Solver::simplify. (#3170)
Aina Niemetz [Fri, 9 Aug 2019 00:19:05 +0000 (17:19 -0700)]
New C++ API: Add checks and tests for Solver::simplify. (#3170)

5 years agoNew C++ API: Fix test names of solver_black unit test. (#3170)
Aina Niemetz [Fri, 9 Aug 2019 00:08:50 +0000 (17:08 -0700)]
New C++ API: Fix test names of solver_black unit test. (#3170)

5 years agoNew C++ API: Reorganize Solver code (move only). (#3170)
Aina Niemetz [Thu, 8 Aug 2019 22:19:05 +0000 (15:19 -0700)]
New C++ API: Reorganize Solver code (move only). (#3170)

5 years ago Track sygus variable to term relationship via attribute (#3182)
Andrew Reynolds [Tue, 13 Aug 2019 20:08:00 +0000 (15:08 -0500)]
 Track sygus variable to term relationship via attribute (#3182)

5 years agoUpdate option to disable symbolic definitions in strings (#3180)
Andrew Reynolds [Tue, 13 Aug 2019 19:08:11 +0000 (14:08 -0500)]
Update option to disable symbolic definitions in strings (#3180)

5 years agoAdd string rewrite involving allchar stars (#3167)
Andrew Reynolds [Tue, 13 Aug 2019 18:19:18 +0000 (13:19 -0500)]
Add string rewrite involving allchar stars (#3167)

5 years agoProperly implement logic info for separation logic (#3176)
Andrew Reynolds [Tue, 13 Aug 2019 16:29:47 +0000 (11:29 -0500)]
Properly implement logic info for separation logic (#3176)

5 years agoImplement check abduct feature (#3152)
Andrew Reynolds [Tue, 13 Aug 2019 15:39:45 +0000 (10:39 -0500)]
Implement check abduct feature (#3152)

5 years agoIntroduce smt2 parsing utility ParseOp and refactor (#3165)
Andrew Reynolds [Tue, 13 Aug 2019 15:08:27 +0000 (10:08 -0500)]
Introduce smt2 parsing utility ParseOp and refactor (#3165)

5 years agoClean smt2 parsing of named attributes (#3172)
Andrew Reynolds [Mon, 12 Aug 2019 20:40:26 +0000 (15:40 -0500)]
Clean smt2 parsing of named attributes (#3172)

5 years ago Give rewrite engine pointer to conflict-based instantiation module (#3174)
Andrew Reynolds [Mon, 12 Aug 2019 19:23:31 +0000 (14:23 -0500)]
 Give rewrite engine pointer to conflict-based instantiation module (#3174)

5 years agoNew C++ API: Add documentation/guidelines for API guards. (#3178)
Aina Niemetz [Sun, 11 Aug 2019 21:08:30 +0000 (14:08 -0700)]
New C++ API: Add documentation/guidelines for API guards. (#3178)

5 years agoNew C++ API: Add templated getIndices method for OpTerm (#3073)
makaimann [Sun, 11 Aug 2019 16:07:31 +0000 (09:07 -0700)]
New C++ API: Add templated getIndices method for OpTerm (#3073)

* Implement templated getIndices method for OpTerm

* Add getIndices unit tests

* Update src/api/cvc4cpp.cpp

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update src/api/cvc4cpp.cpp

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add comment about DIVISIBLE_OP

* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add exception checks to other unit tests (instead of having its own function)

* Fix unit test names in opterm_black.h

* Add description to docstring for getIndices

* Formatting

* Clang format older commits

* Use '-' in docstring list to match other docstrings

* Support creating DIVISIBLE_OP with a string (for arbitrary precision integers)

* Move mkOpTerm(DIVISIBLE_OP, <str>) test to solver_black.h

* Fix pointer access

* Replace switch statement with if statement

* Guard string input for CVC4::Integer in mkOpTerm for consistency on GMP/CLN back-end

5 years agoSimplify how defined functions are tracked during parsing (#3177)
Andrew Reynolds [Sat, 10 Aug 2019 19:26:02 +0000 (14:26 -0500)]
Simplify how defined functions are tracked during parsing (#3177)

5 years agoAdd option to only dump unsolved queries for --sygus-query-gen (#3173)
Andrew Reynolds [Sat, 10 Aug 2019 17:56:05 +0000 (12:56 -0500)]
Add option to only dump unsolved queries for --sygus-query-gen (#3173)

5 years agoReorganize includes for quantifiers engine (#3169)
Andrew Reynolds [Thu, 8 Aug 2019 21:49:08 +0000 (16:49 -0500)]
Reorganize includes for quantifiers engine (#3169)

5 years agoAdd subdirectories to contrib for competition scripts (#3164)
Andrew Reynolds [Thu, 8 Aug 2019 20:16:41 +0000 (15:16 -0500)]
Add subdirectories to contrib for competition scripts (#3164)

5 years agoFix issues with Ninja build system and add configure option. (#3166)
Mathias Preiner [Thu, 8 Aug 2019 18:19:23 +0000 (11:19 -0700)]
Fix issues with Ninja build system and add configure option. (#3166)

Adds option --ninja to configure.sh.

5 years agoNew C++ API: Add checks and tests for push/pop. (#3121)
Aina Niemetz [Wed, 15 May 2019 20:03:24 +0000 (13:03 -0700)]
New C++ API: Add checks and tests for push/pop. (#3121)

5 years agoNew C++ API: Introduce macros for try-catch blocks in Solver. (#3121)
Aina Niemetz [Mon, 13 May 2019 20:51:07 +0000 (13:51 -0700)]
New C++ API: Introduce macros for try-catch blocks in Solver. (#3121)

5 years agoNew C++ API: Fix branch prediction in CHECK macros. (#3161)
Aina Niemetz [Tue, 6 Aug 2019 23:25:07 +0000 (16:25 -0700)]
New C++ API: Fix branch prediction in CHECK macros. (#3161)

5 years agoProperly parse qualified identifiers (#3111)
Andrew Reynolds [Tue, 6 Aug 2019 22:18:50 +0000 (17:18 -0500)]
Properly parse qualified identifiers  (#3111)

5 years agoScripts for CASC-27 (#3163)
Haniel Barbosa [Tue, 6 Aug 2019 19:14:36 +0000 (14:14 -0500)]
Scripts for CASC-27 (#3163)

5 years agoFix drat signature wrt side condition return types. (#3160)
Andrew Reynolds [Tue, 6 Aug 2019 00:28:54 +0000 (19:28 -0500)]
Fix drat signature wrt side condition return types. (#3160)

5 years agoRemove forward declarations in quantifiers engine (#3156)
Andrew Reynolds [Mon, 5 Aug 2019 17:04:02 +0000 (12:04 -0500)]
Remove forward declarations in quantifiers engine (#3156)

5 years agoFix regression script for incremental SMT-LIB v2 benchmarks. (#3155)
Mathias Preiner [Sun, 4 Aug 2019 07:04:20 +0000 (00:04 -0700)]
Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)

The regression script did not extract the expected status from incremental
SMT-LIB v2 benchmarks correctly if status was given via (set-info :status ...). The
script used re.search for finding the status, which only searches for
the first occurrence instead of finding all (set-info :status ...).

This commit fixes the issue by using re.findall instead.

5 years agoFix printing issue related to nested quotes (#3154)
Andrew Reynolds [Sat, 3 Aug 2019 16:56:51 +0000 (11:56 -0500)]
Fix printing issue related to nested quotes (#3154)

5 years agoCollapse @ chains in SMT2 printer (#3140)
Haniel Barbosa [Sat, 3 Aug 2019 15:40:36 +0000 (10:40 -0500)]
Collapse @ chains in SMT2 printer (#3140)

5 years agoUpdate CaDiCaL to version 1.0.3. (#3137)
Mathias Preiner [Fri, 2 Aug 2019 23:20:45 +0000 (16:20 -0700)]
Update CaDiCaL to version 1.0.3. (#3137)

* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()

Fixes #3011

5 years agoFlip the polarity of the argument of get-abduct (#3153)
Andrew Reynolds [Fri, 2 Aug 2019 21:04:43 +0000 (16:04 -0500)]
Flip the polarity of the argument of get-abduct (#3153)

5 years agoAdd better Python detection for contrib scripts. (#3150)
Mathias Preiner [Fri, 2 Aug 2019 20:49:03 +0000 (13:49 -0700)]
Add better Python detection for contrib scripts. (#3150)

5 years ago Move basic sygus enumerator to its own file (#3149)
Andrew Reynolds [Fri, 2 Aug 2019 20:25:26 +0000 (15:25 -0500)]
 Move basic sygus enumerator to its own file (#3149)

5 years agoRemove simplification specialized for sygus si solution reconstruction (#3147)
Andrew Reynolds [Fri, 2 Aug 2019 19:34:38 +0000 (14:34 -0500)]
Remove simplification specialized for sygus si solution reconstruction (#3147)

5 years agoSupport default sygus grammar for strings (#3148)
Andrew Reynolds [Fri, 2 Aug 2019 18:56:39 +0000 (13:56 -0500)]
Support default sygus grammar for strings (#3148)

5 years agoThrow option exception when track inst lemmas is not used (#3145)
Andrew Reynolds [Fri, 2 Aug 2019 17:01:27 +0000 (12:01 -0500)]
Throw option exception when track inst lemmas is not used (#3145)

5 years agoFix solution filtering for streaming abducts (#3143)
Andrew Reynolds [Fri, 2 Aug 2019 14:40:36 +0000 (09:40 -0500)]
Fix solution filtering for streaming abducts (#3143)

5 years agoFix BVGauss unit tests. (#3142)
Mathias Preiner [Fri, 2 Aug 2019 05:55:25 +0000 (22:55 -0700)]
Fix BVGauss unit tests. (#3142)

pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the
anonymous namespace, which resulted in ODR (one definition rule)
violations reported by ASAN.

This commit exposes the functionality required in the unit tests as
private static members of the BVGauss class. Since this is a white unit
test, we can access private members in the tests.

5 years agoEnable sygus logic when produce-abducts is true (#3144)
Andrew Reynolds [Fri, 2 Aug 2019 03:11:08 +0000 (22:11 -0500)]
Enable sygus logic when produce-abducts is true (#3144)

5 years agoUse python realpath instead of relying on shell realpath (#3117)
makaimann [Fri, 2 Aug 2019 00:52:37 +0000 (17:52 -0700)]
Use python realpath instead of relying on shell realpath (#3117)

* Use a custom implementation instead of relying on realpath, because it doesn't exist on Mac

* Use local variables and move portable_realpath to its own file

* Replace portable_realpath with python realpath

* Consistent command substitution

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
* Substitute pwd directly

5 years agoFix memory leak in rewriter (debug mode). (#3141)
Mathias Preiner [Thu, 1 Aug 2019 20:07:18 +0000 (13:07 -0700)]
Fix memory leak in rewriter (debug mode). (#3141)

s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit
wraps s_rewriteStack in a std::unique_ptr to automatically free the
memory.

5 years agoMove some generic utilities out of quantifiers (#3139)
Andrew Reynolds [Thu, 1 Aug 2019 14:26:26 +0000 (09:26 -0500)]
Move some generic utilities out of quantifiers (#3139)

5 years ago Regular expression intersection modes (#3134)
Andrew Reynolds [Thu, 1 Aug 2019 14:08:46 +0000 (09:08 -0500)]
 Regular expression intersection modes (#3134)

5 years agoParsing THF and adding several regressions (#3131)
Haniel Barbosa [Wed, 31 Jul 2019 17:17:29 +0000 (12:17 -0500)]
Parsing THF and adding several regressions (#3131)

5 years agoadding bv_gauss unit test to build files (#3135)
yoni206 [Wed, 31 Jul 2019 16:37:49 +0000 (09:37 -0700)]
adding bv_gauss unit test to build files (#3135)

5 years agoAdd some missing cases in evaluator (#3133)
Andrew Reynolds [Wed, 31 Jul 2019 16:01:33 +0000 (11:01 -0500)]
Add some missing cases in evaluator (#3133)

5 years agoEager conflict detection in strings based on constant prefix/suffix (#3110)
Andrew Reynolds [Wed, 31 Jul 2019 05:24:25 +0000 (00:24 -0500)]
Eager conflict detection in strings based on constant prefix/suffix (#3110)

5 years ago Track solver execution mode (#3132)
Andrew Reynolds [Tue, 30 Jul 2019 18:52:28 +0000 (13:52 -0500)]
 Track solver execution mode (#3132)

5 years agoCode to activate hoelim preprocessing pass (#3129)
Haniel Barbosa [Tue, 30 Jul 2019 15:21:01 +0000 (10:21 -0500)]
Code to activate hoelim preprocessing pass (#3129)

5 years agoMinor improvement for rewriter for str.replace (#3124)
Andrew Reynolds [Tue, 30 Jul 2019 14:57:33 +0000 (09:57 -0500)]
Minor improvement for rewriter for str.replace (#3124)

5 years ago Handle RE intersections modulo equality (#3120)
Andrew Reynolds [Tue, 30 Jul 2019 14:17:00 +0000 (09:17 -0500)]
 Handle RE intersections modulo equality (#3120)