cvc5.git
5 years agoAdd interface for term enumeration (#2956)
Andrew Reynolds [Tue, 16 Apr 2019 20:06:00 +0000 (15:06 -0500)]
Add interface for term enumeration (#2956)

5 years agoMake bv{add,mul,and,or,xor,xnor} left-associative (#2955)
Andres Noetzli [Tue, 16 Apr 2019 19:11:37 +0000 (12:11 -0700)]
Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)

The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`.  This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.

References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)

5 years agoStratify enumerative instantiation (#2954)
Andrew Reynolds [Tue, 16 Apr 2019 16:53:45 +0000 (11:53 -0500)]
Stratify enumerative instantiation (#2954)

5 years agoMinor simplifications to theory quantifiers (#2953)
Andrew Reynolds [Tue, 16 Apr 2019 15:38:35 +0000 (10:38 -0500)]
Minor simplifications to theory quantifiers (#2953)

5 years agoCheck for rt library in configuration -- support for glibc<2.17 (#2854)
makaimann [Tue, 16 Apr 2019 00:17:29 +0000 (17:17 -0700)]
Check for rt library in configuration -- support for glibc<2.17 (#2854)

This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page.

5 years agoInitial version of run scripts for SMT-COMP 2019 (#2951)
Andres Noetzli [Mon, 15 Apr 2019 22:03:00 +0000 (15:03 -0700)]
Initial version of run scripts for SMT-COMP 2019 (#2951)

For now, they are just copies of the 2018 version of the scripts.

5 years agoReferring to prerelease 1.8 (#2943)
Haniel Barbosa [Fri, 12 Apr 2019 21:16:33 +0000 (16:16 -0500)]
Referring to prerelease 1.8 (#2943)

5 years ago Eliminate Boolean ITE within terms, fixes 2947 (#2949)
Andrew Reynolds [Thu, 11 Apr 2019 18:06:08 +0000 (13:06 -0500)]
 Eliminate Boolean ITE within terms, fixes 2947 (#2949)

5 years agoRemoving references to cvc4-bugs@... (#2945)
Haniel Barbosa [Tue, 9 Apr 2019 16:14:31 +0000 (11:14 -0500)]
Removing references to cvc4-bugs@... (#2945)

5 years ago"prerelease -> release" in INSTALL (#2944)
Haniel Barbosa [Tue, 9 Apr 2019 00:55:50 +0000 (19:55 -0500)]
"prerelease -> release" in INSTALL (#2944)

5 years agoFix email address of the bugs email list and delete obsolete RELEASE-NOTES.
Aina Niemetz [Tue, 9 Apr 2019 00:11:57 +0000 (17:11 -0700)]
Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.

5 years agofix copyright year in configuration file (#2942)
Haniel Barbosa [Mon, 8 Apr 2019 16:26:58 +0000 (11:26 -0500)]
fix copyright year in configuration file (#2942)

5 years agoprerelease -> release (#2941)
Haniel Barbosa [Fri, 5 Apr 2019 21:02:41 +0000 (16:02 -0500)]
prerelease -> release (#2941)

5 years agoFix another corner case of datatypes+PBE (#2938)
Andrew Reynolds [Fri, 5 Apr 2019 20:31:20 +0000 (15:31 -0500)]
Fix another corner case of datatypes+PBE (#2938)

5 years agofix fp issue (#2940)
Haniel Barbosa [Fri, 5 Apr 2019 19:01:33 +0000 (14:01 -0500)]
fix fp issue (#2940)

5 years agoSatClauseSetHashFunction (#2916)
Alex Ozdemir [Fri, 5 Apr 2019 17:03:05 +0000 (10:03 -0700)]
SatClauseSetHashFunction (#2916)

* SatClauseHashFunction

Added to the same file as SatLiteralHashFunction.

* clang-format

Thanks Andres!

5 years agoadding sygus news (#2934)
Haniel Barbosa [Thu, 4 Apr 2019 18:30:27 +0000 (13:30 -0500)]
adding sygus news (#2934)

5 years agoIgnoring FP benchmarks with "unsafe" sizes unless option (#2931)
Haniel Barbosa [Thu, 4 Apr 2019 17:31:21 +0000 (12:31 -0500)]
Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)

5 years agoUpdate release notes and lib version (#2933)
Haniel Barbosa [Thu, 4 Apr 2019 02:06:25 +0000 (21:06 -0500)]
Update release notes and lib version (#2933)

5 years agoUpdate copyright headers.
Aina Niemetz [Wed, 3 Apr 2019 22:54:55 +0000 (15:54 -0700)]
Update copyright headers.

5 years agoget-authors: Add GitHub user ayveejay -> Andrew V. Jones.
Aina Niemetz [Wed, 3 Apr 2019 22:53:49 +0000 (15:53 -0700)]
get-authors: Add GitHub user ayveejay -> Andrew V. Jones.

5 years agoFix combination of datatypes + strings in PBE (#2930)
Andrew Reynolds [Wed, 3 Apr 2019 20:53:52 +0000 (15:53 -0500)]
Fix combination of datatypes + strings in PBE (#2930)

5 years agoFP: Fix wrong model due to partial assignment (#2910)
Andres Noetzli [Mon, 1 Apr 2019 22:07:05 +0000 (15:07 -0700)]
FP: Fix wrong model due to partial assignment (#2910)

For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting
a wrong model. The issue was that `(sign x)` was not assigned a value
and did not appear in the shared terms. In
`TheoryFp::collectModelInfo()`, however, we generate an expression that
connects the components of `x` to `x`, which contains `(sign x)`. As a
result, the normalization while building a model did not result in a
constant. This commit fixes the issue by marking `(sign x)` (and
`(significand x)`) as assignable. Assignable terms can take any value
while building a model if there is no existing value.

5 years agoFix RewriteITEBv to ensure rewrite to fixpoint (#2878)
Andres Noetzli [Mon, 1 Apr 2019 21:26:23 +0000 (14:26 -0700)]
Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)

`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.

5 years agoUpdate includes to use cvc4 top-level directory in examples (#2877)
makaimann [Mon, 1 Apr 2019 20:22:04 +0000 (13:22 -0700)]
Update includes to use cvc4 top-level directory in examples (#2877)

Because the headers are now installed in a `cvc4` directory, the examples need to include from there as well.

5 years agoMove slow string regression to regress3 (#2913)
Andres Noetzli [Mon, 1 Apr 2019 17:45:40 +0000 (10:45 -0700)]
Move slow string regression to regress3 (#2913)

5 years agoModify strategy in sets+cardinality (#2909)
Andrew Reynolds [Mon, 1 Apr 2019 15:36:38 +0000 (10:36 -0500)]
Modify strategy in sets+cardinality (#2909)

5 years agoApply empty splits more aggressively in sets+cardinality (#2907)
Andrew Reynolds [Fri, 29 Mar 2019 13:38:30 +0000 (08:38 -0500)]
Apply empty splits more aggressively in sets+cardinality (#2907)

5 years agoremoving deprecated rewriting signature / example (#2906)
Haniel Barbosa [Fri, 29 Mar 2019 05:02:03 +0000 (00:02 -0500)]
removing deprecated rewriting signature / example (#2906)

5 years agoFix freeing nodes with maxed refcounts (#2903)
Andres Noetzli [Fri, 29 Mar 2019 04:02:37 +0000 (21:02 -0700)]
Fix freeing nodes with maxed refcounts (#2903)

5 years agoFix issues in cvc parser (#2901)
Andrew Reynolds [Fri, 29 Mar 2019 03:21:34 +0000 (22:21 -0500)]
Fix issues in cvc parser (#2901)

5 years agofix ex_bv.plf (#2905)
Haniel Barbosa [Thu, 28 Mar 2019 23:30:50 +0000 (18:30 -0500)]
fix ex_bv.plf (#2905)

5 years agoUpdate copyright headers.
Aina Niemetz [Tue, 26 Mar 2019 18:33:55 +0000 (11:33 -0700)]
Update copyright headers.

5 years agoupdate-copyright: Update to 2019.
Aina Niemetz [Tue, 26 Mar 2019 18:11:56 +0000 (11:11 -0700)]
update-copyright: Update to 2019.

5 years agoget-authors: Exclude empty lines.
Mathias Preiner [Tue, 26 Mar 2019 18:22:21 +0000 (11:22 -0700)]
get-authors: Exclude empty lines.

5 years agoFix warnings about wrong line numbers (#2899)
Andres Noetzli [Tue, 26 Mar 2019 15:28:09 +0000 (08:28 -0700)]
Fix warnings about wrong line numbers (#2899)

5 years agoFix a few warnings (#2898)
Andrew Reynolds [Tue, 26 Mar 2019 15:03:29 +0000 (10:03 -0500)]
Fix a few warnings (#2898)

5 years agoget-authors: Exclude common source code patterns. (#2900)
Mathias Preiner [Tue, 26 Mar 2019 01:19:45 +0000 (18:19 -0700)]
get-authors: Exclude common source code patterns. (#2900)

Exclude lines that #include header files and define namespaces.
Since we use git blame -C -M to determine the current top contributors,
git tries to match all #include and namespace definitions to an original
author, which is not accurate since these lines are usually not
copied over from other files.

5 years agoupdate-copyright: Fix matching of excluded paths.
Aina Niemetz [Mon, 25 Mar 2019 19:31:59 +0000 (12:31 -0700)]
update-copyright: Fix matching of excluded paths.

5 years agoget-authors: Readd option -C to git blame command.
Aina Niemetz [Mon, 25 Mar 2019 18:39:17 +0000 (11:39 -0700)]
get-authors: Readd option -C to git blame command.

5 years ago Split regular expression solver (#2891)
Andrew Reynolds [Sun, 24 Mar 2019 19:26:25 +0000 (14:26 -0500)]
 Split regular expression solver (#2891)

5 years agoNew C++ API: Fix include. (#2896)
Aina Niemetz [Sun, 24 Mar 2019 18:46:36 +0000 (11:46 -0700)]
New C++ API: Fix include. (#2896)

5 years agoBV: Fix typerules for rotate operators. (#2895)
Aina Niemetz [Sun, 24 Mar 2019 05:58:31 +0000 (22:58 -0700)]
BV: Fix typerules for rotate operators. (#2895)

5 years agoFix memory leak when using subsolvers (#2893)
Andres Noetzli [Sat, 23 Mar 2019 20:30:35 +0000 (13:30 -0700)]
Fix memory leak when using subsolvers (#2893)

ASAN was reporting memory leaks in regression tests that were using
subsolvers. First, I am going to describe the origin of the leaks and
then the solution implemented in this commit.

Recall an `Expr` stores the `NodeManager` that the internal node is
associated with. `Node::toExpr()` converts a `Node` to an `Expr` and
assumes that the active `NodeManager` (returned by
`NodeManager::currentNM()` is the one associated with the node. In
`ExportPrivate::exportInternal()`, when we were exporting a skolem, we
created a skolem in the target `NodeManager` by calling
`NodeManager::mkSkolem()` (`ExprManager`s do not support the creation of
skolems) but then we called `Node::toExpr()` on the resulting skolem
while the origin `NodeManager` was the active `NodeManager`. One of the
issues of having the wrong `NodeManager` in the `Expr` is that when the
`Expr` is destroyed and the internal node's refcount reaches zero in
destructor of `Expr`, then the node value associated with the node is
added to the set of zombie nodes (nodes waiting to be garbage collected
or resurrected) of the wrong `NodeManager`. The problem here is that the
set of zombie nodes uses the node id to hash and compare nodes. Node
ids, however, are only unique within a given `NodeManager`. Thus, if we
have two nodes with the same id from different `NodeManager`s and both
reach refcount zero in the context of the same `NodeManager`, only one
of them will end up in the set of zombies and thus only that one will be
freed.
Using a subsolver realiably triggered this issue.
`ExportPrivate::exportInternal()` stored the `Expr` with the wrong
`NodeManager` in an `ExprManagerMapCollection` which associates
variables in the original `ExprManager` with the variables in the target
`ExprManager`. When we created a subsolver, we created the
`ExprManagerMapCollection` before creating our subsolver, so it was
deleted after the subsolver and so deleting the
`ExprManagerMapCollection` deleted the last reference to `Expr`s holding
skolem nodes associated with the wrong `NodeManager`.

This commit fixes the issue by making sure that the correct
`NodeManager` is in scope when converting the skolem/bound variable
nodes to an `Expr`. It also swaps the creation order of
`ExprManagerMapCollection` and `ExprManager` to make sure that
`ExprManagerMapCollection` is deleted before the `ExprManager` that the
`Expr`s belong to. Additionally, the commit makes it harder to make a
similar mistake by asserting that the `Expr`s in the
`ExprManagerMapCollection` are associated with the expected
`ExprManager`s. Finally, it adds an assertion that tries to identify
such issues by checking whether the list of zombies contains a node with
the same id but located at a different address.

5 years agoStrip non-matching beginning from indexof operator (#2885)
Andres Noetzli [Sat, 23 Mar 2019 00:15:53 +0000 (00:15 +0000)]
Strip non-matching beginning from indexof operator (#2885)

This commit adds a rewrite that strips endpoints from `str.indexof`
operators if they don't overlap with the string that is being searched
for using `stripConstantEndpoints()`. In addition to that, it makes
`stripConstantEndpoints()` slightly more aggressive by allowing it to
drop substring components that have zero overlap with the string that we
are looking at. Finally, the commit fixes the default argument for
`fullRewriter` of `checkEntailContains()` to be true instead of false,
which should allow for more rewriting opportunities.

5 years agoRevisit strings extended function decomposition (#2892)
Andrew Reynolds [Fri, 22 Mar 2019 21:24:05 +0000 (16:24 -0500)]
Revisit strings extended function decomposition  (#2892)

5 years agoFix instantiation stat for fmf (#2889)
Andrew Reynolds [Fri, 22 Mar 2019 20:28:50 +0000 (15:28 -0500)]
Fix instantiation stat for fmf (#2889)

5 years agoMore fixes for PBE with datatypes (#2882)
Andrew Reynolds [Fri, 22 Mar 2019 14:01:13 +0000 (09:01 -0500)]
More fixes for PBE with datatypes (#2882)

5 years agofix help information on TPTP parsing (#2884)
Haniel Barbosa [Fri, 22 Mar 2019 06:11:06 +0000 (01:11 -0500)]
fix help information on TPTP parsing (#2884)

5 years agoFix stripConstantEndpoints in strings rewriter (#2883)
Andres Noetzli [Fri, 22 Mar 2019 03:48:56 +0000 (03:48 +0000)]
Fix stripConstantEndpoints in strings rewriter (#2883)

`TheoryStringsRewriter::stripConstantEndpoints()` returns the stripped
endpoints in the vectors `nb` and `ne`. These endpoints were not
computed correctly if string literal had to be split. For example:

```
stripConstantEndpoints({ "ABC" }, { "C" }, {}, {}, 1)
```

returned `true` and only "A" for `nb` (instead of "AB") because we
mistakenly used the amount of overlap between "ABC" and "C" (which is
one) for the length of the stripped prefix.

This commit fixes the issue and adds several unit tests.

5 years agoUse empty vector instead of false in query with null Expr assumption (#2876)
makaimann [Fri, 22 Mar 2019 01:10:01 +0000 (18:10 -0700)]
Use empty vector instead of false in query with null Expr assumption (#2876)

This solution is less confusing than using a `false` assumption.

5 years ago Fix bad comparison in RE solver's addMembership (#2880)
Andrew Reynolds [Thu, 21 Mar 2019 19:21:39 +0000 (14:21 -0500)]
 Fix bad comparison in RE solver's addMembership (#2880)

5 years agoRewrite selectors correctly applied to constructors (#2875)
Andrew Reynolds [Thu, 21 Mar 2019 18:41:46 +0000 (13:41 -0500)]
Rewrite selectors correctly applied to constructors (#2875)

5 years agoAdd more NEWS (#2859)
Andres Noetzli [Thu, 21 Mar 2019 17:21:02 +0000 (17:21 +0000)]
Add more NEWS (#2859)

5 years agoSygus abduction feature (#2744)
Andrew Reynolds [Wed, 20 Mar 2019 01:54:40 +0000 (20:54 -0500)]
Sygus abduction feature (#2744)

5 years agoMake declare-datatype(s) a standard, non-extended command in the Smt2 parser. (#2874)
Andrew Reynolds [Tue, 19 Mar 2019 19:15:24 +0000 (14:15 -0500)]
Make declare-datatype(s) a standard, non-extended command in the Smt2 parser. (#2874)

5 years agoFix fairness issue with fast sygus enumerator (#2873)
Andrew Reynolds [Tue, 19 Mar 2019 16:51:11 +0000 (11:51 -0500)]
Fix fairness issue with fast sygus enumerator (#2873)

5 years agoNew C++: Remove redundant mkBoundVar function.
Aina Niemetz [Mon, 18 Mar 2019 22:58:43 +0000 (15:58 -0700)]
New C++: Remove redundant mkBoundVar function.

5 years agoNew C++: Remove redundant mkVar function.
Aina Niemetz [Mon, 18 Mar 2019 22:05:00 +0000 (15:05 -0700)]
New C++: Remove redundant mkVar function.

s

5 years agoBitVector: Allow base 10 in constructor. (#2870)
Aina Niemetz [Mon, 18 Mar 2019 23:07:03 +0000 (16:07 -0700)]
BitVector: Allow base 10 in constructor. (#2870)

5 years agoLimit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)
Andres Noetzli [Sat, 16 Mar 2019 06:23:06 +0000 (06:23 +0000)]
Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)

Fixes #1715. We do not support the `--solve-int-as-bv=X` preprocessing
pass with logics other than pure QF_NIA/QF_LIA/QF_IDL. This commit adds
a corresponding check and throws an option exception if an incompatible
logic has been set.

5 years agoEnable CryptoMiniSat-backed BV proofs (#2847)
Alex Ozdemir [Sat, 16 Mar 2019 01:51:47 +0000 (18:51 -0700)]
Enable CryptoMiniSat-backed BV proofs (#2847)

* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
   * Specifically, CNF proofs broke when proving tautological clauses.
     Now they don't.

5 years agoNew beta-reduction for HOL solving (#2869)
Haniel Barbosa [Fri, 15 Mar 2019 23:35:43 +0000 (18:35 -0500)]
New beta-reduction for HOL solving (#2869)

5 years agoAdding capture avoiding substitution (#2867)
Haniel Barbosa [Fri, 15 Mar 2019 22:01:42 +0000 (17:01 -0500)]
Adding capture avoiding substitution (#2867)

5 years agoFix non-variable function head elimination in UF. (#2864)
Andrew Reynolds [Fri, 15 Mar 2019 02:33:07 +0000 (21:33 -0500)]
Fix non-variable function head elimination in UF. (#2864)

5 years agoFix function term set for theory strings compute care graph. (#2862)
Andrew Reynolds [Thu, 14 Mar 2019 22:51:39 +0000 (17:51 -0500)]
Fix function term set for theory strings compute care graph. (#2862)

5 years agoImprove INSTALL instructions. (#2866)
Aina Niemetz [Thu, 14 Mar 2019 22:17:31 +0000 (15:17 -0700)]
Improve INSTALL instructions. (#2866)

5 years agoUse zero slope tangent planes for transcendental functions (#2803)
Andrew Reynolds [Thu, 14 Mar 2019 21:32:25 +0000 (16:32 -0500)]
Use zero slope tangent planes for transcendental functions (#2803)

5 years agoProperly handle lambdas in relevant domain (#2853)
Andrew Reynolds [Thu, 14 Mar 2019 20:47:48 +0000 (15:47 -0500)]
Properly handle lambdas in relevant domain (#2853)

5 years ago Add getFreeVariables method to node algorithm (#2852)
Andrew Reynolds [Thu, 14 Mar 2019 20:13:55 +0000 (15:13 -0500)]
 Add getFreeVariables method to node algorithm (#2852)

5 years agoDisable DCO signing for organization members.
Mathias Preiner [Thu, 14 Mar 2019 19:45:49 +0000 (12:45 -0700)]
Disable DCO signing for organization members.

5 years agoImplement proper semantics for TPTP predicate is_rat. (#2861)
Andrew Reynolds [Thu, 14 Mar 2019 19:06:48 +0000 (14:06 -0500)]
Implement proper semantics for TPTP predicate is_rat. (#2861)

5 years ago Fix substitution step in ho matching (#2825)
Andrew Reynolds [Thu, 14 Mar 2019 18:36:56 +0000 (13:36 -0500)]
 Fix substitution step in ho matching (#2825)

5 years agoGeneralize sygus-rr-verify for fast enumerator (#2829)
Andrew Reynolds [Thu, 14 Mar 2019 12:46:52 +0000 (07:46 -0500)]
Generalize sygus-rr-verify for fast enumerator (#2829)

5 years agocheck for null assumption in query and replace with false (#2858)
makaimann [Thu, 14 Mar 2019 07:08:15 +0000 (00:08 -0700)]
check for null assumption in query and replace with false (#2858)

The default assumption argument in query was a null `Expr`, but the implementation asserted that the assumption is not null:

declaration: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.h#L593
implementation: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3548

The change is to simply check if the assumption is null and replaces it with the `false` expression if it is.

It should be `false` not `true` because it is negated in checkSatisfiability (when it's a query) as seen here: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3607

Note: I couldn't find a clean way to make `false` the default argument of assumption, because the expression manager is non-static.

5 years agoAdd statistics for proof gen./checking time, size (#2850)
Andres Noetzli [Wed, 13 Mar 2019 22:47:04 +0000 (22:47 +0000)]
Add statistics for proof gen./checking time, size (#2850)

This commit adds a statistic that records the total size of all proofs
generated by an instance of `SmtEngine`. The commit also moves
`SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know
the complete type of `d_stats` (and the separate file for that method
didn't seem that useful). Additionally, it changes
`smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime`
that only measures the time spent in LFSC and adds a statistic
`proof::ProofManager::proofProductionTime` that measures the proof
production time separately (also works with `get-proof`/`--dump-proof`).

5 years agoRemove spurious data member. (#2857)
Andrew Reynolds [Wed, 13 Mar 2019 16:37:03 +0000 (11:37 -0500)]
Remove spurious data member. (#2857)

5 years agoFix public headers for make install. (#2856)
Mathias Preiner [Wed, 13 Mar 2019 03:09:35 +0000 (20:09 -0700)]
Fix public headers for make install. (#2856)

This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4.
Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API).

5 years agoAdd option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)
Andrew Reynolds [Tue, 12 Mar 2019 20:18:30 +0000 (15:18 -0500)]
Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)

5 years ago Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)
Andrew Reynolds [Tue, 12 Mar 2019 19:43:42 +0000 (14:43 -0500)]
 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)

5 years agoErProof class with LFSC output (#2812)
Alex Ozdemir [Fri, 1 Mar 2019 05:54:08 +0000 (21:54 -0800)]
ErProof class with LFSC output (#2812)

* ErProof class with LFSC output

* Created a TraceCheckProof class
   * parsable from text
* Created an ErProof class
   * constructible from a TraceCheckProof
   * writable as LFSC
* A bunch of unit tests

* Reponded to Mathias's first set of comments.

Credits to Mathias for many of the fixes!

* Responed to Andres's first set, fixed tests

I accidentally deleted a "!" last time, causing stuff to fail.

* Use Configuration::isAssertionBuild

* Clarified comment

* Responded to Andres's 2nd review

* Gaurding against a memory error.
* Renaming a file.
* Aggressively unlinking temporary files.

5 years agoUse string stream for proofs instead of tmp files (#2841)
Andres Noetzli [Wed, 27 Feb 2019 00:49:59 +0000 (00:49 +0000)]
Use string stream for proofs instead of tmp files (#2841)

This commit changes CVC4 to use a string stream instead of a temporary
files for proof checking. Note: This change requires a version of LFSC
that supports checking streams (see
https://github.com/CVC4/LFSC/pull/14).

Tested: `make check` passed, changing `holds` to `xholds` in the proof
produced by proof_manager.cpp makes the proofs fail.

5 years agoClangFormat: Disable DerivePointerAlignment (#2842)
Andres Noetzli [Tue, 26 Feb 2019 22:46:04 +0000 (22:46 +0000)]
ClangFormat: Disable DerivePointerAlignment (#2842)

The option `DerivePointerAlignment` tries to automatically determine the
pointer alignment used by the input. In our case, we would eventually
like the code base to be consistent throughtout, so this commit disables
that option.

5 years agoNew C++ API: Remove redundant declareFun function. (#2837)
Aina Niemetz [Wed, 13 Feb 2019 20:52:17 +0000 (12:52 -0800)]
New C++ API: Remove redundant declareFun function. (#2837)

5 years agoRewrite simple regexp pattern to str.contains (#2827)
Andres Noetzli [Wed, 13 Feb 2019 20:18:09 +0000 (12:18 -0800)]
Rewrite simple regexp pattern to str.contains (#2827)

5 years agoNew C++ API: Remove redundant mkTerm function. (#2836)
Aina Niemetz [Wed, 13 Feb 2019 04:16:24 +0000 (20:16 -0800)]
New C++ API: Remove redundant mkTerm function. (#2836)

5 years agoDelete temporary proof files when aborting CVC4 (#2834)
Andres Noetzli [Tue, 12 Feb 2019 19:30:59 +0000 (11:30 -0800)]
Delete temporary proof files when aborting CVC4 (#2834)

CVC4 was not deleting temporary proof files when crashing or being
terminated externally. This commit uses an early `unlink()` to remove
the files as soon as CVC4 terminates.

5 years agoNew C++ API: Unit tests for declare* functions. (#2831)
Aina Niemetz [Mon, 11 Feb 2019 17:04:54 +0000 (09:04 -0800)]
New C++ API: Unit tests for declare* functions. (#2831)

5 years agoMake stripConstantEndpoints() less aggressive (#2830)
Andres Noetzli [Tue, 5 Feb 2019 18:09:15 +0000 (10:09 -0800)]
Make stripConstantEndpoints() less aggressive (#2830)

5 years agoAdd rewrite for contains + const strings replace (#2828)
Andres Noetzli [Mon, 4 Feb 2019 00:17:37 +0000 (16:17 -0800)]
Add rewrite for contains + const strings replace (#2828)

5 years agoFix corner case in stripConstantEndpoints (#2824)
Andres Noetzli [Sat, 2 Feb 2019 08:36:42 +0000 (00:36 -0800)]
Fix corner case in stripConstantEndpoints (#2824)

`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.

5 years agoFix warning due to catching polymorphic exceptions (#2821)
Andres Noetzli [Tue, 29 Jan 2019 22:05:47 +0000 (14:05 -0800)]
Fix warning due to catching polymorphic exceptions (#2821)

5 years agoNew C++ API: Fix checks for mkTerm. (#2820)
Aina Niemetz [Tue, 29 Jan 2019 19:47:04 +0000 (11:47 -0800)]
New C++ API: Fix checks for mkTerm. (#2820)

This required fixing the OpTerm handling for mkTerm functions in the API.

5 years agoStrings: Remove redundant replace rewrite (#2822)
Andres Noetzli [Tue, 29 Jan 2019 18:17:06 +0000 (10:17 -0800)]
Strings: Remove redundant replace rewrite (#2822)

Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.

5 years agoExtended DRAT signature to operational DRAT (#2815)
Alex Ozdemir [Thu, 24 Jan 2019 19:45:12 +0000 (11:45 -0800)]
Extended DRAT signature to operational DRAT (#2815)

* Extended DRAT signature to operational DRAT

The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.

The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).

You can run the new AND old DRAT tests by running

```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```

* Apply suggestions from code review (Yoni)

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
5 years agoAvoid using ProofManager in non-proof CMS build (#2814)
Andres Noetzli [Wed, 23 Jan 2019 18:08:11 +0000 (10:08 -0800)]
Avoid using ProofManager in non-proof CMS build (#2814)

PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.

5 years agoStrings: Strengthen multiset reasoning (#2817)
Andres Noetzli [Wed, 23 Jan 2019 02:47:08 +0000 (18:47 -0800)]
Strings: Strengthen multiset reasoning (#2817)

This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.

5 years ago Fix tuple and record CVC printing (#2818)
Andrew Reynolds [Tue, 22 Jan 2019 21:48:48 +0000 (15:48 -0600)]
 Fix tuple and record CVC printing (#2818)

5 years ago Fix parsing of overloaded parametric datatype selectors (#2819)
Andrew Reynolds [Tue, 22 Jan 2019 20:43:17 +0000 (14:43 -0600)]
 Fix parsing of overloaded parametric datatype selectors (#2819)

5 years agoNew README (markdown). (#2797)
Aina Niemetz [Tue, 22 Jan 2019 18:55:13 +0000 (10:55 -0800)]
New README (markdown). (#2797)