cvc5.git
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.

4 years agoRemove portfolio leftovers (#3821)
Andres Noetzli [Wed, 26 Feb 2020 08:08:20 +0000 (00:08 -0800)]
Remove portfolio leftovers (#3821)

Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.

4 years agoMinor cleaning of smt2 parser (#3823)
Andrew Reynolds [Wed, 26 Feb 2020 06:40:52 +0000 (00:40 -0600)]
Minor cleaning of smt2 parser (#3823)

Towards parser migration, will make the diff of the eventual conversion a bit smaller.

4 years agoEmbed mkAssociative utilities within the API. (#3801)
Andrew Reynolds [Wed, 26 Feb 2020 02:52:10 +0000 (20:52 -0600)]
Embed mkAssociative utilities within the API. (#3801)

Towards parser/API migration.

4 years agoSets & Relations Java example (#3816)
mudathirmahgoub [Tue, 25 Feb 2020 17:51:10 +0000 (11:51 -0600)]
Sets & Relations Java example (#3816)

Fixes [(Bugzilla #677)](https://github.com/CVC4/cvc4-projects/issues/25).

4 years agoSets & Relations Java example (#3816)
mudathirmahgoub [Tue, 25 Feb 2020 17:47:24 +0000 (11:47 -0600)]
Sets & Relations Java example (#3816)

4 years agoremove redundant includes (#3815)
yoni206 [Tue, 25 Feb 2020 15:23:30 +0000 (07:23 -0800)]
remove redundant includes (#3815)

I came across these two redundant includes in theory_uf.h and removed them.

4 years agobv_to_int preprocessing pass
yoni206 [Tue, 25 Feb 2020 03:58:01 +0000 (19:58 -0800)]
bv_to_int preprocessing pass

Introduces a preprocessing pass that translates bv problems to integer problems.

4 years agoFixes for quantifiers documentation (#3811)
Andrew Reynolds [Mon, 24 Feb 2020 23:28:03 +0000 (17:28 -0600)]
Fixes for quantifiers documentation (#3811)

Minor fixes discovered during development of sygus-inst.

4 years agoUtilities for words (#3797)
Andrew Reynolds [Mon, 24 Feb 2020 22:21:45 +0000 (16:21 -0600)]
Utilities for words (#3797)

This adds a utility file for handling operations over constant "words" (this will eventually generalize string or sequence constants). This is work towards CVC4/cvc4-projects#23.

Also improves documentation in regexp.h.

4 years agoConvert parser input interface to api::Term (#3809)
Andrew Reynolds [Mon, 24 Feb 2020 21:37:48 +0000 (15:37 -0600)]
Convert parser input interface to api::Term (#3809)

4 years agoFix bugs related to printing Sygus commands (#3804)
Abdalrhman Mohamed [Mon, 24 Feb 2020 20:30:02 +0000 (14:30 -0600)]
Fix bugs related to printing Sygus commands (#3804)

With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.

4 years agoAdd missing functions to new C++ API (#3769)
Andrew Reynolds [Mon, 24 Feb 2020 17:35:37 +0000 (11:35 -0600)]
Add missing functions to new C++ API (#3769)

4 years agoMake lambda rewriter more robust (#3806)
Andres Noetzli [Mon, 24 Feb 2020 15:46:47 +0000 (07:46 -0800)]
Make lambda rewriter more robust (#3806)

The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.

4 years agoMinor refactoring of equality notifications (#3798)
Andrew Reynolds [Sun, 23 Feb 2020 05:41:42 +0000 (23:41 -0600)]
Minor refactoring of equality notifications (#3798)

Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.

4 years agoRIP th_lra.plf (#3796)
Alex Ozdemir [Sat, 22 Feb 2020 18:48:05 +0000 (10:48 -0800)]
RIP th_lra.plf (#3796)

Rest in Peace, old LRA signature.

4 years ago Move check memberships to reg exp solver (#3793)
Andrew Reynolds [Sat, 22 Feb 2020 16:07:44 +0000 (10:07 -0600)]
 Move check memberships to reg exp solver (#3793)

There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified.

4 years agoMove cardinality inference scheme to base solver in strings (#3792)
Andrew Reynolds [Sat, 22 Feb 2020 07:05:43 +0000 (01:05 -0600)]
Move cardinality inference scheme to base solver in strings (#3792)

Moves handling of cardinality to the base solver, refactors how cardinality is accessed.

No intended behavior change in this commit.

4 years agoDump boolean propagations and conflicts for decision tree org-mode viewer (#3788)
makaimann [Sat, 22 Feb 2020 06:13:31 +0000 (22:13 -0800)]
Dump boolean propagations and conflicts for decision tree org-mode viewer (#3788)

PR #2871 added trace tags for dumping the decision tree in org-mode format. However, it only dumped theory propagations/conflicts. This could be confusing because it would appear to backtrack without reaching a conflict (but actually the conflict was at the propositional level). This commit also adds dumping of boolean propagations and conflicts.

4 years agoSwitch to th_lira.plf (#3741)
Alex Ozdemir [Sat, 22 Feb 2020 00:16:19 +0000 (16:16 -0800)]
Switch to th_lira.plf (#3741)

Switches arith_proof.cpp from th_lra to th_lira.

Changes:

Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.

4 years agoNew C++ API: Remove TOTAL kinds. (#3794)
Aina Niemetz [Fri, 21 Feb 2020 22:20:15 +0000 (14:20 -0800)]
New C++ API: Remove TOTAL kinds. (#3794)

4 years agoSimple changes towards unicode string standard (#3791)
Andrew Reynolds [Fri, 21 Feb 2020 19:36:01 +0000 (13:36 -0600)]
Simple changes towards unicode string standard (#3791)

This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

The next steps will be to address the more invasive changes required to support the standard.

4 years agoAdding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT...
Andrew V. Jones [Fri, 21 Feb 2020 18:19:45 +0000 (18:19 +0000)]
Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT solver is compiled-in (#3771)

4 years agoSplit extended functions solver in strings (#3768)
Andrew Reynolds [Fri, 21 Feb 2020 16:55:04 +0000 (10:55 -0600)]
Split extended functions solver in strings (#3768)

4 years agoRemove IntReal tightening axioms from th_lira.plf (#3787)
Alex Ozdemir [Fri, 21 Feb 2020 15:25:25 +0000 (07:25 -0800)]
Remove IntReal tightening axioms from th_lira.plf (#3787)

4 years agoRemove front-end support for Chain (#3767)
Andrew Reynolds [Thu, 20 Feb 2020 20:49:02 +0000 (14:49 -0600)]
Remove front-end support for Chain (#3767)

4 years agoRemove unused code (#3782)
Andres Noetzli [Thu, 20 Feb 2020 20:07:46 +0000 (12:07 -0800)]
Remove unused code (#3782)

4 years agoMinor removals (#3786)
Andrew Reynolds [Thu, 20 Feb 2020 19:07:22 +0000 (13:07 -0600)]
Minor removals (#3786)

Found while working on parser migration of datatypes.

4 years agoRemove parser from bindings (#3779)
Andres Noetzli [Thu, 20 Feb 2020 17:02:58 +0000 (09:02 -0800)]
Remove parser from bindings (#3779)

4 years agoresource manager: Add statistic for every resource. (#3772)
Mathias Preiner [Thu, 20 Feb 2020 00:59:58 +0000 (16:59 -0800)]
resource manager: Add statistic for every resource. (#3772)

This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).

Fixes #3751.

4 years agoFix symmetry breaking for multiple sygus types (#3775)
Andrew Reynolds [Wed, 19 Feb 2020 23:14:01 +0000 (17:14 -0600)]
Fix symmetry breaking for multiple sygus types (#3775)

4 years agoAdd Python bindings using Cython -- see below for more details (#2879)
makaimann [Wed, 19 Feb 2020 21:54:17 +0000 (13:54 -0800)]
Add Python bindings using Cython -- see below for more details (#2879)

4 years agoDelay enumerative instantiation if theory engine does not need check (#3774)
Andrew Reynolds [Wed, 19 Feb 2020 21:15:22 +0000 (15:15 -0600)]
Delay enumerative instantiation if theory engine does not need check (#3774)

4 years agoChange Record to shared_ptr (#3778)
Andrew Reynolds [Wed, 19 Feb 2020 20:19:09 +0000 (14:19 -0600)]
Change Record to shared_ptr (#3778)

4 years agoFix approximate bounds for transcendental functions whose model values rewrite (...
Andrew Reynolds [Wed, 19 Feb 2020 07:23:43 +0000 (01:23 -0600)]
Fix approximate bounds for transcendental functions whose model values rewrite (#3747)

* Fix bounds for negative sine apps

* Format

* Comment

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
4 years agoChange datatype selector/constructor/tester to terms (#3773)
makaimann [Wed, 19 Feb 2020 04:11:52 +0000 (20:11 -0800)]
Change datatype selector/constructor/tester to terms (#3773)

4 years agoAdd missing kinds for the new API (#3757)
Andrew Reynolds [Tue, 18 Feb 2020 18:00:14 +0000 (12:00 -0600)]
Add missing kinds for the new API (#3757)

4 years agoOption to limit the number of rounds of enumerative instantiation (#3760)
Andrew Reynolds [Mon, 17 Feb 2020 19:29:09 +0000 (13:29 -0600)]
Option to limit the number of rounds of enumerative instantiation (#3760)

4 years ago Fix soundness bug in reduction of integer div/mod (#3766)
Andrew Reynolds [Mon, 17 Feb 2020 17:17:02 +0000 (11:17 -0600)]
 Fix soundness bug in reduction of integer div/mod (#3766)

This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec4101f190b8f1fa21c30752.

This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not.

Fixes #3765.

Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.

4 years agoUsing ParseOp in TPTP (#3764)
Haniel Barbosa [Mon, 17 Feb 2020 16:11:17 +0000 (13:11 -0300)]
Using ParseOp in TPTP (#3764)

4 years agoSupport dumping Sygus commands. (#3763)
Abdalrhman Mohamed [Mon, 17 Feb 2020 14:58:42 +0000 (08:58 -0600)]
Support dumping Sygus commands. (#3763)

4 years agoFix simple issue with cache (#3762)
Andrew Reynolds [Sun, 16 Feb 2020 22:06:21 +0000 (16:06 -0600)]
Fix simple issue with cache (#3762)

4 years agoAdd temporary global API conversion utilities. (#3759)
Andrew Reynolds [Sun, 16 Feb 2020 21:47:31 +0000 (15:47 -0600)]
Add temporary global API conversion utilities. (#3759)

4 years agoActivate reverse variant of F-Split inference (#3745)
Andres Noetzli [Sun, 16 Feb 2020 18:09:31 +0000 (10:09 -0800)]
Activate reverse variant of F-Split inference (#3745)

This commit activates the reverse variant of the F-Split inference.

4 years agoDisable regression (#3761)
Andrew Reynolds [Sun, 16 Feb 2020 03:39:06 +0000 (21:39 -0600)]
Disable regression (#3761)

Should fix recurring issue with nightlies.

Also fixes a warning.

4 years agoMove proxy variables to InferenceManager in strings (#3758)
Andrew Reynolds [Sat, 15 Feb 2020 22:38:23 +0000 (16:38 -0600)]
Move proxy variables to InferenceManager in strings (#3758)

4 years agoRemove quantifiers rewrite rules infrastructure (#3754)
Andrew Reynolds [Fri, 14 Feb 2020 23:09:59 +0000 (17:09 -0600)]
Remove quantifiers rewrite rules infrastructure (#3754)

4 years agoUpdate sygus v1 parser to use ParseOp utility (#3756)
Andrew Reynolds [Fri, 14 Feb 2020 05:31:13 +0000 (23:31 -0600)]
Update sygus v1 parser to use ParseOp utility (#3756)

4 years agoForcing rewrite pass rather than asserting if formula has been rewritten (#3748)
Haniel Barbosa [Fri, 14 Feb 2020 03:50:00 +0000 (00:50 -0300)]
Forcing rewrite pass rather than asserting if formula has been rewritten (#3748)

This ensures that users or developers don't accidentally break the solver either via options or changing the SMT engine flow so that the formula is not rewritten up to a given point.

4 years agoConst input for sygus print callback (#3755)
Andrew Reynolds [Thu, 13 Feb 2020 21:22:20 +0000 (15:22 -0600)]
Const input for sygus print callback (#3755)

4 years ago[Python] Properly destroy CVC4 object (#3753)
Andres Noetzli [Thu, 13 Feb 2020 00:16:21 +0000 (16:16 -0800)]
[Python] Properly destroy CVC4 object (#3753)

4 years agoRename Java package to edu.stanford.CVC4 (#3752)
Andres Noetzli [Wed, 12 Feb 2020 22:48:10 +0000 (14:48 -0800)]
Rename Java package to edu.stanford.CVC4 (#3752)

4 years agoEnsure ext rewrites for associative ops dont throw assertions for kind arities (...
Andrew Reynolds [Wed, 12 Feb 2020 22:24:13 +0000 (16:24 -0600)]
Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681)

4 years agorun_regression: Distinguish between timeout and failure. (#3750)
Mathias Preiner [Wed, 12 Feb 2020 07:33:21 +0000 (23:33 -0800)]
run_regression: Distinguish between timeout and failure. (#3750)

If --use-skip-return-code is enabled and a regression test times out it
will return EXIT_SKIP instead of EXIT_FAILURE.

4 years agoFix non-linear equality solving that involves mixed real/integer arithmetic (#3739)
Andrew Reynolds [Wed, 12 Feb 2020 00:20:25 +0000 (18:20 -0600)]
Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)

* Fix non-linear equality solving that involves mixed real/integer.

* Format

* Fix

* Revert

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
4 years agocmake: Remove unused ENABLE_OPTIMIZED option. (#3749)
Mathias Preiner [Tue, 11 Feb 2020 21:26:38 +0000 (13:26 -0800)]
cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)

4 years agoFix term simplification based on entailment in quantifiers rewriter (#3746)
Andrew Reynolds [Tue, 11 Feb 2020 17:59:58 +0000 (11:59 -0600)]
Fix term simplification based on entailment in quantifiers rewriter (#3746)

4 years agoUpdate issue templates
Mathias Preiner [Tue, 11 Feb 2020 17:36:01 +0000 (09:36 -0800)]
Update issue templates

4 years agoRemove `--strings-binary-csp` option (#3743)
Andres Noetzli [Tue, 11 Feb 2020 14:27:29 +0000 (06:27 -0800)]
Remove `--strings-binary-csp` option (#3743)

4 years agoRefactor `CoreSolver::processSimpleNEq()` (#3736)
Andres Noetzli [Tue, 11 Feb 2020 07:51:34 +0000 (23:51 -0800)]
Refactor `CoreSolver::processSimpleNEq()` (#3736)

This commit refactors and documents `CoreSolver::processSimpleNEq()`.
This method processes equalities between normal forms.

4 years agoUse example evaluation cache instead of sygus PBE (#3733)
Andrew Reynolds [Tue, 11 Feb 2020 04:41:18 +0000 (22:41 -0600)]
Use example evaluation cache instead of sygus PBE  (#3733)

4 years agoImplement LFSCArithProof::equalityType. (#3740)
Alex Ozdemir [Tue, 11 Feb 2020 02:32:20 +0000 (18:32 -0800)]
Implement LFSCArithProof::equalityType. (#3740)

Also, missed an armType use.

4 years agoAdd function for tightening literals (#3732)
Alex Ozdemir [Mon, 10 Feb 2020 21:53:54 +0000 (13:53 -0800)]
Add function for tightening literals (#3732)

* Add function for tightening literals

The function tightens a literal if it can be tightened, and prints a
proof of the result.

* Include a #include

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
4 years agocmake: Use ld.gold if available for faster link times. (#3738)
Mathias Preiner [Mon, 10 Feb 2020 19:34:11 +0000 (11:34 -0800)]
cmake: Use ld.gold if available for faster link times. (#3738)

4 years agoAdd more IntReal predicates (#3731)
Alex Ozdemir [Mon, 10 Feb 2020 18:50:28 +0000 (10:50 -0800)]
Add more IntReal predicates (#3731)

4 years agoFix rewrite rules sat regressions (#3734)
Andrew Reynolds [Sat, 8 Feb 2020 23:08:13 +0000 (17:08 -0600)]
Fix rewrite rules sat regressions (#3734)

Quantifier rewrite rules are not robust to preprocessing within our check-model infrastructure. This disables check-model on 2 satisfiable rewrite rules regressions. Fixes nightlies.

4 years agoMake "unknown" non-critical for unsat cores check (#3728)
Andres Noetzli [Sat, 8 Feb 2020 06:31:08 +0000 (22:31 -0800)]
Make "unknown" non-critical for unsat cores check (#3728)

4 years agoSplit strings finite model finding strategy (#3727)
Andrew Reynolds [Sat, 8 Feb 2020 05:16:12 +0000 (23:16 -0600)]
Split strings finite model finding strategy (#3727)

4 years agoSplit core solver from the theory of strings (#3713)
Andrew Reynolds [Sat, 8 Feb 2020 03:35:30 +0000 (21:35 -0600)]
Split core solver from the theory of strings (#3713)

This splits the main procedure from Liang et al CAV 2014 to its own file, the "core solver" of theory of strings.

I have intentionally not updated or clang-formatted the code in core_solver.cpp since I would prefer this PR to involve as little change to behavior as possible (it is copied verbatim from theory_strings.cpp). Future PRs will clean this code up.

4 years agoInterface for example evaluation cache utilities (#3726)
Andrew Reynolds [Sat, 8 Feb 2020 02:54:05 +0000 (20:54 -0600)]
Interface for example evaluation cache utilities (#3726)

This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator.
It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization.  This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators.

The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples.

4 years agoUniveset Cardinality constraints for infinite types (#3712)
mudathirmahgoub [Fri, 7 Feb 2020 23:49:58 +0000 (17:49 -0600)]
Univeset Cardinality constraints for infinite types (#3712)

4 years agoRefactor check-model handling in SmtEngine (#3723)
Andrew Reynolds [Fri, 7 Feb 2020 20:47:46 +0000 (14:47 -0600)]
Refactor check-model handling in SmtEngine (#3723)

4 years agoPropagate expected types through UF arguments (#3717)
Alex Ozdemir [Fri, 7 Feb 2020 18:37:33 +0000 (10:37 -0800)]
Propagate expected types through UF arguments (#3717)

4 years agoAdd `ArithProof::{printInteger,getLfscFunction}` (#3716)
Alex Ozdemir [Fri, 7 Feb 2020 17:08:09 +0000 (09:08 -0800)]
Add `ArithProof::{printInteger,getLfscFunction}` (#3716)

4 years agoStatistics for fast enumerator (#3699)
Andrew Reynolds [Fri, 7 Feb 2020 16:41:09 +0000 (10:41 -0600)]
Statistics for fast enumerator (#3699)