cvc5.git
3 years agoIntegrate Lazard into CAD module (#6812)
Gereon Kremer [Tue, 6 Jul 2021 23:01:13 +0000 (01:01 +0200)]
Integrate Lazard into CAD module (#6812)

This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.

3 years agoIntegrate learned rewrite preprocessing pass (#6840)
Andrew Reynolds [Tue, 6 Jul 2021 22:44:09 +0000 (17:44 -0500)]
Integrate learned rewrite preprocessing pass (#6840)

This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.

3 years agoAdd implementation of learned rewrite pass (#6843)
Andrew Reynolds [Tue, 6 Jul 2021 20:00:38 +0000 (15:00 -0500)]
Add implementation of learned rewrite pass (#6843)

3 years agoAdd learned rewrite preprocessing pass (#6842)
Andrew Reynolds [Tue, 6 Jul 2021 17:23:45 +0000 (12:23 -0500)]
Add learned rewrite preprocessing pass (#6842)

Adds the basic skeleton of the pass.

3 years agoPorting C++ API examples to SMT-LIB examples (#6789)
Haniel Barbosa [Tue, 6 Jul 2021 16:29:25 +0000 (13:29 -0300)]
Porting C++ API examples to SMT-LIB examples (#6789)

SyGuS examples will come later.

3 years agoAdd some printing functions for OptimizationObjective and OptimizationResult (#6809)
Ouyancheng [Tue, 6 Jul 2021 03:22:14 +0000 (20:22 -0700)]
Add some printing functions for OptimizationObjective and OptimizationResult (#6809)

Implement the operator << with std::ostream for OptimizationObjective and OptimizationResult. Currently only supports SMTLib2 or Sygus as output languages.
Objective: (maximize [node] :signed) or (minimize [node]) or ...
Result: (sat [expr]) or (unsat) or (unknown([explanation]) [expr/null])

3 years agoAdd doc page about transcendentals (#6755)
Gereon Kremer [Tue, 6 Jul 2021 02:13:47 +0000 (04:13 +0200)]
Add doc page about transcendentals (#6755)

This PR adds a theory reference page for the transcendental extension.

3 years ago[Strings] Fix incorrect rewrite (#6837)
Andres Noetzli [Mon, 5 Jul 2021 13:29:09 +0000 (06:29 -0700)]
[Strings] Fix incorrect rewrite (#6837)

Fixes #6834. There were two cases in our extended rewriter for string
equalities that were modifying the node without returning and without
updating information computed from the original node. This mismatch led
to incorrect rewrites. This commit fixes the issue by adding a flag to
returnRewrite() that determines whether node that was an equality
before and after the rewrite should be rewritten again with the extended
rewriter. We generally do not do that (we'd run in danger of rewriting
equality nodes with the extended rewriter even though we shouldn't) but
for the rewrites that were previously continuing to rewrite the node, we
set this flag and return. This ensures that we do not have an issue with
information being out of date. The commit additionally fixes an issue
where we would apply the rewrite STR_EQ_UNIFY even though the node
hadn't changed.

3 years agoMake buffered inference manager more robust to backtracking (#6833)
Andrew Reynolds [Mon, 5 Jul 2021 13:03:33 +0000 (08:03 -0500)]
Make buffered inference manager more robust to backtracking (#6833)

This makes TheoryEngine notify all theories when a theory sends a conflict. This means that buffered inference managers always clear their buffers when any theory sends a conflict.

This is required for making theories robust to conflicts that may arise when using the central equality engine, where a different theory may raise a conflict during another theory's check.

3 years agoFix performance of string regression (#6832)
Andres Noetzli [Sat, 3 Jul 2021 19:11:57 +0000 (12:11 -0700)]
Fix performance of string regression (#6832)

Regression cmu-dis-0707-3.smt2 has been timing out when using an ASan
build after commit a4f38d6. Before that
commit --strings-exp implicitly enabled --fmf-bound. After the
commit, the solver was supposed to apply the same reasoning but only to
interal quantifiers and without enabling --fmf-bound. However, the
commit missed some options checks that now also have to check whether
--strings-exp is enabled. This commit updates those option checks.
With this fix, we get a slightly different value for bug590.smt2 after
replying unknown. This commit updates the regression to be more lenient
with the value returned.

3 years agoAdd output tags -o, --output. (#6826)
Mathias Preiner [Sat, 3 Jul 2021 17:44:30 +0000 (10:44 -0700)]
Add output tags -o, --output. (#6826)

Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.

Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.

Co-authored-by: Gereon Kremer <nafur42@gmail.com>
3 years agoFix bv assert input reset assertions (#6820)
Mathias Preiner [Fri, 2 Jul 2021 22:13:17 +0000 (15:13 -0700)]
Fix bv assert input reset assertions (#6820)

If reset-assertions was called it will now reset the SAT solver and the
CNF stream if clauses were permanently added to the SAT solver via
option --bv-assert-input.

3 years agoFix rewriter for negative constant seq.nth (#6827)
Andrew Reynolds [Fri, 2 Jul 2021 13:55:19 +0000 (08:55 -0500)]
Fix rewriter for negative constant seq.nth (#6827)

Fixes #6777.

3 years agoFix CaDiCaL auto-download on macOS (#6828)
Andres Noetzli [Fri, 2 Jul 2021 07:42:13 +0000 (00:42 -0700)]
Fix CaDiCaL auto-download on macOS (#6828)

* Fix CaDiCaL auto-download on macOS

If we are auto-downloading CaDiCaL, we are manually instantiating its makefile.
To do that, we use `CMAKE_CXX_COMPILER` for the compiler and assemble some
flags. However, we are missing the platform dependent flags. Specifically, we
need to set `-isysroot` on macOS to make sure that the header files are found
because they are not at /usr/include on newer versions of Apple's XCode [0].
Unfortunately, I could not find a CMake variable with the platform specific
flags. They are assembled here [1]. To solve this problem, the commit checks if
`CMAKE_OSX_SYSROOT` is set and adds a corresponding compiler flag if it is.

[0] https://developer.apple.com/documentation/xcode-release-notes/xcode-10-release-notes
[1] https://github.com/Kitware/CMake/blob/d60d6c269ae7ad15adbb82028e9ab50290db2a2b/Source/cmLocalGenerator.cxx#L1900-L1923

3 years agoRefactor lexer for SMT-LIB in sphinx (#6805)
Gereon Kremer [Fri, 2 Jul 2021 06:42:28 +0000 (08:42 +0200)]
Refactor lexer for SMT-LIB in sphinx (#6805)

This PR refactors the lexer used by sphinx for highlighting SMT-LIB files. This new lexer properly checks for word boundaries and uses the proper character sets from the SMT-LIB standard.

3 years agoAdd reverse iterators to `Node`/`TNode` (#6825)
Andres Noetzli [Fri, 2 Jul 2021 04:44:47 +0000 (21:44 -0700)]
Add reverse iterators to `Node`/`TNode` (#6825)

This feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.

3 years agoAdd recursive function definitions to subsolver in sygus (#6824)
Andrew Reynolds [Thu, 1 Jul 2021 22:35:13 +0000 (17:35 -0500)]
Add recursive function definitions to subsolver in sygus (#6824)

This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.

This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.

3 years agoFix message to show that cadical and symfpu are required (#6823)
Gereon Kremer [Thu, 1 Jul 2021 17:34:56 +0000 (19:34 +0200)]
Fix message to show that cadical and symfpu are required (#6823)

As mentioned in #6822, we are currently printing an incorrect message if CaDiCaL or SymFPU are not found but auto-download is disabled. This PR fixes this issue.

3 years agoAdd option to limit the number of instantiation rounds (#6818)
Andrew Reynolds [Thu, 1 Jul 2021 15:07:39 +0000 (10:07 -0500)]
Add option to limit the number of instantiation rounds (#6818)

This adds an option to limit the number of instantiation rounds used by quantifiers engine.

This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.

This PR also makes minor improvements to the quantifier utility infrastructure.

3 years agoUse SAT context level for --bv-assert-input instead of decision level. (#6758)
Mathias Preiner [Wed, 30 Jun 2021 22:07:47 +0000 (15:07 -0700)]
Use SAT context level for --bv-assert-input instead of decision level. (#6758)

The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.

3 years agoUse authored date instead of commit date. (#6815)
Gereon Kremer [Wed, 30 Jun 2021 21:34:31 +0000 (23:34 +0200)]
Use authored date instead of commit date. (#6815)

This commit fixes a subtle issue with pruning the old docs from docs-ci. We remove docs that are older than one week. However, we used the commit date instead of the authored date. Since we actually squash the old commits (that are older than four weeks) regularly, the commit date is always newer.

3 years agopow2: new test (#6819)
yoni206 [Wed, 30 Jun 2021 20:22:17 +0000 (13:22 -0700)]
pow2: new test (#6819)

This PR adds a more "real life" unit test for the pow2 solver. Thanks @4tXJ7f for the help with the options.

3 years agoDo not notify during equality engine initialization (#6817)
Andrew Reynolds [Wed, 30 Jun 2021 18:09:45 +0000 (13:09 -0500)]
Do not notify during equality engine initialization (#6817)

This is an alternative fix to https://github.com/cvc5/cvc5/pull/6808.

This ensures that we do not notify the provided class of an equality engine during initialization.

3 years agoDo not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)
Andrew Reynolds [Wed, 30 Jun 2021 16:50:33 +0000 (11:50 -0500)]
Do not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)

There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.

After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.

Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.

3 years agoFix pre vs. post-rewrite in proofs for theory preprocessor (#6801)
Andrew Reynolds [Wed, 30 Jun 2021 12:52:35 +0000 (07:52 -0500)]
Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)

This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.

3 years agoint-to-bv: correct model values (#6811)
yoni206 [Wed, 30 Jun 2021 12:11:56 +0000 (05:11 -0700)]
int-to-bv: correct model values (#6811)

the int-to-bv preprocessing pass produced wrong models.
This PR fixes this in a similar fashion to other preprocessing passes, by adding a substitution to the preprocessing pass context. This requires moving the main translation function to be a class method, rather than a helper method in an empty namespace.

Thanks to @alex-ozdemir for raising this issue and producing a triggering benchmark (added to regressions in this PR).

3 years agoAdd new variants for the CAD projection (#6794)
Gereon Kremer [Tue, 29 Jun 2021 17:43:39 +0000 (19:43 +0200)]
Add new variants for the CAD projection (#6794)

This PR adds variants for the CAD projection operator to use Lazard's projection operator.

3 years agoFix statistics in AigBitblaster. (#6810)
Mathias Preiner [Tue, 29 Jun 2021 17:34:42 +0000 (10:34 -0700)]
Fix statistics in AigBitblaster. (#6810)

Fixes #6788

3 years agoFP: Refactor, rewrite and clean up word blasting. (#6802)
Aina Niemetz [Tue, 29 Jun 2021 16:18:55 +0000 (09:18 -0700)]
FP: Refactor, rewrite and clean up word blasting. (#6802)

This rewrites the word blasting function FpConverter::convert to be
easier to follow and read. It further cleans up several things.

This additionally prepares for allowing to convert incoming facts rather
than terms registered with theory FP. That is, when word blasting more
lazily, in preNotifyFact rather than in registerTerm.

3 years agoRewrite POW to POW2 when the base is 2 (#6806)
yoni206 [Mon, 28 Jun 2021 23:42:13 +0000 (16:42 -0700)]
Rewrite POW to POW2 when the base is 2 (#6806)

This PR introduces a rewrite from (^ 2 t) to (pow2 t) in order to make use of the specialized pow2 solver.
One regression that expects an error when t is not a constant is changed accordingly.

3 years agoRename internal string kinds to match API (#6797)
Andrew Reynolds [Mon, 28 Jun 2021 20:45:51 +0000 (15:45 -0500)]
Rename internal string kinds to match API (#6797)

This commit replaces (old) internal string kind names to match the API / smt2 standard names.

3 years agoFurther fix #6453 (#6804)
Ouyancheng [Mon, 28 Jun 2021 19:10:55 +0000 (12:10 -0700)]
Further fix #6453 (#6804)

There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.

3 years ago[proof] [dot] Make dot printer stateful (#6799)
Haniel Barbosa [Mon, 28 Jun 2021 13:39:49 +0000 (10:39 -0300)]
[proof] [dot] Make dot printer stateful (#6799)

In preparation for further changes in the printer.

3 years agopow2 -- final changes (#6800)
yoni206 [Sat, 26 Jun 2021 02:42:43 +0000 (19:42 -0700)]
pow2 -- final changes (#6800)

This commit adds the remaining changes for a working and integrated `pow2` solver.

In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.

The next steps are new rewrites and and more lemma schemas.

3 years agopow2: Adding monotonicity lemma (#6793)
yoni206 [Fri, 25 Jun 2021 03:09:06 +0000 (20:09 -0700)]
pow2: Adding monotonicity lemma  (#6793)

We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver.
Additionally, some renaming of variables is introduced for better clarity.

3 years agoapi: getRealValue: Fix printing of integer values. (#6795)
Aina Niemetz [Thu, 24 Jun 2021 21:19:11 +0000 (14:19 -0700)]
api: getRealValue: Fix printing of integer values. (#6795)

3 years agocmake: Add new code coverage targets. (#6796)
Mathias Preiner [Thu, 24 Jun 2021 21:04:13 +0000 (14:04 -0700)]
cmake: Add new code coverage targets. (#6796)

This commit adds the following new code coverage targets:

- coverage-reset: Resets the code coverage counters

- coverage: Generates code coverage report for all cvc5 executions since the
            last coverage-reset

- coverage-test: This was previously the coverage target that runs the
                 tests and generates the coverage report (as used for
                 nightlies).

By using `make coverage-reset` and `make coverage` it is now possible to
generate coverage reports for arbitrary executions of cvc5.

3 years agoFix linear arithmetic for duplicate lemmas in incremental (#6784)
Andrew Reynolds [Thu, 24 Jun 2021 11:37:20 +0000 (06:37 -0500)]
Fix linear arithmetic for duplicate lemmas in incremental (#6784)

The linear arithmetic solver was not robust to cases where a duplicate lemma is emitted. This leads to non-linear arithmetic not being called to check at full effort, leading to potential model soundness issues.

Fixes #6773.

3 years agoAdd CoCoA implementation (#6733)
Gereon Kremer [Thu, 24 Jun 2021 11:27:30 +0000 (13:27 +0200)]
Add CoCoA implementation (#6733)

This PR adds the actual implementation for the Lazard evaluation based on CoCoALib. It is only used if CoCoALib is available and falls back to a default libpoly-based implementation otherwise.

3 years ago[hol] Disable bound fmf when HOL (#6792)
Haniel Barbosa [Wed, 23 Jun 2021 23:23:30 +0000 (20:23 -0300)]
[hol] Disable bound fmf when HOL (#6792)

Fixes #6536

3 years agopow2: more implementations (#6756)
yoni206 [Wed, 23 Jun 2021 22:16:58 +0000 (15:16 -0700)]
pow2: more implementations (#6756)

This PR adds implementations of functions from the pow2 solver, rewriter and type checker.

3 years ago[regressions] Adding regression from #5371 (#6791)
Haniel Barbosa [Wed, 23 Jun 2021 22:07:56 +0000 (19:07 -0300)]
[regressions] Adding regression from #5371 (#6791)

3 years ago[proofs] [dot] Adding a counter for subproofs (#6735)
Haniel Barbosa [Wed, 23 Jun 2021 20:36:23 +0000 (17:36 -0300)]
[proofs] [dot] Adding a counter for subproofs (#6735)

3 years ago[parser] [hol] Fix parser check for allowing functions when HOL is enabled (#6790)
Haniel Barbosa [Wed, 23 Jun 2021 20:01:13 +0000 (17:01 -0300)]
[parser] [hol] Fix parser check for allowing functions when HOL is enabled (#6790)

Fixes #6526

3 years agodocs: Add quickstart guide. (#6782)
Aina Niemetz [Wed, 23 Jun 2021 19:08:21 +0000 (12:08 -0700)]
docs: Add quickstart guide. (#6782)

3 years agoFP: Remove sections guarded with undefined macro SYMFPUPROPISBOOL. (#6786)
Aina Niemetz [Wed, 23 Jun 2021 18:19:13 +0000 (11:19 -0700)]
FP: Remove sections guarded with undefined macro SYMFPUPROPISBOOL. (#6786)

3 years agoRemove `--tear-down-incremental` (#6745)
Andres Noetzli [Wed, 23 Jun 2021 01:12:15 +0000 (18:12 -0700)]
Remove `--tear-down-incremental` (#6745)

Recent experiments have shown that `--tear-down-incremental` is actually
not really helping anymore and it has always been a bit of a workaround.
It is also broken on current master. This commit removes the option.

3 years agoAvoid full normalization of lambdas in getValue (#6787)
Andrew Reynolds [Tue, 22 Jun 2021 23:26:58 +0000 (18:26 -0500)]
Avoid full normalization of lambdas in getValue (#6787)

This ensures that we don't apply lambda rewriting, which involves array value normalization, to lambda terms returned by TheoryModel::getValue.

This can significantly speed up our time to return function terms for getValue.

3 years agopython api unit tests for Op (#6785)
yoni206 [Tue, 22 Jun 2021 23:02:00 +0000 (16:02 -0700)]
python api unit tests for Op (#6785)

Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.

The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.

For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206

3 years agomodular bv2int: Stubs and some implementations (#6760)
yoni206 [Tue, 22 Jun 2021 19:11:22 +0000 (12:11 -0700)]
modular bv2int: Stubs and some implementations (#6760)

This PR adds the file int_blaster.cpp. Most of the functions are not yet implemented. Two main functions are implemented.
Additionally, code that will no longer be needed is removed from the BV rewriter.

3 years agoMinor simplification to equality engine notifications (#6726)
Andrew Reynolds [Tue, 22 Jun 2021 17:32:22 +0000 (12:32 -0500)]
Minor simplification to equality engine notifications (#6726)

This removes the d_performNotify flag from equality engine which was supposedly used to guard a very old dependency concerning notifications during initialization. We are now robust to this and hence the flag can be removed.

3 years agoAlways check legal eliminations in quantified logics (#6720)
Andrew Reynolds [Tue, 22 Jun 2021 17:04:00 +0000 (12:04 -0500)]
Always check legal eliminations in quantified logics (#6720)

Fixes #6699.

3 years agoFix type enumeration for non first-class sorts in FMF (#6719)
Andrew Reynolds [Tue, 22 Jun 2021 16:51:07 +0000 (11:51 -0500)]
Fix type enumeration for non first-class sorts in FMF (#6719)

Fixes #6690.

3 years agoPython api unit tests for Result (#6763)
yoni206 [Tue, 22 Jun 2021 14:47:55 +0000 (07:47 -0700)]
Python api unit tests for Result (#6763)

This PR translates the cpp API unit tests about results to python.
The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test/unit/api/result_black.cpp

The translation made rise to one addition to the python API:
The UnknownExplanation object from the cpp API was represented by a string in the python API.
Now we have a more faithful representation, as an enum.

3 years agoFix cases of ITE within regular expressions (#6783)
Andrew Reynolds [Tue, 22 Jun 2021 03:50:29 +0000 (22:50 -0500)]
Fix cases of ITE within regular expressions (#6783)

Fixes #6776.

Our computation of when a regular expression was constant did not account for when ITE was embedded in an RE, leading to an unsound rewrite.

That benchmark now gives:

(error "Regular expression variables are not supported.")

3 years agoSet up fine grained equality notifications (#6734)
Andrew Reynolds [Tue, 22 Jun 2021 02:24:40 +0000 (21:24 -0500)]
Set up fine grained equality notifications (#6734)

This adds fields to equality engine setup information which will be used to hook up theories to the central equality engine.

This PR does not impact any behavior.

This is in preparation for the central equality engine.

3 years agoUpdate to CaDiCaL 1.4.1. (#6780)
Mathias Preiner [Mon, 21 Jun 2021 23:06:05 +0000 (16:06 -0700)]
Update to CaDiCaL 1.4.1. (#6780)

3 years agodocs: Split out and merge C++ class hierarchy. (#6781)
Aina Niemetz [Mon, 21 Jun 2021 22:46:07 +0000 (15:46 -0700)]
docs: Split out and merge C++ class hierarchy. (#6781)

This restructures the entry page for the C++ API documentation in
preparation for adding a quickstart and linking to examples and adding
more content.

3 years ago[Attributes] Remove parameter `context_dependent` (#6772)
Andres Noetzli [Mon, 21 Jun 2021 19:41:00 +0000 (12:41 -0700)]
[Attributes] Remove parameter `context_dependent` (#6772)

After commit d70a63324c95210f1d78c2efc46395d2369d2e2b, context-dependent
attributes have not been supported and, as a result, the template
parameter `context_dependent` of `Attribute` has not been used.
Context-dependent attributes also do not fit with our current design of
sharing attributes across different solvers, so it is unlikely that we
will add that feature back in the future. This commit removes the unused
template parameter.

3 years agoFix model issues with --bitblast=eager. (#6753)
Mathias Preiner [Mon, 21 Jun 2021 19:11:10 +0000 (12:11 -0700)]
Fix model issues with --bitblast=eager. (#6753)

For model construction we only compute model values for relevant terms. The set of relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src/theory/model_manager_distributed.cpp#L58, which skips equalities by default because equalities are usually handled by the equality engine.
When --bitblast=eager is enabled all assertions are wrapped into BITVECTOR_EAGER_ATOM nodes and passed to the BV solver, which results in equalities below BITVECTOR_EAGER_ATOM nodes not being handled by the equality engine but by the BV solver directly. These equalities, however, are skipped when computing the relevant terms and therefore the BV solver is not asked to compute model values for variables below these equalities.

If --bitblast=eager is enabled the BV solver now additionally adds the variables encountered during bit-blasting to the relevant terms via computeRelevantTerms.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
3 years agoAdd Grammar.java to the java API (#6388)
mudathirmahgoub [Mon, 21 Jun 2021 18:36:47 +0000 (13:36 -0500)]
Add Grammar.java to the java API (#6388)

This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.

3 years agoMove cnfConversionTime statistic to CnfStream. (#6769)
Mathias Preiner [Mon, 21 Jun 2021 17:41:37 +0000 (10:41 -0700)]
Move cnfConversionTime statistic to CnfStream. (#6769)

The statistic in `smt_solver.cpp` was not accurate.

3 years agoMake CaDiCaL a required dependency. (#6761)
Mathias Preiner [Mon, 21 Jun 2021 17:11:16 +0000 (10:11 -0700)]
Make CaDiCaL a required dependency. (#6761)

Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.

3 years ago[proof] Fix documentation of array rule (#6770)
Haniel Barbosa [Mon, 21 Jun 2021 14:40:42 +0000 (11:40 -0300)]
[proof] Fix documentation of array rule (#6770)

3 years agoAdding python API test part 5 (#6743)
Ying Sheng [Sat, 19 Jun 2021 06:41:41 +0000 (23:41 -0700)]
Adding python API test part 5 (#6743)

This commit (follow #6553) adds more functions and unit tests for python API.
Subsequent PR will include additional missing functions and unit tests.

1. Adding getNullSort() and mkEmptyBag() functions.
2. Allowing mkOp() with a list of arguments (previously allowed at most 2).
3. Allowing mkString() with additional boolean argument useEscSequences.
4. Corresponding changes to the tests.

3 years agodocs: Fix config to produce unique Sphinx section labels. (#6767)
Aina Niemetz [Sat, 19 Jun 2021 04:16:29 +0000 (21:16 -0700)]
docs: Fix config to produce unique Sphinx section labels. (#6767)

3 years ago[CI] Build with all available cores (#6768)
Andres Noetzli [Sat, 19 Jun 2021 04:07:10 +0000 (21:07 -0700)]
[CI] Build with all available cores (#6768)

macOS virtual machines have three available cores but we were only using two of them for our CI. This commit changes the CI to retrieve the number of available cores and then to use that to number to build and test cvc5.

3 years agodocs: Remove 'View page source' link in right corner. (#6771)
Aina Niemetz [Sat, 19 Jun 2021 02:18:16 +0000 (19:18 -0700)]
docs: Remove 'View page source' link in right corner. (#6771)

We don't upload the source files to the website, so this will always be
a 404.

3 years agoMake CnfStream::toCNF iterative (#6757)
Mathias Preiner [Fri, 18 Jun 2021 17:31:53 +0000 (10:31 -0700)]
Make CnfStream::toCNF iterative (#6757)

This commit makes toCNF() iterative to avoid this issue.
Note that the order in which nodes are visited and thus SatLiterals are
created remains the same.

Fixes #6111

3 years agoRemove obsolete libpoly patch (#6762)
Andres Noetzli [Fri, 18 Jun 2021 02:32:43 +0000 (19:32 -0700)]
Remove obsolete libpoly patch (#6762)

The following commit made our libpoly patch for our Windows builds
obsolete:
https://github.com/SRI-CSL/libpoly/commit/ce7e620c54bd907200ce8b11812d123bf5f4ec8e
This resulted in our build getting stuck because it detected that the
patch had already been applied and was prompting the user what to do.
This commit removes that patch file and the corresponding command.

3 years agoFix CaDiCaL build on Windows (#6764)
Andres Noetzli [Fri, 18 Jun 2021 02:22:19 +0000 (19:22 -0700)]
Fix CaDiCaL build on Windows (#6764)

The Windows version of CaDiCaL does not require the `sys/resource.h`
file, so this commit removes that check. It does, however, require
linking against the Process Status API (psapi), because of a call to
`GetProcessMemoryInfo()`, so this commit adds that dependency for
Windows builds.

3 years agoFix build without libpoly (#6759)
Andres Noetzli [Fri, 18 Jun 2021 00:49:15 +0000 (17:49 -0700)]
Fix build without libpoly (#6759)

Commit f10087c3b347da6ef625a2ad92846551ad324d73 added new files that do
not compile without libpoly. This commit excludes those files when
building without libpoly. It also updates one of the regressions to
ignore a warning about approximate values in the model.

3 years agoMake symfpu a required dependency. (#6749)
Aina Niemetz [Wed, 16 Jun 2021 21:04:09 +0000 (14:04 -0700)]
Make symfpu a required dependency. (#6749)

3 years agoArchive SMT-COMP 2021 run scripts (#6748)
Andres Noetzli [Wed, 16 Jun 2021 20:30:56 +0000 (13:30 -0700)]
Archive SMT-COMP 2021 run scripts (#6748)

This commit copies the run-script-smtcomp-current* scripts to run-script-smtcomp2021* to archive them.

3 years agoProperly consider aliases in option handlers (#6683)
Gereon Kremer [Wed, 16 Jun 2021 08:46:01 +0000 (10:46 +0200)]
Properly consider aliases in option handlers (#6683)

This PR makes sure that option handlers have access to both the canonical option name and the option name that was actually used. It also updates the options README and gets rid of the base_handlers.h of which only a fraction was used.

3 years ago[Optimization] Use Result in OptimizationResult (#6740)
Ouyancheng [Tue, 15 Jun 2021 23:20:20 +0000 (16:20 -0700)]
[Optimization] Use Result in OptimizationResult (#6740)

OptimizationResult now contains:
- cvc5::Result
- optimal value for objective
- whether the objective is unbounded

This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API.

Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)...

3 years agopow2: adding a kind, inference rules, and some implementations in the pow2 solver...
yoni206 [Tue, 15 Jun 2021 22:44:52 +0000 (15:44 -0700)]
pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736)

This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.

3 years agoUpdate to a more recent libpoly version. (#6730)
Gereon Kremer [Tue, 15 Jun 2021 21:09:10 +0000 (23:09 +0200)]
Update to a more recent libpoly version. (#6730)

This PR updates to the latest version of libpoly, which has a memory leak fixed.

3 years agoAdd cocoalib (#6731)
Gereon Kremer [Tue, 15 Jun 2021 21:00:47 +0000 (23:00 +0200)]
Add cocoalib (#6731)

This PR adds CoCoALib as an optional dependency. It will be used in the CAD-based nonlinear solver for computer algebra routines beyond the capabilities of libpoly like quotient rings and polynomial factorization.

3 years agoRemove public option wrappers (#6716)
Gereon Kremer [Tue, 15 Jun 2021 20:30:19 +0000 (22:30 +0200)]
Remove public option wrappers (#6716)

This PR gets rid of almost all remaining public option wrappers. It does so by
- making base, main and parser options public such that they can directly be used from the driver and the parser
- moving incremental and the resource limiting options to base
- moving dumping options to main

After this PR, the only option wrapper left is becoming obsolete as well after (the follow-up of) #6697.

3 years agodocs: Fix reference in sep logic reference. (#6747)
Aina Niemetz [Tue, 15 Jun 2021 18:46:22 +0000 (11:46 -0700)]
docs: Fix reference in sep logic reference. (#6747)

3 years agoCVC4 -> cvc5 in cpp API examples (#6746)
Haniel Barbosa [Tue, 15 Jun 2021 18:29:08 +0000 (15:29 -0300)]
CVC4 -> cvc5 in cpp API examples (#6746)

3 years agodocs: Add references instead of links in theory reference pages. (#6729)
Aina Niemetz [Tue, 15 Jun 2021 17:30:07 +0000 (10:30 -0700)]
docs: Add references instead of links in theory reference pages. (#6729)

3 years agoAn example for a quick start guide (#6686)
yoni206 [Tue, 15 Jun 2021 16:28:40 +0000 (09:28 -0700)]
An example for a quick start guide (#6686)

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
3 years agoFinal update to SMT-COMP 2021 options (#6739)
Andres Noetzli [Mon, 14 Jun 2021 23:45:17 +0000 (16:45 -0700)]
Final update to SMT-COMP 2021 options (#6739)

This commit:

- Disables `--tear-down-incremental=X` for the competition since
  it currently does not work correctly on master and a fixed version did
  not show significant benefits.
- Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it
  is now a mode option.
- Removes the use of `--bv-assert-input` because the option currently
  has some issues in incremental mode (#6738)
- Removes the use of `--bitblast=eager` for the model validation track
  because it produces invalid models (#6741)

3 years agoMinor simplifications to LogicInfo (#6737)
Andrew Reynolds [Sun, 13 Jun 2021 02:27:33 +0000 (21:27 -0500)]
Minor simplifications to LogicInfo (#6737)

3 years agoBetter support for HOL parsing and set up (#6697)
Haniel Barbosa [Fri, 11 Jun 2021 21:29:19 +0000 (18:29 -0300)]
Better support for HOL parsing and set up (#6697)

This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.

For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).

3 years agoAdd skeleton for new Lazard evaluation (#6732)
Gereon Kremer [Fri, 11 Jun 2021 14:18:45 +0000 (16:18 +0200)]
Add skeleton for new Lazard evaluation (#6732)

This PR add the interface and a dummy implementation for the new Lazard evaluation. The dummy implementation is used when CoCoALib is not available and simply falls back to poly::infeasible_regions. The proper implementation that actually does that the comment says will be added with subsequent PRs.

3 years agoRemove support for lazy BV extended function reductions and inferences (#6728)
Andrew Reynolds [Fri, 11 Jun 2021 13:54:32 +0000 (08:54 -0500)]
Remove support for lazy BV extended function reductions and inferences (#6728)

solve-int-as-bv is now the preferred method for solving these benchmarks.

Adds solve-int-as-bv to a regression that became slow in my previous commit.

3 years agoEnsure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)
Andrew Reynolds [Thu, 10 Jun 2021 21:53:38 +0000 (16:53 -0500)]
Ensure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)

This PR ensures we do not eagerly rewrite bv2nat and int2bv when using solve-bv-as-int. Instead they are rewritten during expandDefinitions (at the end of preprocessing).

It also updates regressions that relied on lazy extended function reductions in the lazy solver to use solve-bv-as-int, and adds a missing case (INT_TO_BITVECTOR) in the solve-int-as-bv preprocessing pass.

A followup PR will remove support for lazy extended function reductions for bv2nat / int2bv altogether.

3 years agosmtcomp: Change some BV configs for SQ and INC track. (#6721)
Mathias Preiner [Thu, 10 Jun 2021 18:27:10 +0000 (11:27 -0700)]
smtcomp: Change some BV configs for SQ and INC track. (#6721)

3 years agodocs: Migrate sets and relations theory reference. (#6698)
Aina Niemetz [Wed, 9 Jun 2021 20:44:13 +0000 (13:44 -0700)]
docs: Migrate sets and relations theory reference. (#6698)

This migrates page https://cvc4.github.io/sets-and-relations.
It further adds the SMT2 version of examples/api/cpp/sets.cpp and adds
test/regress/regress0/rels/relations-ops.smt2 as smtlib example for
relations.

3 years agoMake `--solve-int-as-bv=X` robust to rewriting (#6722)
Andres Noetzli [Wed, 9 Jun 2021 20:31:45 +0000 (13:31 -0700)]
Make `--solve-int-as-bv=X` robust to rewriting (#6722)

After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.

3 years agoUpdate CVC4 URLs/macros (#6666)
Andres Noetzli [Wed, 9 Jun 2021 20:14:38 +0000 (13:14 -0700)]
Update CVC4 URLs/macros (#6666)

3 years agoReorder ITE rewrites (#6723)
Andres Noetzli [Wed, 9 Jun 2021 19:53:31 +0000 (12:53 -0700)]
Reorder ITE rewrites (#6723)

Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.

3 years agoMake squasing more robust (#6713)
Gereon Kremer [Wed, 9 Jun 2021 19:25:04 +0000 (21:25 +0200)]
Make squasing more robust (#6713)

This PR makes squashing olds commits in the docs-cleanup CI job more robust: it makes sure that the squash commit has a proper commit date and that we gracefully handle if there is nothing to squash.

3 years agoIntegrate learned literal manager into preprocessing pass context (#6718)
Andrew Reynolds [Wed, 9 Jun 2021 18:52:13 +0000 (13:52 -0500)]
Integrate learned literal manager into preprocessing pass context (#6718)

Towards "learned rewrite" preprocessing pass / improvements to Int <-> BV.

3 years agoFixes related to printing tuples, define-fun commands in smt2 (#6679)
Andrew Reynolds [Wed, 9 Jun 2021 17:50:31 +0000 (12:50 -0500)]
Fixes related to printing tuples, define-fun commands in smt2 (#6679)

This PR fixes some initial issues with printing datatypes in smt2.

It does not yet address further issues on printing define-fun as a result of dump=raw-benchmark, which requires deeper refactoring of the implementation of the API / SmtEngine.

3 years agoPush complex check inside GetInstantiationsCommand (#6715)
Gereon Kremer [Wed, 9 Jun 2021 17:15:30 +0000 (19:15 +0200)]
Push complex check inside GetInstantiationsCommand (#6715)

This PR pushes a rather complex check from the CommandExecutor inside the GetInstantiationsCommand.
The aim is to only use the instFormatMode option in the library (command.cpp) but not the main driver (command_executor.cpp).

3 years agoUpdate options for SMT-COMP (#6704)
Andres Noetzli [Wed, 9 Jun 2021 16:40:10 +0000 (09:40 -0700)]
Update options for SMT-COMP (#6704)

This commit removes obsolete options for BV and strings logics, and
updates QF_NIA to spend more time on our best configuration.

Co-authored-by: Gereon Kremer nafur42@gmail.com
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com