cvc5.git
7 years agoRemove decl. of getStatisticsRegistry(SmtEngine*)
Andres Notzli [Fri, 31 Mar 2017 22:02:39 +0000 (15:02 -0700)]
Remove decl. of getStatisticsRegistry(SmtEngine*)

Commit f4ef7af0a2295691f281ee1604dfeb4082fe229c removed the definition
of getStatisticsRegistry(SmtEngine*) but not the declaration.

7 years agoAdd option multi-trigger-linear, minor optimization to E-matching.
ajreynol [Fri, 31 Mar 2017 13:43:29 +0000 (08:43 -0500)]
Add option multi-trigger-linear, minor optimization to E-matching.

7 years agoMerge pull request #139 from 4tXJ7f/remove_throw
Clark Barrett [Thu, 30 Mar 2017 19:49:38 +0000 (12:49 -0700)]
Merge pull request #139 from 4tXJ7f/remove_throw

[Coverity] Remove throw qualifiers in src/smt

7 years ago[Coverity] Remove throw qualifiers in src/smt
Andres Notzli [Wed, 29 Mar 2017 21:27:56 +0000 (23:27 +0200)]
[Coverity] Remove throw qualifiers in src/smt

Addresses coverity issues:

1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413

7 years agoMinor fixes for trigger selection max.
ajreynol [Thu, 30 Mar 2017 14:11:52 +0000 (09:11 -0500)]
Minor fixes for trigger selection max.

7 years agoAdd quantifiers options related to model and master equality engine.
ajreynol [Wed, 29 Mar 2017 18:49:51 +0000 (13:49 -0500)]
Add quantifiers options related to model and master equality engine.

7 years agoMerge pull request #138 from PaulMeng/master
PaulMeng [Wed, 29 Mar 2017 14:36:29 +0000 (09:36 -0500)]
Merge pull request #138 from PaulMeng/master

Refactor the standard effort of relational solver

7 years agoRefactor the standard effort of relational solver
Paul Meng [Wed, 29 Mar 2017 04:08:52 +0000 (23:08 -0500)]
Refactor the standard effort of relational solver

7 years agoFix bug 787.
ajreynol [Wed, 29 Mar 2017 03:22:05 +0000 (22:22 -0500)]
Fix bug 787.

7 years agoFix for bug 733
Clark Barrett [Wed, 29 Mar 2017 01:29:48 +0000 (18:29 -0700)]
Fix for bug 733

7 years agoMinor refactoring sygus.
ajreynol [Tue, 28 Mar 2017 21:21:12 +0000 (16:21 -0500)]
Minor refactoring sygus.

7 years agoMore work on sygus. Add regress4 to Makefile.
ajreynol [Tue, 28 Mar 2017 14:35:43 +0000 (09:35 -0500)]
More work on sygus. Add regress4 to Makefile.

7 years agoFixing a bug for checking whether a node was visited.
Tim King [Tue, 28 Mar 2017 06:26:34 +0000 (23:26 -0700)]
Fixing a bug for checking whether a node was visited.

7 years agoMinor cleanups to ExtTheory.
Tim King [Tue, 28 Mar 2017 05:15:23 +0000 (22:15 -0700)]
Minor cleanups to ExtTheory.

7 years agoRemoving the friend class modifier from ExtTheory to Theory.
Tim King [Tue, 28 Mar 2017 03:59:48 +0000 (20:59 -0700)]
Removing the friend class modifier from ExtTheory to Theory.

7 years agoMerge pull request #137 from 4tXJ7f/throw_quals
Clark Barrett [Mon, 27 Mar 2017 20:20:27 +0000 (13:20 -0700)]
Merge pull request #137 from 4tXJ7f/throw_quals

Remove throw qualifiers in type enumerators

7 years agoMaking the ExtTheory object a private member of Theory.
Tim King [Mon, 27 Mar 2017 19:26:14 +0000 (12:26 -0700)]
Making the ExtTheory object a private member of Theory.

7 years agoMaking ppNotifyAssertions take a const vector.
Tim King [Mon, 27 Mar 2017 17:24:13 +0000 (10:24 -0700)]
Making ppNotifyAssertions take a const vector.

7 years agoMoving the CareGraph into its own file.
Tim King [Mon, 27 Mar 2017 17:02:11 +0000 (10:02 -0700)]
Moving the CareGraph into its own file.

7 years agoMoving the theory::Assertion struct into its own file.
Tim King [Mon, 27 Mar 2017 16:40:30 +0000 (09:40 -0700)]
Moving the theory::Assertion struct into its own file.

7 years agoRemove throw qualifiers in type enumerators
Andres Notzli [Mon, 27 Mar 2017 09:40:45 +0000 (11:40 +0200)]
Remove throw qualifiers in type enumerators

This addresses Coverity issues:

1172154
1172156
1172157
1172158
1172159
1379612
1379612
1421430
1172166
1172144
1362709
1362696
1172145
1172147
1172148
1379610
1362772
1362676
1362704
1362749
1362876
1362843
1362837
1362881
1172223
1172155

7 years agoAlphabetizing libcvc4_la_SOURCES.
Tim King [Mon, 27 Mar 2017 04:59:36 +0000 (21:59 -0700)]
Alphabetizing libcvc4_la_SOURCES.

7 years agoAdd some regressions. Minor.
ajreynol [Fri, 24 Mar 2017 14:56:12 +0000 (09:56 -0500)]
Add some regressions. Minor.

7 years agoRefactor model building for quantifiers to be a single pass, simplification. Modify...
ajreynol [Fri, 24 Mar 2017 14:37:13 +0000 (09:37 -0500)]
Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.

7 years agoFixing warning message.
Clark Barrett [Thu, 23 Mar 2017 22:15:56 +0000 (15:15 -0700)]
Fixing warning message.

7 years agosupport incremental unsat cores
guykatzz [Thu, 23 Mar 2017 21:13:46 +0000 (14:13 -0700)]
support incremental unsat cores

7 years agoFix more cases of rewritten explanations in strings for bug 784. Minor.
ajreynol [Wed, 22 Mar 2017 16:15:19 +0000 (11:15 -0500)]
Fix more cases of rewritten explanations in strings for bug 784. Minor.

7 years agoMinor fix for bounded integers.
ajreynol [Wed, 22 Mar 2017 15:58:03 +0000 (10:58 -0500)]
Minor fix for bounded integers.

7 years agoWork on new approach for sygus involving conditional solutions. Refactoring of sygus...
ajreynol [Wed, 22 Mar 2017 13:52:42 +0000 (08:52 -0500)]
Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.

7 years agoImprove computeCareGraph functions to check shared term equality status once per...
ajreynol [Tue, 21 Mar 2017 21:39:25 +0000 (16:39 -0500)]
Improve computeCareGraph functions to check shared term equality status once per equivalence class pair.

7 years agoMerge pull request #135 from PaulMeng/master
Andrew Reynolds [Mon, 20 Mar 2017 20:42:16 +0000 (15:42 -0500)]
Merge pull request #135 from PaulMeng/master

fixed cvc4 parser for set complement

7 years agofixed cvc4 parser for set complement
Paul Meng [Mon, 20 Mar 2017 18:49:31 +0000 (13:49 -0500)]
fixed cvc4 parser for set complement

7 years agoFix for bug 707.
Clark Barrett [Sat, 18 Mar 2017 23:20:56 +0000 (16:20 -0700)]
Fix for bug 707.

7 years agoFix to help with bug 717
Clark Barrett [Sat, 18 Mar 2017 20:46:37 +0000 (13:46 -0700)]
Fix to help with bug 717

7 years agobetter support for proof production when encountering bool terms: handle the new...
guykatzz [Fri, 17 Mar 2017 21:11:41 +0000 (14:11 -0700)]
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.

proof production for bool-array.smt2 passes

7 years agoFixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.
Tim King [Thu, 16 Mar 2017 21:06:17 +0000 (14:06 -0700)]
Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.

7 years agoMore fixes, features to examples.
ajreynol [Thu, 16 Mar 2017 19:19:58 +0000 (14:19 -0500)]
More fixes, features to examples.

7 years agoMinor fixes, always expand applications of lambdas at preprocess.
ajreynol [Thu, 16 Mar 2017 19:05:23 +0000 (14:05 -0500)]
Minor fixes, always expand applications of lambdas at preprocess.

7 years agoSupport for SMT LIB 2.6 syntax declare-datatype and match.
ajreynol [Thu, 16 Mar 2017 18:24:31 +0000 (13:24 -0500)]
Support for SMT LIB 2.6 syntax declare-datatype and match.

7 years agoParsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGround...
ajreynol [Thu, 16 Mar 2017 16:37:53 +0000 (11:37 -0500)]
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.

7 years agoFix regress1 Makefile for rewriterules, fixes bug 783.
ajreynol [Wed, 15 Mar 2017 21:28:55 +0000 (16:28 -0500)]
Fix regress1 Makefile for rewriterules, fixes bug 783.

7 years agoMerge pull request #134 from 4tXJ7f/fix_host
Clark Barrett [Wed, 15 Mar 2017 21:00:17 +0000 (14:00 -0700)]
Merge pull request #134 from 4tXJ7f/fix_host

Fix win-build script to use MinGW-w64 by default

7 years agoAllow 0 argument recursive functions. Fixes bug 782.
ajreynol [Wed, 15 Mar 2017 18:11:08 +0000 (13:11 -0500)]
Allow 0 argument recursive functions. Fixes bug 782.

7 years agoFix win-build script to use MinGW-w64 by default
Andres Notzli [Wed, 15 Mar 2017 08:25:39 +0000 (01:25 -0700)]
Fix win-build script to use MinGW-w64 by default

Previous changes to the win-build script left the script in an
inconsistent state: the script was updated to refer to MinGW-w64 but the
default host was still referring to MinGW.

7 years agoMerge pull request #133 from 4tXJ7f/fix_uninitialized
guykatzz [Tue, 14 Mar 2017 19:52:42 +0000 (12:52 -0700)]
Merge pull request #133 from 4tXJ7f/fix_uninitialized

Fix uninitialized variable

7 years agofix uninitialized variable
Andres Notzli [Tue, 14 Mar 2017 18:32:26 +0000 (11:32 -0700)]
fix uninitialized variable

7 years agoMerge pull request #132 from 4tXJ7f/fix_mingw64
Clark Barrett [Tue, 14 Mar 2017 17:40:26 +0000 (10:40 -0700)]
Merge pull request #132 from 4tXJ7f/fix_mingw64

Fix MinGW-w64 build

7 years agoMinor fix for cbqi-all.
ajreynol [Fri, 10 Mar 2017 22:36:10 +0000 (16:36 -0600)]
Minor fix for cbqi-all.

7 years agobug fix
guykatzz [Thu, 9 Mar 2017 22:46:33 +0000 (14:46 -0800)]
bug fix

7 years agobetter proof support for bools and formulas
guykatzz [Thu, 9 Mar 2017 20:13:12 +0000 (12:13 -0800)]
better proof support for bools and formulas

7 years agoFix MinGW-w64 build
Andres Notzli [Wed, 8 Mar 2017 10:50:56 +0000 (02:50 -0800)]
Fix MinGW-w64 build

This commit fixes configure.ac to try to get clock_gettime() from
pthread. Without it, clock_gettime() is detected as missing at
configuration time for MinGW-w64 but exists at compile time, which
causes conflicts. Additionally, this commit updates the helper script
for Windows to use MinGW-w64 by default instead of MinGW.

7 years agoMore fixes for printing/parsing sets, fix kind name.
ajreynol [Tue, 7 Mar 2017 17:17:34 +0000 (11:17 -0600)]
More fixes for printing/parsing sets, fix kind name.

7 years agoFix cvc parser for set compliment.
ajreynol [Tue, 7 Mar 2017 15:11:33 +0000 (09:11 -0600)]
Fix cvc parser for set compliment.

7 years agoDo not eagerly construct explanations in relation solver.
ajreynol [Mon, 6 Mar 2017 16:18:17 +0000 (10:18 -0600)]
Do not eagerly construct explanations in relation solver.

7 years agoSupport for set compliment and universe set. Simplify approach for sep.nil nodes.
ajreynol [Mon, 6 Mar 2017 15:39:03 +0000 (09:39 -0600)]
Support for set compliment and universe set. Simplify approach for sep.nil nodes.

7 years agoAdding support for bool-to-bv
Clark Barrett [Mon, 6 Mar 2017 08:25:26 +0000 (00:25 -0800)]
Adding support for bool-to-bv

Squashed commit of the following:

commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Mar 6 00:16:16 2017 -0800

    Remove IFF case

commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date:   Mon Feb 20 12:37:06 2017 -0800

    proof support for bvcomp

commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 21:09:04 2017 -0800

    Added missing cases to operator<< for bv rewrite rules.

commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 11:43:51 2017 -0800

    Added rewrite rules for new bitvector kinds.

commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Feb 13 14:41:49 2017 -0800

    First draft of bool-to-bv pass.

7 years agoFix for collectModelInfo related to finite types + preregistration. Generalize previo...
ajreynol [Fri, 3 Mar 2017 22:17:24 +0000 (16:17 -0600)]
Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.

7 years agoAnother minor fix for sets related to sharing + finite element types.
ajreynol [Fri, 3 Mar 2017 16:33:03 +0000 (10:33 -0600)]
Another minor fix for sets related to sharing + finite element types.

7 years agoFixes related to sets.
ajreynol [Thu, 2 Mar 2017 22:40:39 +0000 (16:40 -0600)]
Fixes related to sets.

7 years agoMinor cleanup and reorganization related to last commit.
ajreynol [Thu, 2 Mar 2017 21:24:07 +0000 (15:24 -0600)]
Minor cleanup and reorganization related to last commit.

7 years agoEliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms...
ajreynol [Thu, 2 Mar 2017 20:45:21 +0000 (14:45 -0600)]
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

7 years agoMinor fixes for relations, quantifiers dsplit.
ajreynol [Thu, 16 Feb 2017 22:19:51 +0000 (16:19 -0600)]
Minor fixes for relations, quantifiers dsplit.

7 years agoFixes for sets+rels check. Minor.
ajreynol [Thu, 16 Feb 2017 19:26:10 +0000 (13:26 -0600)]
Fixes for sets+rels check. Minor.

7 years agoMinimization modes for fmf bound.
ajreynol [Wed, 15 Feb 2017 17:26:56 +0000 (11:26 -0600)]
Minimization modes for fmf bound.

7 years agoGeneralize finite bound inference to unifiable variables in set membership literals.
ajreynol [Tue, 7 Feb 2017 19:26:57 +0000 (13:26 -0600)]
Generalize finite bound inference to unifiable variables in set membership literals.

7 years agoFix regexp cache issue in strings, add regression.
ajreynol [Mon, 30 Jan 2017 17:20:29 +0000 (11:20 -0600)]
Fix regexp cache issue in strings, add regression.

7 years agoFix non-idempotent rewrite in Array rewriter
Andres Noetzli [Wed, 4 Jan 2017 17:20:34 +0000 (09:20 -0800)]
Fix non-idempotent rewrite in Array rewriter

This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.

7 years agoMerge pull request #128 from 4tXJ7f/fix_lfsc_perf
Andrew Reynolds [Wed, 18 Jan 2017 19:32:55 +0000 (13:32 -0600)]
Merge pull request #128 from 4tXJ7f/fix_lfsc_perf

[LFSC] Fix performance issues, more determinism

7 years agoMinor fix in relations.
ajreynol [Wed, 18 Jan 2017 18:39:24 +0000 (12:39 -0600)]
Minor fix in relations.

7 years ago[LFSC] Fix performance issues, more determinism
Andres Notzli [Tue, 10 Jan 2017 22:23:22 +0000 (01:23 +0300)]
[LFSC] Fix performance issues, more determinism

For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.

7 years agoFix call to SExpr constructor for greater portability.
Clark Barrett [Sat, 14 Jan 2017 05:23:42 +0000 (21:23 -0800)]
Fix call to SExpr constructor for greater portability.

7 years agoMerge pull request #130 from chadbrewbaker/master
Clark Barrett [Sat, 14 Jan 2017 04:18:16 +0000 (20:18 -0800)]
Merge pull request #130 from chadbrewbaker/master

Fixing memory leak

7 years agoDo not rewrite explanations in strings.
ajreynol [Fri, 13 Jan 2017 15:40:15 +0000 (09:40 -0600)]
Do not rewrite explanations in strings.

7 years agoMerge pull request #129 from timothy-king/regression-scrubber
Clark Barrett [Wed, 11 Jan 2017 22:20:22 +0000 (14:20 -0800)]
Merge pull request #129 from timothy-king/regression-scrubber

Adding regression test scrubbing.

7 years agoMerge pull request #131 from makaimann/fix_702
Clark Barrett [Wed, 11 Jan 2017 22:03:11 +0000 (14:03 -0800)]
Merge pull request #131 from makaimann/fix_702

Proposed fix for bug 702

7 years agoProposed fix for bug 702. Checks to make sure the Expr's operator is not of kind...
makaimann [Wed, 11 Jan 2017 21:47:06 +0000 (13:47 -0800)]
Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind BUILTIN before passing to prefixPrintGetValue()

7 years agoFix for when variables are (partially) bound in multiple ways, add regression. Improv...
ajreynol [Wed, 11 Jan 2017 20:34:18 +0000 (14:34 -0600)]
Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.

7 years agoMerge pull request #127 from cristian-mattarei/issue_679
Clark Barrett [Wed, 11 Jan 2017 19:03:22 +0000 (11:03 -0800)]
Merge pull request #127 from cristian-mattarei/issue_679

Bug 679 fix

7 years agorevert
Chad Brewbaker [Wed, 11 Jan 2017 02:59:20 +0000 (20:59 -0600)]
revert

7 years agoQuashing memory leak
Chad Brewbaker [Wed, 11 Jan 2017 02:51:24 +0000 (20:51 -0600)]
Quashing memory leak

7 years agoAdding regression test scrubbing.
Tim King [Wed, 11 Jan 2017 01:51:14 +0000 (17:51 -0800)]
Adding regression test scrubbing.

7 years agoWith reference to Bug 679, this commit integrates part of the patch proposed, and...
Cristian Mattarei [Mon, 9 Jan 2017 03:00:09 +0000 (19:00 -0800)]
With reference to Bug 679, this commit integrates part of the patch proposed, and it fixes the correct float parsing of an std::istringstream.

The compilation issue in Bug 679 does not apply anymore with gcc6.3.1

7 years agoquashing debug memory leak
Chad Brewbaker [Sat, 7 Jan 2017 04:56:07 +0000 (22:56 -0600)]
quashing debug memory leak

7 years agoMinor fix for sets.
ajreynol [Fri, 6 Jan 2017 19:27:18 +0000 (13:27 -0600)]
Minor fix for sets.

7 years agoDisabling a regression test that assumes CVC4 is configured with proofs on. Modifying...
Tim King [Thu, 5 Jan 2017 23:07:33 +0000 (15:07 -0800)]
Disabling a regression test that assumes CVC4 is configured with proofs on. Modifying the travis rules so there are instances with proofs disabled.

7 years agoFix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes.
ajreynol [Wed, 4 Jan 2017 21:28:24 +0000 (15:28 -0600)]
Fix for tff type declarations inTPTP parser, fixes bug 748.  Other minor changes.

7 years agoMarking regression test files as non-executable.
Tim King [Wed, 4 Jan 2017 21:36:30 +0000 (13:36 -0800)]
Marking regression test files as non-executable.

7 years agoMarking the proof signature files as non-executable.
Tim King [Wed, 4 Jan 2017 21:00:25 +0000 (13:00 -0800)]
Marking the proof signature files as non-executable.

7 years agoSetting the executable bit for the newer run scripts in contrib.
Tim King [Wed, 4 Jan 2017 20:59:16 +0000 (12:59 -0800)]
Setting the executable bit for the newer run scripts in contrib.

7 years agoReverting two files encoding with DOS linebreaks back into using unix linebreaks.
Tim King [Wed, 4 Jan 2017 20:57:55 +0000 (12:57 -0800)]
Reverting two files encoding with DOS linebreaks back into using unix linebreaks.

7 years agoMerge pull request #122 from 4tXJ7f/fix_lfsc_str
Andrew Reynolds [Wed, 4 Jan 2017 18:21:52 +0000 (12:21 -0600)]
Merge pull request #122 from 4tXJ7f/fix_lfsc_str

[LFSC] Minor fixes/improvements

7 years agoMerge pull request #120 from 4tXJ7f/fix_f_pp_holes
guykatzz [Wed, 4 Jan 2017 18:18:36 +0000 (10:18 -0800)]
Merge pull request #120 from 4tXJ7f/fix_f_pp_holes

Fix dependency tracing for fewerPreprocessingHoles

7 years agoMerge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks
Andrew Reynolds [Wed, 4 Jan 2017 17:47:52 +0000 (11:47 -0600)]
Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks

[LFSC] Fix memory leaks when creating CExprs

7 years agoChanging a set of TNodes to a set of Nodes in the BV inequality solver. The ref count...
Tim King [Thu, 29 Dec 2016 23:43:04 +0000 (15:43 -0800)]
Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.

7 years agoEliminating a signed vs. unsigned comparison.
Tim King [Thu, 29 Dec 2016 22:42:59 +0000 (14:42 -0800)]
Eliminating a signed vs. unsigned comparison.

7 years agoChanging getTearDownIncremental() to return the type of options::tearDownIncremental.
Tim King [Thu, 29 Dec 2016 22:36:36 +0000 (14:36 -0800)]
Changing getTearDownIncremental() to return the type of options::tearDownIncremental.

7 years agoAdding a destructor to InstantiationNotify.
Tim King [Thu, 29 Dec 2016 22:36:00 +0000 (14:36 -0800)]
Adding a destructor to InstantiationNotify.

7 years agoAdding a destructor to RepBoundExt.
Tim King [Thu, 29 Dec 2016 22:35:02 +0000 (14:35 -0800)]
Adding a destructor to RepBoundExt.

7 years agoReordering sep and sets in Makefile.theories.
Tim King [Thu, 29 Dec 2016 22:34:29 +0000 (14:34 -0800)]
Reordering sep and sets in Makefile.theories.

7 years ago[LFSC] Minor fixes/improvements
Andres Notzli [Thu, 22 Dec 2016 12:45:29 +0000 (04:45 -0800)]
[LFSC] Minor fixes/improvements

- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions