cvc5.git
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)

6 years agoFix rewriter for lambda (#2211)
Andrew Reynolds [Thu, 26 Jul 2018 19:48:40 +0000 (14:48 -0500)]
Fix rewriter for lambda (#2211)

The rewriter for lambda is currently too aggressive, there are cases like:

lambda xy. x = y

that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to:

lambda fv_1 fv_2. fv_1 = y

where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free.

To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR).

Some parts of the code were formatted as a result.

6 years ago Fix a few issues in the sygus sampler related to evaluation (#2215)
Andrew Reynolds [Thu, 26 Jul 2018 19:27:37 +0000 (14:27 -0500)]
 Fix a few issues in the sygus sampler related to evaluation (#2215)

6 years agoAvoid explicit dependency on Python 3 (#2195)
ayveejay [Thu, 26 Jul 2018 18:27:46 +0000 (19:27 +0100)]
Avoid explicit dependency on Python 3 (#2195)

6 years agoNew C++ API: Third batch of commands (SMT-LIB). (#2212)
Aina Niemetz [Thu, 26 Jul 2018 17:00:21 +0000 (10:00 -0700)]
New C++ API: Third batch of commands (SMT-LIB). (#2212)

6 years agoNew C++ API: Second batch of commands (SMT-LIB). (#2201)
Aina Niemetz [Thu, 26 Jul 2018 16:00:18 +0000 (09:00 -0700)]
New C++ API: Second batch of commands (SMT-LIB). (#2201)

6 years agoChanging ArithIteUtils to use CDInsertHashMap. (#2206)
Tim King [Wed, 25 Jul 2018 23:56:34 +0000 (16:56 -0700)]
Changing ArithIteUtils to use CDInsertHashMap. (#2206)

 This is 1/3 PRs for deprecating CDTrailHashMap.

6 years agoRemoving support for CDHashMap::iterator's postfix increment. (#2208)
Tim King [Wed, 25 Jul 2018 23:13:18 +0000 (16:13 -0700)]
Removing support for CDHashMap::iterator's postfix increment. (#2208)

6 years ago Move reg exp rewrites from prerewrite to postrewrite (#2204)
Andrew Reynolds [Wed, 25 Jul 2018 17:34:32 +0000 (12:34 -0500)]
 Move reg exp rewrites from prerewrite to postrewrite (#2204)

6 years agoPerforming clang-format on the original change-set of #2194 (#2203)
ayveejay [Wed, 25 Jul 2018 16:59:05 +0000 (17:59 +0100)]
Performing clang-format on the original change-set of #2194 (#2203)

6 years agoUse CryptoMiniSat 5.6.3. (#2205)
Mathias Preiner [Wed, 25 Jul 2018 16:40:22 +0000 (09:40 -0700)]
Use CryptoMiniSat 5.6.3. (#2205)

6 years agoImprovements to sets + cardinality + quantifiers (#2200)
Andrew Reynolds [Tue, 24 Jul 2018 22:01:38 +0000 (17:01 -0500)]
Improvements to sets + cardinality + quantifiers (#2200)

6 years agoAdding API access methods to get heap/nil expressions when using separation logic...
ayveejay [Tue, 24 Jul 2018 21:16:16 +0000 (22:16 +0100)]
Adding API access methods to get heap/nil expressions when using separation logic (#2194)

6 years ago New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)
Aina Niemetz [Tue, 24 Jul 2018 17:11:24 +0000 (10:11 -0700)]
 New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)

6 years ago Improve rewriter for regular expression concatenation (#2196)
Andrew Reynolds [Mon, 23 Jul 2018 23:02:36 +0000 (18:02 -0500)]
 Improve rewriter for regular expression concatenation (#2196)

6 years agoGeneralize symmetry detection for 1 symmetry variable mapped to n input variables...
Andrew Reynolds [Mon, 23 Jul 2018 22:39:12 +0000 (17:39 -0500)]
Generalize symmetry detection for 1 symmetry variable mapped to n input variables  (#1888)

6 years agoNew C++ API: Implementation of Solver class: OpTerm handling. (#2164)
Aina Niemetz [Mon, 23 Jul 2018 21:38:37 +0000 (14:38 -0700)]
New C++ API: Implementation of Solver class: OpTerm handling. (#2164)

6 years agoNew C++ API: declare-datatype. (#2166)
Aina Niemetz [Mon, 23 Jul 2018 19:29:03 +0000 (12:29 -0700)]
New C++ API: declare-datatype. (#2166)

6 years ago sygusComp2018: add regressions (#2191)
Andrew Reynolds [Mon, 23 Jul 2018 18:36:53 +0000 (13:36 -0500)]
 sygusComp2018: add regressions (#2191)

6 years agoFix warning in sygus PBE (#2190)
Andrew Reynolds [Mon, 23 Jul 2018 17:01:02 +0000 (12:01 -0500)]
Fix warning in sygus PBE (#2190)

6 years ago sygusComp2018: Improvements to CEGIS loop (#2187)
Andrew Reynolds [Sun, 22 Jul 2018 04:50:57 +0000 (23:50 -0500)]
 sygusComp2018: Improvements to CEGIS loop (#2187)

6 years agoOptimizations and fixes for computing whether a type is finite (#2179)
Andrew Reynolds [Sat, 21 Jul 2018 14:19:31 +0000 (09:19 -0500)]
Optimizations and fixes for computing whether a type is finite (#2179)

6 years ago sygusComp2018: refactor and improve sygus io utility (#2185)
Andrew Reynolds [Sat, 21 Jul 2018 12:27:28 +0000 (07:27 -0500)]
 sygusComp2018: refactor and improve sygus io utility (#2185)

6 years agoRemove --no-check-proofs and --no-check-unsat-cores from a satisfiable test (#2184)
yoni206 [Sat, 21 Jul 2018 12:02:01 +0000 (05:02 -0700)]
Remove --no-check-proofs and --no-check-unsat-cores from a satisfiable test (#2184)

6 years agoCleanup and additions for candidate generator (#2173)
Andrew Reynolds [Fri, 20 Jul 2018 23:42:25 +0000 (01:42 +0200)]
Cleanup and additions for candidate generator (#2173)

6 years ago sygusComp2018: minor changes to repair constant utility (#2110)
Andrew Reynolds [Fri, 20 Jul 2018 20:34:18 +0000 (22:34 +0200)]
 sygusComp2018: minor changes to repair constant utility (#2110)

6 years ago sygusComp2018: pbe multi-enumerator fairness option (#2178)
Andrew Reynolds [Tue, 17 Jul 2018 23:51:28 +0000 (01:51 +0200)]
 sygusComp2018: pbe multi-enumerator fairness option (#2178)

6 years agoRefactor sep-pre-skolem-emp preprocessing pass
yoni206 [Tue, 17 Jul 2018 21:20:46 +0000 (14:20 -0700)]
Refactor sep-pre-skolem-emp preprocessing pass

6 years agoMinor cleanup and fixes for conflict-based instantiation (#2123)
Andrew Reynolds [Tue, 17 Jul 2018 17:53:14 +0000 (19:53 +0200)]
Minor cleanup and fixes for conflict-based instantiation (#2123)

6 years agoDo extended rewrite on results of quantifier elimination. (#2119)
Andrew Reynolds [Tue, 17 Jul 2018 17:07:22 +0000 (19:07 +0200)]
Do extended rewrite on results of quantifier elimination. (#2119)

6 years ago Purify applications of exp to transcendental arguments (#2097)
Andrew Reynolds [Tue, 17 Jul 2018 16:25:13 +0000 (18:25 +0200)]
 Purify applications of exp to transcendental arguments (#2097)

6 years ago sygusComp2018: update policies for solution reconstruction (#2109)
Andrew Reynolds [Tue, 17 Jul 2018 15:37:03 +0000 (17:37 +0200)]
 sygusComp2018: update policies for solution reconstruction (#2109)

6 years agosygusComp2018: Improvements to datatypes sygus solver (#2177)
Andrew Reynolds [Tue, 17 Jul 2018 14:17:43 +0000 (16:17 +0200)]
sygusComp2018: Improvements to datatypes sygus solver (#2177)

6 years agosygusComp 2018: updates to sygus term database (#2170)
Andrew Reynolds [Tue, 17 Jul 2018 11:02:32 +0000 (13:02 +0200)]
sygusComp 2018: updates to sygus term database (#2170)

6 years agoAvoid ambiguous overloads in BitVector (#2169)
Andres Noetzli [Sun, 15 Jul 2018 11:25:57 +0000 (04:25 -0700)]
Avoid ambiguous overloads in BitVector (#2169)

`long` is a 32-bit integer on Windows. CVC4's BitVector class had a
constructor for `unsigned int` and `unsigned long`, which lead to issues
with the new CVC4 C++ API because the two constructors were ambiguous
overloads. This commit changes the constructors to use `uint32_t` and
`uint64_t`, which are plattform independent and more explicit (mirroring

6 years agoexportTo only if needed for --sygus-rr-synth-check (#2168)
Andres Noetzli [Sat, 14 Jul 2018 08:45:58 +0000 (01:45 -0700)]
exportTo only if needed for --sygus-rr-synth-check (#2168)

6 years agosygusComp2018: update semantics for declare-fun in sygus. (#2102)
Andrew Reynolds [Sat, 14 Jul 2018 08:08:11 +0000 (10:08 +0200)]
sygusComp2018: update semantics for declare-fun in sygus. (#2102)

6 years agoFix and improve grammar normalization for any constant. (#2101)
Andrew Reynolds [Fri, 13 Jul 2018 22:30:04 +0000 (00:30 +0200)]
Fix and improve grammar normalization for any constant. (#2101)

6 years agoProperly clean up assertion stack in CnfProof (#2147)
Andres Noetzli [Fri, 13 Jul 2018 20:24:43 +0000 (13:24 -0700)]
Properly clean up assertion stack in CnfProof (#2147)

Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.

6 years ago sygusComp2018: optimization for collect model info (#2105)
Andrew Reynolds [Fri, 13 Jul 2018 15:36:01 +0000 (17:36 +0200)]
 sygusComp2018: optimization for collect model info (#2105)

6 years agoNew C++ API: Minor reorder. (#2163)
Aina Niemetz [Fri, 13 Jul 2018 10:04:49 +0000 (03:04 -0700)]
New C++ API: Minor reorder. (#2163)

6 years agoNew C++ API: Implementation of datatype classes. (#2142)
Aina Niemetz [Fri, 13 Jul 2018 08:57:24 +0000 (01:57 -0700)]
New C++ API: Implementation of datatype classes. (#2142)

6 years agoNew C++ API: Implementation of Solver class: Consts handling. (#2145)
Aina Niemetz [Fri, 13 Jul 2018 08:06:18 +0000 (01:06 -0700)]
New C++ API: Implementation of Solver class: Consts handling. (#2145)

6 years agoMove rewrite to pass (#2128)
Caleb Donovick [Wed, 11 Jul 2018 00:27:16 +0000 (17:27 -0700)]
Move rewrite to pass (#2128)

6 years agoAdd more sophisticated floating-point sampler (#2155)
Andres Noetzli [Sun, 8 Jul 2018 20:38:45 +0000 (13:38 -0700)]
Add more sophisticated floating-point sampler (#2155)

This commit adds a floating-point sampler inspired by PyMPF [0]. It also
creates a new Sampler class that can be used for creating random values
of different sorts (currently BV and FP values).

[0] https://github.com/florianschanda/PyMPF

6 years ago sygusComp2018: improve extended rewriter for Bool (#2107)
Andrew Reynolds [Sat, 7 Jul 2018 06:49:11 +0000 (07:49 +0100)]
 sygusComp2018: improve extended rewriter for Bool (#2107)

6 years agoSplit ext theory to own file and document (#1809)
Andrew Reynolds [Fri, 6 Jul 2018 19:58:31 +0000 (20:58 +0100)]
Split ext theory to own file and document (#1809)

6 years agoFeature/fp rewrite improvement (#2154)
Martin [Fri, 6 Jul 2018 18:22:57 +0000 (19:22 +0100)]
Feature/fp rewrite improvement (#2154)

6 years agoNew C++ API: Implementation of Solver class: Term handling. (#2144)
Aina Niemetz [Fri, 6 Jul 2018 17:26:00 +0000 (10:26 -0700)]
New C++ API: Implementation of Solver class: Term handling. (#2144)

6 years agoNew C++ API: Implementation of Solver class: Sort handling. (#2143)
Aina Niemetz [Fri, 6 Jul 2018 16:53:21 +0000 (09:53 -0700)]
New C++ API: Implementation of Solver class: Sort handling. (#2143)

6 years agoAdd option for timeout for rewrite candidate check (#2156)
Andres Noetzli [Fri, 6 Jul 2018 11:03:58 +0000 (04:03 -0700)]
Add option for timeout for rewrite candidate check (#2156)

6 years agosygusComp2018: simplify beta reduction in uf rewriter. (#2106)
Andrew Reynolds [Fri, 6 Jul 2018 07:20:23 +0000 (08:20 +0100)]
sygusComp2018: simplify beta reduction in uf rewriter. (#2106)

This is PR 8/18 from the sygus comp 2018 branch (https://github.com/ajreynol/CVC4/tree/sygusComp2018-2).

I am not sure how it is possible in any circumstance that the complication in the comment I am deleting would ever happen, without doing something very strange. I think it is referring to some sort of inter-dependence between macro expansion + beta-reductions. This should not concern the rewriter. Here is the commit that introduced it: bdaa304.

6 years ago Make string length lemmas more robust to rewriting (#2150)
Andrew Reynolds [Thu, 5 Jul 2018 16:22:53 +0000 (17:22 +0100)]
 Make string length lemmas more robust to rewriting (#2150)

6 years agoMinor changes to sygus-rr utilities to support floating point rewrites (#2148)
Andrew Reynolds [Thu, 5 Jul 2018 03:23:19 +0000 (04:23 +0100)]
Minor changes to sygus-rr utilities to support floating point rewrites (#2148)

6 years agosygusComp2018: Improve string rewriter (#2141)
Andres Noetzli [Thu, 5 Jul 2018 02:32:29 +0000 (19:32 -0700)]
sygusComp2018: Improve string rewriter (#2141)

6 years agoMore cleanup in strings (#2138)
Andrew Reynolds [Wed, 4 Jul 2018 15:34:17 +0000 (16:34 +0100)]
More cleanup in strings (#2138)

6 years agoNew C++ API: Implementation of datatype declaration classes. (#2136)
Aina Niemetz [Wed, 4 Jul 2018 15:10:27 +0000 (08:10 -0700)]
New C++ API: Implementation of datatype declaration classes. (#2136)

6 years agoReorganize candidate rewrite rule filtering (#2116)
Andrew Reynolds [Wed, 4 Jul 2018 13:31:14 +0000 (14:31 +0100)]
Reorganize candidate rewrite rule filtering (#2116)

6 years agoRemove unused CDVector (#2139)
Andres Noetzli [Wed, 4 Jul 2018 10:58:24 +0000 (03:58 -0700)]
Remove unused CDVector (#2139)

6 years agoNew C++ API: Implementation of OpTerm. (#2132)
Aina Niemetz [Wed, 4 Jul 2018 08:31:02 +0000 (01:31 -0700)]
New C++ API: Implementation of OpTerm. (#2132)

6 years agoFix fmf-fun for non-equality function definitions (#2134)
Andrew Reynolds [Wed, 4 Jul 2018 05:21:01 +0000 (00:21 -0500)]
Fix fmf-fun for non-equality function definitions (#2134)

Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.

6 years agoNew C++ API: Implementation of Term. (#2131)
Aina Niemetz [Tue, 3 Jul 2018 16:27:59 +0000 (09:27 -0700)]
New C++ API: Implementation of Term. (#2131)

6 years agoNew C++ API: Implementation of Kind maps. (#2130)
Aina Niemetz [Tue, 3 Jul 2018 15:59:35 +0000 (08:59 -0700)]
New C++ API: Implementation of Kind maps. (#2130)