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.")
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.
Mathias Preiner [Mon, 21 Jun 2021 23:06:05 +0000 (16:06 -0700)]
Update to CaDiCaL 1.4.1. (#6780)
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.
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.
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>
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.
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.
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.
Haniel Barbosa [Mon, 21 Jun 2021 14:40:42 +0000 (11:40 -0300)]
[proof] Fix documentation of array rule (#6770)
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.
Aina Niemetz [Sat, 19 Jun 2021 04:16:29 +0000 (21:16 -0700)]
docs: Fix config to produce unique Sphinx section labels. (#6767)
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.
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.
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
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.
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.
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.
Aina Niemetz [Wed, 16 Jun 2021 21:04:09 +0000 (14:04 -0700)]
Make symfpu a required dependency. (#6749)
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.
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.
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)...
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.
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.
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.
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.
Aina Niemetz [Tue, 15 Jun 2021 18:46:22 +0000 (11:46 -0700)]
docs: Fix reference in sep logic reference. (#6747)
Haniel Barbosa [Tue, 15 Jun 2021 18:29:08 +0000 (15:29 -0300)]
CVC4 -> cvc5 in cpp API examples (#6746)
Aina Niemetz [Tue, 15 Jun 2021 17:30:07 +0000 (10:30 -0700)]
docs: Add references instead of links in theory reference pages. (#6729)
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>
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)
Andrew Reynolds [Sun, 13 Jun 2021 02:27:33 +0000 (21:27 -0500)]
Minor simplifications to LogicInfo (#6737)
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).
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.
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.
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.
Mathias Preiner [Thu, 10 Jun 2021 18:27:10 +0000 (11:27 -0700)]
smtcomp: Change some BV configs for SQ and INC track. (#6721)
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.
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.
Andres Noetzli [Wed, 9 Jun 2021 20:14:38 +0000 (13:14 -0700)]
Update CVC4 URLs/macros (#6666)
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.
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.
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.
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.
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).
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
Ouyancheng [Wed, 9 Jun 2021 15:53:16 +0000 (08:53 -0700)]
[Optimization] support for push/pop (#6706)
Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.
Haniel Barbosa [Wed, 9 Jun 2021 14:34:22 +0000 (11:34 -0300)]
Removing spurious HO checks (#6707)
Gereon Kremer [Wed, 9 Jun 2021 14:03:04 +0000 (16:03 +0200)]
Require statistics for regression (#6714)
This PR makes a new regression explicitly require statistics.
Aina Niemetz [Wed, 9 Jun 2021 07:20:14 +0000 (00:20 -0700)]
docs: Migrate separation logic theory reference. (#6702)
This migrates page https://cvc4.github.io/separation-logic.
Andres Noetzli [Wed, 9 Jun 2021 07:09:26 +0000 (00:09 -0700)]
docs: Fix `Kind` description (#6712)
This commit changes the Kind description not to include C/C++
preprocessor statements and updates the kind of bit-vector addtion.
It also marks some of the information as internal to exclude it from the
public documentation.
Andrew Reynolds [Tue, 8 Jun 2021 23:47:40 +0000 (18:47 -0500)]
Fix for 2 dimensional dependent bounded quantifiers (#6710)
This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.
Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.
Andrew Reynolds [Tue, 8 Jun 2021 21:50:41 +0000 (16:50 -0500)]
Add learned literal manager utility (#6709)
This is a simple class to maintain a list of literals that we have learned that may be useful during preprocessing.
This is work towards a "learned rewrite" preprocessing pass / better support for Int/BV translations during preprocessing.
Gereon Kremer [Tue, 8 Jun 2021 15:21:45 +0000 (17:21 +0200)]
Fix statistics option handler (#6703)
This PR fixes a typo in the option handler for the statistics options, which lead to options not properly propagating.
Gereon Kremer [Tue, 8 Jun 2021 13:43:13 +0000 (15:43 +0200)]
Make env hold a pointer to the original options to properly initialize subsolvers (#6705)
This PR extends the Env class to hold a pointer to the original options that are owned by the api::Solver. These original options will be used to properly initialize subsolvers as using the current options leads to subtle issues as setDefaults is not (in general) idempotent.
Gereon Kremer [Tue, 8 Jun 2021 07:05:35 +0000 (09:05 +0200)]
Remove `binary_name` option (#6693)
The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().
Alex Ozdemir [Tue, 8 Jun 2021 06:42:59 +0000 (23:42 -0700)]
Change output of getRealValue to a fraction. (#6692)
Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.
We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.
Also, document some (potential) weirdness with calling mkReal on floating-point values.
Andrew Reynolds [Tue, 8 Jun 2021 06:29:10 +0000 (01:29 -0500)]
Make TheoryUF compatible with central equality engine (#6695)
Work towards central equality engine.
This does some minor reorganization to TheoryUF, related to UF+cardinality constraints that makes it compatible with central equality engine. In particular, preNotifyFact is removed in favor of adding conflicts after cardinality constraints are added to the equality engine. This ensures that the central equality engine can explain conflicts that involve cardinality constraints (which will no longer be the responsibility of UF when --ee-mode=central).
Andrew Reynolds [Tue, 8 Jun 2021 06:11:28 +0000 (01:11 -0500)]
Fix str.update reduction (#6696)
Fixes the 2nd benchmark from #6653.
Andrew Reynolds [Mon, 7 Jun 2021 17:44:20 +0000 (12:44 -0500)]
(proof-new) Fix missing connection in trust substitution proofs (#6685)
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
Gereon Kremer [Mon, 7 Jun 2021 17:00:10 +0000 (19:00 +0200)]
Remove `Options::wasSetByUser()` (#6682)
This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.
Andrew Reynolds [Mon, 7 Jun 2021 14:09:59 +0000 (09:09 -0500)]
(proof-new) Lazy proof chain debug names (#6680)
Gereon Kremer [Sun, 6 Jun 2021 11:09:40 +0000 (13:09 +0200)]
Support public option modules (#6691)
This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).
Andres Noetzli [Sat, 5 Jun 2021 03:22:57 +0000 (20:22 -0700)]
Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)
Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.
Andrew Reynolds [Fri, 4 Jun 2021 21:05:43 +0000 (16:05 -0500)]
Miscellaneous changes from central ee branch (#6687)
Minor reorganization to make calls to theory engine from combination engine / shared solver more organized.
yoni206 [Fri, 4 Jun 2021 17:01:45 +0000 (10:01 -0700)]
pow2: header file for pow2 solver (#6676)
This PR adds a header file for the pow2 solver. It also includes an empty test file, to trigger compilation of the header file. The next PR will include implementations and tests.
Mathias Preiner [Fri, 4 Jun 2021 13:30:35 +0000 (06:30 -0700)]
bv: Enable bitblast solver by default. (#6660)
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.
Fixes #3958, #5396, #5736, #5743, #5947.
Gereon Kremer [Fri, 4 Jun 2021 13:17:57 +0000 (15:17 +0200)]
Add missing dereference (#6684)
Andres Noetzli [Fri, 4 Jun 2021 00:41:40 +0000 (17:41 -0700)]
Fix handling of start index in `str.indexof_re` (#6674)
Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.
Gereon Kremer [Fri, 4 Jun 2021 00:14:27 +0000 (02:14 +0200)]
Some cleanup in `mkoptions.py` (#6667)
This PR does some general cleanup in the mkoptions.py script: removal of obsolete code and some fixes to the comments.
Aina Niemetz [Fri, 4 Jun 2021 00:07:05 +0000 (17:07 -0700)]
docs: Migrate datatypes theory reference. (#6662)
This migrates https://cvc4.github.io/datatypes.
yoni206 [Thu, 3 Jun 2021 23:57:29 +0000 (16:57 -0700)]
Adding unit tests for the datatypes python API (#6658)
This commit adds unit tests that are translated from `datatype_api_black.cpp`. One API function is also added to the python API.
This is the last part of the python api unit tests for datatypes.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Andrew Reynolds [Thu, 3 Jun 2021 22:49:32 +0000 (17:49 -0500)]
Simplify automatic set-logic in smt2 parser (#6678)
This simplifies the smt2 parser so that automatically setting the logic is done directly instead of being buffered as a command.
This prevents spurious errors for features that require (A) checking the logic is set and (B) fully intialize the underlying SMT engine. `declare-pool` is an example of an smt2 command where the user will get an error (instead of a warning) when set-logic is not used due to setting the logic, after fully initing SMT engine and then executing the buffered set-logic command.
Note this should also make dump=raw-benchmark more accurate (no set-logic is included when dumping benchmarks with no set-logic command).
Andres Noetzli [Thu, 3 Jun 2021 22:26:52 +0000 (15:26 -0700)]
[GitHub Actions] Make caching of dependencies depend on image version (#6677)
Our Clang builds started to fail to link when the environment changed. This commit changes our CI to only use cached dependencies if the build environment has not changed.
yoni206 [Thu, 3 Jun 2021 14:39:55 +0000 (07:39 -0700)]
Renaming pow2 to p2 in regression tests (#6675)
We plan to add a unary pow2 operator to cvc5, that is obtained from the binary operator pow by fixing the first argument to 2.
An initial working branch is here: https://github.com/yoni206/cvc5/tree/pow2
This PR does the first step, which is to rename some uninterpreted symbols in regression tests from pow2 to p2, to avoid clashing with the new operator.
Andres Noetzli [Wed, 2 Jun 2021 21:37:48 +0000 (14:37 -0700)]
Remove references to `bv-div-zero-const` in docs (#6672)
The bv-div-zero-const option has been removed and is now always
enabled, so this commit updates the documentation of the kinds to
reflect that. It also makes the language to describe the special cases a
bit more uniform.
Andrew Reynolds [Wed, 2 Jun 2021 21:16:40 +0000 (16:16 -0500)]
Fixes for printing define-fun-rec (#6673)
Andres Noetzli [Wed, 2 Jun 2021 19:41:14 +0000 (12:41 -0700)]
Remove option to ignore negative memberships (#6665)
Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.
yoni206 [Wed, 2 Jun 2021 19:30:46 +0000 (12:30 -0700)]
Adding getters to the python API and testing them (#6652)
This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.
Aina Niemetz [Wed, 2 Jun 2021 17:16:26 +0000 (10:16 -0700)]
Remove redundant logic ALL_SUPPORTED. (#6664)
yoni206 [Wed, 2 Jun 2021 16:47:09 +0000 (09:47 -0700)]
Move `toPythonObj` tests to the new API unit test directory (#6656)
This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.
Gereon Kremer [Wed, 2 Jun 2021 16:01:08 +0000 (18:01 +0200)]
Use proper variable name (#6670)
This PR fixes the driver which used an incorrect variable name in competition mode.
Andrew Reynolds [Wed, 2 Jun 2021 15:28:36 +0000 (10:28 -0500)]
Fix unsat core proofs (#6655)
Fixes cases of satisfiable unsat cores when proofs are enabled.
Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
Andres Noetzli [Wed, 2 Jun 2021 13:50:51 +0000 (06:50 -0700)]
Make `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)
Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.
Gereon Kremer [Wed, 2 Jun 2021 13:21:22 +0000 (15:21 +0200)]
Remove `Options::operator[]` (#6649)
This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.
Gereon Kremer [Wed, 2 Jun 2021 12:11:05 +0000 (14:11 +0200)]
Move public wrapper functions out of options class (#6600)
This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
Gereon Kremer [Wed, 2 Jun 2021 11:55:40 +0000 (13:55 +0200)]
Fix issues with double negation in circuit propagator (#6669)
This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.
Gereon Kremer [Wed, 2 Jun 2021 10:11:13 +0000 (12:11 +0200)]
Fix issues when poly is disabled (#6668)
Recent changes introduced issues when libpoly is disabled.
Gereon Kremer [Wed, 2 Jun 2021 06:55:24 +0000 (08:55 +0200)]
Make `Options::assign()` specializations free functions (#6648)
This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.
Gereon Kremer [Wed, 2 Jun 2021 06:29:02 +0000 (08:29 +0200)]
Do manual squash cleanup for docs (#6646)
This PR abandons the attempt to do the cleanup in a single rebase command, and instead squashes the old commits manually. The current solution does not handle conflicts properly. The new approach (which seems to be more robust) proceeds as follows (to squash $first..$last):
- checkout $last
- soft reset to $first (checkout $first, but keep changes in working copy)
- commit to squashed commit
- cherry-pick $last..HEAD from main branch
Aina Niemetz [Wed, 2 Jun 2021 00:21:56 +0000 (17:21 -0700)]
docs: Migrate input languages page. (#6659)
This migrates page https://cvc4.github.io/input-languages.
Aina Niemetz [Wed, 2 Jun 2021 00:05:52 +0000 (17:05 -0700)]
docs: Restructure index page, fix style issue. (#6657)
yoni206 [Tue, 1 Jun 2021 21:24:43 +0000 (14:24 -0700)]
Some additions to the datatypes python API (#6640)
This commit makes the following additions, in order to sync the python API with the cpp API.
1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.
Andrew Reynolds [Tue, 1 Jun 2021 18:58:49 +0000 (13:58 -0500)]
Use top-level substitutions in ITE simp (#6651)
With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.
Since the top-level substitutions now are the authority on models, this led to model failures after this change:
ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.
This is required for SMT-COMP.
Andrew Reynolds [Tue, 1 Jun 2021 14:59:41 +0000 (09:59 -0500)]
Disable timeout regressions (#6650)
Disables two regressions that have been timing out causing nightlies to fail.
yoni206 [Tue, 1 Jun 2021 09:40:54 +0000 (02:40 -0700)]
FP value support in python API (#6644)
This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.
getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.
Gereon Kremer [Mon, 31 May 2021 14:05:39 +0000 (16:05 +0200)]
Remove Options::ref() (#6647)
This PR gets rid of the templated Options::ref() method (and all its specializations for every option).
Andres Noetzli [Mon, 31 May 2021 04:13:37 +0000 (21:13 -0700)]
Remove invalid options from run scripts (#6645)
This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.
yoni206 [Mon, 31 May 2021 00:56:14 +0000 (17:56 -0700)]
Update `toPythonObj` to use new getters -- part 1 (#6623)
Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.
A future PR will add more getters to the python API.
Co-authored-by: Gereon Kremer nafur42@gmail.com
Andres Noetzli [Mon, 31 May 2021 00:35:08 +0000 (17:35 -0700)]
Compute model values for nested sequences in order (#6631)
Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.
While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.
This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.
cc @yoni206