cvc5.git
4 years agoIncorporate sequences into the word interface (#4543)
Andrew Reynolds [Mon, 1 Jun 2020 14:14:23 +0000 (09:14 -0500)]
Incorporate sequences into the word interface (#4543)

Also renames a function mkWord -> mkWordFlatten.

4 years agoDo not cache operator eliminations in arith (#4542)
Andres Noetzli [Sun, 31 May 2020 16:13:39 +0000 (09:13 -0700)]
Do not cache operator eliminations in arith (#4542)

Fixes #4525. The actual problem in the issue is not that the unsat core
is satisfiable but that our unsat core check is not working as intended.
Our unsat core check uses the same `ExprManager` as the main `SmtEngine`
and thus also shares the same attributes for nodes. However, since we
have a different `SmtEngine` instance for the check, we also have
different instances of `TheoryArith`. This leads to the check failing
due to the following:

- Our only input assertion is `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
  0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
  expanded as expected but no attribute is set because it happens in a
  simple `TheoryArith::eliminateOperators()` call.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
  `(/ 1 0)` (not cached) and then we expand it recursively to the
  expected term and cache `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/
  1 0))`.

Up to this point, things are suboptimal but there are no correctness
issues. The problem starts when we do the same process in the unsat core
check:

- Our only input assertion is again `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
  0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
  expanded as expected but no attribute is set or checked because it
  happens in a simple `TheoryArith::eliminateOperators()` call. Note
  that the skolem introduced here for the division-by-zero case is
  different from the skolem introduced above because this is in a
  different `TheoryArith` instance that does not know the existing
  skolems.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
  `(/ 1 0)` (not cached) and then we use the cache from our solving call
  to expand it `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/ 1 0))`.
  Note that `divByZero` here is the skolem from the main solver.

As a result, the preprocessed assertions mix skolems from the main
`SmtEngine` with the `SmtEngine` of the unsat core check, making the
constraints satisfiable.

To solve this problem, this commit removes the caching-by-attribute
mechanism. The reason for removing it is that it is currently
ineffective (since most eliminations do not seem to be cached) and there
are caches at other levels, e.g. when expanding definitions. If we deem
the operator elimination to be a bottleneck, we can introduce a similar
mechanism at the level of `TheoryArith`.

4 years agoupdate example in README to use ctest. (#4540)
yoni206 [Sun, 31 May 2020 04:17:59 +0000 (21:17 -0700)]
update example in README to use ctest. (#4540)

An example for restricting timeout in tests uses the old `make regress0` instead of the new `ctest -L regress0`

4 years agoAdd the sequence type (#4539)
Andrew Reynolds [Sat, 30 May 2020 18:10:54 +0000 (13:10 -0500)]
Add the sequence type (#4539)

This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.

The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.

4 years agoFix term registry for constant case, simplify. (#4538)
Andrew Reynolds [Thu, 28 May 2020 20:05:06 +0000 (15:05 -0500)]
Fix term registry for constant case, simplify. (#4538)

We were getting an assertion failure (causing nightlies to fail) due to the recent optimization to the strings skolem cache (978f455). This ensures we ignore constant strings in TermRegistry::getRegisterTermAtomicLemma.

It also removes a deprecated option that is deleted in the proof-new branch.

4 years agoAdd the Expr-level sequence datatype (#4526)
Andrew Reynolds [Wed, 27 May 2020 23:05:07 +0000 (18:05 -0500)]
Add the Expr-level sequence datatype (#4526)

This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.

4 years agoTweak the use of static_assert to support older compilers. (#4536)
Martin [Wed, 27 May 2020 18:26:51 +0000 (19:26 +0100)]
Tweak the use of static_assert to support older compilers. (#4536)

C++11 introduces static_assert(bool, string).
C++17 introduces static_assert(bool)

By adding a message we can support older compilers such as those
used by our nightly build system...

4 years agoFix an incorrect limit in conversion from real to float (#4418)
Martin [Tue, 26 May 2020 18:49:01 +0000 (19:49 +0100)]
Fix an incorrect limit in conversion from real to float (#4418)

This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.

4 years agoConvert more uses of strings to words (#4527)
Andrew Reynolds [Tue, 26 May 2020 17:41:31 +0000 (12:41 -0500)]
Convert more uses of strings to words (#4527)

4 years agoFix mismatched iterators (CID 1493892). (#4531)
Mathias Preiner [Tue, 26 May 2020 16:44:51 +0000 (09:44 -0700)]
Fix mismatched iterators (CID 1493892). (#4531)

Issue found by coverity.

4 years ago(proof-new) Update proof checker. (#4511)
Andrew Reynolds [Tue, 26 May 2020 15:27:45 +0000 (10:27 -0500)]
(proof-new) Update proof checker. (#4511)

This adds new required features to proof checker and the base class of proof rule checker.

This is required as the first dependency towards merging further infrastructure related to proofs.

4 years ago(proof-new) Updates to strings skolem cache. (#4524)
Andrew Reynolds [Tue, 26 May 2020 14:51:13 +0000 (09:51 -0500)]
(proof-new) Updates to strings skolem cache. (#4524)

This PR makes strings skolem cache call the ProofSkolemCache. This is required for proper proof checking, as it makes all skolems be associated with their formal definition, encapsulated by a witness term.

It furthermore makes skolem sharing more uniform and aggressive by noting that most string skolems correspond to purification variables (typically for some substr term). A purification variable for a term that rewrites to a constant can be replaced by the constant itself.

It also introduces an attribute IndexVarAttribute which is used to ensure reductions involving universal variables are deterministic.

4 years agoUpdate to CaDiCaL version 1.2.1. (#4530)
Mathias Preiner [Tue, 26 May 2020 01:56:39 +0000 (18:56 -0700)]
Update to CaDiCaL version 1.2.1. (#4530)

4 years ago[SMT-COMP] Redirect non-answers to /dev/null (#4528)
Andres Noetzli [Sun, 24 May 2020 03:52:29 +0000 (20:52 -0700)]
[SMT-COMP] Redirect non-answers to /dev/null (#4528)

Commit 00badd3a63a2fa568373d5c58553944b579d42bb changed our run script
to write output other than `sat`/`unsat` to a file if `$2` is passed to
it. However, it looks like StarExec does not pass that parameter to our
script despite the documentation claiming that it does [0]. This commit
makes our check more defensive by redirecting our unnecessary output to
`/dev/null` if `STAREXEC_WALLCLOCK_LIMIT` is set. I've done a quick test
run on StarExec and it looks like this does the trick.

[0]
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-SpecialVariables

4 years agoremove unused field d_emp_exp in TheorySetsPrivate (#4521)
mudathirmahgoub [Sat, 23 May 2020 15:28:50 +0000 (10:28 -0500)]
remove unused field d_emp_exp in TheorySetsPrivate (#4521)

Remove unused field d_emp_exp in TheorySetsPrivate

4 years agoAdd the sequence datatype (#4153)
Andrew Reynolds [Sat, 23 May 2020 12:13:42 +0000 (07:13 -0500)]
Add the sequence datatype (#4153)

This class is the Node-level representation of a sequence. It is analogous to CVC4::String.

4 years agoFix mistakes in sygus API comments. (#4520)
Abdalrhman Mohamed [Sat, 23 May 2020 04:55:29 +0000 (23:55 -0500)]
Fix mistakes in sygus API comments. (#4520)

4 years agoRefactor operator elimination in arithmetic (#4519)
Andrew Reynolds [Sat, 23 May 2020 03:39:16 +0000 (22:39 -0500)]
Refactor operator elimination in arithmetic (#4519)

This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong:
(1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers.
(2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental.

The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way.

As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR.

This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts.

Also notice that --rewrite-divk is effectively now enabled by default always.

Fixes #4484, fixes #4486, fixes #4481.

4 years ago[SMT-COMP] Use tear-down-incremental for arithmetic (#4518)
Andres Noetzli [Fri, 22 May 2020 22:33:04 +0000 (15:33 -0700)]
[SMT-COMP] Use tear-down-incremental for arithmetic (#4518)

This commit changes the run-script for the incremental track to use
`--tear-down-incremental=1` for all logics that involve arithmetic. The
main motivation for this change is avoid issues that we have with the
lemmas generated for `mod`/`div` during `ppRewrite` that cause
model-soundness issues.

4 years agoCaDiCaL: Clean up initialization on creation. (#4516)
Aina Niemetz [Fri, 22 May 2020 21:09:54 +0000 (14:09 -0700)]
CaDiCaL: Clean up initialization on creation. (#4516)

4 years ago(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)
Andrew Reynolds [Fri, 22 May 2020 19:27:13 +0000 (14:27 -0500)]
(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)

This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function).

This allows us to justify the regular expression inclusion inference as a rewrite.

4 years agoCryptominisat: Clean up initialization on creation. (#4515)
Aina Niemetz [Fri, 22 May 2020 16:47:55 +0000 (09:47 -0700)]
Cryptominisat: Clean up initialization on creation. (#4515)

4 years agoAdd support for SAT solver Kissat. (#4514)
Aina Niemetz [Fri, 22 May 2020 13:41:50 +0000 (06:41 -0700)]
Add support for SAT solver Kissat. (#4514)

4 years ago(proof-new) Proof node to SExpr utility. (#4512)
Andrew Reynolds [Fri, 22 May 2020 13:01:59 +0000 (08:01 -0500)]
(proof-new) Proof node to SExpr utility. (#4512)

This is required for dag-ifying ProofNode output.

4 years agoUpdate string kind names in new API (#4509)
Andrew Reynolds [Fri, 22 May 2020 04:40:44 +0000 (23:40 -0500)]
Update string kind names in new API (#4509)

To match the smt2 Unicode standard. The internal ones are left unchanged for now.

4 years ago(proof-new) Minor update to strings solver state (#4510)
Andrew Reynolds [Fri, 22 May 2020 04:10:24 +0000 (23:10 -0500)]
(proof-new) Minor update to strings solver state (#4510)

4 years agoDisable re-elim by default (#4508)
Andrew Reynolds [Thu, 21 May 2020 23:33:14 +0000 (18:33 -0500)]
Disable re-elim by default (#4508)

Disabling re-elim performs better overall in many recent experiments.

4 years agoMake Grammar reusable. (#4506)
Abdalrhman Mohamed [Thu, 21 May 2020 18:01:14 +0000 (13:01 -0500)]
Make Grammar reusable. (#4506)

This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.

4 years agoThrow logic exception for equality between regular expressions (#4505)
Andrew Reynolds [Thu, 21 May 2020 03:27:04 +0000 (22:27 -0500)]
Throw logic exception for equality between regular expressions (#4505)

Fixes #4503.

4 years agoFix missing check for cardinality one in unconstrained simplifier (#4504)
Andrew Reynolds [Thu, 21 May 2020 02:22:25 +0000 (21:22 -0500)]
Fix missing check for cardinality one in unconstrained simplifier (#4504)

Fixes #4482.

4 years agoNormal form equality conflicts and uniqueness check (#4497)
Andrew Reynolds [Wed, 20 May 2020 15:20:34 +0000 (10:20 -0500)]
Normal form equality conflicts and uniqueness check (#4497)

This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.

It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.

4 years agoAdd proof skolem cache (#4485)
Andrew Reynolds [Wed, 20 May 2020 14:14:54 +0000 (09:14 -0500)]
Add proof skolem cache (#4485)

This adds the general utility for maintaining mappings from Skolems to their witness form via attributes.

I am sending this as a PR now since it would be helpful to use this class for fixing some of the recent unconstrained-simp bugs.

4 years agoFix parametric datatype instantiation (#4493)
Andrew Reynolds [Wed, 20 May 2020 12:47:24 +0000 (07:47 -0500)]
Fix parametric datatype instantiation (#4493)

A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.

4 years agoCegqiBv: Clean up after renaming options. (#4487)
Aina Niemetz [Wed, 20 May 2020 07:08:43 +0000 (00:08 -0700)]
CegqiBv: Clean up after renaming options. (#4487)

4 years agoUse debug-check-model to enable internal debugging in check-model (#4480)
Andrew Reynolds [Wed, 20 May 2020 05:05:58 +0000 (00:05 -0500)]
Use debug-check-model to enable internal debugging in check-model (#4480)

Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.

Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.

4 years agoAdd a simple script to convert sygus v1 files to v2. (#4409)
Abdalrhman Mohamed [Wed, 20 May 2020 03:33:03 +0000 (22:33 -0500)]
Add a simple script to convert sygus v1 files to v2. (#4409)

4 years agoDo not eliminate variables that are equal to unevaluatable terms (#4267)
Andrew Reynolds [Wed, 20 May 2020 02:48:01 +0000 (21:48 -0500)]
Do not eliminate variables that are equal to unevaluatable terms (#4267)

When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.

This PR ensures we only eliminate variables when v contains only evaluated operators.

Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.

Fixes #4500.

4 years agoFix cached free variable identifiers in sygus term database (#4394)
Andrew Reynolds [Wed, 20 May 2020 00:34:18 +0000 (19:34 -0500)]
Fix cached free variable identifiers in sygus term database (#4394)

Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.

Fixes #4383.

4 years agoRenamed operator CHOICE to WITNESS (#4207)
mudathirmahgoub [Tue, 19 May 2020 21:24:59 +0000 (16:24 -0500)]
Renamed operator CHOICE to WITNESS (#4207)

Renamed operator CHOICE to WITNESS, and removed it from the front end

4 years agoUse fresh variables when miniscoping (#4296)
Andrew Reynolds [Tue, 19 May 2020 20:38:05 +0000 (15:38 -0500)]
Use fresh variables when miniscoping (#4296)

Fixes #4288.

When applying miniscoping, we previously were reusing variables across quantified formulas in the resulting conjunction. This ensures our miniscoping ensures fresh variables.

4 years agoUpdate enum and option names for sygus languages (#4388)
Andrew Reynolds [Tue, 19 May 2020 19:51:19 +0000 (14:51 -0500)]
Update enum and option names for sygus languages (#4388)

This ensures sygus is interpreted as sygus version 2; sygus1 must be used to specify sygus version 1.

Required for the 1.8 release.

4 years agoMake SolveEq and PlusCombineLikeTerms idempotent (#4438)
Andres Noetzli [Tue, 19 May 2020 18:31:42 +0000 (11:31 -0700)]
Make SolveEq and PlusCombineLikeTerms idempotent (#4438)

Fixes #3692 and an assertion failure that came up during the test runs
for SMT-COMP. The bit-vector rewrites `SolveEq` and
`PlusCombineLikeTerms` were not always idempotent. At a high level,
`SolveEq` combines common terms from two sides of an equality and
`PlusCombineLikeTerms` combines common terms within an addition.
However, in doing so, these rewrites were reordering the operands of the
bit-vector addition based on the node ids of the terms that were
multiplied with their coefficients. Consider the addition `3 * x * y + 5
* y * z` (the bit-width does not matter). `PlusCombineLikeTerms` would
reorder this addition to `5 * y * z + 3 * x * y` if the node id of `y *
z` was smaller than the node id of `x * y`. The issue is that node ids
are not fixed for a given term: If we have a term `x * y` and that term
reaches ref count 0, we may get a different id for that same term if we
recreate it later on. When terms reach ref count 0, we don't immediately
delete them but add them to our set of zombies to be deleted whenever
the list of zombies grows larger than some fixed size. When applying
`SolveEq` and `PlusCombineLikeTerms` multiple times (even in direct
succession without doing anything else), the node order may change
because some of the terms like `x * y` may be zombies while others have
been deleted and get new ids, leading to the relative order of node ids
changing. I suspect that we could construct a case where we get into an
infinite rewrite loop.

This commit addresses the issue as follows: It does not perform the
rewrites `SolveEq` and `PlusCombineLikeTerms` if none of the operands
change. This makes the rewrites idempotent. Note however that we are
still not guaranteeing that a term has the same rewritten form
throughout an execution because the node ids may change if the term has
been freed in the meantime. However, this limitation is consistent with
other rewrites such as the reordering of equalities.

I am including the minimized test case from our run on SMT-LIB. I am
ommittin the test case from #3692 because I couldn't trigger it on
master (not surprising since the issue requires very specific
circumstances to actually occur). However, I was able to reproduce the
issue on the CVC4 version mentioned in the issue and confirmed that this
fix worked for that older version.

4 years agoDo not enable unconstrained simplification if arithmetic is present (#4489)
Andrew Reynolds [Tue, 12 May 2020 16:47:47 +0000 (11:47 -0500)]
Do not enable unconstrained simplification if arithmetic is present (#4489)

For now we do not enable unconstrained simplification when arithmetic is present. Post SMT COMP, we should investigate making arithmetic not output lemmas during preprocessing (CVC4/cvc4-wishues#71).

4 years agoUpdate run scripts for SMT-COMP 2020 (#4454)
Andres Noetzli [Wed, 6 May 2020 18:44:34 +0000 (11:44 -0700)]
Update run scripts for SMT-COMP 2020 (#4454)

This commit adds additional options for the model validation track and
makes sure that non-"sat"/"unsat" outputs from the sequential porfolio
approaches are written to a file instead of stderr when running on
StarExec.

4 years agoAlways introduce fresh variable for unconstrained APPLY_UF (#4472)
Andrew Reynolds [Tue, 5 May 2020 21:35:44 +0000 (16:35 -0500)]
Always introduce fresh variable for unconstrained APPLY_UF (#4472)

Fixes an unsoundness in unconstrained simplification, fixes #4469.

4 years agoUpdate copyright year and AUTHORS/THANKS files. (#4468)
Aina Niemetz [Tue, 5 May 2020 19:56:57 +0000 (12:56 -0700)]
Update copyright year and AUTHORS/THANKS files. (#4468)

4 years agoSMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432)
Aina Niemetz [Sat, 2 May 2020 04:18:55 +0000 (21:18 -0700)]
SMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432)

4 years agoMove slow regression to regress3 (#4430)
Andrew Reynolds [Sat, 2 May 2020 03:07:45 +0000 (22:07 -0500)]
Move slow regression to regress3 (#4430)

4 years agoFix regression (#4424)
Andrew Reynolds [Fri, 1 May 2020 00:59:45 +0000 (19:59 -0500)]
Fix regression (#4424)

Fixes regress1.

4 years agoRemove skolem share involving pre_first_ctn. (#4423)
Andrew Reynolds [Thu, 30 Apr 2020 23:48:21 +0000 (18:48 -0500)]
Remove skolem share involving pre_first_ctn. (#4423)

This fixes a soundness issue in strings caused by an incorrect skolem share.

This adds a regression that corresponds to the rewrite that this skolem share was justified by, which is "sat" (the rewrite does not hold). This benchmark in fact was answered "unsat" by CVC4 prior to this PR.

4 years agoDo not mark congruent terms are reduced (#4419)
Andrew Reynolds [Thu, 30 Apr 2020 18:18:26 +0000 (13:18 -0500)]
Do not mark congruent terms are reduced (#4419)

This fixes a potential model soundness issue in strings where a justification for why a string term was reduced relied on a circular argument. The issue involved "reduced by congruence" which states that when f(a) = f(b) ^ a = b in the current context, then one of f(a) or f(b) can be ignored.

However, it may be the case that a is an extended function whose reduction relies on f(b). If we were to assume that f(b) can be ignored due to f(a), then our reduction of f(a) is circular: the reduction of f(a) in the context where a=b relies on itself.

This was causing an incorrect model for QF_S/2020-sygus-qgen/queries/query3214.smt2. The sequence of dependencies was:

[1] (str.contains (str.substr x 1 (+ (- 1) (str.len x))) "CA")
is congruent to
(str.contains (str.substr x (+ 2 (str.indexof x "CA" 1)) (+ (- 2) (str.len x) (* (- 1) (str.indexof x "CA" 1)))) "CA")
in the current context since they are equal and their arguments are equal.

[2] (str.substr x (+ 2 (str.indexof x "CA" 1)) (+ (- 2) (str.len x) (* (- 1) (str.indexof x "CA" 1))))
reduction relies on the length constraint:
(= (str.indexof x "CA" 1) (+ (- 2) (str.len sspre_66)))

[3] (str.indexof x "CA" 1)
reduction relies on:
(not (str.contains (str.substr x 1 (+ (- 1) (str.len x))) "CA"))
which was marked congruent above.
The benchmark now solves in 5 minutes 30 seconds (sat, with a correct model):

andrew@andrew-Latitude-7480:~/misc/strings$ time ajr-cvc4 query3214.smt2 --strings-exp --rewrite-divk --check-models --dump-models
sat
(model
(define-fun x () String "QACOACA")
)

4 years agoSMT-COMP 2020: Fix scripts to use --no-type-checking instead of --no-checking. (...
Aina Niemetz [Wed, 29 Apr 2020 20:14:46 +0000 (13:14 -0700)]
SMT-COMP 2020: Fix scripts to use --no-type-checking instead of --no-checking. (#4417)

4 years agoAvoid circular dependencies for justifying reductions in strings extf eval (#4415)
Andrew Reynolds [Wed, 29 Apr 2020 18:02:02 +0000 (13:02 -0500)]
Avoid circular dependencies for justifying reductions in strings extf eval (#4415)

An incorrect answer of "sat" could be found after 8 seconds on the given benchmark (with --strings-fmf) due to a circular justification for why an extended function was reduced. In particular, we ran checkExtfInference on the same term twice and then marked it as reduced since we had already seen it. This makes the code more conservative.

Notice I'm making the code doubly conservative in case there is any chance for duplication again (e.g. if ExtTheory provides duplicate terms).

4 years agoFix strings 2.6 regression (#4413)
Andrew Reynolds [Wed, 29 Apr 2020 17:00:19 +0000 (12:00 -0500)]
Fix strings 2.6 regression (#4413)

Fixes nightlies.

4 years agoRegister lower bound for str.to_int (#4408)
Andres Noetzli [Tue, 28 Apr 2020 20:10:16 +0000 (13:10 -0700)]
Register lower bound for str.to_int (#4408)

This commit changes the term registration for str.to_int terms. Before, we were not sending out any lemmas when registering str.to_int terms. Now, we send a simple lemma that asserts that the value is greater or equal to negative one.

4 years agoUpdates to SMT COMP script for 20 minute timeout (#4406)
Andrew Reynolds [Tue, 28 Apr 2020 19:37:51 +0000 (14:37 -0500)]
Updates to SMT COMP script for 20 minute timeout (#4406)

Changes run script to be consistent for 20 minute timeout. This divides most of the previous time allocation by 2, with a few exceptions (for non-linear).

It adds a configuration involving --no-arith-brab to QF_NIA and reallocates some time.

4 years agoupdate Haniel's affiliation (#4404)
Haniel Barbosa [Tue, 28 Apr 2020 19:02:06 +0000 (16:02 -0300)]
update Haniel's affiliation (#4404)

4 years agocontrib/get-gmp: Rename and update install instructions with a warning. (#4407)
Aina Niemetz [Tue, 28 Apr 2020 17:43:48 +0000 (10:43 -0700)]
contrib/get-gmp: Rename and update install instructions with a warning. (#4407)

4 years agoSupport the SMT-LIB Unicode string standard by default (#4378)
Andrew Reynolds [Tue, 28 Apr 2020 16:15:00 +0000 (11:15 -0500)]
Support the SMT-LIB Unicode string standard by default (#4378)

This PR merges --lang=smt2.6.1 and --lang=smt2.6 (default). It makes it so that 2.6 always expects the syntax of the string standard http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

I've updated the regressions so that the 2.6 benchmarks are now compliant with the standard. Some of the <=2.5 benchmarks I've updated to 2.6. Others I have left for now, in particular the ones that rely on special characters or ad-hoc escape sequences. The old formats will be supported in the release but removed shortly afterwards.

This PR is a prerequisite for the release, but not necessarily SMT-COMP (which will use --lang=smt2.6.1 if needed). Notice that we still do not have parsing support for str.replace_re or str.replace_re_all. This is required to be fully compliant.

4 years agoUpdate cardinality in strings to unicode standard (#4402)
Andrew Reynolds [Tue, 28 Apr 2020 13:07:54 +0000 (08:07 -0500)]
Update cardinality in strings to unicode standard (#4402)

This updates the default cardinality in strings to match the Unicode standard, 196608.

This avoids a check-model failure from 25 benchmarks in SMT-LIB, which were related to a split due to insufficient constants being required during collectModelInfo.

This also makes a few places throw an AlwaysAssert(false) that otherwise would lead to incorrect models. These regardless should never throw, but it would be better to have an assertion failure.

4 years agoFix sygus unit (#4371)
Andrew Reynolds [Mon, 27 Apr 2020 22:04:49 +0000 (17:04 -0500)]
Fix sygus unit (#4371)

4 years agoFix examples instructions in INSTALL.md. (#4397)
Mathias Preiner [Mon, 27 Apr 2020 20:42:28 +0000 (13:42 -0700)]
Fix examples instructions in INSTALL.md. (#4397)

4 years ago Fix sets cardinality cycle rule (#4392)
Andrew Reynolds [Sun, 26 Apr 2020 05:05:28 +0000 (00:05 -0500)]
 Fix sets cardinality cycle rule (#4392)

Fixes #4391.

The sets cardinality cycle rule is analogous to the S-Cycle rule for strings (see Liang et al CAV 2014). This rule is typically never applied but can be applied in rare cases where theory combination does not determine a correct arrangement of equalities over sets terms that is consistent with the arithmetic arrangement of their cardinalities at full effort. Notice the regression from #4391 has non-linear arithmetic, (mod 0 d), which is translated to UF.

The cardinality cycle rule had a bug: it assumed that cycles that were encountered were loops e1 = e2 = ... = e1 but in general they can be lassos e1 = ... = e2 = ... = e2. This ensures the Venn region cycle e2 = ... = e2 is the conclusion in this case, instead of unsoundly concluding e1 = ... = e2.

Strings does not have a similar issue:
https://github.com/CVC4/CVC4/blob/master/src/theory/strings/core_solver.cpp#L488
Here, when a cycle is encountered, it is processed at the point in traversal where the loop is closed.

This is not critical for SMT-COMP but should be in the 1.8 release.

4 years agoIntroduce best content heuristic for strings (#4382)
Andres Noetzli [Thu, 23 Apr 2020 12:58:00 +0000 (05:58 -0700)]
Introduce best content heuristic for strings (#4382)

* Introduce best content heuristic for strings

This commit introduces a "best content heuristic" to perform
context-dependent simplifications. The high-level idea is that for each
equivalence class for strings, we compute a representation that is a
string concatentation of constants and other string terms. For this
representation, we try to get as many letters in the string constants as
we can (i.e. the best approximation of the content). This "best content"
representation is then used by `EXTF_EVAL` to perform simplifications.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
4 years agoStrings: Register skolems before sending lemma (#4381)
Andres Noetzli [Thu, 23 Apr 2020 00:55:33 +0000 (17:55 -0700)]
Strings: Register skolems before sending lemma (#4381)

This commit fixes a performance regression introduced by commit 6255c03. The issue seems to be that registering terms manually after sending the lemma on the output channel is too late because the output channel processes the lemma eagerly.

4 years agoEnsure disequality splits are processed as lemmas (#4380)
Andrew Reynolds [Wed, 22 Apr 2020 18:32:20 +0000 (13:32 -0500)]
Ensure disequality splits are processed as lemmas (#4380)

Fixes #4379. This was caused by a splitting lemma rewriting to a conjunction, being processed as a fact, and having a pending phase requirement sent out assuming the inference was to be processed as a lemma. This forces 2 of the splits in the core solver to be always processed as lemmas.

4 years agoAllow eager bitblasting with solve bv as int in QF_NIA (#4373)
Andrew Reynolds [Wed, 22 Apr 2020 13:45:52 +0000 (08:45 -0500)]
Allow eager bitblasting with solve bv as int in QF_NIA (#4373)

This also updates the SMT COMP script to revert to our previous behavior.

This is required for SMT COMP. It should be beneficial for satisfiable QF_NIA instances. I will revisit/test this independently.

4 years agoConvert V2.5 SMT regressions to V2.6. (#4319)
Abdalrhman Mohamed [Wed, 22 Apr 2020 12:06:24 +0000 (07:06 -0500)]
Convert V2.5 SMT regressions to V2.6. (#4319)

This commit converts all v2.5 smt2 regressions to v2.6 (except for regress/regress0/lang_opts_2_5.smt2).

4 years agoReinstantiate support for conjunctions in facts (#4377)
Andres Noetzli [Wed, 22 Apr 2020 11:32:06 +0000 (04:32 -0700)]
Reinstantiate support for conjunctions in facts (#4377)

Fixes #4376. Commit 6255c0356bd78140a9cf075491c1d4608ac27704 removed
support for conjunctions in the conclusion of facts. However,
`F_ENDPOINT_EMP` generates a conjunction in the conclusion of the
inference if multiple components are inferred to be empty. This commit
reinstantiates support for conjunctions in the conclusion of facts.

4 years agoUpdate to sygus version 2 (#4372)
Andrew Reynolds [Tue, 21 Apr 2020 18:40:02 +0000 (13:40 -0500)]
Update to sygus version 2 (#4372)

4 years agoFix for parse options related to binary name (#4368)
Andrew Reynolds [Tue, 21 Apr 2020 05:33:50 +0000 (00:33 -0500)]
Fix for parse options related to binary name (#4368)

Possible fix for the nightlies.

In some configurations, a unit test fails when using the function for parsing options via manual argv construction
https://github.com/CVC4/CVC4/blob/master/test/unit/expr/expr_public.h#L58

This reverts a behavior change from 3dfb48b.
In particular, we always parse and ignore the binary name instead of skipping it outright. This more accurately reflects the original code.

4 years agoIntroduce a public interface for Sygus commands. (#4204)
Abdalrhman Mohamed [Tue, 21 Apr 2020 03:07:42 +0000 (22:07 -0500)]
Introduce a public interface for Sygus commands. (#4204)

This commit addresses issue #38 in cvc4-projects by introducing public API for Sygus commands. It also includes two simple examples of how to use the API.

4 years agoMake option names related to CEGQI consistent (#4316)
Andrew Reynolds [Tue, 21 Apr 2020 00:47:35 +0000 (19:47 -0500)]
Make option names related to CEGQI consistent (#4316)

This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.

Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.

The changes were done by these commands in the given directories:

src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done

And a few minor fixes afterwards.

This should be merged close to the time of the next stable release.

4 years agoRefactor inference manager in strings to be amenable to proofs (#4363)
Andrew Reynolds [Mon, 20 Apr 2020 20:16:18 +0000 (15:16 -0500)]
Refactor inference manager in strings to be amenable to proofs (#4363)

This is a key refactoring towards proofs for strings.

This ensures that InferInfo is maintained until just before facts, lemmas and conflicts are processed. This allows us both to:
(1) track more accurate stats and debug information,
(2) have enough information to ensure that proofs can be constructed at the moment facts, lemmas, and conflicts are processed.

Changes in this PR:

PendingInfer and InferInfo were merged, CoreInferInfo is now the previous equivalent of InferInfo, extended with core-solver-specific information, which is only used by CoreSolver.
sendInference( const InferInfo& info, ... ) is now the central method for sending inferences which is called by the other variants, not the other way around.
sendLemma is inlined into sendInference(...) for clarity.
doPendingLemmas and doPendingFacts are extended to process the side effects of the inference infos.
There is actually a further issue with pending inferences related to eagerly processing the side effect of CoreInferInfo before we know the lemma is sent. I believe this issue does not occur in practice based on our strategy. Further refactoring could tighten this, e.g. virtual void InferInfo::processSideEffect. I will do this in another PR.

Further refactoring can address whether asLemma should be a field of InferInfo (it probably should), and whether we should explicitly check for AND in conclusions instead of making it the responsibility of the user of this class.

4 years agoAdd SCOPE proof rule (#4332)
Andrew Reynolds [Mon, 20 Apr 2020 19:53:07 +0000 (14:53 -0500)]
Add SCOPE proof rule (#4332)

This rule is dual to ASSUME. It is a way of closing free assumptions to conclude an implication.

It also changes getId -> getRule.

4 years agoDisable unsat cores on nec regression (#4330)
Andrew Reynolds [Sun, 19 Apr 2020 00:48:04 +0000 (19:48 -0500)]
Disable unsat cores on nec regression (#4330)

Should fix the nightlies.

4 years agoTrack inference id for pending facts in strings (#4331)
Andrew Reynolds [Sat, 18 Apr 2020 22:47:31 +0000 (17:47 -0500)]
Track inference id for pending facts in strings (#4331)

This improves our tracking of pending inferences in strings so that we record pending inferences as a triple (id, fact, exp). This will ensure that proof steps can be constructed at the time we decide to process facts. It also inlines the sendInfer method into sendInference for simplicity.

This also improves the policy for reference counting facts and their explanations: we add them to d_keep when they are added to the equality engine. Previously, we were adding them when they were registered as pending. This means we would collect facts in this pending set that were added but later abandoned, which is unnecessary.

4 years agoImproving EqProof printing (#4329)
Haniel Barbosa [Sat, 18 Apr 2020 12:22:37 +0000 (09:22 -0300)]
Improving EqProof printing (#4329)

4 years agoAdd (context-dependent) Proof (#4323)
Andrew Reynolds [Fri, 17 Apr 2020 16:57:07 +0000 (11:57 -0500)]
Add (context-dependent) Proof (#4323)

A (context-dependent) collection of proof steps that are linked to together to form a ProofNode dag.

Note that the name "Proof" is currently taken. I am calling this class "CDProof", although it is optionally context dependent.

4 years agoantlr: Use relative path in ANTLR script. (#4324)
Mathias Preiner [Fri, 17 Apr 2020 05:50:05 +0000 (22:50 -0700)]
antlr: Use relative path in ANTLR script. (#4324)

This will fix the CI caching issues we sometimes encountered on GH actions.

4 years agoSyGuS instantiation quantifiers module (#3910)
Mathias Preiner [Fri, 17 Apr 2020 02:31:42 +0000 (19:31 -0700)]
SyGuS instantiation quantifiers module (#3910)

4 years agoAdd ProofNodeManager and ProofChecker (#4317)
Andrew Reynolds [Thu, 16 Apr 2020 21:00:25 +0000 (16:00 -0500)]
Add ProofNodeManager and ProofChecker (#4317)

Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure.

ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker).

ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker.

This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.

4 years agoEliminate remaining references to parent TheoryStrings object (#4315)
Andrew Reynolds [Thu, 16 Apr 2020 14:50:43 +0000 (09:50 -0500)]
Eliminate remaining references to parent TheoryStrings object (#4315)

This PR makes it so that the module dependencies in the theory of strings are acyclic. This is important for further organization towards proofs for strings.

The main change in this PR is to ensure that InferenceManager has a pointer to ExtTheory, which is needed for several of its methods. This required changing several solvers into unique_ptr to properly initialize.

4 years agoAdd ProofNode data structure (#4311)
Andrew Reynolds [Wed, 15 Apr 2020 22:09:40 +0000 (17:09 -0500)]
Add ProofNode data structure (#4311)

This is the core data structure for proofs in the new proofs infrastructure. PfRule is a global enumeration of ids of proof nodes (analogous to Kind for Nodes).

4 years agoMove regular expression inclusion test to RegExpEntail (#4310)
Andrew Reynolds [Wed, 15 Apr 2020 14:00:47 +0000 (09:00 -0500)]
Move regular expression inclusion test to RegExpEntail (#4310)

In preparation for rephrasing this inference as a rewrite.

4 years agoChange option names --default-dag-thresh and --default-expr-depth (#4309)
Andrew Reynolds [Wed, 15 Apr 2020 13:37:46 +0000 (08:37 -0500)]
Change option names --default-dag-thresh and --default-expr-depth (#4309)

4 years agoSplit TermRegistry object from TheoryStrings (#4312)
Andrew Reynolds [Wed, 15 Apr 2020 13:23:27 +0000 (08:23 -0500)]
Split TermRegistry object from TheoryStrings (#4312)

This consolidates functionalities from TheoryStrings and InferenceManager related to registering terms, including sending "preregistration lemmas" for them. The main purpose of this PR is to detangle this module from InferenceManager so that these two modules have exactly one call to OutputChannel::lemma each.

For the purposes of the theory solvers, TermRegistry contains the official SkolemCache of TheoryStrings, and can be seen as subsuming the previous interface for this class.

This PR is needed for further progress on strings proofs, marking as major since this will be a blocker shortly for this project.

A few things were cleaned in this PR. One function changed name InferenceManager::registerTerm --> TermRegistry::getRegisterTermLemma. No major behavior changes.

4 years agoDo not mark string extended functions as eliminated after reduction lemmas (#4306)
Andrew Reynolds [Wed, 15 Apr 2020 12:55:41 +0000 (07:55 -0500)]
Do not mark string extended functions as eliminated after reduction lemmas (#4306)

The current policy marked extended functions in strings as "reduced" (eliminated) when we generated their reduction lemma. The upside is that the solver can effectively ignore them. The downside is that we cannot do context-dependent simplification on them, and hence we miss out conflicts during the remainder of the check-sat call.

This changes the policy so they are not marked as reduced. Instead, reduction lemmas are cached in the standard way while allowing context-dependent simplification.

4 years agoFix assertion in enumerative instantiation (#4313)
Andrew Reynolds [Wed, 15 Apr 2020 08:02:50 +0000 (03:02 -0500)]
Fix assertion in enumerative instantiation (#4313)

Fixes regress1.

4 years agoConvert more cases of strings to words (#4206)
Andrew Reynolds [Wed, 15 Apr 2020 07:34:33 +0000 (02:34 -0500)]
Convert more cases of strings to words (#4206)

4 years agoAbort if in conflict in enumerative instantiation (#4298)
Andrew Reynolds [Wed, 15 Apr 2020 06:28:18 +0000 (01:28 -0500)]
Abort if in conflict in enumerative instantiation (#4298)

In very rare cases, quantifiers engine can be the first to detect a quantifier-free conflict while constructing term indices. When this occurs, instantiation modules can quit immediately. This was not happening in a case of enumerative instantiation.

Fixes #4293.

4 years agoAlways flush lemmas from downwards closure in sets (#4297)
Andrew Reynolds [Wed, 15 Apr 2020 05:52:33 +0000 (00:52 -0500)]
Always flush lemmas from downwards closure in sets (#4297)

Fixes #4283.

This also makes a few minor improvements to how lemmas are sent in sets. In particular, lemmas are not sent if we are already in conflict.

4 years agoDo not normalize to representatives for variable equalities in conflict-based instant...
Andrew Reynolds [Wed, 15 Apr 2020 05:15:10 +0000 (00:15 -0500)]
Do not normalize to representatives for variable equalities in conflict-based instantiation (#4280)

Conflict-based instantiation would sometimes initialize a match x -> getRepresentative(t) when a quantified formula contained x = t. This leads to issues where getRepresentative(t) is an illegal term (say, in combination with CEGQI). This makes it so the representative is accessed when necessary instead of being set as part of the match.

Fixes #4275.

4 years agoAlways assign function values in higher order (#4279)
Andrew Reynolds [Wed, 15 Apr 2020 03:02:31 +0000 (22:02 -0500)]
Always assign function values in higher order (#4279)

Fixes #4277.

4 years agoFix combinations of cegqi and non-standard triggers (#4271)
Andrew Reynolds [Wed, 15 Apr 2020 02:28:57 +0000 (21:28 -0500)]
Fix combinations of cegqi and non-standard triggers (#4271)

Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic.

Fixes #4250, fixes #4254, fixes #4269 and fixes #4281.

4 years agoDisable preregistration of instantiations for cegqi in incremental (#4251)
Andrew Reynolds [Wed, 15 Apr 2020 01:54:54 +0000 (20:54 -0500)]
Disable preregistration of instantiations for cegqi in incremental (#4251)

Fixes #4243.

4 years agoDisable macros when higher-order (#4266)
Andrew Reynolds [Tue, 14 Apr 2020 23:19:06 +0000 (18:19 -0500)]
Disable macros when higher-order (#4266)

Fixes #4160.

4 years agoFix relevant domain computation for nested quantifiers coming from CEGQI (#4235)
Andrew Reynolds [Tue, 14 Apr 2020 21:27:29 +0000 (16:27 -0500)]
Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)

Fixes #4228. That benchmark now times out.

4 years agoRemove a few options (#4295)
Andrew Reynolds [Tue, 14 Apr 2020 20:27:33 +0000 (15:27 -0500)]
Remove a few options (#4295)

These options are not robust and are not used.

Fixes #4282 and fixes #4291.

4 years agoRemove a few spurious assertions (#4294)
Andrew Reynolds [Tue, 14 Apr 2020 19:38:01 +0000 (14:38 -0500)]
Remove a few spurious assertions (#4294)

Fixes #4290 and fixes #4292.