Andrew Reynolds [Mon, 9 Mar 2020 18:35:59 +0000 (13:35 -0500)]
Convert more uses of strings to words (#3921)
Towards theory of sequences.
Also adds documentation to strncmp/rstrncmp and adds them to the Word interface.
Andres Noetzli [Mon, 9 Mar 2020 17:33:32 +0000 (10:33 -0700)]
Fix quoting of options on Travis (#3981)
For some reason, Travis has started to treat our `TRAVIS_CVC4_CONFIG`
environment variable wrong, leading to failing builds. Travis started to
wrap the argument into double quotes, so when we had single quotes
around our argument list, the arguments were treated as a single
argument and when we had double quotes, the second pair of double quotes
terminated the first one permaturely. Declaring the environment
variables individually seems to work as expected, so this commit is
moving to that format.
Andrew Reynolds [Mon, 9 Mar 2020 14:33:14 +0000 (09:33 -0500)]
Fixes for bounds on transcendental functions (#3832)
This PR refactors and fixes how bounds are set for transcendental functions. The new code ensures that all transcendental function applications are given bounds. (Our previous failures to do so were hindering our ability to say "sat", due to NlModel::checkModel failures).
There were previously two issues on why transcendental function applications were not being assigned bounds:
"Slave" transcendental functions (e.g. those that we reduce via sin(t) = sin(y) ^ -pi <= y <= pi ^ y + 2*pi*N = t) were not being given bounds explicitly,
Transcendental functions that are congruent to others (e.g. f(x) where f(y) exists and x=y in the current context) were being ignored and hence not bound.
This PR clarifies the master/slave relationship that tracks which transcendental function applications have been purified, and furthermore tracks congruence classes.
The setting of bounds and the check-model is further simplified by setting bounds on the original terms, whereas the current code sets bounds on the model values of terms. In other words, previously if we had term sin(y) and y^M = c, then we'd set bounds for sin(c), whereas the new code sets the bound on sin(y) directly.
Fixes #3783. We answer unknown without an assertion failure on that benchmark now. Further work based on ignoring literals from internally generated lemmas is necessary for solving it sat.
Andrew Reynolds [Mon, 9 Mar 2020 05:15:09 +0000 (00:15 -0500)]
Rewrite again full for DIV rewrite (#3945)
Fixes #3944.
Ying Sheng [Sun, 8 Mar 2020 05:01:16 +0000 (21:01 -0800)]
Explicit end marker for models printed in the CVC language (#3934)
Fixes https://github.com/CVC4/cvc4-wishues/issues/9.
When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed.
This change adds begin and end markers as the example below:
```
MODEL BEGIN
x : INT = -3;
y : INT = 0;
z : INT = 0;
MODEL END;
```
Andrew Reynolds [Fri, 6 Mar 2020 23:01:45 +0000 (17:01 -0600)]
Minor refactor for theory of sets (#3924)
Flattens a block of code and refactors the main check loop, will make it easier to incorporate new extensions.
It also avoids a needless call to check() for Relations when there are no relations constraints.
Andrew Reynolds [Fri, 6 Mar 2020 21:55:21 +0000 (15:55 -0600)]
Simplify DatatypeDeclarationCommand command (#3928)
The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here.
It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort.
This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.
Andrew Reynolds [Fri, 6 Mar 2020 20:27:10 +0000 (14:27 -0600)]
Remove tester name from APIs (#3929)
This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.
This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.
This is work towards parser migration.
Andres Noetzli [Fri, 6 Mar 2020 17:45:08 +0000 (09:45 -0800)]
Ignore model check warning in regression test (#3926)
PR #3918 added a new test case that results in a warning when checking
models, which makes the regression fail. This commit adds a flag to the
test to ignore that warning.
Andrew Reynolds [Fri, 6 Mar 2020 16:18:39 +0000 (10:18 -0600)]
Make sygus datatype building independent of parser in sygus v2 (#3923)
The current sygus v2 called the parser's mkMututalDatatypeTypes function, which unecessarily created the datatype and bound its (internally generated) constructor/selector symbols in the symbol tables of the parser. This resolves this dependency.
The same issue also exists in the sygus v1 parser but is harder to resolve; I am leaving this for now since that code will be deleted in the next version of CVC4.
This is work towards the SyGuS API.
Andrew Reynolds [Fri, 6 Mar 2020 15:24:11 +0000 (09:24 -0600)]
Support default sygus grammar construction for sets (#3842)
Fixes #3645.
Andres Noetzli [Fri, 6 Mar 2020 06:10:21 +0000 (22:10 -0800)]
Make output of regression script more readable (#3911)
The output of the regression script was difficult to read (especially
the diffs). This commit makes the output more readable by adding colors,
separators, and using a unified diff.
Andres Noetzli [Fri, 6 Mar 2020 01:23:45 +0000 (17:23 -0800)]
Remove --apply-to-const preprocessing pass (#3919)
Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.
Alex Ozdemir [Thu, 5 Mar 2020 22:59:20 +0000 (14:59 -0800)]
Add a new arith constraint proof rule: IntTightenAP (#3818)
This rule is used when a bound on an integer expression is tightened
because of integer reasoning.
Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.
For IntHoleAP, we will have to omit a hole.
Alex Ozdemir [Thu, 5 Mar 2020 23:57:15 +0000 (15:57 -0800)]
Revert "Add a new arith constraint proof rule: IntTightenAP (#3818)"
This reverts commit
c360b3af4371cf871935a8bae96be5f8fecf741b.
Andres Noetzli [Thu, 5 Mar 2020 22:59:20 +0000 (14:59 -0800)]
Add a new arith constraint proof rule: IntTightenAP (#3818)
This rule is used when a bound on an integer expression is tightened
because of integer reasoning.
Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.
For IntHoleAP, we will have to omit a hole.
Andrew Reynolds [Thu, 5 Mar 2020 22:16:15 +0000 (16:16 -0600)]
Migrate a majority of the functionality in parsers to the new API (#3838)
This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout.
Remaining tasks:
Migrate the Datatypes to the new API in cvc/smt2.
Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL).
For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc.
Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version.
This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
Aina Niemetz [Thu, 5 Mar 2020 21:21:43 +0000 (13:21 -0800)]
Move ownership of DecisionEngine into PropEngine. (#3850)
This is in preparation of fixing the issue we currently have with
reset-assertions. This also removes a competition hack for QF_LRA.
Aina Niemetz [Thu, 5 Mar 2020 21:17:55 +0000 (13:17 -0800)]
Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"
This reverts commit
bbba915f44f9e75eaa6238a10ba667643dacb00b.
Andrew Reynolds [Thu, 5 Mar 2020 21:12:57 +0000 (15:12 -0600)]
Move ownership of DecisionEngine into PropEngine. (#3850)
This is in preparation of fixing the issue we currently have with reset-assertions.
This also removes a competition hack for QF_LRA.
Andrew Reynolds [Thu, 5 Mar 2020 20:38:16 +0000 (14:38 -0600)]
Fix issues with real to int (#3918)
This fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.
Fixes #3915 and fixes #3913 and fixes #3916.
Mathias Preiner [Thu, 5 Mar 2020 19:42:54 +0000 (11:42 -0800)]
Enable -Wshadow and fix warnings. (#3909)
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
mudathirmahgoub [Tue, 3 Mar 2020 18:17:06 +0000 (12:17 -0600)]
Refactoring and cleaning the type enumerator for sets (#3908)
* Miscellaneous changes
* Removed unnecessary vector of enumerators
* cleanup
* cleanup
* cleanup
* refactoring
* cleanup
* refactoring
* used binary numbers for sets
* isFinished for enumerator
* format
* added theory_sets_type_enumerator_white.h
* format
* Used BitVector class
* Tracing
* Documentation
* moved implementation to theory_sets_type_enumerator.cpp
* minor changes
Andrew Reynolds [Tue, 3 Mar 2020 15:18:59 +0000 (09:18 -0600)]
Standardize the interface for SMT engine subsolvers (#3836)
This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
Andres Noetzli [Tue, 3 Mar 2020 04:55:22 +0000 (20:55 -0800)]
Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
A local declaration of `s1` was shadowing `s1`, which meant that the
non-local definition of `s1` could never be not null. This meant that
parts of the code were never run. This commit fixes the issue by
removing the local declaration.
Mathias Preiner [Tue, 3 Mar 2020 01:00:42 +0000 (17:00 -0800)]
Fix variable shadowing bug in sets. (#3898)
Andrew Reynolds [Mon, 2 Mar 2020 17:57:26 +0000 (11:57 -0600)]
Split collect model info by types in strings (#3847)
Towards a theory of sequences.
We will need to do similar splits per type for most of the functions throughout strings.
Andrew Reynolds [Sat, 29 Feb 2020 18:36:08 +0000 (12:36 -0600)]
Convert more uses of string to word (#3834)
Andrew Reynolds [Sat, 29 Feb 2020 16:28:27 +0000 (10:28 -0600)]
Throw warning instead of error for non-constant values in check-model stages (#3844)
Fixes #3729 and fixes #3720.
This updates two more stages of check-model (checking whether values assigned to terms are constants and internally checking whether assertions belonging to theories) to only throw warnings when a term/assertion has a non-constant value in the model. This is to accommodate cases where check-model is infeasible.
Andres Noetzli [Sat, 29 Feb 2020 06:20:18 +0000 (22:20 -0800)]
Add support for str.from_code (#3829)
This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.
Aina Niemetz [Sat, 29 Feb 2020 05:01:49 +0000 (21:01 -0800)]
propEngine: Reorder class declaration according to code style guidelines. (#3846)
Andrew Reynolds [Sat, 29 Feb 2020 04:30:40 +0000 (22:30 -0600)]
Fix assertion related to assignability in the model. (#3843)
Fixes #3813.
It appears that an assertion was hardcoded to check whether a term was a variable or APPLY_UF application whereas this check should use isAssignable. This avoids an assertion failure on the given benchmark.
Andrew Reynolds [Sat, 29 Feb 2020 03:43:49 +0000 (21:43 -0600)]
Replace conditional rewrite pass in quantifiers with the extended rewriter (#3841)
Fixes #3839.
Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.
This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.
Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.
This PR relies on #3840.
Andrew Reynolds [Fri, 28 Feb 2020 19:35:09 +0000 (13:35 -0600)]
Use enum for quantifiers rewrite steps (#3840)
Makes trace messages easier to understand.
Andrew Reynolds [Thu, 27 Feb 2020 23:06:02 +0000 (17:06 -0600)]
Refactor operator applications in the parser (#3831)
This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes:
Indexed ops are carried in ParseOp via api::Op not Expr,
getKindForFunction is limited to "APPLY" kinds from the new API,
The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity.
TPTP should use DIVISION not DIVISION_TOTAL.
This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser.
Haniel Barbosa [Thu, 27 Feb 2020 22:34:42 +0000 (19:34 -0300)]
Changing TPTP parser to accomodate new API (#3837)
Removing dependency of kinds corresponding to expressions.
Andrew Reynolds [Thu, 27 Feb 2020 21:20:12 +0000 (15:20 -0600)]
Update purifySygusGTerm to the new API (#3830)
Towards parser migration.
(Partially) updates the central function used for synth-fun in sygus v2 to the new API.
It also removes an optimization for "pure operators" from the v2 parser that is incompatible with the new API.
Andrew Reynolds [Thu, 27 Feb 2020 19:48:50 +0000 (13:48 -0600)]
Fix large models for strings (#3835)
Fixes #3375.
Marking as "major" since in fact we produce incorrect models in production without the fix.
Andres Noetzli [Thu, 27 Feb 2020 17:03:12 +0000 (09:03 -0800)]
Fix -Wshadow warnings in common headers (#3826)
Andrew Reynolds [Thu, 27 Feb 2020 03:54:29 +0000 (21:54 -0600)]
Add support for is_digit and regular expression difference (#3828)
Towards support for the strings standard. This adds support for str.is_digit and re.diff, which both can be eliminated eager during preprocessing.
Andrew Reynolds [Thu, 27 Feb 2020 03:15:04 +0000 (21:15 -0600)]
Disable regression that times out on debug (#3833)
Andrew Reynolds [Thu, 27 Feb 2020 02:08:01 +0000 (20:08 -0600)]
Move fix for vacuous sygus types out of the parser (#3820)
This moves a fix for vacuous sygus types out of the parser and into the Expr-level datatype.
This is a temporary fix so that further progress can be made on parser migration (and to declutter the parser).
This will be refactored when an API for SyGuS is established (CVC4/cvc4-projects#38).
Andrew Reynolds [Thu, 27 Feb 2020 01:11:31 +0000 (19:11 -0600)]
Initial work towards -Wshadow (#3817)
Andrew Reynolds [Thu, 27 Feb 2020 00:04:16 +0000 (18:04 -0600)]
Some initial work on using words (#3819)
Towards support for sequences (CVC4/cvc4-projects#23.)
Andrew Reynolds [Wed, 26 Feb 2020 23:15:02 +0000 (17:15 -0600)]
Infrastructure for tautological literals in nonlinear solver (#3795)
Work towards CVC4/cvc4-projects#113 and #3783.
This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".
This PR is required for further refactoring of check-model for transcendental functions.
Andrew Reynolds [Wed, 26 Feb 2020 22:39:39 +0000 (16:39 -0600)]
Use side effect utility for non-linear lemmas (#3780)
Fixes #3647.
Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.
This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.
Andrew Reynolds [Wed, 26 Feb 2020 21:43:07 +0000 (15:43 -0600)]
Fix regression (#3827)
Andrew Reynolds [Wed, 26 Feb 2020 20:59:38 +0000 (14:59 -0600)]
More fixes for printing sygus commands (#3812)
Towards v1 -> v2 sygus conversion.
This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).
Andrew Reynolds [Wed, 26 Feb 2020 19:54:41 +0000 (13:54 -0600)]
Basic support for regular expression complement (#3437)
Fixes #3408 .
Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h
Andrew Reynolds [Wed, 26 Feb 2020 19:09:51 +0000 (13:09 -0600)]
Refactor type ascriptions in the parser (#3825)
Towards parser migration.
This consolidates two blocks of code (cvc/smt2) that do type ascriptions to a utility function in the parser. It updates this function to use the new API.
This code will be further refactored when the interface for parametric datatype constructors is further developed in the new API.
Andrew Reynolds [Wed, 26 Feb 2020 18:33:00 +0000 (12:33 -0600)]
Minor improvement to ParseOp (#3808)
Andrew Reynolds [Wed, 26 Feb 2020 17:47:05 +0000 (11:47 -0600)]
Use default consts when not using any const during grammar normalization (#3807)
Fixes #3802.
If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.
Andrew Reynolds [Wed, 26 Feb 2020 17:00:48 +0000 (11:00 -0600)]
Fix node arity issue in reduction of int2bv (#3777)
Andrew Reynolds [Wed, 26 Feb 2020 16:17:30 +0000 (10:17 -0600)]
Move equivalence class info to its own file in strings (#3799)
Code move only, no updates to behavior or content of code in this PR.
Andrew Reynolds [Wed, 26 Feb 2020 15:02:15 +0000 (09:02 -0600)]
Support for witnessing choice in models (#3781)
Fixes #3300.
This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
Andres Noetzli [Wed, 26 Feb 2020 08:08:20 +0000 (00:08 -0800)]
Remove portfolio leftovers (#3821)
Commit
1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
Andrew Reynolds [Wed, 26 Feb 2020 06:40:52 +0000 (00:40 -0600)]
Minor cleaning of smt2 parser (#3823)
Towards parser migration, will make the diff of the eventual conversion a bit smaller.
Andrew Reynolds [Wed, 26 Feb 2020 02:52:10 +0000 (20:52 -0600)]
Embed mkAssociative utilities within the API. (#3801)
Towards parser/API migration.
mudathirmahgoub [Tue, 25 Feb 2020 17:51:10 +0000 (11:51 -0600)]
Sets & Relations Java example (#3816)
Fixes [(Bugzilla #677)](https://github.com/CVC4/cvc4-projects/issues/25).
mudathirmahgoub [Tue, 25 Feb 2020 17:47:24 +0000 (11:47 -0600)]
Sets & Relations Java example (#3816)
yoni206 [Tue, 25 Feb 2020 15:23:30 +0000 (07:23 -0800)]
remove redundant includes (#3815)
I came across these two redundant includes in theory_uf.h and removed them.
yoni206 [Tue, 25 Feb 2020 03:58:01 +0000 (19:58 -0800)]
bv_to_int preprocessing pass
Introduces a preprocessing pass that translates bv problems to integer problems.
Andrew Reynolds [Mon, 24 Feb 2020 23:28:03 +0000 (17:28 -0600)]
Fixes for quantifiers documentation (#3811)
Minor fixes discovered during development of sygus-inst.
Andrew Reynolds [Mon, 24 Feb 2020 22:21:45 +0000 (16:21 -0600)]
Utilities for words (#3797)
This adds a utility file for handling operations over constant "words" (this will eventually generalize string or sequence constants). This is work towards CVC4/cvc4-projects#23.
Also improves documentation in regexp.h.
Andrew Reynolds [Mon, 24 Feb 2020 21:37:48 +0000 (15:37 -0600)]
Convert parser input interface to api::Term (#3809)
Abdalrhman Mohamed [Mon, 24 Feb 2020 20:30:02 +0000 (14:30 -0600)]
Fix bugs related to printing Sygus commands (#3804)
With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.
Andrew Reynolds [Mon, 24 Feb 2020 17:35:37 +0000 (11:35 -0600)]
Add missing functions to new C++ API (#3769)
Andres Noetzli [Mon, 24 Feb 2020 15:46:47 +0000 (07:46 -0800)]
Make lambda rewriter more robust (#3806)
The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.
Andrew Reynolds [Sun, 23 Feb 2020 05:41:42 +0000 (23:41 -0600)]
Minor refactoring of equality notifications (#3798)
Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.
Alex Ozdemir [Sat, 22 Feb 2020 18:48:05 +0000 (10:48 -0800)]
RIP th_lra.plf (#3796)
Rest in Peace, old LRA signature.
Andrew Reynolds [Sat, 22 Feb 2020 16:07:44 +0000 (10:07 -0600)]
Move check memberships to reg exp solver (#3793)
There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified.
Andrew Reynolds [Sat, 22 Feb 2020 07:05:43 +0000 (01:05 -0600)]
Move cardinality inference scheme to base solver in strings (#3792)
Moves handling of cardinality to the base solver, refactors how cardinality is accessed.
No intended behavior change in this commit.
makaimann [Sat, 22 Feb 2020 06:13:31 +0000 (22:13 -0800)]
Dump boolean propagations and conflicts for decision tree org-mode viewer (#3788)
PR #2871 added trace tags for dumping the decision tree in org-mode format. However, it only dumped theory propagations/conflicts. This could be confusing because it would appear to backtrack without reaching a conflict (but actually the conflict was at the propositional level). This commit also adds dumping of boolean propagations and conflicts.
Alex Ozdemir [Sat, 22 Feb 2020 00:16:19 +0000 (16:16 -0800)]
Switch to th_lira.plf (#3741)
Switches arith_proof.cpp from th_lra to th_lira.
Changes:
Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.
Aina Niemetz [Fri, 21 Feb 2020 22:20:15 +0000 (14:20 -0800)]
New C++ API: Remove TOTAL kinds. (#3794)
Andrew Reynolds [Fri, 21 Feb 2020 19:36:01 +0000 (13:36 -0600)]
Simple changes towards unicode string standard (#3791)
This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
The next steps will be to address the more invasive changes required to support the standard.
Andrew V. Jones [Fri, 21 Feb 2020 18:19:45 +0000 (18:19 +0000)]
Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT solver is compiled-in (#3771)
Andrew Reynolds [Fri, 21 Feb 2020 16:55:04 +0000 (10:55 -0600)]
Split extended functions solver in strings (#3768)
Alex Ozdemir [Fri, 21 Feb 2020 15:25:25 +0000 (07:25 -0800)]
Remove IntReal tightening axioms from th_lira.plf (#3787)
Andrew Reynolds [Thu, 20 Feb 2020 20:49:02 +0000 (14:49 -0600)]
Remove front-end support for Chain (#3767)
Andres Noetzli [Thu, 20 Feb 2020 20:07:46 +0000 (12:07 -0800)]
Remove unused code (#3782)
Andrew Reynolds [Thu, 20 Feb 2020 19:07:22 +0000 (13:07 -0600)]
Minor removals (#3786)
Found while working on parser migration of datatypes.
Andres Noetzli [Thu, 20 Feb 2020 17:02:58 +0000 (09:02 -0800)]
Remove parser from bindings (#3779)
Mathias Preiner [Thu, 20 Feb 2020 00:59:58 +0000 (16:59 -0800)]
resource manager: Add statistic for every resource. (#3772)
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
Andrew Reynolds [Wed, 19 Feb 2020 23:14:01 +0000 (17:14 -0600)]
Fix symmetry breaking for multiple sygus types (#3775)
makaimann [Wed, 19 Feb 2020 21:54:17 +0000 (13:54 -0800)]
Add Python bindings using Cython -- see below for more details (#2879)
Andrew Reynolds [Wed, 19 Feb 2020 21:15:22 +0000 (15:15 -0600)]
Delay enumerative instantiation if theory engine does not need check (#3774)
Andrew Reynolds [Wed, 19 Feb 2020 20:19:09 +0000 (14:19 -0600)]
Change Record to shared_ptr (#3778)
Andrew Reynolds [Wed, 19 Feb 2020 07:23:43 +0000 (01:23 -0600)]
Fix approximate bounds for transcendental functions whose model values rewrite (#3747)
* Fix bounds for negative sine apps
* Format
* Comment
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
makaimann [Wed, 19 Feb 2020 04:11:52 +0000 (20:11 -0800)]
Change datatype selector/constructor/tester to terms (#3773)
Andrew Reynolds [Tue, 18 Feb 2020 18:00:14 +0000 (12:00 -0600)]
Add missing kinds for the new API (#3757)
Andrew Reynolds [Mon, 17 Feb 2020 19:29:09 +0000 (13:29 -0600)]
Option to limit the number of rounds of enumerative instantiation (#3760)
Andrew Reynolds [Mon, 17 Feb 2020 17:17:02 +0000 (11:17 -0600)]
Fix soundness bug in reduction of integer div/mod (#3766)
This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/
9098391fe334d829ec4101f190b8f1fa21c30752.
This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not.
Fixes #3765.
Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.
Haniel Barbosa [Mon, 17 Feb 2020 16:11:17 +0000 (13:11 -0300)]
Using ParseOp in TPTP (#3764)
Abdalrhman Mohamed [Mon, 17 Feb 2020 14:58:42 +0000 (08:58 -0600)]
Support dumping Sygus commands. (#3763)
Andrew Reynolds [Sun, 16 Feb 2020 22:06:21 +0000 (16:06 -0600)]
Fix simple issue with cache (#3762)
Andrew Reynolds [Sun, 16 Feb 2020 21:47:31 +0000 (15:47 -0600)]
Add temporary global API conversion utilities. (#3759)
Andres Noetzli [Sun, 16 Feb 2020 18:09:31 +0000 (10:09 -0800)]
Activate reverse variant of F-Split inference (#3745)
This commit activates the reverse variant of the F-Split inference.
Andrew Reynolds [Sun, 16 Feb 2020 03:39:06 +0000 (21:39 -0600)]
Disable regression (#3761)
Should fix recurring issue with nightlies.
Also fixes a warning.
Andrew Reynolds [Sat, 15 Feb 2020 22:38:23 +0000 (16:38 -0600)]
Move proxy variables to InferenceManager in strings (#3758)