cvc5.git
4 years agoInitialize theory rewriters in theories (#4197)
Andres Noetzli [Thu, 2 Apr 2020 02:35:25 +0000 (19:35 -0700)]
Initialize theory rewriters in theories (#4197)

Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).

4 years agoSupport char smt-lib syntax (#4188)
Andrew Reynolds [Wed, 1 Apr 2020 05:30:44 +0000 (00:30 -0500)]
Support char smt-lib syntax (#4188)

Towards support for the strings standard.

Adds support to (_ char #x ... ) syntax for characters.

4 years agoFix install for ANTLR contrib script and CI dependency caching. (#4196)
Mathias Preiner [Wed, 1 Apr 2020 04:31:13 +0000 (21:31 -0700)]
Fix install for ANTLR contrib script and CI dependency caching. (#4196)

4 years agoRename checkValid/query to checkEntailed. (#4191)
Aina Niemetz [Wed, 1 Apr 2020 01:12:16 +0000 (18:12 -0700)]
Rename checkValid/query to checkEntailed. (#4191)

This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.

4 years agoSwitch to GitHub actions for CI (#4190)
Mathias Preiner [Tue, 31 Mar 2020 23:44:03 +0000 (16:44 -0700)]
Switch to GitHub actions for CI (#4190)

Enable CI with GitHub actions, add macOS builds and disable Travis CI.

4 years agoFix fmf benchmark (#4193)
Andrew Reynolds [Tue, 31 Mar 2020 20:25:01 +0000 (15:25 -0500)]
Fix fmf benchmark (#4193)

Fixes regress1.

This benchmark is too delicate in the current state.

4 years agoRemove replay and use-theory options and idl (#4186)
Andrew Reynolds [Tue, 31 Mar 2020 19:27:04 +0000 (14:27 -0500)]
Remove replay and use-theory options and idl (#4186)

Towards disentangling Options / NodeManager / SmtEngine.

This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.

The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.

The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.

It also removes the solver in src/theory/idl, which cannot be enabled after this commit.

4 years agoFix strange bound regression (#4192)
Andrew Reynolds [Tue, 31 Mar 2020 16:49:02 +0000 (11:49 -0500)]
Fix strange bound regression (#4192)

Several things have happened with this regression lately, in chronological order:
(1) Instantiations involving bounded set quantifiers were changed to use choice to represent symbolic instantiations,
(2) fmf-bound was decoupled from finite-model-find (the latter is not enabled when the former is),
(3) choice was set to be an "unevaluated" kind (in 0060de3).

After (1) and (2), for the regression test/regress/regress1/fmf/fmf-strange-bounds.smt2, CVC4 was answering "sat" correctly but internally there was a source of incompleteness. In particular, a choice term was being generated in an instantiation that was later incorrectly evaluated, thus allowing CVC4 to skip an instantiation it shouldn't have.

The recent commit of (3) resolved this issue, making it so that choice is not an evaluated kind. This meant the benchmark went "sat" -> "unknown".

This PR fixes this issue by enabling --finite-model-find, which is now necessary to answer "sat".

It also adds a further test quantifier that was used in debugging this issue.

Fixes regress1.

4 years agoConvert more uses of string-specific functions (#4158)
Andrew Reynolds [Tue, 31 Mar 2020 15:07:29 +0000 (10:07 -0500)]
Convert more uses of string-specific functions (#4158)

Towards theory of sequences.

4 years agoFixing regressions (#4189)
Andrew Reynolds [Tue, 31 Mar 2020 13:39:21 +0000 (08:39 -0500)]
Fixing regressions (#4189)

An option was recently deleted, forgot to disable it from a regression. Fixes a failure in regress1.

4 years agoRewrites for all remaining return statements in strings rewriter (#4178)
Andrew Reynolds [Mon, 30 Mar 2020 23:15:07 +0000 (18:15 -0500)]
Rewrites for all remaining return statements in strings rewriter (#4178)

Towards proofs for string rewrites. All return statements all now associated with an enum value.

An indentation in a block of code changed in rewriteMembership.

4 years agoSupport indexed operators re.loop and re.^ (#4167)
Andrew Reynolds [Mon, 30 Mar 2020 21:29:23 +0000 (16:29 -0500)]
Support indexed operators re.loop and re.^ (#4167)

Towards support for the strings standard.

This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).

This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.

Also fixes #4161.

4 years agoRemove ref skolem datatype option (#4185)
Andrew Reynolds [Mon, 30 Mar 2020 19:52:55 +0000 (14:52 -0500)]
Remove ref skolem datatype option (#4185)

Fixes #4180, fixes CVC4/cvc4-projects#133, fixes CVC4/cvc4-projects#134.

4 years agoAdd coverage badge. (#4187)
Mathias Preiner [Mon, 30 Mar 2020 18:08:52 +0000 (11:08 -0700)]
Add coverage badge. (#4187)

Coverage information is updated nightly.

4 years agoFix arguments to print callback (#4171)
Andrew Reynolds [Mon, 30 Mar 2020 15:46:45 +0000 (10:46 -0500)]
Fix arguments to print callback (#4171)

The method applyParseOp may modify the argument vector. In the case of the sygus V1 parser, this argument vector was then being used to set up a print callback, leading to incorrect printing and failures.

Work towards having a working V1 -> V2 conversion for the release.

FYI @abdoo8080

4 years agoFrontend support for the choice operator (#4175)
mudathirmahgoub [Mon, 30 Mar 2020 14:04:52 +0000 (09:04 -0500)]
Frontend support for the choice operator (#4175)

Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue

4 years agoEnumeration for String rewrites (#4173)
Andrew Reynolds [Sun, 29 Mar 2020 00:50:35 +0000 (19:50 -0500)]
Enumeration for String rewrites (#4173)

In preparation for string proof infrastructure.

This introduces an enumeration type to track string rewrites.

It also makes inference printing more consistent.

4 years agoChange is-cons to (_ is cons) in Sygus benchmarks. (#4174)
Abdalrhman Mohamed [Sat, 28 Mar 2020 19:31:37 +0000 (14:31 -0500)]
Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)

4 years agoConvert the last few Sygus benchmarks to V2. (#4172)
Abdalrhman Mohamed [Sat, 28 Mar 2020 17:39:47 +0000 (12:39 -0500)]
Convert the last few Sygus benchmarks to V2. (#4172)

4 years agoStop printing datatype declaration for Sygus V1 grammar. (#4168)
Abdalrhman Mohamed [Sat, 28 Mar 2020 16:41:22 +0000 (11:41 -0500)]
Stop printing datatype declaration for Sygus V1 grammar. (#4168)

4 years agoNode traversal iterator (#3845)
Alex Ozdemir [Sat, 28 Mar 2020 06:22:41 +0000 (23:22 -0700)]
Node traversal iterator (#3845)

Implement an iterator for pre- and post-order traversals.

I believe that this will be useful in pre-processing passes, many of
which do postorder traversals that they implement by hand.

Right now this iterator does not support modification of the traversal
pattern, but we could add this later on, if we want it.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
4 years agoSplit transcendental solver to its own file (#4156)
Andrew Reynolds [Sat, 28 Mar 2020 00:53:59 +0000 (19:53 -0500)]
Split transcendental solver to its own file (#4156)

* Attempting to split transcendental function solver

* Clean

* Format

* More

* Format

* Attempt link

* Format

* Fix

* Another refactor

* More

* More

* Rename

* Format

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
4 years agoFix issues with unsat cores and reset-assertions (#4159)
Andres Noetzli [Fri, 27 Mar 2020 23:37:14 +0000 (16:37 -0700)]
Fix issues with unsat cores and reset-assertions (#4159)

Fixes #4151. Commit e9f4cec2cad02e270747759223090c16b9d2d44c fixed how
`(reset-assertions)` is handled by destroying and recreating the
`PropEngine` owned by `SmtEngine`. When unsat cores are enabled,
creating a `PropEngine` triggers the creation of a SAT proof and a CNF
proof. In the `ProofManager`, we had assertions that checked that those
kinds of proofs were only created once, which is not true anymore. This
commit removes the assertions, cleans up the memory management in
`ProofManager` to use `std::unique_ptr` and makes all the
`ProofManager::init*` methods non-static for consistency.

The commit also fixes an additional issue that I encountered while
testing the fix: When creating the new `PropEngine`, we were not
asserting `true` and `(not false)`, which lead to an error if we tried
to get the unsat core after a `(reset-assertion)` command and we had
asserted `(assert false)`. The commit fixes this by asserting `true` and
`(not false)` in the constructor of `PropEngine`.

The regression test is an extension of the example in #4151 and covers
both issues.

4 years agoFix expected output on arith regression (#4162)
Andrew Reynolds [Fri, 27 Mar 2020 22:45:30 +0000 (17:45 -0500)]
Fix expected output on arith regression (#4162)

A benchmark went unknown -> sat, likely due to the arith-brab commit, thus leading to a failure on regress1.This updates the status on this benchmark (also adds --nl-ext-tplanes to it).

4 years agoMove string utility file (#4164)
Andrew Reynolds [Fri, 27 Mar 2020 19:04:44 +0000 (14:04 -0500)]
Move string utility file (#4164)

Moves the string file to string.h. This is required since other required utilities will soon need to be added to regexp.h.

4 years agoDo not require that function sorts are first class internally (#4128)
Andrew Reynolds [Fri, 27 Mar 2020 15:23:42 +0000 (10:23 -0500)]
Do not require that function sorts are first class internally (#4128)

This PR removes the requirement in the NodeManager that argument types to the function sort are first class.

Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633

Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.

FYI @abdoo8080 .

4 years agoSupport unicode internal representation and escape sequences (#3852)
Andrew Reynolds [Fri, 27 Mar 2020 14:01:38 +0000 (09:01 -0500)]
Support unicode internal representation and escape sequences (#3852)

Work towards support for the strings standard.

This updates the string solver and parser such that:

The internal representation of strings is vectors of code points,
Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models,
The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings,
Handle unicode escape sequences according to the SMT-LIB standard in String,
Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary,
Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.

4 years agoMove set defaults function to its own file (#4154)
Andrew Reynolds [Fri, 27 Mar 2020 04:13:39 +0000 (23:13 -0500)]
Move set defaults function to its own file (#4154)

This moves SmtEngine::setDefaults to its own file.

This design is not final. One could imagine this being a part of a "OptionsSetter" utility. I am leaving this as is until we refactor the relationship between SmtEngine and Options.

Regardless, the general file structure should be such that this method is separate from SmtEngine, since setting default options is a large task that should be addressed independently from the core of SmtEngine.

This is initial preparation towards converting the SmtEngine from Expr -> Node.

A few very minor changes were made to the code to make the separation possible.

4 years agoAdded unit-cube-like test for branch and bound (#3922)
Amalee [Thu, 26 Mar 2020 23:32:51 +0000 (16:32 -0700)]
Added unit-cube-like test for branch and bound (#3922)

* unit-cude test wip

* test for wip unit cube test

* fixed simple rounding

* wip

* Passing tests except for sat vs unknown ones

* added flag for cube test

* put example back to normal

* Fixed for style guidelines.

* fixed rewrite bug

* removed extra comments

* unit-cude test wip

* test for wip unit cube test

* fixed simple rounding

* wip

* Passing tests except for sat vs unknown ones

* added flag for cube test

* put example back to normal

* Fixed for style guidelines.

* fixed rewrite bug

* removed extra comments

* Small fixes based on PR feedback

* replace NodeManager::currentNM with nm and clang formatted

* renamed test

* Added a regression test that triggers branch and bound

* Added ; COMMAND-LINE: --arith-brab

* Updated arith-brab test

* arith-brab enabled by default

* Added --nl-ext-tplanes to regress0/nl/ext-rew-aggr-test.smt2

Co-authored-by: Amalee Wilson <amalee@cis.uab.edu>
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
4 years agoDisable slow regression (#4157)
Andrew Reynolds [Thu, 26 Mar 2020 19:42:49 +0000 (14:42 -0500)]
Disable slow regression (#4157)

Should fix timeout in asan build.

4 years agoAdd stats for string reductions, lemmas and conflicts (#4149)
Andrew Reynolds [Thu, 26 Mar 2020 14:52:28 +0000 (09:52 -0500)]
Add stats for string reductions, lemmas and conflicts (#4149)

This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).

Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.

4 years agoGeneralize more string-specific functions (#4152)
Andrew Reynolds [Thu, 26 Mar 2020 13:37:13 +0000 (08:37 -0500)]
Generalize more string-specific functions (#4152)

Towards theory of sequences.

Note this PR also changes design in core/base solver. Previously I had estimated that we should have separate instances per type for these solvers, but I think it is better to have these classes handle all string-like types simultaneously. This means they should not have a d_type field.

4 years agoCare graphs based on polymorphic operators in strings (#4150)
Andrew Reynolds [Thu, 26 Mar 2020 06:38:08 +0000 (01:38 -0500)]
Care graphs based on polymorphic operators in strings (#4150)

Towards theory of sequences.

To compute a care graphs, we need to group function applications by the string type they are associated with. This PR introduces a utility to function to get the "owning string type" for a function application, and updates the care graph computation so that it partitions function applications according to this type.

4 years agoSupport async-signal-safe printing of inferences (#4148)
Andres Noetzli [Wed, 25 Mar 2020 19:22:25 +0000 (12:22 -0700)]
Support async-signal-safe printing of inferences (#4148)

Commit c9b7c3d introduced code for
counting the number of string inferences done per type of inference.
However, it did not add support for printing the inference names in an
async-signal-safe manner via safe_print() (note that printing in
signal handlers is done differently from the regular stats printing).
This commit adds the corresponding code, s.t. we get the inference names
when printing the stats when CVC4 is interrupted or crashes.

4 years agobv2int : linear mult opt (#4142)
Ahmed Irfan [Wed, 25 Mar 2020 16:37:57 +0000 (09:37 -0700)]
bv2int : linear mult opt (#4142)

4 years ago Generalize more uses of string-specific functions (#4145)
Andrew Reynolds [Wed, 25 Mar 2020 13:48:14 +0000 (08:48 -0500)]
 Generalize more uses of string-specific functions (#4145)

Towards theory of sequences.

4 years agoInt2BV fail on demand (#4079)
yoni206 [Tue, 24 Mar 2020 17:53:18 +0000 (10:53 -0700)]
Int2BV fail on demand (#4079)

This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.

4 years agoRestrict partial triggers to standard quantified formulas (#4144)
Andrew Reynolds [Tue, 24 Mar 2020 15:45:55 +0000 (10:45 -0500)]
Restrict partial triggers to standard quantified formulas (#4144)

Fixes #4143.

4 years agoRestrict cases of sygus grammar reduction based on argument variants (#4131)
Andrew Reynolds [Tue, 24 Mar 2020 02:20:32 +0000 (21:20 -0500)]
Restrict cases of sygus grammar reduction based on argument variants (#4131)

An assertion is triggered for some V2 versions of SyGuS V1 benchmarks during sygus grammar reduction. This PR updates this technique so that it only applies to sygus constructors whose sygus operators are lambdas of the form
lambda x1 ... xn. f( x1 ... xn ).

FYI @abdoo8080 .

4 years agoInfer when sygus operators are equivalent to builtin kinds (#4140)
Andrew Reynolds [Mon, 23 Mar 2020 22:12:56 +0000 (17:12 -0500)]
Infer when sygus operators are equivalent to builtin kinds (#4140)

The V2 parser always turns sygus operators into lambdas for consistency. This PR ensures that we nevertheless infer when a sygus operator is equivalent to a builtin operator, e.g.
(lambda x y. (+ x y)) is equivalent to +.

The main reason this is required is to ensure that solution reconstruction heuristics work optimally when we make the switch SyGuS V1 -> V2 (see 5 failing benchmarks due to --cegqi-si=all on #4136).

4 years agoSimplify auxiliary variable handling in CEGQI (#4141)
Andrew Reynolds [Mon, 23 Mar 2020 19:04:32 +0000 (14:04 -0500)]
Simplify auxiliary variable handling in CEGQI (#4141)

Fixes #3849 and fixes #4062.

Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables.

In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be:
(1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 )
(2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2).
Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities).

This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above.

Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given.

4 years agoThrow exception for non-well-founded unimplemented SyGuS types. (#4125)
Andrew Reynolds [Mon, 23 Mar 2020 18:30:48 +0000 (13:30 -0500)]
Throw exception for non-well-founded unimplemented SyGuS types. (#4125)

Fixes #3931.

Currently we print a warning for unimplemented types when constructing default SyGuS grammars. We should additionally throw an exception when the unimplemented type would lead to a non-well-founded datatype.

4 years agoChange transcendental function app slave list to unordered_set (#4139)
Andrew Reynolds [Mon, 23 Mar 2020 15:49:46 +0000 (10:49 -0500)]
Change transcendental function app slave list to unordered_set (#4139)

Fixes #4112.

4 years agoCollect statistics about normal form inferences (#4127)
Andres Noetzli [Mon, 23 Mar 2020 04:05:37 +0000 (21:05 -0700)]
Collect statistics about normal form inferences (#4127)

This commit adds code to count the number of inferences made of each
inference type for normal form inferences. It extends the Inference
enum in `infer_info.h` and adds two new `sendInference()` methods in the
`InferenceManager` to send and count inferences that have a corresonding
entry in the `Inference` enum.

4 years agoSort inference does not handle APPLY_UF when higher-order is enabled (#4138)
Andrew Reynolds [Sun, 22 Mar 2020 14:23:57 +0000 (09:23 -0500)]
Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)

Fixes #4092 and fixes #4134.

Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.

4 years agoConvert V1 Sygus files to V2. (#4136)
Abdalrhman Mohamed [Sun, 22 Mar 2020 03:33:15 +0000 (22:33 -0500)]
Convert V1 Sygus files to V2. (#4136)

4 years agoSimplify heuristic in `processNEqc` (#4129)
Andres Noetzli [Sat, 21 Mar 2020 19:57:22 +0000 (12:57 -0700)]
Simplify heuristic in `processNEqc` (#4129)

This commit removes a special case in `CoreSolver::processNEqc()` where
we stopped looking for inferences for a given normal form as soon as we
found the highest priority inference (currently that an element in the
normal form is empty). This effectively elevates the priority of this
inference to the other inferences that are done immediately instead of
being added to the `pinfer` vector that holds the possible inferences.
The experiments that I've run seem to confirm that it is unnecessary to
have this special case.

4 years agoDon't run bv_nat parse test with competition build (#4126)
Andres Noetzli [Sat, 21 Mar 2020 03:47:53 +0000 (20:47 -0700)]
Don't run bv_nat parse test with competition build (#4126)

This commit should fix the nightlies.

4 years agoGeneralize mkConcat for types (#4123)
Andrew Reynolds [Fri, 20 Mar 2020 23:09:27 +0000 (18:09 -0500)]
Generalize mkConcat for types (#4123)

Towards theory of sequences.

The utility function mkConcat needs a type to know what to construct in the empty string case.

4 years agoFix variable shadowing issue in sygus-inference (#4121)
Andrew Reynolds [Fri, 20 Mar 2020 22:29:41 +0000 (17:29 -0500)]
Fix variable shadowing issue in sygus-inference (#4121)

This makes the sygus-inference preprocessing pass avoid variable shadowing, which technically could happen by forcing unexpected options.

Fixes #4083.

4 years agoFix sort comparison within assertion in cegis (#4113)
Andrew Reynolds [Fri, 20 Mar 2020 20:36:35 +0000 (15:36 -0500)]
Fix sort comparison within assertion in cegis (#4113)

4 years agoGuard cases of sort inference in quantifier free logics in uf cardinality (#4074)
Andrew Reynolds [Fri, 20 Mar 2020 19:45:13 +0000 (14:45 -0500)]
Guard cases of sort inference in quantifier free logics in uf cardinality (#4074)

Fixes #4068 and fixes #4085 and fixes #4063.

4 years agoSplit string-specific operators from TheoryStringsRewriter (#3920)
Andrew Reynolds [Fri, 20 Mar 2020 19:07:37 +0000 (14:07 -0500)]
Split string-specific operators from TheoryStringsRewriter (#3920)

Organization towards theory of sequences.

The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.

4 years agoDo not assign higher-order representative if function does not exist (#4073)
Andrew Reynolds [Fri, 20 Mar 2020 18:18:11 +0000 (13:18 -0500)]
Do not assign higher-order representative if function does not exist (#4073)

4 years agoHandle failures for sygus QE preprocess (#4072)
Andrew Reynolds [Fri, 20 Mar 2020 17:41:49 +0000 (12:41 -0500)]
Handle failures for sygus QE preprocess (#4072)

If the user explicitly disabled the QE algorithm and asked for QE, then we should resort to normal methods. Fixes #4064 and fixes #4109.

4 years agoParse error for SyGuS version 1.0 vs 2.0 (#4057)
Andrew Reynolds [Fri, 20 Mar 2020 16:04:31 +0000 (11:04 -0500)]
Parse error for SyGuS version 1.0 vs 2.0 (#4057)

This adds a useful error message that recognizes a divergence in the expected input format (version 1 vs. version 2), which will be useful when we switch to SyGuS version 2 by default. This warning message is already potentially useful for users who are using --lang=sygus2.

4 years agoMake handling of illegal internal representatives in quantifiers engine more robust...
Andrew Reynolds [Fri, 20 Mar 2020 15:16:21 +0000 (10:16 -0500)]
Make handling of illegal internal representatives in quantifiers engine more robust (#4034)

Fixes #4002 (that benchmark is now unknown).

The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation.

The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs.

A block of code changed indentation in this PR, which was updated to the new standards.

4 years agoRefactor enumerator for strings (#4014)
Andrew Reynolds [Fri, 20 Mar 2020 14:25:24 +0000 (09:25 -0500)]
Refactor enumerator for strings (#4014)

Towards theory of sequences. This separates out a virtual base class and utility class for the strings enumerator, which will be extended for sequences later.

4 years agoFix regression output related to sygus+bv-div-zero (#4122)
Andrew Reynolds [Thu, 19 Mar 2020 22:57:42 +0000 (17:57 -0500)]
Fix regression output related to sygus+bv-div-zero (#4122)

4 years agoBv2int fail on demand
yoni206 [Thu, 19 Mar 2020 17:12:10 +0000 (10:12 -0700)]
Bv2int fail on demand

Postpone failure in bv-to-int preprocessing pass.

4 years agoOnly apply testConstStringInRegExp to const regexp (#4120)
Andres Noetzli [Thu, 19 Mar 2020 14:18:58 +0000 (07:18 -0700)]
Only apply testConstStringInRegExp to const regexp (#4120)

Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.

4 years agoSyGuS must use total bitvector division (#4119)
Andrew Reynolds [Thu, 19 Mar 2020 08:37:26 +0000 (03:37 -0500)]
SyGuS must use total bitvector division (#4119)

Our SyGuS utilities are not designed to deal with partial bitvector division. If a user forced an older version of SMT-LIB semantics while using SyGuS, this led to a number of issues.

For now, we disable this option when it is combined with SyGuS, regardless of whether the user turns it on.

A more permanent solution will be to remove the old SMT-LIB semantics option bv-div-zero-const entirely.

Fixes #4097 and fixes #4088 and fixes #4104.

4 years agoOnly allow bv2nat/int2bv with BV and integer logic (#4118)
Andres Noetzli [Thu, 19 Mar 2020 06:46:50 +0000 (23:46 -0700)]
Only allow bv2nat/int2bv with BV and integer logic (#4118)

CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.

4 years agoRemove spurious assertion (#4117)
Andrew Reynolds [Thu, 19 Mar 2020 06:01:05 +0000 (01:01 -0500)]
Remove spurious assertion (#4117)

Fixes #4106.

The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).

4 years agoExplicitly handle isFinite for rounding modes (#4115)
Andrew Reynolds [Thu, 19 Mar 2020 04:54:57 +0000 (23:54 -0500)]
Explicitly handle isFinite for rounding modes (#4115)

The function TypeNode::isFinite is designed to compute finiteness without computing cardinality for the sake of efficiency; there was a missing case for rounding modes, leading to an assertion failure.

Fixes #4101.

4 years agoAlways enable cbqi literal dependency (#4116)
Andrew Reynolds [Thu, 19 Mar 2020 01:42:55 +0000 (20:42 -0500)]
Always enable cbqi literal dependency (#4116)

Fixes #4105.

It appears that the two (experimental) options in that issue were incompatible.

A block of code changed indentation in this PR and was updated to guidelines.

4 years agoFix issue with multiple infinities in CEGQI for LIRA (#4114)
Andrew Reynolds [Thu, 19 Mar 2020 01:13:27 +0000 (20:13 -0500)]
Fix issue with multiple infinities in CEGQI for LIRA (#4114)

Fixes #4086.

Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.

4 years agoMove node visitor class from smt_util/ to expr/ (#4110)
Alex Ozdemir [Wed, 18 Mar 2020 21:30:30 +0000 (14:30 -0700)]
Move node visitor class from smt_util/ to expr/ (#4110)

Done by:

Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes
Moving the file
Changing src/expr/CMakeLists.txt and src/CMakeLists.txt
clang-format, omitting node_visitor.h.
In reference to discussion, here.

4 years agoSmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)
Aina Niemetz [Tue, 17 Mar 2020 04:35:21 +0000 (21:35 -0700)]
SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)

4 years agoRemove AlwaysAssert(false) for hole.
Alex Ozdemir [Mon, 16 Mar 2020 19:36:07 +0000 (12:36 -0700)]
Remove AlwaysAssert(false) for hole.

4 years agoclang-format
Alex Ozdemir [Mon, 16 Mar 2020 19:35:17 +0000 (12:35 -0700)]
clang-format

4 years agoFix simplicity check in prop
Alex Ozdemir [Mon, 16 Mar 2020 19:34:41 +0000 (12:34 -0700)]
Fix simplicity check in prop

4 years agoFix antecedent loop. Whoops
Alex Ozdemir [Mon, 16 Mar 2020 19:19:06 +0000 (12:19 -0700)]
Fix antecedent loop. Whoops

4 years agoOnly save farkas+tightening proofs. Error on holes
Alex Ozdemir [Mon, 16 Mar 2020 19:17:43 +0000 (12:17 -0700)]
Only save farkas+tightening proofs. Error on holes

I'll remove the error later

4 years agoExpand the definition of a "simple" farkas proof.
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.

4 years agoDecisionEngine: Use single unique pointer for ITE strategy . (#4078)
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.

4 years agoIssue 4077: Add unit test to reproduce issue. (#4107)
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.

4 years agoCreate master equality engine at context level 0 (#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.

4 years agoHandle cases in --sygus-rr where evaluation is not constant (#4100)
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.

4 years agoRemoving a few deprecated options (#4052)
Andrew Reynolds [Fri, 13 Mar 2020 19:53:00 +0000 (14:53 -0500)]
Removing a few deprecated options (#4052)

4 years agoRemove regress for real to int (#4071)
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.

4 years agoGeneralize type rules for strings to sequences (#3987)
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.

4 years agoFix case of non-constant value for sygus sampling (#4051)
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.

4 years agoAdd options for nec regression (#4056)
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.

4 years agoConvert most instances of dataypes in parsers to the new API (#4054)
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.

4 years agoDo not allow quantifiers over real variables in real to int pass. (#4049)
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.

4 years agoRemove local theory extension option (#4048)
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.

4 years agoDo not make models for quantified function variables (#4039)
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.

4 years agoNew C++ API: Remove support for (reset). (#4037)
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.

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.