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

7 years ago[LFSC] Fix memory leaks when creating CExprs
Andres Notzli [Thu, 22 Dec 2016 04:03:29 +0000 (20:03 -0800)]
[LFSC] Fix memory leaks when creating CExprs

In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).

7 years agoFix dependency tracing for fewerPreprocessingHoles
Andres Notzli [Thu, 15 Dec 2016 05:20:17 +0000 (21:20 -0800)]
Fix dependency tracing for fewerPreprocessingHoles

Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed.  Additionally, it fixes
a similar issue in the theory engine.

NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.

7 years agoMerge pull request #119 from 4tXJ7f/smt_v2_5
Clark Barrett [Wed, 14 Dec 2016 21:45:54 +0000 (13:45 -0800)]
Merge pull request #119 from 4tXJ7f/smt_v2_5

Switch from SMT-LIB v2.0 to v2.5 for smt2 files

7 years agoSwitch from SMT-LIB v2.0 to v2.5 for smt2 files
Andres Notzli [Wed, 14 Dec 2016 19:33:08 +0000 (11:33 -0800)]
Switch from SMT-LIB v2.0 to v2.5 for smt2 files

As mentioned in bug 741, CVC4 was parsing `.smt2` files using the
SMT-LIB v2.0 standard by default. This commit switches to v2.5.

7 years agoMade tear-down-incremental more like it used to be: when tear-down value
Clark Barrett [Wed, 14 Dec 2016 19:12:58 +0000 (11:12 -0800)]
Made tear-down-incremental more like it used to be: when tear-down value
is 1, it does not automatically enable incremental mode.

7 years agoMerge pull request #118 from 4tXJ7f/fix_emp
Andrew Reynolds [Tue, 13 Dec 2016 21:20:58 +0000 (15:20 -0600)]
Merge pull request #118 from 4tXJ7f/fix_emp

Fix split-find-unsat-w-emp test