cvc5.git
3 years agoNew C++ Api: Comprehensive guards for member functions of Datatype classes. (#6141)
Aina Niemetz [Mon, 15 Mar 2021 17:40:31 +0000 (10:40 -0700)]
New C++ Api: Comprehensive guards for member functions of Datatype classes. (#6141)

3 years ago[proof-new] Adding a dot printer for proof nodes (#6144)
Diego Della Rocca de Camargos [Sun, 14 Mar 2021 14:55:55 +0000 (11:55 -0300)]
[proof-new] Adding a dot printer for proof nodes (#6144)

Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).

Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>
3 years agoNew C++ Api: Move checks to separate file. (#6138)
Aina Niemetz [Fri, 12 Mar 2021 22:45:14 +0000 (14:45 -0800)]
New C++ Api: Move checks to separate file. (#6138)

3 years agoNew C++ API: Rename TRY CATCH macros. (#6135)
Aina Niemetz [Fri, 12 Mar 2021 20:51:50 +0000 (12:51 -0800)]
New C++ API: Rename TRY CATCH macros. (#6135)

3 years agoSchedule preregistration lemmas to be satisfied after user assertions (#6134)
Andres Noetzli [Fri, 12 Mar 2021 20:26:55 +0000 (12:26 -0800)]
Schedule preregistration lemmas to be satisfied after user assertions (#6134)

Commit d47a8708171f1cf488fe9ce05f56f2566db53093 refactored the interface of
prop engine. In doing so, it changed the order in which preregistration lemmas
were asserted. Before the commit, they were asserted after all the user
assertions. After the commit, they were asserted after each user assertion that
generated them. This, however, seems to have a negative performance impact,
especially for string benchmarks because the justification heuristic tries to
justify the assertions in the order in which they appear. Intuitively, it makes
sense to first try to satisfy the user assertions before trying to satisfy the
preregistration lemmas.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>
3 years agocmake: Remove install rules for old API headers. (#6120)
Mathias Preiner [Fri, 12 Mar 2021 19:26:44 +0000 (11:26 -0800)]
cmake: Remove install rules for old API headers. (#6120)

3 years ago(proof-new) Miscellaneous sync to master (#6129)
Andrew Reynolds [Fri, 12 Mar 2021 19:06:03 +0000 (13:06 -0600)]
(proof-new) Miscellaneous sync to master (#6129)

Towards having proofs working on master.

3 years ago[proof-new] Fix arity check when building equality engine proofs (#6133)
Haniel Barbosa [Fri, 12 Mar 2021 18:03:41 +0000 (15:03 -0300)]
[proof-new] Fix arity check when building equality engine proofs  (#6133)

Broken in dc679ed.

3 years agoAdd missing includes for statistics (#6124)
Gereon Kremer [Fri, 12 Mar 2021 17:53:04 +0000 (18:53 +0100)]
Add missing includes for statistics (#6124)

3 years agoSimplify instantiation match generator interface (#6121)
Andrew Reynolds [Fri, 12 Mar 2021 01:50:00 +0000 (19:50 -0600)]
Simplify instantiation match generator interface (#6121)

3 years agoAdd more unit tests for api::Sort. (#6122)
Aina Niemetz [Fri, 12 Mar 2021 01:32:09 +0000 (17:32 -0800)]
Add more unit tests for api::Sort. (#6122)

3 years agoci: Replace debug builds with assertion enabled production builds. (#6098)
Mathias Preiner [Fri, 12 Mar 2021 00:44:45 +0000 (16:44 -0800)]
ci: Replace debug builds with assertion enabled production builds. (#6098)

This will help reduce the CI times and ccache sizes.

3 years agoMake linear arithmetic use its inference manager (#5934)
Gereon Kremer [Thu, 11 Mar 2021 22:48:11 +0000 (23:48 +0100)]
Make linear arithmetic use its inference manager (#5934)

This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.

3 years agoarith proof rules shuffle & add ARITH_SUM_UB (#6118)
Alex Ozdemir [Thu, 11 Mar 2021 22:13:57 +0000 (14:13 -0800)]
arith proof rules shuffle & add ARITH_SUM_UB (#6118)

Preparation for making ARITH_SCALE_SUM_UB a macro.

Adds a proof rule for summing upper bounds: ARITH_SUM_UB.
Moves ARITH_MULT_* rules from the non-linear extension to the main
arithmetic checker, since they will be needed for all of arith now.
Aligns the ARITH_SCALE_SUM_UB documentation with its checker.

3 years agoIntroduce inference ids for quantifier instantiation (#6119)
Andrew Reynolds [Thu, 11 Mar 2021 20:59:40 +0000 (14:59 -0600)]
Introduce inference ids for quantifier instantiation (#6119)

This makes quantifiers use standard inference ids.

This eliminates the need to track ad-hoc statistics, per instantiation type.

This makes minor modifications to a few interfaces in quantifiers to enable this.

3 years agoFirst refactoring of statistics classes (#6105)
Gereon Kremer [Thu, 11 Mar 2021 20:20:19 +0000 (21:20 +0100)]
First refactoring of statistics classes (#6105)

This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.

Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.

3 years agoDelete Expr layer. (#6117)
Aina Niemetz [Thu, 11 Mar 2021 19:05:58 +0000 (11:05 -0800)]
Delete Expr layer. (#6117)

3 years agoImprovements and refactoring for enumeratative strategy (#6030)
MikolasJanota [Thu, 11 Mar 2021 16:28:51 +0000 (17:28 +0100)]
Improvements and refactoring for enumeratative strategy (#6030)

Refactoring out the code from  `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.

Signed-off-by: mikolas <mikolas.janota@gmail.com>
3 years ago(proof-new) Clean up uses of witness with skolem lemmas (#6109)
Andrew Reynolds [Thu, 11 Mar 2021 09:21:06 +0000 (03:21 -0600)]
(proof-new) Clean up uses of witness with skolem lemmas (#6109)

This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.

It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.

3 years agoDirect lemmas and inference ids for sygus extension (#5960)
Andrew Reynolds [Thu, 11 Mar 2021 08:44:30 +0000 (02:44 -0600)]
Direct lemmas and inference ids for sygus extension (#5960)

This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.

3 years agoFix compile warnings when compiling with GLPK. (#6115)
Mathias Preiner [Thu, 11 Mar 2021 03:08:01 +0000 (19:08 -0800)]
Fix compile warnings when compiling with GLPK. (#6115)

Fixes -Wshadow and -Wsuggest-override wranings.

3 years agoRemove obsolete test/api/statistics.cpp. (#6116)
Aina Niemetz [Thu, 11 Mar 2021 02:29:57 +0000 (18:29 -0800)]
Remove obsolete test/api/statistics.cpp. (#6116)

This test shouldn't be an API test and is not portable to the new API
right now statistics are not retrievable via the API. When we add
methods for retrieving statistics to the new API, we'll need thorough
unit tests this, which makes this test obsolete.

3 years agoClean up ownership of Datatypes in NodeManager. (#6113)
Aina Niemetz [Thu, 11 Mar 2021 02:00:22 +0000 (18:00 -0800)]
Clean up ownership of Datatypes in NodeManager. (#6113)

This is in preparation for deleting the Expr layer.
This further fixes incorrect handling of ownership for the datatypes
owned by the NodeManager.

3 years agoRefactor Node::getOperator() to fix compiler warning. (#6110)
Aina Niemetz [Thu, 11 Mar 2021 01:18:11 +0000 (17:18 -0800)]
Refactor Node::getOperator() to fix compiler warning. (#6110)

3 years agoUse CVC4_ASSERTIONS instead of NDEBUG. (#6099)
Mathias Preiner [Thu, 11 Mar 2021 00:51:12 +0000 (16:51 -0800)]
Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)

Ensures that all checks are performed in production builds with enabled assertions.

3 years agoAdd GitHub action to automatically update approved PRs. (#6114)
Mathias Preiner [Thu, 11 Mar 2021 00:09:27 +0000 (16:09 -0800)]
Add GitHub action to automatically update approved PRs. (#6114)

3 years agoUse Assert instead of assert. (#6095)
Mathias Preiner [Wed, 10 Mar 2021 23:58:11 +0000 (15:58 -0800)]
Use Assert instead of assert. (#6095)

This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.

3 years agoNew C++ Api: Add missing argument checks in Solver functions. (#6094)
Aina Niemetz [Wed, 10 Mar 2021 23:27:17 +0000 (15:27 -0800)]
New C++ Api: Add missing argument checks in Solver functions. (#6094)

This adds missing checks to guard that Term and Sort arguments are
associated with the solver object that is called.

3 years agoAdd Env class (#6093)
Andrew Reynolds [Wed, 10 Mar 2021 23:00:59 +0000 (17:00 -0600)]
Add Env class (#6093)

This class contains all globally available utilities for internal code.

3 years agoImproved handing of 'lib64' vs. 'lib' for glpk-cut-log and antlr-3.4 (#6091)
Andrew V. Jones [Wed, 10 Mar 2021 22:10:12 +0000 (22:10 +0000)]
Improved handing of 'lib64' vs. 'lib' for glpk-cut-log and antlr-3.4 (#6091)

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
3 years ago[proof-new] Clarifying doc (#6108)
Haniel Barbosa [Wed, 10 Mar 2021 21:33:41 +0000 (18:33 -0300)]
[proof-new] Clarifying doc (#6108)

3 years agoMove ExprManager::isNAryKind to NodeManager. (#6107)
Aina Niemetz [Wed, 10 Mar 2021 21:28:58 +0000 (13:28 -0800)]
Move ExprManager::isNAryKind to NodeManager. (#6107)

This also renames metakind::getLowerBoundForKind and
metakind::getUpperBoundForKind for consistency.

Note that the NodeManager class needs to be reordered to comply to our
style guidelines. This PR does not reorder but introduces a public block
at the top (where the rest of the public interface of the class should
go eventually).

3 years agoImprove arithmetic proofs (#6106)
Gereon Kremer [Wed, 10 Mar 2021 20:48:13 +0000 (21:48 +0100)]
Improve arithmetic proofs (#6106)

The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.

3 years agocmake: Fix optimization level for debug builds. (#6097)
Mathias Preiner [Wed, 10 Mar 2021 19:40:15 +0000 (11:40 -0800)]
cmake: Fix optimization level for debug builds. (#6097)

Further cleans up some unused variables and moves the configuration of
best to configure.sh.

3 years ago(proof-new) Update ppRewrite to use skolem lemmas (#6102)
Andrew Reynolds [Wed, 10 Mar 2021 19:07:39 +0000 (13:07 -0600)]
(proof-new) Update ppRewrite to use skolem lemmas (#6102)

This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.

As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:

(P (witness ((x T)) (A x)))

now we return:

(P k), with skolem lemma ( (A k), k )

Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.

3 years agoFix extended equality rewrite involving replace. (#6104)
Andrew Reynolds [Wed, 10 Mar 2021 18:32:19 +0000 (12:32 -0600)]
Fix extended equality rewrite involving replace. (#6104)

Fixes #6075.

3 years agoFix term registration and non-theory-preprocessed terms in substitutions (#6080)
Andrew Reynolds [Wed, 10 Mar 2021 16:06:27 +0000 (10:06 -0600)]
Fix term registration and non-theory-preprocessed terms in substitutions (#6080)

This fixes two issues for preprocessing:
(1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to.
(2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing.

To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing.

These two fixes are required to fix #6071.

Note: we should performance test this on SMT-LIB.

3 years agoAdd quant elim regression (#6103)
Andrew Reynolds [Wed, 10 Mar 2021 15:55:46 +0000 (09:55 -0600)]
Add quant elim regression (#6103)

Fixes #5658.

This was fixed by recent refactoring to quantifier elimination, adding the regression to close the issue.

3 years ago(proof-new) Replace witness form by original form in the internal proof calculus...
Andrew Reynolds [Wed, 10 Mar 2021 13:33:49 +0000 (07:33 -0600)]
(proof-new) Replace witness form by original form in the internal proof calculus  (#6051)

This makes a simplification to the internal proof calculus. In particular, purification skolems are no longer are special case of witness skolems. They are now independent concepts. The concept of "witness form" is replaced in most places by "original form".

This is required for fixing two issues:
(1) variable shadowing issues in skolemization.
(2) bookkeeping issues for bound variables introduced to construct witness terms. This made the LFSC proof conversion extremely cumbersome for e.g. string reductions.

In this PR, the main changes:

The internals of SkolemManager are changed to use original form vs witness form when necessary. This eliminates the need to do variable renaming in SkolemManager::skolemize.
the rule WITNESS_INTRO is replaced by SKOLEM_INTRO
MACRO_SR_* rules use original form
Proof post processing is simplified
These changes imply that ppRewrite should not return WITNESS terms. Followup PRs will modify arithmetic preprocessing so that its ppRewrite method returns skolems instead.

3 years agotest: Fix missing std::. (#6096)
Mathias Preiner [Wed, 10 Mar 2021 00:32:40 +0000 (16:32 -0800)]
test: Fix missing std::. (#6096)

3 years agoNew C++ Api: Use const ref for arguments when possible. (#6092)
Aina Niemetz [Tue, 9 Mar 2021 23:10:40 +0000 (15:10 -0800)]
New C++ Api: Use const ref for arguments when possible. (#6092)

3 years agoMerge initialization steps in TheoryModelBuilder (#4901)
Andrew Reynolds [Tue, 9 Mar 2021 22:31:38 +0000 (16:31 -0600)]
Merge initialization steps in TheoryModelBuilder (#4901)

Currently when constructing models, we traverse the equality engine of the model 3 times during initialization. This PR merges these 3 traversals.

This refactoring is necessary to update model building for the "centralized" approach for equality reasoning, where it will be important to traverse the equality engine of the model in a careful way (to skip irrelevant terms).

The PR also makes a few minor optimizations for e.g. reducing map lookups, and adds more documentation.

3 years agoRemove logic request (#6089)
Andrew Reynolds [Tue, 9 Mar 2021 22:07:30 +0000 (16:07 -0600)]
Remove logic request (#6089)

This removes use of the logic request utility.

It generally bad practice to change the logic dynamically, e.g. during preprocessing, since it makes it so that CVC4 does not properly initialize. We now insist that logic is changed upfront in set_defaults.

This is in preparation for the smt::Env class, which will change the ownership of logic.

3 years agoNew C++ Api: Migrate stats collection for consts, vars, terms. (#6090)
Aina Niemetz [Tue, 9 Mar 2021 21:44:06 +0000 (13:44 -0800)]
New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)

3 years agoContextObj::destroy(): Guard against invalid use. (#6082)
Aina Niemetz [Tue, 9 Mar 2021 20:59:13 +0000 (12:59 -0800)]
ContextObj::destroy(): Guard against invalid use. (#6082)

We do not allow that a context object is invalid on destruction.
This guards against invalid use as described in #2607. Note that #2607
proposed to skip invalid objects on destruction. We now rather do not
allow for such a case to occur at all.

3 years agoNew C++ Api: Clean up usage of internal kind. (#6087)
Aina Niemetz [Tue, 9 Mar 2021 20:11:35 +0000 (12:11 -0800)]
New C++ Api: Clean up usage of internal kind. (#6087)

3 years ago(proof-new) Minor fix and allow proof option (#6085)
Andrew Reynolds [Tue, 9 Mar 2021 19:02:14 +0000 (13:02 -0600)]
(proof-new) Minor fix and allow proof option (#6085)

This is in preparation for enabling CI / proofs on master.

This does not throw an option exception when proofs are enabled, it also makes a fix that was missing on master and needed for regressions to pass on master.

This is partially taken from #5980.

3 years agoNew C++ API: Reorder and clean up cpp file. (#6086)
Aina Niemetz [Tue, 9 Mar 2021 18:00:47 +0000 (10:00 -0800)]
New C++ API: Reorder and clean up cpp file. (#6086)

3 years agoAdd missing include if GLPK is enabled. (#6084)
Gereon Kremer [Tue, 9 Mar 2021 14:05:22 +0000 (15:05 +0100)]
Add missing include if GLPK is enabled. (#6084)

Fixes the nightly builds with GLPK.

3 years agoSome more cleanup of includes (#6083)
Gereon Kremer [Tue, 9 Mar 2021 12:48:43 +0000 (13:48 +0100)]
Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

3 years agoUpdate copyright headers to 2021. (#6081)
Aina Niemetz [Tue, 9 Mar 2021 07:27:03 +0000 (23:27 -0800)]
Update copyright headers to 2021. (#6081)

3 years agoNew C++ API: Migrate to Node layer. (#6070)
Aina Niemetz [Tue, 9 Mar 2021 00:59:35 +0000 (16:59 -0800)]
New C++ API: Migrate to Node layer. (#6070)

The following items will be added / adressed in subsequent PRs:

* migrate statistics tracking for variables and bound variables

* migrate adding of listeners when variables and bound variables
  are created

* consistent and clean NodeManagerScope handling
  (out of scope for this PR)

* clean up all interfaces to use const references when possible

3 years agoRefactor ouroborous API test to not use Expr. (#6079)
Aina Niemetz [Mon, 8 Mar 2021 22:48:36 +0000 (14:48 -0800)]
Refactor ouroborous API test to not use Expr. (#6079)

3 years agocontrib: Do not use HOST env variable for cross-compilation host target. (#6078)
Mathias Preiner [Mon, 8 Mar 2021 20:24:41 +0000 (12:24 -0800)]
contrib: Do not use HOST env variable for cross-compilation host target. (#6078)

On some systems HOST is set by default to the host name. This commit adds a --host option for the get-antlr-3.4 and get-gmp-dev scripts. It further simplifies the machine type check in get-antlr-3.4 and updates the GMP version to 6.2.1.

3 years agoFix handling of negation of Boolean bound variables in FMF (#6066)
Andrew Reynolds [Mon, 8 Mar 2021 20:11:24 +0000 (14:11 -0600)]
Fix handling of negation of Boolean bound variables in FMF (#6066)

Fixes #5922. We were not correctly handling when a Boolean bound variable was negated.

3 years agoBuild api tests in build/bin/test/api. (#6076)
Aina Niemetz [Mon, 8 Mar 2021 19:10:14 +0000 (11:10 -0800)]
Build api tests in build/bin/test/api. (#6076)

Previously, api tests where built in build/test/api instead of in the
bin directory for the tests.

3 years ago(proof-new) Separating optimizations for strings skolem caching (#6064)
Andrew Reynolds [Mon, 8 Mar 2021 17:32:43 +0000 (11:32 -0600)]
(proof-new) Separating optimizations for strings skolem caching (#6064)

This PR ensures that several optimizations are not performed in the reference implementation of skolem sharing (d_useOpts=false). This is to ensure that the many of the rules in the strings proof checker do not depend on the rewriter.

These errors were caught by the LFSC proof checker.

3 years ago(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)
Andrew Reynolds [Mon, 8 Mar 2021 17:06:45 +0000 (11:06 -0600)]
(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)

Due to recent simplifications in the internal calculus, we will no longer reason about WITNESS terms in conclusions of ProofNode, instead WITNESS terms will only be for bookkeeping.This means that some implementations of ppRewrite must change to return SKOLEM instead of WITNESS terms.

Since witness terms are currently used as a way of specifying "replace t by skolem k, and send a lemma about k", a followup PR will update Theory::ppRewrite to take an additional argument std::vector<SkolemLemma>& lems where new lemmas must be explicitly added to a vector (instead of encoded as witness). Then, all Theory::ppRewrite will return skolems instead of witness terms.

This PR changes arithmetic in preparation for this change.

Notice that I'm introducing SkolemLemma in this PR, which is a very common pattern that can simplify some of our interfaces, e.g. see https://github.com/CVC4/CVC4/blob/master/src/smt/term_formula_removal.h#L93, https://github.com/CVC4/CVC4/blob/master/src/prop/prop_engine.h#L94.

Note that the indentation of code in operator_elim.cpp changed.

3 years agoSimplify theory preprocessing (#6058)
Andrew Reynolds [Mon, 8 Mar 2021 16:50:39 +0000 (10:50 -0600)]
Simplify theory preprocessing (#6058)

Theory preprocessing now theory-preprocesses lemmas until fixed point. This eliminates the old code for rewriting them only, which is no longer necessary as theory-preprocessing subsumes rewriting.

3 years agoFix justification heuristic again (#6074)
Gereon Kremer [Mon, 8 Mar 2021 14:46:30 +0000 (15:46 +0100)]
Fix justification heuristic again (#6074)

This PR replaces all TNode types in datatypes by Node within justification heuristic.
Fixes #6073.
Unfortunately, the example from #6073 times out now, thus there is no new regression.

3 years agoDo not process conjunctions as facts in strings (#6065)
Andrew Reynolds [Mon, 8 Mar 2021 09:40:05 +0000 (03:40 -0600)]
Do not process conjunctions as facts in strings (#6065)

This changes things so we process inferences with AND conclusions as lemmas always.

This fixes #6056, that benchmark times out.

3 years agoRemove partial UDIV/UREM operators. (#6069)
Mathias Preiner [Sat, 6 Mar 2021 03:28:19 +0000 (19:28 -0800)]
Remove partial UDIV/UREM operators. (#6069)

This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.

3 years agoRemove SMT-LIB 2.5 and 2.0 support. (#6068)
Mathias Preiner [Sat, 6 Mar 2021 00:17:15 +0000 (16:17 -0800)]
Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

3 years agoSet logic in interpolation unit test. (#6067)
yoni206 [Fri, 5 Mar 2021 20:09:41 +0000 (12:09 -0800)]
Set logic in interpolation unit test. (#6067)

The logic QF_LIA was not set in the api interpolation test.
Setting it brings the solving time from ~37s to ~2s.
Also, a comment is fixed.

3 years agoInitial implementation of an optimization solver with unit tests. (#5849)
mcjuneho [Fri, 5 Mar 2021 19:51:23 +0000 (11:51 -0800)]
Initial implementation of an optimization solver with unit tests. (#5849)

3 years agogoogle test: Remove obsolete Expr test fixtures. (#6060)
Aina Niemetz [Fri, 5 Mar 2021 14:09:06 +0000 (06:09 -0800)]
google test: Remove obsolete Expr test fixtures. (#6060)

3 years agoReimplement time limit mechanism for windows (#6049)
Gereon Kremer [Fri, 5 Mar 2021 11:37:50 +0000 (12:37 +0100)]
Reimplement time limit mechanism for windows (#6049)

As noted in #5034, --tlimit is not working properly on windows. It turns out that the timer mechanism provided by the windows API are not suitable for our use case. Thus, this PR implements a generic std::thread-based timer mechanism which is used whenever the POSIX timers (setitimer) are not available. It also adds some documentation on the timer options and the reasons we ended up with this.
Fixes #5034.

3 years agogoogle test: Remove dependency on ExprManager in type_cardinality_black. (#6061)
Aina Niemetz [Fri, 5 Mar 2021 07:21:08 +0000 (23:21 -0800)]
google test: Remove dependency on ExprManager in type_cardinality_black. (#6061)

3 years agoNew C++ API: Clean up usage of interal datatype classes. (#6055)
Aina Niemetz [Thu, 4 Mar 2021 23:29:00 +0000 (15:29 -0800)]
New C++ API: Clean up usage of interal datatype classes. (#6055)

This disables the temporarily available internals of datatype classes.

3 years agoAdd initial bit-blaster for proof logging. (#6053)
Aina Niemetz [Thu, 4 Mar 2021 22:07:16 +0000 (14:07 -0800)]
Add initial bit-blaster for proof logging. (#6053)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
3 years agoNew C++ Api: Clean up usage of internal types in Term. (#6054)
Aina Niemetz [Thu, 4 Mar 2021 20:07:13 +0000 (12:07 -0800)]
New C++ Api: Clean up usage of internal types in Term. (#6054)

This disables the temporarily available internals of Term.
Note: getExpr() is still available and will be disabled when the API is
      fully converted to Nodes.

3 years agoAdd proper define for libpoly usage (#6050)
Gereon Kremer [Thu, 4 Mar 2021 19:36:02 +0000 (20:36 +0100)]
Add proper define for libpoly usage (#6050)

When adding libpoly, we forgot to add a proper define to cvc4autoconfig and included real_algebraic_number.h everywhere to get this define. This PR introduces the CVC4_POLY_IMP define and removes all obsolete includes to real_algebraic_number.h.

3 years agoAdd cmake scripts for iwyu targets. (#6042)
Gereon Kremer [Thu, 4 Mar 2021 19:03:24 +0000 (20:03 +0100)]
Add cmake scripts for iwyu targets. (#6042)

This PR adds some utility targets that simplify the usage of iwyu (include-what-you-use) on our code base.

3 years agoFix nightlies. (#6052)
Aina Niemetz [Thu, 4 Mar 2021 18:49:28 +0000 (10:49 -0800)]
Fix nightlies. (#6052)

3 years agoIgnore isInConflict when adding conflicts (#5995)
Gereon Kremer [Thu, 4 Mar 2021 14:24:21 +0000 (15:24 +0100)]
Ignore isInConflict when adding conflicts (#5995)

Right now, the inference manager infrastructure drops conflicts (and literal propagations) if the solver already is in a conflict.
This PR removes this behavior. The current setup in linear arithmetic requires adding conflicts, even when already in conflict, and experiments showed a small but beneficial effect of this change.

3 years agoFix nightlies. (#6048)
Aina Niemetz [Thu, 4 Mar 2021 03:06:53 +0000 (19:06 -0800)]
Fix nightlies. (#6048)

3 years agocontext_black: Clean up classes. (#6046)
Aina Niemetz [Thu, 4 Mar 2021 02:24:00 +0000 (18:24 -0800)]
context_black: Clean up classes. (#6046)

This cleans up the MyContext* classes defined for the tests according to
the code style guidelines. It further converts non-fixed width integer
types to fixed-width types. This was missed in #5587.

3 years agoNew C++ API: Clean up usage of internal Type/TypeNodes. (#6044)
Aina Niemetz [Thu, 4 Mar 2021 01:58:33 +0000 (17:58 -0800)]
New C++ API: Clean up usage of internal Type/TypeNodes. (#6044)

This disables the temporarily available internals of Sort.

3 years agoNew C++ API: Clean up usage of internal Result. (#6043)
Aina Niemetz [Thu, 4 Mar 2021 01:36:57 +0000 (17:36 -0800)]
New C++ API: Clean up usage of internal Result. (#6043)

This disables the temporarily available internals of Result.
It further changes the interface for getUnknownExplanation, which now
returns an enum value instead of a string.

3 years agoNew C++ API: Clean up usage of internal types in Op. (#6045)
Aina Niemetz [Thu, 4 Mar 2021 01:17:17 +0000 (17:17 -0800)]
New C++ API: Clean up usage of internal types in Op. (#6045)

This disables the temporarily available internals of Op.

3 years agoRemove obsolete gcc check. (#6041)
Gereon Kremer [Wed, 3 Mar 2021 17:59:43 +0000 (18:59 +0100)]
Remove obsolete gcc check. (#6041)

This PR removes a cmake check for gcc 4.5.1. As this version is more than a decade old and would not work anyway, as it does not fully support C++11, not to mention C++17.

3 years ago(proof-new) Simplifications to arithmetic operator elimination and preprocessing...
Andrew Reynolds [Wed, 3 Mar 2021 17:25:02 +0000 (11:25 -0600)]
(proof-new) Simplifications to arithmetic operator elimination and preprocessing (#6040)

Due to refactoring in theory preprocessor, which does fixed point preprocessing on created lemmas, several things can be simplified in arithmetic operator elimination.

This is required for further simplification to witness forms in the internal proof calculus.

3 years agoMore cleanup of includes to reduce compilation times (#6037)
Gereon Kremer [Wed, 3 Mar 2021 16:50:45 +0000 (17:50 +0100)]
More cleanup of includes to reduce compilation times (#6037)

Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.

3 years agoRemove uses of SExpr class. (#6035)
Abdalrhman Mohamed [Wed, 3 Mar 2021 10:28:45 +0000 (04:28 -0600)]
Remove uses of SExpr class. (#6035)

This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.

3 years agoAdd tuple projection operator (#5904)
mudathirmahgoub [Wed, 3 Mar 2021 08:16:32 +0000 (02:16 -0600)]
Add tuple projection operator (#5904)

This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.

3 years agoRemove non-ASCII characters from source files. (#6039)
Mathias Preiner [Tue, 2 Mar 2021 23:22:03 +0000 (15:22 -0800)]
Remove non-ASCII characters from source files. (#6039)

Make collect_tags.py more robust for non-ASCII characters.

3 years agoImprove handling of utf8 encoded inputs (#5694)
Gereon Kremer [Tue, 2 Mar 2021 22:49:29 +0000 (23:49 +0100)]
Improve handling of utf8 encoded inputs (#5694)

This PR fixes an issue where utf8 encoded inputs are incorrectly parsed into CVC4::String. We now use std::mbtowc to first turn the char sequence from the std::string input into a std::wstring and then process this std::wstring one charactor (wchar_t) at a time.
Fixes #5673

3 years agoRemove obsolete dependency on CxxTest. (#6038)
Aina Niemetz [Tue, 2 Mar 2021 22:06:38 +0000 (14:06 -0800)]
Remove obsolete dependency on CxxTest. (#6038)

3 years agoAdd aarch64 (ARM64) cross-compile support. (#6033)
Mathias Preiner [Tue, 2 Mar 2021 08:26:29 +0000 (00:26 -0800)]
Add aarch64 (ARM64) cross-compile support. (#6033)

This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64.

Fixes #1479 #5769.

3 years agoFix nightly errors. (#6034)
Mathias Preiner [Tue, 2 Mar 2021 04:18:24 +0000 (20:18 -0800)]
Fix nightly errors. (#6034)

Fixes warnings with CVC4_FALLTHROUGH and -Werror for debug/production with gcc/clang. Clang detects that a CVC4_FALLTHROUGH after an Assert(false); is unreachable and issues a warning, while gcc issues a warning about an implicit fall-through if CVC4_FALLTHROUGH is not present.

3 years agoIntroduce quantifiers term registry (#5983)
Andrew Reynolds [Tue, 2 Mar 2021 03:37:03 +0000 (21:37 -0600)]
Introduce quantifiers term registry (#5983)

This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.

3 years agoClean up includes to reduce compile times (#6031)
Gereon Kremer [Tue, 2 Mar 2021 00:58:20 +0000 (01:58 +0100)]
Clean up includes to reduce compile times (#6031)

This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.

3 years agogoogle test: util: Migrate floatingpoint_black. (#6021)
Aina Niemetz [Tue, 2 Mar 2021 00:07:25 +0000 (16:07 -0800)]
google test: util: Migrate floatingpoint_black. (#6021)

3 years agogoogle test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)
Aina Niemetz [Mon, 1 Mar 2021 23:32:16 +0000 (15:32 -0800)]
google test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)

3 years agogoogle test: util: Migrate bitvector_black. (#6015)
Aina Niemetz [Mon, 1 Mar 2021 22:46:53 +0000 (14:46 -0800)]
google test: util: Migrate bitvector_black. (#6015)

3 years agogoogle test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)
Aina Niemetz [Mon, 1 Mar 2021 22:00:51 +0000 (14:00 -0800)]
google test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)

3 years agoRefactor collection of debug and trace tags (#5996)
Gereon Kremer [Mon, 1 Mar 2021 21:17:54 +0000 (22:17 +0100)]
Refactor collection of debug and trace tags (#5996)

We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags.
This mechanism relies on a collection of more or less readable shell scripts.
#5921 hinted to a problem with the current setup, as it passes all source files via command line.
This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line.
As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable.
Fixes #5921.

3 years agoMake -Werror optional but enable it for CI. (#6032)
Mathias Preiner [Mon, 1 Mar 2021 18:36:58 +0000 (10:36 -0800)]
Make -Werror optional but enable it for CI. (#6032)

3 years agogoogle test: util: Migrate stats_black. (#6029)
Aina Niemetz [Mon, 1 Mar 2021 16:40:11 +0000 (08:40 -0800)]
google test: util: Migrate stats_black. (#6029)

3 years agogoogle test: util: Migrate real_algebraic_number_black. (#6028)
Aina Niemetz [Mon, 1 Mar 2021 16:04:01 +0000 (08:04 -0800)]
google test: util: Migrate real_algebraic_number_black. (#6028)