Alex Ozdemir [Wed, 4 Mar 2020 08:20:10 +0000 (00:20 -0800)]
Expand the definition of a "simple" farkas proof.
Before, a "simple farkas proof" was one that just applied the farkas
lemma.
Now it allows for the antecedents to (optionally) be tightened.
Note that hasSimpleFarkasProof was (and is) dead code.
We will use it to decide whether to print a proof or a hole.
Aina Niemetz [Mon, 16 Mar 2020 20:10:05 +0000 (13:10 -0700)]
DecisionEngine: Use single unique pointer for ITE strategy . (#4078)
Previously, DecisionEngine maintained a vector of ITE strategies.
However, only one was ever created. This uses a single unique_ptr member
for the ITE strategy instead of a vector.
Aina Niemetz [Mon, 16 Mar 2020 18:22:15 +0000 (11:22 -0700)]
Issue 4077: Add unit test to reproduce issue. (#4107)
This adds the unit test reported in issue #4077.
The issue was fixed in #4081.
Andres Noetzli [Mon, 16 Mar 2020 17:37:19 +0000 (10:37 -0700)]
Create master equality engine at context level 0 (#4081)
Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.
Andrew Reynolds [Mon, 16 Mar 2020 04:51:51 +0000 (23:51 -0500)]
Handle cases in --sygus-rr where evaluation is not constant (#4100)
Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant.
Fixes #4096 and fixes #4089.
Andrew Reynolds [Fri, 13 Mar 2020 19:53:00 +0000 (14:53 -0500)]
Removing a few deprecated options (#4052)
Andrew Reynolds [Fri, 13 Mar 2020 18:44:07 +0000 (13:44 -0500)]
Remove regress for real to int (#4071)
Missed this one when real to int was disabled for quantifiers. Fixes regress1.
Andrew Reynolds [Fri, 13 Mar 2020 18:11:21 +0000 (13:11 -0500)]
Generalize type rules for strings to sequences (#3987)
Towards theory of sequences.
Andrew Reynolds [Fri, 13 Mar 2020 16:52:13 +0000 (11:52 -0500)]
Fix case of non-constant value for sygus sampling (#4051)
Fixes #4050.
Andrew Reynolds [Thu, 12 Mar 2020 22:32:11 +0000 (17:32 -0500)]
Add options for nec regression (#4056)
Currently an nec benchmark in regress2 is very slow (57 seconds in production) due to disabling the nec-specific options in
67c730c). This reenables these options for this benchmark.
Andrew Reynolds [Thu, 12 Mar 2020 21:57:42 +0000 (16:57 -0500)]
Convert most instances of dataypes in parsers to the new API (#4054)
I am still accessing Expr-level Datatypes for the sygus v1/v2 parsers (within smt2). This will be addressed in two ways in the future:
(1) The sygus v1 parser will be deleted,
(2) The sygus v2 parser will be updated to use a "Grammar" object as an extension of the new API, which will hide all calls to the underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus-api). FYI @abdoo8080 .
Note I've renamed "mkMutualDatatypeTypes" to "bindMutualDatatypeTypes" to be more accurate and follow the updated name conventions in the parser.
The next step will be to handle parametric datatypes, which are not specifically addressed by this PR.
Andrew Reynolds [Thu, 12 Mar 2020 21:13:27 +0000 (16:13 -0500)]
Do not allow quantifiers over real variables in real to int pass. (#4049)
With quantifiers over real variables, --solve-real-as-int is neither sound nor complete. Thus we should abort in this case.
Andrew Reynolds [Thu, 12 Mar 2020 20:25:06 +0000 (15:25 -0500)]
Remove local theory extension option (#4048)
This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.
Andrew Reynolds [Thu, 12 Mar 2020 19:42:45 +0000 (14:42 -0500)]
Do not make models for quantified function variables (#4039)
If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
Aina Niemetz [Thu, 12 Mar 2020 19:04:48 +0000 (12:04 -0700)]
New C++ API: Remove support for (reset). (#4037)
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
Andrew Reynolds [Thu, 12 Mar 2020 18:34:18 +0000 (13:34 -0500)]
Ensure legal candidate equalities when using relational triggers (#4035)
Andrew Reynolds [Thu, 12 Mar 2020 06:55:18 +0000 (01:55 -0500)]
Fix double notify in equality engine (#4036)
Fixes #3955.
Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.
This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.
A block of code changed indentation in this commit.
Aina Niemetz [Thu, 12 Mar 2020 05:27:32 +0000 (22:27 -0700)]
Hide options for and related to the BV abstraction module. (#4041)
All things related to the current BV solver are obsolete in the sense
that we are working on a new BV solver implementation. The BV abstraction
module has several issues and is quite hacky, it should only be enabled
in experimental settings. We don't want to remove it yet though, we want
to keep it around for future evaluation purposes. This commit
categorizes the option to enable the module and a second option related
to the module as 'undocumented'.
Andrew Reynolds [Thu, 12 Mar 2020 03:45:03 +0000 (22:45 -0500)]
Simplifications to the Datatypes API (#4040)
Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument.
I updated the Python files, although would be helpful to double check this is correct.
Co-authored-by: makaimann <makaim@stanford.edu>
makaimann [Thu, 12 Mar 2020 00:03:29 +0000 (17:03 -0700)]
Add automatic Cython binding installation (#3933)
* Remove getIndices for Kinds
* Test importing pycvc4
* Distutils install for pycvc4
* Use full path for cvc4kinds prefix
* Remove zip_safe option (not needed for distutils)
* Automatically clean up setup.py intermediate files
* Rely on make install to install pycvc4
* Run make install when testing python bindings
* Fix: Check importing pycvc4 when python bindings are built
* Remove one -Wshadow warning for cython-generated files
* Put the fake kinds submodule in generated __init__.py
* Remove unnecessary file permission options in python CMakeLists
* Respect install prefix unless in a virtualenv
* Handle python2 print function
* Use VIRTUAL_ENV environment variable to check if in python virtualenv
* Add header and documentation to setup.py.in
* Capitalize CVC4 in PyCVC4Install
* Update src/api/python/CMakeLists.txt
Co-Authored-By: Mathias Preiner <mathias.preiner@gmail.com>
* Simplify CMakeLists for setup.py configuration
* Shorten virtualenv check with Mathias's suggestion
* Set TRAVIS_CVC4_PYTHON_BINDINGS to no in other builds
* minor: bash syntax fix
* Move pycvc4 import check to makeInstallCheck
* Include installed pycvc4 location on PYTHONPATH
* Better way to set PYTHONPATH
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Andrew Reynolds [Wed, 11 Mar 2020 23:33:25 +0000 (18:33 -0500)]
Do not enable some SMT-COMP specific options by default (#4038)
Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops).
Issue #789 can be downgraded to "minor" after this PR.
Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.
Andrew Reynolds [Wed, 11 Mar 2020 22:54:07 +0000 (17:54 -0500)]
Guard against null relevancy condition in SyGuS (#4033)
Fixes #4025.
Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).
Andrew Reynolds [Wed, 11 Mar 2020 21:05:59 +0000 (16:05 -0500)]
Add missing datatype functions to new API (#3930)
This is in preparation for migrating the parser to use the Term-level API for datatypes.
Notably, this adds the function mkDatatypeSorts for making mutually recursive datatypes. I've added a unit test that demonstrates this method (which mirrors the Expr-level datatype API).
Andrew Reynolds [Wed, 11 Mar 2020 19:53:19 +0000 (14:53 -0500)]
Switch to Nodes for conjecture generator (#4026)
Fixes #4022.
Andres Noetzli [Wed, 11 Mar 2020 18:57:22 +0000 (11:57 -0700)]
reset-assertions: Update TheoryEngine's PropEngine* (#4032)
Fixes #4028. TheoryEngine's pointer was not updated to the new
PropEngine when resetting assertions. This commit fixes that. As far
as I can tell, this was the only class storing a PropEngine* that
isn't owned by PropEngine, so we should hopefully not have other
similar issues.
Andrew Reynolds [Wed, 11 Mar 2020 18:01:42 +0000 (13:01 -0500)]
Remove experimental symmetry breaker (#4005)
This never impacted performance positively. Fixes #3997 and fixes #4015.
There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.
Andrew Reynolds [Wed, 11 Mar 2020 17:18:59 +0000 (12:18 -0500)]
Fix non-parametrized operators in subgoal generation (#4023)
Fixes #4021.
We were previously constructing a malformed HO_APPLY as part of a subgoal for induction.
Andrew Reynolds [Wed, 11 Mar 2020 16:27:40 +0000 (11:27 -0500)]
Remove partial instantiation for local theory extensions (#4020)
Fixes #4019.
This feature was never fully implemented.
Andrew Reynolds [Wed, 11 Mar 2020 15:57:00 +0000 (10:57 -0500)]
Fix (#4017)
Fixes #4001.
This assertion was more of a conjecture (stating that easy cases of miniscoping are already handled). However some option combinations can break this invariant, regardless the code should do the correct thing.
Andrew Reynolds [Wed, 11 Mar 2020 15:13:24 +0000 (10:13 -0500)]
Fix duplicate variable issue in sygus-qe-preproc (#4013)
Andres Noetzli [Wed, 11 Mar 2020 13:54:50 +0000 (06:54 -0700)]
Introduce tables in the rewriter (#3742)
This commit adds tables in the rewriter that store which function should
be used to rewrite which kind. We have separate tables for `EQUAL`
because every theory has its own equality rewriter.
Andres Noetzli [Wed, 11 Mar 2020 06:25:21 +0000 (23:25 -0700)]
Set assertion in `CnfStream::ensureLiteral()` (#3927)
Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/
ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).
Aina Niemetz [Wed, 11 Mar 2020 05:42:49 +0000 (22:42 -0700)]
bv-gauss-elim: Fix handling of inconsistent case. (#4027)
This fixes the case when all rows are inconsistent.
Fixes #3999.
Andrew Reynolds [Wed, 11 Mar 2020 00:17:40 +0000 (19:17 -0500)]
Fix real to int for parameterized kinds (#4016)
Andrew Reynolds [Tue, 10 Mar 2020 23:40:29 +0000 (18:40 -0500)]
Fix options for regression: --sort-inference is incompatible with unsat cores. (#4011)
Andrew Reynolds [Tue, 10 Mar 2020 22:58:44 +0000 (17:58 -0500)]
Fix sort inference for top-level Boolean variables (#4012)
Fixes #4010.
Aina Niemetz [Tue, 10 Mar 2020 21:51:32 +0000 (14:51 -0700)]
Fix issue with reset-assertions. (#3988)
Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
Andrew Reynolds [Tue, 10 Mar 2020 21:19:31 +0000 (16:19 -0500)]
Logic exception instead of assertion failure for instantiate (#4006)
Fixes #4003.
Protects against a (class of) nonsensical option combinations.
Mathias Preiner [Tue, 10 Mar 2020 20:44:34 +0000 (13:44 -0700)]
Update bug report template
Andrew Reynolds [Tue, 10 Mar 2020 18:54:11 +0000 (13:54 -0500)]
Remove assertion in resolution bound inferences (#3980)
* Fix assertion in resolution bound inferences
* Format
* Minor
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Aina Niemetz [Tue, 10 Mar 2020 16:47:36 +0000 (09:47 -0700)]
Use fixed-width types in test/unit/context/contest_mm_black. (#3985)
Aina Niemetz [Mon, 9 Mar 2020 18:47:03 +0000 (11:47 -0700)]
Fix -Wshadow warning in test/unit/context/context_mm_black. (#3985)
Andrew Reynolds [Tue, 10 Mar 2020 17:40:54 +0000 (12:40 -0500)]
Consolidate options that disable produceModels (#3973)
Also adds --sort-inference to this list, fixes #3936.
Andrew Reynolds [Tue, 10 Mar 2020 16:58:06 +0000 (11:58 -0500)]
Fix assertion failure in sort inference for Boolean equalities (#3993)
Fixes #3990.
Aina Niemetz [Tue, 10 Mar 2020 16:27:19 +0000 (09:27 -0700)]
Fix -Wshadow warnings in sygus_grammar_cons.cpp. (#3986)
Andrew Reynolds [Tue, 10 Mar 2020 15:56:58 +0000 (10:56 -0500)]
Do not set values for non-linear mult terms in collectModelInfo (#3983)
Fixes #3803.
When non-linear arithmetic determines there is a model, then it should not send model values for multiplication terms that the linear solver assigned when abstracting (non-linear) multiplication. This avoids conflicts if the non-linear solver changed a value for a variable occurring in a non-linear monomial. This avoids check-model failures.
Andrew Reynolds [Tue, 10 Mar 2020 15:00:07 +0000 (10:00 -0500)]
Fix real as int for incremental (#3979)
Fixes #3956 and fixes #3969.
Andrew Reynolds [Tue, 10 Mar 2020 14:25:57 +0000 (09:25 -0500)]
Do not traverse quantifiers in nl ext purify (#3982)
Andrew Reynolds [Tue, 10 Mar 2020 05:35:31 +0000 (00:35 -0500)]
Only register sygus terms to unfold if option is set (#3978)
Fixes #3953.
Alex Ozdemir [Tue, 10 Mar 2020 05:06:57 +0000 (22:06 -0700)]
Document bv-to-bool recursion (#3848)
The BV-to-bool pass is implemented recursively.
This commit documents that.
We may want to change it at some point.
makaimann [Tue, 10 Mar 2020 04:13:21 +0000 (21:13 -0700)]
Enhancement: make the bool-to-bv pass more robust and targeted (#3021)
This pull request is an improvement to the bool-to-bv preprocessing pass. The existing pass is both too weak and too strong, depending on the circumstance. Throughout this description, "lower" refers to lowering a boolean to a bit-vector.
Andrew Reynolds [Tue, 10 Mar 2020 03:18:58 +0000 (22:18 -0500)]
Rename sygus option name (#3977)
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).
It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
Andrew Reynolds [Tue, 10 Mar 2020 02:36:24 +0000 (21:36 -0500)]
Remove instantiation propagator infrastructure (#3975)
Andrew Reynolds [Tue, 10 Mar 2020 00:23:05 +0000 (19:23 -0500)]
Ensure standard miniscoping is applied before aggressive miniscoping (#3974)
Fixes #3947.
Andrew Reynolds [Mon, 9 Mar 2020 22:44:39 +0000 (17:44 -0500)]
Eliminate spurious assertion (#3976)
Aina Niemetz [Mon, 9 Mar 2020 21:54:30 +0000 (14:54 -0700)]
DecisionEngine: Use unique_ptr for enabled strategies. (#3984)
Andrew Reynolds [Mon, 9 Mar 2020 21:18:43 +0000 (16:18 -0500)]
Fix type issue in arith rewrite equality (#3972)
Fixes #3952 and fixes #3940 and fixes #3941 and fixes #3968.
Andres Noetzli [Mon, 9 Mar 2020 20:49:10 +0000 (13:49 -0700)]
Make registration of unit clauses more robust (#3965)
Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.
Andres Noetzli [Mon, 9 Mar 2020 20:15:34 +0000 (13:15 -0700)]
Increase stack size for Windows builds to 100 MB (#3943)
Fixes #3528. The default stack size for Windows builds is very limited
(it seems to be 1 MB). This leads to problems for some of our users'
benchmarks (see the previously mentioned issue and another email that
we've received recently). Bumping the stack size to 100 MB seems to
solve the issues for the benchmarks that we have received. This of
course does not mean that we shouldn't continue working towards making
less of our code recursive.
Andrew Reynolds [Mon, 9 Mar 2020 19:33:01 +0000 (14:33 -0500)]
Clean up more uses of ExprManager in parsers (#3932)
Towards parser migration.
Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers.
This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used.
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.