cvc5.git
3 years agoRefactor ANTLR3 dependency (#6202)
Gereon Kremer [Sat, 27 Mar 2021 09:41:49 +0000 (10:41 +0100)]
Refactor ANTLR3 dependency (#6202)

This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.

Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.

3 years agoUse color output to print configuration. (#6219)
Aina Niemetz [Sat, 27 Mar 2021 01:07:27 +0000 (18:07 -0700)]
Use color output to print configuration. (#6219)

3 years agoFloatingPointLiteral: Make constructors that shouldn't be used outside of FloatingPoi...
Aina Niemetz [Fri, 26 Mar 2021 18:32:38 +0000 (11:32 -0700)]
FloatingPointLiteral: Make constructors that shouldn't be used outside of FloatingPoint(Literal) private. (#6211)

3 years agoPass term registry to quantifiers modules (#6216)
Andrew Reynolds [Fri, 26 Mar 2021 16:47:22 +0000 (11:47 -0500)]
Pass term registry to quantifiers modules (#6216)

3 years agoEnsure nonlinear extensions properly reconsiders its model (#6204)
Gereon Kremer [Thu, 25 Mar 2021 20:40:58 +0000 (21:40 +0100)]
Ensure nonlinear extensions properly reconsiders its model (#6204)

In certain cases, the nonlinear extension would not re-check properly but only repeat an (already failed) model repair. The result lemma would then already be in cache and thus not be sent to the solver.
This PR ensures that modelBasedRefinement is always run and entirely removes the d_builtModel flag that was responsible for this behavior. Additionally, it asserts that the lemma that (tries to) force the model to be reconciled during theory combination is actually sent.
Fixes #6192.

3 years agoFP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)
Aina Niemetz [Thu, 25 Mar 2021 19:18:51 +0000 (12:18 -0700)]
FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)

This pushes all symfpu specific parts from FloatingPoint into
FloatingPointLiteral. FloatingPoint is now generic. An additional
FloatingPointLiteral implementation using MPFR will be made configurable
similiarly to how we handle Integers with either GMP or CLN backend.

3 years agoRefactor construction of triggers (#6209)
Andrew Reynolds [Thu, 25 Mar 2021 18:17:30 +0000 (13:17 -0500)]
Refactor construction of triggers (#6209)

This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.

3 years agoDo not use Configuration class in API black tests. (#6205)
Mathias Preiner [Thu, 25 Mar 2021 18:04:54 +0000 (11:04 -0700)]
Do not use Configuration class in API black tests. (#6205)

3 years agoAdd missing includes. (#6207)
Gereon Kremer [Thu, 25 Mar 2021 17:34:39 +0000 (18:34 +0100)]
Add missing includes. (#6207)

This PR adds includes that are missing from source files, but currently provided by other includes.
This mostly concerns <sstream> which is currently included by the statistics, which will change in the future.

3 years agoDeleting old LFSC signatures (#6194)
Haniel Barbosa [Thu, 25 Mar 2021 04:26:17 +0000 (01:26 -0300)]
Deleting old LFSC signatures (#6194)

3 years agoUse inference manager to access intantiate utility instead of quantifiers engine...
Andrew Reynolds [Wed, 24 Mar 2021 22:44:52 +0000 (17:44 -0500)]
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)

Towards breaking dependencies on quantifers engine.

3 years agoOnly consider relevant terms for integer branches (#6181)
Gereon Kremer [Wed, 24 Mar 2021 15:24:25 +0000 (16:24 +0100)]
Only consider relevant terms for integer branches (#6181)

Linear arithmetic simply tried to branch on the first integer variable that had a non-integral assignment.
If it holds stale variables that are not part of the current input, these branches can be emitted and are processed by the solver, but the resulting new assertions will not be considered relevant and thus not added to the theory.
As it still triggers a new theory check, linear arithmetic repeats the same procedure and causes an infinite loop.
This PR explicitly tracks the currently relevant nodes by storing all preregistered nodes and only allows branching on variables from this set.
Fixes #6146.

3 years agoRefactor our integration of LFSC (#6201)
Gereon Kremer [Wed, 24 Mar 2021 15:07:15 +0000 (16:07 +0100)]
Refactor our integration of LFSC (#6201)

This PR further decouples LFSC from the remaining build system, but makes it more convenient to use at the same time.
The contrib/get-lfsc-checker script is now completely standalone and installs LFSC and the necessary signatures to deps/, as well as wrapper scripts to conveniently run lfscc from there and directly check cvc4 proofs.
The goal would be to automatically use LFSC in our regressions as well.

3 years agoRemove unused code for axioms (#6197)
Andrew Reynolds [Tue, 23 Mar 2021 22:44:28 +0000 (17:44 -0500)]
Remove unused code for axioms (#6197)

This is leftover from a previous way of eliminating extended operators

3 years agoRemoving unused build options and deprecated proof compile flag (#6195)
Haniel Barbosa [Tue, 23 Mar 2021 22:27:39 +0000 (19:27 -0300)]
Removing unused build options and deprecated proof compile flag (#6195)

3 years agoPassing term registry to ematching utilities (#6190)
Andrew Reynolds [Tue, 23 Mar 2021 20:41:13 +0000 (15:41 -0500)]
Passing term registry to ematching utilities (#6190)

Model is now nested into term registry.

This PR also resolves some complications due to namespaces within quantifiers.

3 years agoRemove internal includes of Api header. (#6193)
Aina Niemetz [Tue, 23 Mar 2021 18:51:01 +0000 (11:51 -0700)]
Remove internal includes of Api header. (#6193)

3 years agoReplace old sygus term reconstruction algorithm with a new one. (#5779)
Abdalrhman Mohamed [Tue, 23 Mar 2021 14:44:39 +0000 (09:44 -0500)]
Replace old sygus term reconstruction algorithm with a new one. (#5779)

This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.

3 years agoMoving instantiate and skolemize into quantifiers inference manager (#6188)
Andrew Reynolds [Tue, 23 Mar 2021 01:32:32 +0000 (20:32 -0500)]
Moving instantiate and skolemize into quantifiers inference manager (#6188)

After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR.

3 years agoMove statistics from the driver into the SmtEngine (#6170)
Gereon Kremer [Mon, 22 Mar 2021 21:09:55 +0000 (22:09 +0100)]
Move statistics from the driver into the SmtEngine (#6170)

This PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.

    The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
    The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
    The node manager no longer holds a statistics registry (that nobody used anymore anyway)
    The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)

The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.

3 years agoMove equality query utility into quantifiers model (#6186)
Andrew Reynolds [Mon, 22 Mar 2021 18:42:46 +0000 (13:42 -0500)]
Move equality query utility into quantifiers model (#6186)

This simplifies the initialization of quantifiers engine.

This PR also makes general improvements to EqualityQuery.

3 years ago Function types are always first-class (#6167)
Andrew Reynolds [Mon, 22 Mar 2021 17:45:19 +0000 (12:45 -0500)]
 Function types are always first-class (#6167)

This eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class.

This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints.

3 years agoAdd skolem definition manager (#6187)
Andrew Reynolds [Mon, 22 Mar 2021 17:30:21 +0000 (12:30 -0500)]
Add skolem definition manager (#6187)

This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.

This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.

Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.

It also makes some minor reorganization to prop engine.

3 years agoFP: Add documentation for FloatingPointLiteral constructors. (#6183)
Aina Niemetz [Mon, 22 Mar 2021 15:07:02 +0000 (08:07 -0700)]
FP: Add documentation for FloatingPointLiteral constructors. (#6183)

3 years agoGuard for non-unique skolems in term formula removal (#6179)
Andrew Reynolds [Mon, 22 Mar 2021 14:51:05 +0000 (09:51 -0500)]
Guard for non-unique skolems in term formula removal (#6179)

In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.

Fixes #6132.

3 years agoSimplify strings term registration (#6174)
Andrew Reynolds [Sun, 21 Mar 2021 14:01:04 +0000 (09:01 -0500)]
Simplify strings term registration (#6174)

String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode.

This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered.

The PR also simplifies our policies for when string terms are registered slightly.

Fixes #6072.

3 years agoClean up remaining raw uses of output channel (#6161)
Andrew Reynolds [Sun, 21 Mar 2021 13:12:11 +0000 (08:12 -0500)]
Clean up remaining raw uses of output channel (#6161)

After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.

This is work towards standardizing the statistics for theories.

3 years agoImproved tracing for equivalence classes of EE (#6169)
Andrew Reynolds [Sat, 20 Mar 2021 11:42:51 +0000 (06:42 -0500)]
Improved tracing for equivalence classes of EE (#6169)

Helps debugging model issues.

3 years agoGenerate cvc/Kind.java for the java API (#6143)
mudathirmahgoub [Sat, 20 Mar 2021 10:23:44 +0000 (05:23 -0500)]
Generate cvc/Kind.java for the java API (#6143)

PR changes:

Refactor python/genkinds.py by separating parsing from file generation.
Add java/genkinds.py to generate file Kind.java.
Enable java API in ./configure.sh with "under development" warning.

3 years agoRefactor initialization of quantifiers model and builder (#6175)
Andrew Reynolds [Fri, 19 Mar 2021 18:05:47 +0000 (13:05 -0500)]
Refactor initialization of quantifiers model and builder (#6175)

This is in preparation for breaking several circular dependencies and moving
the instantiate utility into the theory inference manager.

3 years agoBitVector: Change setBit to set the bit in place. (#6176)
Aina Niemetz [Fri, 19 Mar 2021 17:28:14 +0000 (10:28 -0700)]
BitVector: Change setBit to set the bit in place. (#6176)

Creating BitVectors (and deleting them) is in general expensive because
of the underlying multi-precision Integer. If possible, unnecessary
constructions and desctructions of BitVectors should be avoided.
The most common use case for `setBit` is that for an existing BitVector,
a given bit should be set to a certain value. Not doing this in place
generates unnecessary constructions and destructions of BitVectors.

3 years agoFP: Use setBit instead of bv or in conversion from Real. (#6177)
Aina Niemetz [Fri, 19 Mar 2021 17:16:56 +0000 (10:16 -0700)]
FP: Use setBit instead of bv or in conversion from Real. (#6177)

This is a minor optimization that goes into effect as soon as #6176 goes
in.

3 years agoWhen giving an SMT-LIB version, defaulting to SMT-LIB 2.6 (#6171)
Haniel Barbosa [Thu, 18 Mar 2021 21:57:11 +0000 (18:57 -0300)]
When giving an SMT-LIB version, defaulting to SMT-LIB 2.6 (#6171)

Warning if not a supported version.

3 years agoMove stats registry to env. (#6173)
Gereon Kremer [Thu, 18 Mar 2021 21:27:35 +0000 (22:27 +0100)]
Move stats registry to env. (#6173)

This PR moves the statistics registry from SmtEngine to Env.

3 years agoEliminate dependency on quantifiers engine in quantifiers model (#6165)
Andrew Reynolds [Thu, 18 Mar 2021 19:51:38 +0000 (14:51 -0500)]
Eliminate dependency on quantifiers engine in quantifiers model (#6165)

3 years agoEliminate more uses of SExpr. (#6149)
Abdalrhman Mohamed [Thu, 18 Mar 2021 18:33:47 +0000 (13:33 -0500)]
Eliminate more uses of SExpr. (#6149)

This PR eliminates all remaining uses of SExpr outside of statistics.

3 years agoNew C++ Api: Comprehensive guards for member functions of class Solver. (#6153)
Aina Niemetz [Thu, 18 Mar 2021 00:28:59 +0000 (17:28 -0700)]
New C++ Api: Comprehensive guards for member functions of class Solver. (#6153)

3 years ago(proof-new) Fixes to set defaults (#6163)
Andrew Reynolds [Wed, 17 Mar 2021 20:45:26 +0000 (15:45 -0500)]
(proof-new) Fixes to set defaults (#6163)

This copies most of the remaining changes to set_defaults.cpp from proof-new.

In particular, it recognizes when proofs must be disabled.

This is required to fix the regressions (locally) and the nightlies.

3 years agoMove utilities for inferred bounds on quantifers to own class (#6159)
Andrew Reynolds [Wed, 17 Mar 2021 18:43:39 +0000 (13:43 -0500)]
Move utilities for inferred bounds on quantifers to own class (#6159)

This also moves some methods from TermEnumeration to QuantifiersBoundInference.

This is required for breaking several cyclic dependencies within quantifiers.

3 years agoNew C++ Api: Comprehensive guards for member functions of class Term. (#6150)
Aina Niemetz [Wed, 17 Mar 2021 18:19:35 +0000 (11:19 -0700)]
New C++ Api: Comprehensive guards for member functions of class Term. (#6150)

3 years agoRename test/unit/expr to test/unit/node. (#6156)
Aina Niemetz [Wed, 17 Mar 2021 18:07:48 +0000 (11:07 -0700)]
Rename test/unit/expr to test/unit/node. (#6156)

This is in preparation for renaming src/expr to src/node.

3 years agoRename fixtures in test/unit/context to conform to naming scheme. (#6158)
Aina Niemetz [Wed, 17 Mar 2021 17:47:39 +0000 (10:47 -0700)]
Rename fixtures in test/unit/context to conform to naming scheme. (#6158)

Naming scheme is `Test<directory><Black|White><name>`.

3 years agoRename fixtures in test/unit/base to conform to naming scheme. (#6157)
Aina Niemetz [Wed, 17 Mar 2021 08:40:21 +0000 (01:40 -0700)]
Rename fixtures in test/unit/base to conform to naming scheme. (#6157)

Naming scheme is `Test<directory><Black|White><name>`.

3 years agoci: Enable checking of proofs + unsat cores. (#6088)
Mathias Preiner [Tue, 16 Mar 2021 20:30:21 +0000 (13:30 -0700)]
ci: Enable checking of proofs + unsat cores. (#6088)

This commit refactors the run_regression.py script and adds options for enabling/disabling checking of proofs and unsat cores. Both options are enabled by default and disabled for each corresponding CI build.

3 years ago[proof-new] Activating proofs when dumping proofs (#6155)
Haniel Barbosa [Tue, 16 Mar 2021 19:59:03 +0000 (16:59 -0300)]
[proof-new] Activating proofs when dumping proofs (#6155)

3 years agoFurther standardization of strings statistics (#6128)
Andrew Reynolds [Tue, 16 Mar 2021 19:14:33 +0000 (14:14 -0500)]
Further standardization of strings statistics (#6128)

Also eliminates use of raw output channel in strings.

3 years agocmake: Generate cvc4_export.h and set visibility to hidden. (#6139)
Mathias Preiner [Tue, 16 Mar 2021 17:56:01 +0000 (10:56 -0700)]
cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)

The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.

Co-authored-by: Gereon Kremer <nafur42@gmail.com>
3 years ago[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)
Haniel Barbosa [Tue, 16 Mar 2021 15:19:46 +0000 (12:19 -0300)]
[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)

3 years ago[proof-new] Disabling proofs on regressions with known bug (#6151)
Haniel Barbosa [Tue, 16 Mar 2021 13:16:31 +0000 (10:16 -0300)]
[proof-new] Disabling proofs on regressions with known bug (#6151)

This is so that we can use CI in master for proofs.

3 years agoNew C++ Api: Comprehensive guards for member functions of class Sort. (#6136)
Aina Niemetz [Tue, 16 Mar 2021 00:13:08 +0000 (17:13 -0700)]
New C++ Api: Comprehensive guards for member functions of class Sort. (#6136)

3 years agoFix rewrite for double replace (#6152)
Andrew Reynolds [Mon, 15 Mar 2021 23:09:16 +0000 (18:09 -0500)]
Fix rewrite for double replace (#6152)

Fixes #6142.

3 years agoNew C++ Api: Comprehensive guards for member functions of class Grammar. (#6148)
Aina Niemetz [Mon, 15 Mar 2021 23:03:05 +0000 (16:03 -0700)]
New C++ Api: Comprehensive guards for member functions of class Grammar. (#6148)

3 years agoReplace HistogramStat by IntegralHistogramStat (#6126)
Gereon Kremer [Mon, 15 Mar 2021 19:58:57 +0000 (20:58 +0100)]
Replace HistogramStat by IntegralHistogramStat (#6126)

This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.

3 years agoDisable sqlite (#6145)
Gereon Kremer [Mon, 15 Mar 2021 19:45:58 +0000 (20:45 +0100)]
Disable sqlite (#6145)

Cryptominisat supports writing statistics to a sqlite3 database, and automatically enabled it when it can find sqlite bindings.
This disables sqlite3, as we don't need it anyway.
Fixes #6131.

3 years agoMake nonlinear extension account for relevant term set (#6147)
Andrew Reynolds [Mon, 15 Mar 2021 19:08:03 +0000 (14:08 -0500)]
Make nonlinear extension account for relevant term set (#6147)

This fixes a subtle issue with non-linear and theory combination.

It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.

In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.

Fixes #5662.

3 years agoSplit inst match generator class to own file (#6125)
Andrew Reynolds [Mon, 15 Mar 2021 18:53:33 +0000 (13:53 -0500)]
Split inst match generator class to own file (#6125)

3 years agoLetify quantifier bodies independently (#6112)
Andrew Reynolds [Mon, 15 Mar 2021 18:46:31 +0000 (13:46 -0500)]
Letify quantifier bodies independently (#6112)

This fixes a subtle bug with how quantifier bodies are letified.

It makes our letification more conservative so that let symbols are never pushed inside quantifier bodies, instead quantifier bodies are letified independently of the context.

3 years agoReorganizing initialization of term registry in quantifiers (#6127)
Andrew Reynolds [Mon, 15 Mar 2021 18:17:19 +0000 (13:17 -0500)]
Reorganizing initialization of term registry in quantifiers (#6127)

This is in preparation for moving several utilities into the quantifiers inference manager.

This PR moves ownership of TermRegistry and QuantifiersRegistry to TheoryQuantifiers from QuantifiersEngine.

3 years agoNew C++ Api: Comprehensive guards for member functions of class Op. (#6140)
Aina Niemetz [Mon, 15 Mar 2021 17:54:16 +0000 (10:54 -0700)]
New C++ Api: Comprehensive guards for member functions of class Op. (#6140)

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)