cvc5.git
4 years agoEnsure legal candidate equalities when using relational triggers (#4035)
Andrew Reynolds [Thu, 12 Mar 2020 18:34:18 +0000 (13:34 -0500)]
Ensure legal candidate equalities when using relational triggers (#4035)

4 years agoFix double notify in equality engine (#4036)
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.

4 years agoHide options for and related to the BV abstraction module. (#4041)
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'.

4 years agoSimplifications to the Datatypes API (#4040)
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>
4 years agoAdd automatic Cython binding installation (#3933)
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>
4 years agoDo not enable some SMT-COMP specific options by default (#4038)
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.

4 years agoGuard against null relevancy condition in SyGuS (#4033)
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 ).

4 years agoAdd missing datatype functions to new API (#3930)
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).

4 years agoSwitch to Nodes for conjecture generator (#4026)
Andrew Reynolds [Wed, 11 Mar 2020 19:53:19 +0000 (14:53 -0500)]
Switch to Nodes for conjecture generator (#4026)

Fixes #4022.

4 years agoreset-assertions: Update TheoryEngine's PropEngine* (#4032)
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.

4 years agoRemove experimental symmetry breaker (#4005)
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.

4 years agoFix non-parametrized operators in subgoal generation (#4023)
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.

4 years agoRemove partial instantiation for local theory extensions (#4020)
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.

4 years agoFix (#4017)
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.

4 years agoFix duplicate variable issue in sygus-qe-preproc (#4013)
Andrew Reynolds [Wed, 11 Mar 2020 15:13:24 +0000 (10:13 -0500)]
Fix duplicate variable issue in sygus-qe-preproc (#4013)

4 years agoIntroduce tables in the rewriter (#3742)
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.

4 years agoSet assertion in `CnfStream::ensureLiteral()` (#3927)
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).

4 years agobv-gauss-elim: Fix handling of inconsistent case. (#4027)
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.

4 years agoFix real to int for parameterized kinds (#4016)
Andrew Reynolds [Wed, 11 Mar 2020 00:17:40 +0000 (19:17 -0500)]
Fix real to int for parameterized kinds (#4016)

4 years agoFix options for regression: --sort-inference is incompatible with unsat cores. (...
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)

4 years agoFix sort inference for top-level Boolean variables (#4012)
Andrew Reynolds [Tue, 10 Mar 2020 22:58:44 +0000 (17:58 -0500)]
Fix sort inference for top-level Boolean variables (#4012)

Fixes #4010.

4 years agoFix issue with reset-assertions. (#3988)
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.

4 years agoLogic exception instead of assertion failure for instantiate (#4006)
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.

4 years agoUpdate bug report template
Mathias Preiner [Tue, 10 Mar 2020 20:44:34 +0000 (13:44 -0700)]
Update bug report template

4 years agoRemove assertion in resolution bound inferences (#3980)
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>
4 years agoUse fixed-width types in test/unit/context/contest_mm_black. (#3985)
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)

4 years agoFix -Wshadow warning in test/unit/context/context_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)

4 years agoConsolidate options that disable produceModels (#3973)
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.

4 years agoFix assertion failure in sort inference for Boolean equalities (#3993)
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.

4 years agoFix -Wshadow warnings in sygus_grammar_cons.cpp. (#3986)
Aina Niemetz [Tue, 10 Mar 2020 16:27:19 +0000 (09:27 -0700)]
Fix -Wshadow warnings in sygus_grammar_cons.cpp. (#3986)

4 years agoDo not set values for non-linear mult terms in collectModelInfo (#3983)
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.

4 years ago Fix real as int for incremental (#3979)
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.

4 years agoDo not traverse quantifiers in nl ext purify (#3982)
Andrew Reynolds [Tue, 10 Mar 2020 14:25:57 +0000 (09:25 -0500)]
Do not traverse quantifiers in nl ext purify (#3982)

4 years agoOnly register sygus terms to unfold if option is set (#3978)
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.

4 years agoDocument bv-to-bool recursion (#3848)
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.

4 years agoEnhancement: make the bool-to-bv pass more robust and targeted (#3021)
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.

4 years agoRename sygus option name (#3977)
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.

4 years agoRemove instantiation propagator infrastructure (#3975)
Andrew Reynolds [Tue, 10 Mar 2020 02:36:24 +0000 (21:36 -0500)]
Remove instantiation propagator infrastructure (#3975)

4 years agoEnsure standard miniscoping is applied before aggressive miniscoping (#3974)
Andrew Reynolds [Tue, 10 Mar 2020 00:23:05 +0000 (19:23 -0500)]
Ensure standard miniscoping is applied before aggressive miniscoping (#3974)

Fixes #3947.

4 years agoEliminate spurious assertion (#3976)
Andrew Reynolds [Mon, 9 Mar 2020 22:44:39 +0000 (17:44 -0500)]
Eliminate spurious assertion (#3976)

4 years agoDecisionEngine: Use unique_ptr for enabled strategies. (#3984)
Aina Niemetz [Mon, 9 Mar 2020 21:54:30 +0000 (14:54 -0700)]
DecisionEngine: Use unique_ptr for enabled strategies. (#3984)

4 years agoFix type issue in arith rewrite equality (#3972)
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.

4 years agoMake registration of unit clauses more robust (#3965)
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.

4 years agoIncrease stack size for Windows builds to 100 MB (#3943)
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.

4 years agoClean up more uses of ExprManager in parsers (#3932)
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.

4 years agoConvert more uses of strings to words (#3921)
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.

4 years agoFix quoting of options on Travis (#3981)
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.

4 years agoFixes for bounds on transcendental functions (#3832)
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.

4 years agoRewrite again full for DIV rewrite (#3945)
Andrew Reynolds [Mon, 9 Mar 2020 05:15:09 +0000 (00:15 -0500)]
Rewrite again full for DIV rewrite (#3945)

Fixes #3944.

4 years agoExplicit end marker for models printed in the CVC language (#3934)
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;
```

4 years agoMinor refactor for theory of sets (#3924)
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.

4 years agoSimplify DatatypeDeclarationCommand command (#3928)
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.

4 years agoRemove tester name from APIs (#3929)
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.

4 years agoIgnore model check warning in regression test (#3926)
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.

4 years agoMake sygus datatype building independent of parser in sygus v2 (#3923)
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.

4 years agoSupport default sygus grammar construction for sets (#3842)
Andrew Reynolds [Fri, 6 Mar 2020 15:24:11 +0000 (09:24 -0600)]
Support default sygus grammar construction for sets (#3842)

Fixes #3645.

4 years agoMake output of regression script more readable (#3911)
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.

4 years agoRemove --apply-to-const preprocessing pass (#3919)
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.

4 years agoAdd a new arith constraint proof rule: IntTightenAP (#3818)
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.

4 years agoRevert "Add a new arith constraint proof rule: IntTightenAP (#3818)"
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.

4 years agoAdd a new arith constraint proof rule: IntTightenAP (#3818)
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.

4 years agoMigrate a majority of the functionality in parsers to the new API (#3838)
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.

4 years agoMove ownership of DecisionEngine into PropEngine. (#3850)
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.

4 years agoRevert "Move ownership of DecisionEngine into PropEngine. (#3850)"
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.

4 years agoMove ownership of DecisionEngine into PropEngine. (#3850)
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.

4 years agoFix issues with real to int (#3918)
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.

4 years agoEnable -Wshadow and fix warnings. (#3909)
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>
4 years agoRefactoring and cleaning the type enumerator for sets (#3908)
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

4 years agoStandardize the interface for SMT engine subsolvers (#3836)
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).

4 years agoFix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
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.

4 years agoFix variable shadowing bug in sets. (#3898)
Mathias Preiner [Tue, 3 Mar 2020 01:00:42 +0000 (17:00 -0800)]
Fix variable shadowing bug in sets. (#3898)

4 years ago Split collect model info by types in strings (#3847)
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.

4 years agoConvert more uses of string to word (#3834)
Andrew Reynolds [Sat, 29 Feb 2020 18:36:08 +0000 (12:36 -0600)]
Convert more uses of string to word (#3834)

4 years ago Throw warning instead of error for non-constant values in check-model stages (#3844)
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.

4 years agoAdd support for str.from_code (#3829)
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.

4 years agopropEngine: Reorder class declaration according to code style guidelines. (#3846)
Aina Niemetz [Sat, 29 Feb 2020 05:01:49 +0000 (21:01 -0800)]
propEngine: Reorder class declaration according to code style guidelines. (#3846)

4 years agoFix assertion related to assignability in the model. (#3843)
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.

4 years agoReplace conditional rewrite pass in quantifiers with the extended rewriter (#3841)
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.

4 years agoUse enum for quantifiers rewrite steps (#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.

4 years agoRefactor operator applications in the parser (#3831)
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.

4 years agoChanging TPTP parser to accomodate new API (#3837)
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.

4 years agoUpdate purifySygusGTerm to the new API (#3830)
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.

4 years agoFix large models for strings (#3835)
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.

4 years agoFix -Wshadow warnings in common headers (#3826)
Andres Noetzli [Thu, 27 Feb 2020 17:03:12 +0000 (09:03 -0800)]
Fix -Wshadow warnings in common headers (#3826)

4 years agoAdd support for is_digit and regular expression difference (#3828)
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.

4 years agoDisable regression that times out on debug (#3833)
Andrew Reynolds [Thu, 27 Feb 2020 03:15:04 +0000 (21:15 -0600)]
Disable regression that times out on debug (#3833)

4 years agoMove fix for vacuous sygus types out of the parser (#3820)
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).

4 years agoInitial work towards -Wshadow (#3817)
Andrew Reynolds [Thu, 27 Feb 2020 01:11:31 +0000 (19:11 -0600)]
Initial work towards -Wshadow (#3817)

4 years agoSome initial work on using words (#3819)
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.)

4 years agoInfrastructure for tautological literals in nonlinear solver (#3795)
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.

4 years agoUse side effect utility for non-linear lemmas (#3780)
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.

4 years agoFix regression (#3827)
Andrew Reynolds [Wed, 26 Feb 2020 21:43:07 +0000 (15:43 -0600)]
Fix regression (#3827)

4 years agoMore fixes for printing sygus commands (#3812)
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).

4 years agoBasic support for regular expression complement (#3437)
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

4 years agoRefactor type ascriptions in the parser (#3825)
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.

4 years agoMinor improvement to ParseOp (#3808)
Andrew Reynolds [Wed, 26 Feb 2020 18:33:00 +0000 (12:33 -0600)]
Minor improvement to ParseOp (#3808)

4 years agoUse default consts when not using any const during grammar normalization (#3807)
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.

4 years agoFix node arity issue in reduction of int2bv (#3777)
Andrew Reynolds [Wed, 26 Feb 2020 17:00:48 +0000 (11:00 -0600)]
Fix node arity issue in reduction of int2bv (#3777)

4 years agoMove equivalence class info to its own file in strings (#3799)
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.

4 years agoSupport for witnessing choice in models (#3781)
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.