cvc5.git
6 years agoFix for issue #2002 (#2012)
Andres Noetzli [Wed, 30 May 2018 22:02:29 +0000 (15:02 -0700)]
Fix for issue #2002 (#2012)

6 years agoFixes for quantifiers + incremental (#2009)
Andrew Reynolds [Wed, 30 May 2018 20:34:05 +0000 (15:34 -0500)]
Fixes for quantifiers + incremental (#2009)

6 years ago[SMT-COMP] Print non-(un)sat output to stderr (#2019)
Andres Noetzli [Wed, 30 May 2018 19:04:38 +0000 (12:04 -0700)]
[SMT-COMP] Print non-(un)sat output to stderr (#2019)

In the SMT-COMP runscript, we are currently discarding output on stdout
that is not "sat" or "unsat" when using `trywith` (this is not the case
with `finishwith`). Due to this, our tests might miss cases where CVC4
fails and prints an error on stdout when using `trywith`. This commit
changes the script to print output other than "sat" or "unsat" to
stderr.

6 years agoNormalize negated bit-vector terms over equalities. (#2017)
Mathias Preiner [Wed, 30 May 2018 18:42:40 +0000 (11:42 -0700)]
Normalize negated bit-vector terms over equalities. (#2017)

6 years agoUse CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)
Mathias Preiner [Wed, 30 May 2018 18:17:35 +0000 (11:17 -0700)]
Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)

6 years agoDraft run script for strings smt comp 2018. (#2016)
Andrew Reynolds [Wed, 30 May 2018 17:49:46 +0000 (12:49 -0500)]
Draft run script for strings smt comp 2018. (#2016)

6 years ago Make user's SMT2 version override file version (#2004)
Andres Noetzli [Tue, 29 May 2018 18:25:13 +0000 (11:25 -0700)]
 Make user's SMT2 version override file version (#2004)

6 years agoDisable minisat elimination when nonlinear is enabled (#2006)
Andrew Reynolds [Tue, 29 May 2018 17:46:35 +0000 (12:46 -0500)]
Disable minisat elimination when nonlinear is enabled (#2006)

6 years agoTrack input language in a single place (#2003)
Andres Noetzli [Tue, 29 May 2018 12:43:20 +0000 (05:43 -0700)]
Track input language in a single place (#2003)

6 years agoBuiltin evaluation functions for sygus (#1991)
Andrew Reynolds [Mon, 28 May 2018 15:35:17 +0000 (10:35 -0500)]
Builtin evaluation functions for sygus (#1991)

6 years agoFix cegqi assertions for quantified non-linear cases. (#1999)
Andrew Reynolds [Sun, 27 May 2018 20:10:08 +0000 (15:10 -0500)]
Fix cegqi assertions for quantified non-linear cases. (#1999)

6 years agoFix no-cbqi-innermost option name in run script (#1994)
Andres Noetzli [Sun, 27 May 2018 18:39:36 +0000 (11:39 -0700)]
Fix no-cbqi-innermost option name in run script (#1994)

6 years agoUpdate SymFPU. (#1992)
Mathias Preiner [Sat, 26 May 2018 22:56:16 +0000 (15:56 -0700)]
Update SymFPU. (#1992)

6 years agoReenable repair const (#1983)
Andrew Reynolds [Fri, 25 May 2018 21:19:58 +0000 (16:19 -0500)]
Reenable repair const (#1983)

6 years agoMiniSat: Be more careful about running proof code (#1982)
Andres Noetzli [Fri, 25 May 2018 20:26:16 +0000 (13:26 -0700)]
MiniSat: Be more careful about running proof code (#1982)

In `addClause_()`, we were checking the condition `ca[confl].size() ==
1` regardless if proofs were enabled or not, even though both branches
of the if statement only do something when proofs are enabled. This lead
to issue #1978 occurring even when not generating proofs. Note: This
commit is *not* a fix for #1978 but it makes sure that the issue does
not occur when not generating proofs/unsat cores.

6 years agoAdd QF_BV configuration for SMTCOMP'18. (#1981)
Mathias Preiner [Fri, 25 May 2018 18:02:32 +0000 (11:02 -0700)]
Add QF_BV configuration for SMTCOMP'18. (#1981)

6 years agoFix various nl assertions. (#1980)
Andrew Reynolds [Fri, 25 May 2018 16:46:56 +0000 (11:46 -0500)]
Fix various nl assertions. (#1980)

6 years agoFix (#1979)
Andrew Reynolds [Fri, 25 May 2018 00:55:47 +0000 (19:55 -0500)]
Fix (#1979)

6 years agoImprove simple constant symmetry breaking for sygus (#1977)
Andrew Reynolds [Thu, 24 May 2018 22:28:59 +0000 (17:28 -0500)]
Improve simple constant symmetry breaking for sygus (#1977)

6 years agoFix compiler warnings (#1959)
Andres Noetzli [Thu, 24 May 2018 20:01:33 +0000 (13:01 -0700)]
Fix compiler warnings (#1959)

6 years agoFix (#1975)
Andrew Reynolds [Thu, 24 May 2018 19:24:44 +0000 (14:24 -0500)]
Fix (#1975)

6 years agoFixes for non-linear check model (#1974)
Andrew Reynolds [Thu, 24 May 2018 19:01:44 +0000 (14:01 -0500)]
Fixes for non-linear check model (#1974)

6 years agoFix nl regression for unsat cores. (#1973)
Andrew Reynolds [Thu, 24 May 2018 15:03:23 +0000 (10:03 -0500)]
Fix nl regression for unsat cores. (#1973)

6 years agoRemove spurious assertion in nonlinear extension (#1972)
Andrew Reynolds [Thu, 24 May 2018 01:41:11 +0000 (20:41 -0500)]
Remove spurious assertion in nonlinear extension (#1972)

6 years agoTowards better symbolic enumeration in SyGuS (#1971)
Haniel Barbosa [Wed, 23 May 2018 23:18:51 +0000 (18:18 -0500)]
Towards better symbolic enumeration in SyGuS (#1971)

6 years agoAdd notions of evaluated kinds in TheoryModel (#1947)
Andrew Reynolds [Wed, 23 May 2018 20:44:50 +0000 (15:44 -0500)]
Add notions of evaluated kinds in TheoryModel (#1947)

6 years agoRemove ProofProxy (#1965)
Andres Noetzli [Wed, 23 May 2018 13:53:06 +0000 (06:53 -0700)]
Remove ProofProxy (#1965)

6 years agoGeneralize check-model in NonLinearExtension for quadratic equations (#1892)
Andrew Reynolds [Wed, 23 May 2018 12:00:40 +0000 (07:00 -0500)]
Generalize check-model in NonLinearExtension for quadratic equations (#1892)

6 years agoSet same options for proofs as for unsat cores (#1957)
Andres Noetzli [Wed, 23 May 2018 05:20:59 +0000 (22:20 -0700)]
Set same options for proofs as for unsat cores (#1957)

In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.

6 years agoRepair constants using symbolic constructors (#1960)
Andrew Reynolds [Wed, 23 May 2018 01:27:32 +0000 (20:27 -0500)]
Repair constants using symbolic constructors (#1960)

6 years agoParse error for sygus grammar term with multiple let bodies (#1961)
Andrew Reynolds [Tue, 22 May 2018 23:12:54 +0000 (18:12 -0500)]
Parse error for sygus grammar term with multiple let bodies (#1961)

6 years agoDisable symmetry breaker for unsat cores (#1958)
Andres Noetzli [Tue, 22 May 2018 18:43:15 +0000 (11:43 -0700)]
Disable symmetry breaker for unsat cores (#1958)

Currently, --check-unsat-cores fails for one of our regressions. It
turns out that the issue is due to preprocessing done by the symmetry
breaker.  The symmetry breaker does not add dependencies and thus the
generated unsat core is incomplete/wrong. This commit disables the
symmetry breaker when we are generating unsat cores (it was previously
only disabled when generating proofs). Fixes issue #1953.

6 years agoMake sygus infer find function definitions (#1951)
Andrew Reynolds [Tue, 22 May 2018 18:08:31 +0000 (13:08 -0500)]
Make sygus infer find function definitions (#1951)

6 years agoInfrastructure for strings strategies (#1883)
Andrew Reynolds [Tue, 22 May 2018 01:54:52 +0000 (20:54 -0500)]
Infrastructure for strings strategies (#1883)

6 years agoAdd SymFPU licensing information. (#1952)
Mathias Preiner [Tue, 22 May 2018 00:54:09 +0000 (17:54 -0700)]
Add SymFPU licensing information. (#1952)

6 years agoImprovements in parsing and printing related to mixed int/real (#1879)
Andrew Reynolds [Mon, 21 May 2018 22:52:26 +0000 (17:52 -0500)]
Improvements in parsing and printing related to mixed int/real (#1879)

This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary.  This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).

6 years agoInfrastructure to mark unused sygus strategies (#1950)
Andrew Reynolds [Mon, 21 May 2018 21:33:17 +0000 (16:33 -0500)]
Infrastructure to mark unused sygus strategies  (#1950)

6 years agoHandle IMPLIES in bool-to-bv and test it in regress0 (#1929)
makaimann [Mon, 21 May 2018 21:07:48 +0000 (14:07 -0700)]
Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)

6 years agoRefactor sygus eval unfold (#1946)
Andrew Reynolds [Mon, 21 May 2018 19:09:12 +0000 (14:09 -0500)]
Refactor sygus eval unfold (#1946)

6 years agoRemove Eclipse project files (#1928)
Andres Noetzli [Mon, 21 May 2018 18:37:26 +0000 (21:37 +0300)]
Remove Eclipse project files (#1928)

No one of the core devs is currently using Eclipse, so the Eclipse
project files are essentially useless since they are not guaranteed to
be up-to-date.

6 years agoFix compiler warning in hashsmt example (#1927)
Andres Noetzli [Mon, 21 May 2018 18:00:44 +0000 (21:00 +0300)]
Fix compiler warning in hashsmt example (#1927)

Previously, we were using delete for an array allocated on the heap,
which caused a warning. @dddejan fixed this and other issues in PR #1909
but after @ajreynol fixed the other issues in a separate PR and to not
waste @dddejan's time, I am submitting this fix separately (note: the
fix is slightly different in that it changes the array to a vector,
making a delete[] unnecessary).

6 years agoAssign weight 1 for Boolean variables in SyGuS default grammars (#1948)
Haniel Barbosa [Mon, 21 May 2018 17:21:33 +0000 (12:21 -0500)]
Assign weight 1 for Boolean variables in SyGuS default grammars (#1948)

6 years agoFix file extension (#1919)
Caleb Donovick [Mon, 21 May 2018 15:29:14 +0000 (08:29 -0700)]
Fix file extension (#1919)

* Fix file extension

* Update Makefile

6 years agochanging default (#1944)
Haniel Barbosa [Sat, 19 May 2018 01:49:13 +0000 (20:49 -0500)]
changing default (#1944)

6 years agoCache isInterpretedFinite (#1943)
Andrew Reynolds [Fri, 18 May 2018 22:54:11 +0000 (17:54 -0500)]
Cache isInterpretedFinite (#1943)

6 years agoCegis unif defaults to cegis when no unif (#1942)
Andrew Reynolds [Fri, 18 May 2018 20:02:18 +0000 (15:02 -0500)]
Cegis unif defaults to cegis when no unif (#1942)

6 years agoUnified fairness scheme for cegis unif (#1941)
Andrew Reynolds [Fri, 18 May 2018 17:53:53 +0000 (12:53 -0500)]
Unified fairness scheme for cegis unif (#1941)

6 years agoCatch type errors in sygus grammars for lambda (define-fun) constructors (#1937)
Andrew Reynolds [Thu, 17 May 2018 21:31:30 +0000 (16:31 -0500)]
Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937)

6 years agoFix debugPrint and add regress. (#1934)
Andrew Reynolds [Thu, 17 May 2018 21:03:39 +0000 (16:03 -0500)]
Fix debugPrint and add regress. (#1934)

6 years agoOption to force return values of Bool functions to be constant in CegisUnif (#1930)
Haniel Barbosa [Thu, 17 May 2018 19:47:30 +0000 (14:47 -0500)]
Option to force return values of Bool functions to be constant in CegisUnif (#1930)

6 years agoCegis-specific infrastructure (#1933)
Andrew Reynolds [Thu, 17 May 2018 19:09:46 +0000 (14:09 -0500)]
Cegis-specific infrastructure (#1933)

6 years agoInternal propagation for refinement lemmas (#1932)
Andrew Reynolds [Thu, 17 May 2018 14:23:14 +0000 (09:23 -0500)]
Internal propagation for refinement lemmas (#1932)

6 years agoImprove the separation resolution scheme in cegis unif (#1931)
Andrew Reynolds [Wed, 16 May 2018 23:22:35 +0000 (18:22 -0500)]
Improve the separation resolution scheme in cegis unif (#1931)

6 years agoRefactor static learning preprocessing pass (#1857)
yoni206 [Wed, 16 May 2018 01:17:01 +0000 (18:17 -0700)]
Refactor static learning preprocessing pass (#1857)

6 years agoRefactoring get enumerator values in construct candidate for cegis unif (#1926)
Andrew Reynolds [Tue, 15 May 2018 20:39:27 +0000 (15:39 -0500)]
Refactoring get enumerator values in construct candidate for cegis unif (#1926)

6 years agoadding regressions (#1925)
Haniel Barbosa [Tue, 15 May 2018 19:48:43 +0000 (14:48 -0500)]
adding regressions (#1925)

6 years agoBuilding and refining solutions with dynamic condition generation in CegisUnif (...
Haniel Barbosa [Tue, 15 May 2018 17:20:13 +0000 (12:20 -0500)]
Building and refining solutions with dynamic condition generation in CegisUnif (#1920)

6 years agoFix free variables in cbqi preregister inst. (#1921)
Andrew Reynolds [Tue, 15 May 2018 15:40:29 +0000 (10:40 -0500)]
Fix free variables in cbqi preregister inst. (#1921)

6 years agoFix annotations in regress2. (#1917)
Andrew Reynolds [Tue, 15 May 2018 03:25:40 +0000 (22:25 -0500)]
Fix annotations in regress2. (#1917)

6 years agoMinor improvements to --nl-ext-purify (#1896)
Andrew Reynolds [Tue, 15 May 2018 02:27:07 +0000 (21:27 -0500)]
Minor improvements to --nl-ext-purify (#1896)

6 years ago Incorporating dynamic condition enumeration into cegis unif (#1916)
Andrew Reynolds [Tue, 15 May 2018 00:27:58 +0000 (19:27 -0500)]
 Incorporating dynamic condition enumeration into cegis unif (#1916)

6 years agoFloating point theory solver based on SymFPU (#1895)
Martin [Mon, 14 May 2018 23:18:31 +0000 (00:18 +0100)]
Floating point theory solver based on SymFPU (#1895)

* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.

* Enable the bit-vector theory when setting the logic, not in expandDefinition.

This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.

* Use symfpu to implement the literal floating-point objects.

* Add kinds for bit-blasted components.

* Print the new kinds.

* Typing rules for the new kinds.

* Constant folding for the component kinds.

* Add support for components to the theory solver.

* Add explicit equivalences between classification functions and equalities.

* Use symfpu to do symbolic conversions of floating-point operations.

* Implement conversions via (over-)approximation and refinement.

* Correct a copy and paste error in the generation of uninterpretted functions for conversions.

6 years agoAdd contrib/get-symfpu for downloading symfpu. (#1905)
Mathias Preiner [Mon, 14 May 2018 22:36:52 +0000 (15:36 -0700)]
Add contrib/get-symfpu for downloading symfpu. (#1905)

6 years agoFix purification in SygusUnifRL (#1912)
Haniel Barbosa [Mon, 14 May 2018 20:09:31 +0000 (15:09 -0500)]
Fix purification in SygusUnifRL (#1912)

6 years agoAdd regressions, change defaults. (#1911)
Andrew Reynolds [Mon, 14 May 2018 16:33:14 +0000 (11:33 -0500)]
Add regressions, change defaults. (#1911)

6 years agoFlag to check invariance of entire values in sygus explain (#1908)
Andrew Reynolds [Mon, 14 May 2018 15:29:08 +0000 (10:29 -0500)]
Flag to check invariance of entire values in sygus explain (#1908)

6 years agoSmall change for more sensible line breaking in the output of get-model. (#1910)
Florian Schanda [Mon, 14 May 2018 12:43:42 +0000 (13:43 +0100)]
Small change for more sensible line breaking in the output of get-model. (#1910)

6 years agoRemove obsolete unit test for ackermannization. (#1906)
Aina Niemetz [Fri, 11 May 2018 18:49:45 +0000 (11:49 -0700)]
Remove obsolete unit test for ackermannization. (#1906)

With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete.

6 years agoFix ackermannize preprocessing pass. (#1904)
Aina Niemetz [Fri, 11 May 2018 15:47:02 +0000 (08:47 -0700)]
Fix ackermannize preprocessing pass. (#1904)

Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.

6 years agoSupport multiple sets of command line args in regs (#1902)
Andres Noetzli [Fri, 11 May 2018 02:34:30 +0000 (19:34 -0700)]
Support multiple sets of command line args in regs (#1902)

This commit adds support for multiple sets of command line arguments for
regressions. Each use of a `COMMAND-LINE` directive is interpreted as a
separate set of command line arguments.

6 years agoAlso exclude ITEs from ITE conditions in SygusUnifStrat (#1903)
Haniel Barbosa [Fri, 11 May 2018 01:43:09 +0000 (20:43 -0500)]
Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)

6 years agoExclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)
Andrew Reynolds [Thu, 10 May 2018 22:43:48 +0000 (17:43 -0500)]
Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)

6 years agoSygus repair constants (#1812)
Andrew Reynolds [Thu, 10 May 2018 21:48:51 +0000 (16:48 -0500)]
Sygus repair constants (#1812)

6 years agoStatic learn redundant operators in CegisUnif (#1899)
Haniel Barbosa [Thu, 10 May 2018 20:57:54 +0000 (15:57 -0500)]
Static learn redundant operators in CegisUnif (#1899)

6 years agoAdd ITE to default Boolean sygus grammar (#1898)
Andrew Reynolds [Thu, 10 May 2018 20:35:51 +0000 (15:35 -0500)]
Add ITE to default Boolean sygus grammar (#1898)

6 years agoRefactored BVAckermann preprocessing pass. (#1889)
Aina Niemetz [Thu, 10 May 2018 18:25:19 +0000 (11:25 -0700)]
Refactored BVAckermann preprocessing pass. (#1889)

6 years agoFix priority of decisions for cegis unif (#1897)
Andrew Reynolds [Thu, 10 May 2018 16:38:03 +0000 (11:38 -0500)]
Fix priority of decisions for cegis unif (#1897)

6 years agoPiecing solutions together in CegisUnif (#1894)
Haniel Barbosa [Wed, 9 May 2018 21:45:43 +0000 (16:45 -0500)]
Piecing solutions together in CegisUnif (#1894)

6 years agoReorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)
yoni206 [Wed, 9 May 2018 19:05:30 +0000 (12:05 -0700)]
Reorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)

6 years agoBetter option names for PBE (#1891)
Andrew Reynolds [Wed, 9 May 2018 16:54:59 +0000 (11:54 -0500)]
Better option names for PBE (#1891)

6 years agoMake symmetry-breaker-exp into a preprocessing pass (#1890)
Andrew Reynolds [Wed, 9 May 2018 15:50:55 +0000 (10:50 -0500)]
Make symmetry-breaker-exp into a preprocessing pass (#1890)

6 years agoAdd the symmetry breaker module (#1847)
PaulMeng [Wed, 9 May 2018 12:41:52 +0000 (07:41 -0500)]
Add the symmetry breaker module (#1847)

6 years agoRefactor bv-abstraction preprocessing pass. (#1860)
Mathias Preiner [Tue, 8 May 2018 22:18:15 +0000 (15:18 -0700)]
Refactor bv-abstraction preprocessing pass. (#1860)

6 years agoInfrastructure for approximations in model output (#1884)
Andrew Reynolds [Tue, 8 May 2018 21:28:22 +0000 (16:28 -0500)]
Infrastructure for approximations in model output (#1884)

6 years agoSupport for str.<= and str.< (#1882)
Andrew Reynolds [Tue, 8 May 2018 19:50:47 +0000 (14:50 -0500)]
Support for str.<= and str.< (#1882)

6 years agoFix order of preprocessing pass registration. (#1887)
Aina Niemetz [Tue, 8 May 2018 19:12:01 +0000 (12:12 -0700)]
Fix order of preprocessing pass registration. (#1887)

6 years agoClassifying data in SygusUnifRL (#1886)
Haniel Barbosa [Tue, 8 May 2018 18:41:37 +0000 (13:41 -0500)]
Classifying data in SygusUnifRL (#1886)

6 years agoInfrastructure for CEGQI handled status (#1873)
Andrew Reynolds [Tue, 8 May 2018 16:47:53 +0000 (11:47 -0500)]
Infrastructure for CEGQI handled status  (#1873)

6 years agoonly lazy trie changes (#1885)
Haniel Barbosa [Tue, 8 May 2018 12:32:10 +0000 (07:32 -0500)]
only lazy trie changes (#1885)

6 years agoAdd support for str.code (#1821)
Andrew Reynolds [Mon, 7 May 2018 15:22:27 +0000 (10:22 -0500)]
Add support for str.code (#1821)

6 years agoFix handling of TO_REAL in cvc printer (#1876)
Andrew Reynolds [Sat, 5 May 2018 07:23:54 +0000 (02:23 -0500)]
Fix handling of TO_REAL in cvc printer (#1876)

6 years agoRemove special case for record selector printing. (#1875)
Andrew Reynolds [Sat, 5 May 2018 00:10:51 +0000 (19:10 -0500)]
Remove special case for record selector printing. (#1875)

6 years agoCegis unif register evaluation points (#1878)
Andrew Reynolds [Fri, 4 May 2018 21:54:40 +0000 (16:54 -0500)]
Cegis unif register evaluation points (#1878)

6 years agoMake --output-lang consistent with --lang (#1877)
Andres Noetzli [Fri, 4 May 2018 18:32:38 +0000 (11:32 -0700)]
Make --output-lang consistent with --lang (#1877)

6 years agoDo not print tuples. (#1874)
Andrew Reynolds [Fri, 4 May 2018 16:46:31 +0000 (11:46 -0500)]
Do not print tuples. (#1874)

6 years agoRefactor bv-intro-pow2 preprocessing pass. (#1851)
Mathias Preiner [Fri, 4 May 2018 05:50:41 +0000 (22:50 -0700)]
Refactor bv-intro-pow2 preprocessing pass. (#1851)

6 years agoFix printing of multiple datatypes (#1872)
Andres Noetzli [Fri, 4 May 2018 04:48:19 +0000 (21:48 -0700)]
Fix printing of multiple datatypes (#1872)

6 years agoMove Lazy trie datastructure to its own file (#1871)
Haniel Barbosa [Fri, 4 May 2018 02:40:30 +0000 (21:40 -0500)]
Move Lazy trie datastructure to its own file (#1871)

Preparation for further developing CegisUnif

6 years agoInitialize cegis unif strategy (#1861)
Andrew Reynolds [Fri, 4 May 2018 02:11:18 +0000 (21:11 -0500)]
Initialize cegis unif strategy (#1861)

6 years agoDocument datatypes sygus (#1818)
Andrew Reynolds [Fri, 4 May 2018 00:54:28 +0000 (19:54 -0500)]
Document datatypes sygus (#1818)