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.
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.
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.
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.
Andrew Reynolds [Wed, 26 Feb 2020 02:52:10 +0000 (20:52 -0600)]
Embed mkAssociative utilities within the API. (#3801)
Towards parser/API migration.
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).
mudathirmahgoub [Tue, 25 Feb 2020 17:47:24 +0000 (11:47 -0600)]
Sets & Relations Java example (#3816)
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.
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.
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.
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.
Andrew Reynolds [Mon, 24 Feb 2020 21:37:48 +0000 (15:37 -0600)]
Convert parser input interface to api::Term (#3809)
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.
Andrew Reynolds [Mon, 24 Feb 2020 17:35:37 +0000 (11:35 -0600)]
Add missing functions to new C++ API (#3769)
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)`.
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.
Alex Ozdemir [Sat, 22 Feb 2020 18:48:05 +0000 (10:48 -0800)]
RIP th_lra.plf (#3796)
Rest in Peace, old LRA signature.
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.
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.
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.
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.
Aina Niemetz [Fri, 21 Feb 2020 22:20:15 +0000 (14:20 -0800)]
New C++ API: Remove TOTAL kinds. (#3794)
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.
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)
Andrew Reynolds [Fri, 21 Feb 2020 16:55:04 +0000 (10:55 -0600)]
Split extended functions solver in strings (#3768)
Alex Ozdemir [Fri, 21 Feb 2020 15:25:25 +0000 (07:25 -0800)]
Remove IntReal tightening axioms from th_lira.plf (#3787)
Andrew Reynolds [Thu, 20 Feb 2020 20:49:02 +0000 (14:49 -0600)]
Remove front-end support for Chain (#3767)
Andres Noetzli [Thu, 20 Feb 2020 20:07:46 +0000 (12:07 -0800)]
Remove unused code (#3782)
Andrew Reynolds [Thu, 20 Feb 2020 19:07:22 +0000 (13:07 -0600)]
Minor removals (#3786)
Found while working on parser migration of datatypes.
Andres Noetzli [Thu, 20 Feb 2020 17:02:58 +0000 (09:02 -0800)]
Remove parser from bindings (#3779)
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.
Andrew Reynolds [Wed, 19 Feb 2020 23:14:01 +0000 (17:14 -0600)]
Fix symmetry breaking for multiple sygus types (#3775)
makaimann [Wed, 19 Feb 2020 21:54:17 +0000 (13:54 -0800)]
Add Python bindings using Cython -- see below for more details (#2879)
Andrew Reynolds [Wed, 19 Feb 2020 21:15:22 +0000 (15:15 -0600)]
Delay enumerative instantiation if theory engine does not need check (#3774)
Andrew Reynolds [Wed, 19 Feb 2020 20:19:09 +0000 (14:19 -0600)]
Change Record to shared_ptr (#3778)
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>
makaimann [Wed, 19 Feb 2020 04:11:52 +0000 (20:11 -0800)]
Change datatype selector/constructor/tester to terms (#3773)
Andrew Reynolds [Tue, 18 Feb 2020 18:00:14 +0000 (12:00 -0600)]
Add missing kinds for the new API (#3757)
Andrew Reynolds [Mon, 17 Feb 2020 19:29:09 +0000 (13:29 -0600)]
Option to limit the number of rounds of enumerative instantiation (#3760)
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.
Haniel Barbosa [Mon, 17 Feb 2020 16:11:17 +0000 (13:11 -0300)]
Using ParseOp in TPTP (#3764)
Abdalrhman Mohamed [Mon, 17 Feb 2020 14:58:42 +0000 (08:58 -0600)]
Support dumping Sygus commands. (#3763)
Andrew Reynolds [Sun, 16 Feb 2020 22:06:21 +0000 (16:06 -0600)]
Fix simple issue with cache (#3762)
Andrew Reynolds [Sun, 16 Feb 2020 21:47:31 +0000 (15:47 -0600)]
Add temporary global API conversion utilities. (#3759)
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.
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.
Andrew Reynolds [Sat, 15 Feb 2020 22:38:23 +0000 (16:38 -0600)]
Move proxy variables to InferenceManager in strings (#3758)
Andrew Reynolds [Fri, 14 Feb 2020 23:09:59 +0000 (17:09 -0600)]
Remove quantifiers rewrite rules infrastructure (#3754)
Andrew Reynolds [Fri, 14 Feb 2020 05:31:13 +0000 (23:31 -0600)]
Update sygus v1 parser to use ParseOp utility (#3756)
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.
Andrew Reynolds [Thu, 13 Feb 2020 21:22:20 +0000 (15:22 -0600)]
Const input for sygus print callback (#3755)
Andres Noetzli [Thu, 13 Feb 2020 00:16:21 +0000 (16:16 -0800)]
[Python] Properly destroy CVC4 object (#3753)
Andres Noetzli [Wed, 12 Feb 2020 22:48:10 +0000 (14:48 -0800)]
Rename Java package to edu.stanford.CVC4 (#3752)
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)
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.
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>
Mathias Preiner [Tue, 11 Feb 2020 21:26:38 +0000 (13:26 -0800)]
cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)
Andrew Reynolds [Tue, 11 Feb 2020 17:59:58 +0000 (11:59 -0600)]
Fix term simplification based on entailment in quantifiers rewriter (#3746)
Mathias Preiner [Tue, 11 Feb 2020 17:36:01 +0000 (09:36 -0800)]
Update issue templates
Andres Noetzli [Tue, 11 Feb 2020 14:27:29 +0000 (06:27 -0800)]
Remove `--strings-binary-csp` option (#3743)
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.
Andrew Reynolds [Tue, 11 Feb 2020 04:41:18 +0000 (22:41 -0600)]
Use example evaluation cache instead of sygus PBE (#3733)
Alex Ozdemir [Tue, 11 Feb 2020 02:32:20 +0000 (18:32 -0800)]
Implement LFSCArithProof::equalityType. (#3740)
Also, missed an armType use.
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>
Mathias Preiner [Mon, 10 Feb 2020 19:34:11 +0000 (11:34 -0800)]
cmake: Use ld.gold if available for faster link times. (#3738)
Alex Ozdemir [Mon, 10 Feb 2020 18:50:28 +0000 (10:50 -0800)]
Add more IntReal predicates (#3731)
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.
Andres Noetzli [Sat, 8 Feb 2020 06:31:08 +0000 (22:31 -0800)]
Make "unknown" non-critical for unsat cores check (#3728)
Andrew Reynolds [Sat, 8 Feb 2020 05:16:12 +0000 (23:16 -0600)]
Split strings finite model finding strategy (#3727)
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.
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.
mudathirmahgoub [Fri, 7 Feb 2020 23:49:58 +0000 (17:49 -0600)]
Univeset Cardinality constraints for infinite types (#3712)
Andrew Reynolds [Fri, 7 Feb 2020 20:47:46 +0000 (14:47 -0600)]
Refactor check-model handling in SmtEngine (#3723)
Alex Ozdemir [Fri, 7 Feb 2020 18:37:33 +0000 (10:37 -0800)]
Propagate expected types through UF arguments (#3717)
Alex Ozdemir [Fri, 7 Feb 2020 17:08:09 +0000 (09:08 -0800)]
Add `ArithProof::{printInteger,getLfscFunction}` (#3716)
Andrew Reynolds [Fri, 7 Feb 2020 16:41:09 +0000 (10:41 -0600)]
Statistics for fast enumerator (#3699)
Andrew Reynolds [Fri, 7 Feb 2020 16:23:47 +0000 (10:23 -0600)]
Example evaluation cache utility (#3698)
Andrew Reynolds [Fri, 7 Feb 2020 01:12:29 +0000 (19:12 -0600)]
Fix exact sqrt (#3721)
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Andrew Reynolds [Thu, 6 Feb 2020 23:30:53 +0000 (17:30 -0600)]
Generalize containsQuantifiers to hasClosure (#3722)
Andrew Reynolds [Wed, 5 Feb 2020 00:27:17 +0000 (18:27 -0600)]
Fix QF_NIA smt comp script (#3715)
mudathirmahgoub [Tue, 4 Feb 2020 18:52:33 +0000 (12:52 -0600)]
Update INSTALL.md (#3714)
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Alex Ozdemir [Tue, 4 Feb 2020 18:31:03 +0000 (10:31 -0800)]
Articulate proof-related debug statements in arith (#3700)
Aina Niemetz [Tue, 4 Feb 2020 16:21:24 +0000 (08:21 -0800)]
--fp-exp: Better warning message. (#3709)
Mathias Preiner [Tue, 4 Feb 2020 15:49:31 +0000 (07:49 -0800)]
Fix header installation on MacOS. (#3660)
On MacOS sed -i requires a suffix to be set.
Andrew Reynolds [Tue, 4 Feb 2020 15:31:22 +0000 (09:31 -0600)]
Split base solver from the theory of strings (#3680)
Andres Noetzli [Tue, 4 Feb 2020 14:31:29 +0000 (06:31 -0800)]
Revert semantic change from refactoring (#3711)
Alex Ozdemir [Tue, 4 Feb 2020 06:42:27 +0000 (22:42 -0800)]
Regression tests for arithmetic proofs. (#3701)
* Add more arith proof regression tests
These tests are designed to test interesting cases of arithmetic proofs,
such as mixing integers and reals and tightening bounds.
Right now, they have the --no-check-proofs flag set, which prevents them
from testing the proof machinery. However, once we check that machinery
into master, we'll remove that flag, thus enabling the full effect of
the tests.
* A few comments explaining things.
* Add another tightening test
* Add new test to CMake
* No --no-check-models. There are no models anyway.
* Delete smt-lib-version, per Yoni
Aina Niemetz [Tue, 4 Feb 2020 00:42:31 +0000 (16:42 -0800)]
Increase regression test time limit to 1200s. (#3704)
Fixes #3565.
Clark Barrett [Mon, 3 Feb 2020 23:18:22 +0000 (15:18 -0800)]
Fix corner case - might need to REWRITE_AGAIN (#3706)
Andrew Reynolds [Mon, 3 Feb 2020 22:57:54 +0000 (16:57 -0600)]
Utility function for getting component types (#3703)
Andrew Reynolds [Mon, 3 Feb 2020 21:05:45 +0000 (15:05 -0600)]
Minor fixes to regressions (#3702)
Fixes two issues in regressions, fixes regress1.
mudathirmahgoub [Mon, 3 Feb 2020 18:44:34 +0000 (12:44 -0600)]
Fix cardinality of uninterpreted types when univset is not used (#3663)
* Fixed bug 3662
* format
* small change
* added bug3663.smt2 file
* throw Logic Exception
* throw Logic Exception
* ;EXIT: 1
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Andrew Reynolds [Mon, 3 Feb 2020 18:23:27 +0000 (12:23 -0600)]
Split on model values when repaired model from non-linear is inconsisent (#3668)
Andrew Reynolds [Mon, 3 Feb 2020 16:19:44 +0000 (10:19 -0600)]
Fix invariant template inference for trivially infeasible conjecture (#3693)
Andrew Reynolds [Mon, 3 Feb 2020 15:31:36 +0000 (09:31 -0600)]
Fix corner case of empty domains in bounded fmf (#3690)
Andrew Reynolds [Mon, 3 Feb 2020 14:51:26 +0000 (08:51 -0600)]
Example inference utility (#3670)
Andrew V. Jones [Mon, 3 Feb 2020 07:16:20 +0000 (07:16 +0000)]
Renaming '--bsd' to '--no-gpl' (#3609)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Alex Ozdemir [Sat, 1 Feb 2020 07:44:24 +0000 (23:44 -0800)]
Handle `expectedType` in TheoryProofEngine (#3691)
`TheoryProofEngine` now uses the `expectedType` optional argument.
* When printing terms, it sets this for theories that it dispatches too
* It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
* It is mindful of `expectedType` when using the let map.
I also moved to hpp function implementations into the cpp.
Andrew Reynolds [Fri, 31 Jan 2020 19:42:36 +0000 (13:42 -0600)]
Allow PBE symmetry breaking with sygus stream (#3686)
Andrew Reynolds [Fri, 31 Jan 2020 17:06:41 +0000 (11:06 -0600)]
Refactor relevance vectors for asserted quantifiers (#3666)