mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
5694 commits 23 branches 48 tags 157 MiB
Commit graph

4647 commits

Author SHA1 Message Date
Murphy Berzish f7ba3ff084 crash avoidance in theory_str search start, fixes length-001.smt2 regression 2016-08-09 20:11:25 -04:00
Murphy Berzish 3dff240bb3 theory_str model validation for Length 2016-08-07 15:50:41 -04:00
Murphy Berzish cb566ad5ce fix model validation for theory_str 2016-08-07 15:43:08 -04:00
Murphy Berzish 395ec4543c avoid crash in theory_str, this leaks memory 2016-08-06 22:19:10 -04:00
Murphy Berzish 43b0cd5010 clean up unused variables in theory_str.cpp 2016-08-06 15:38:58 -04:00
Murphy Berzish 2c91f388df add defensive double-non-concat check in theory_str::simplify_concat_equality() 2016-08-06 15:35:47 -04:00
Murphy Berzish 91c336d7ee fix erroneous vector double-insert in theory_str::group_terms_by_eqc() 2016-08-06 15:32:37 -04:00
Murphy Berzish 0c4e725902 finish theory_str::mk_concat, no caching of generated terms yet 2016-08-04 16:40:05 -04:00
Murphy Berzish bc91d182bf mk_concat fixes WIP 2016-08-03 13:39:14 -04:00
Murphy Berzish 3c2fe497de modify theory_str::get_value() to check EQC for a numeral 
Instead of asking the arithmetic theory for the current assignment,
we return the (unique) numeral in the equivalence class of the term
whose length we want to know.

This is because the arithmetic theory may return a default / internal
value that doesn't correspond to anything actually asserted by the core solver.
 2016-08-02 16:44:54 -04:00
Murphy Berzish 45c4954959 add debugging to theory_str::get_len_value in preparation for fixes 2016-08-02 14:52:44 -04:00
Murphy Berzish a51ad07e3f crash avoidance in propagation of basic string axioms and gen_len_test_options 2016-08-01 20:52:49 -04:00
Murphy Berzish 97f07a8a7c fix debugging statements in theory_str::gen_len_test_options 
this fixes charAt-007.smt2 and prevents two unique crashes
 2016-08-01 18:14:56 -04:00
Murphy Berzish ee1af96f1b add opt_NoQuickReturn_IntegerTheory check in theory_str::new_eq_check() 
This allows us to assert an "inconsistent length" axiom from the integer theory
while continuing in new_eq_handler(). Currently active when
opt_NoQuickReturn_IntegerTheory is 'true' but this may be necessary
here and in other places, in general, to fix integer theory integration.
 2016-08-01 17:05:02 -04:00
Murphy Berzish 6e348720b1 add integer theory integration to theory_str::solve_concat_eq_str case 4 2016-07-31 18:12:57 -04:00
Murphy Berzish 778c0a5563 improve theory_str::group_terms_by_eqc now that we have simplify_concat 2016-07-31 16:55:17 -04:00
Murphy Berzish 9ceb2df28f add integer integration to theory_str::simplify_parent 2016-07-31 16:51:35 -04:00
Murphy Berzish 41497f44c1 prevent checking scope of XOR variables in theory_str::process_concat_eq 2016-07-31 16:30:52 -04:00
Murphy Berzish f5b82740c3 debugging length testers in theory_str::gen_len_val_options_for_free_var 2016-07-31 16:26:56 -04:00
Murphy Berzish 8958eea27c crash avoidance in theory_str cut_var_map writes 2016-07-31 11:22:04 -04:00
Murphy Berzish 7f3a260eda more aggressive simplifications in theory_str::handle equality, WIP, not tested yet 2016-07-30 16:58:59 -04:00
Murphy Berzish 6f67e9cdda fix theory_str::check_length_concat_concat to actually assert the conflict axiom 2016-07-28 17:18:56 -04:00
Murphy Berzish 244b611f1c fix infinite loop bug in theory_str::new_eq_check 2016-07-28 17:10:41 -04:00
Murphy Berzish 999420485b add theory_str::check_length_eq_var_concat and helper methods 2016-07-28 16:49:39 -04:00
Murphy Berzish 76ceac6664 add theory_str::check_length_const_string 2016-07-28 16:31:40 -04:00
Murphy Berzish 95f1cfa5a6 add theory_str::check_length_consistency, WIP 2016-07-27 16:18:05 -04:00
Murphy Berzish a31a948a5b add theory_str::can_concat_eq_concat 2016-07-27 15:21:33 -04:00
Murphy Berzish ceed3f3ff0 add theory_str::can_concat_eq_str 2016-07-27 15:15:01 -04:00
Murphy Berzish 1c518be61d new_eq_handler improvements in theory_str, WIP 2016-07-27 12:46:35 -04:00
Murphy Berzish f555074e27 add option to disable integer theory integration in theory_str; this is currently ENABLED 2016-07-23 23:29:56 -04:00
Murphy Berzish 02a66c425e add option to bypass quick returns in integer theory integration in theory_str 
this might not actually be that useful, if the problem is, as I suspect it to be,
that values we get from the integer theory need not correspond with
assertions in the core (that can get popped off the stack, etc.)
 2016-07-23 22:43:46 -04:00
Murphy Berzish ac16aa7c81 fix out-of-scope variable bug in theory_str::process_concat_eq_type6 
this fix will have to be made to all functions that use varForBreakConcat
 2016-07-23 16:02:11 -04:00
Murphy Berzish 0f38203779 add RegexCharRange to theory_str 2016-07-19 16:39:43 -04:00
Murphy Berzish 9ffcd135d5 add RegexPlus to theory_str 2016-07-19 15:47:41 -04:00
Murphy Berzish 8d47b08244 fix out-of-scope value tester bug in theory_str::gen_free_var_options() 
we now pass tests/z3str/charAt-003.smt2 with detailed debugging turned off!
 2016-07-10 13:05:41 -04:00
Murphy Berzish 8aa6fee0af fixups wip 2016-07-08 12:21:11 -04:00
Murphy Berzish 847a5fc1f8 replace old mk_value behaviour in theory_str that creates placeholders for unused terms instead of crashing 2016-07-07 16:13:48 -04:00
Murphy Berzish 9eead64d03 prevent assertion of basic string axioms on variables that go out of scope (theory_str) 
this is testing a crash avoidance feature, the regression is tests/z3str/regex-026.smt2

this also adds some debugging code for a substr() crash but that is WIP
 2016-07-06 17:31:37 -04:00
Murphy Berzish 7d903ff1fa implement process_concat_eq_unroll, WIP 2016-06-30 04:55:11 -04:00
Murphy Berzish b53da182b6 fix gen_assign_unroll_reg so that it does not assert a contradiction 2016-06-30 04:39:09 -04:00
Murphy Berzish a2d6149df5 add general-case regex unroll model generation 
WIP as there is currently a SAT-as-UNSAT bug I'm trying to fix

This also changes the semantics of lower_bound and upper_bound,
no longer wrapping the expr that is passed in with mk_strlen().
This actually makes these methods useful for checking bounds
of things other than strings.
 2016-06-30 04:00:42 -04:00
Murphy Berzish b4110c886f successful unroll of simple unbounded Str2Reg 2016-06-30 02:46:16 -04:00
Murphy Berzish 427632ede3 let free variable assignment work a bit more towards unrolls 2016-06-30 01:42:00 -04:00
Murphy Berzish 21f0a50aba add Unroll check to get_eqc_allUnroll 2016-06-30 01:24:43 -04:00
Murphy Berzish 03827cb487 add more Unroll support to final_check, ctx_dep_analysis 2016-06-30 01:21:21 -04:00
Murphy Berzish b31d1a92aa add more support for unroll (WIP) 2016-06-27 14:41:57 -04:00
Murphy Berzish 020e8aef6d regex union 2016-06-23 17:14:03 -04:00
Murphy Berzish 04803d7a3b starting regex support 2016-06-23 15:24:35 -04:00
Murphy Berzish 4c34629806 starting regex support, rewriter 2016-06-21 21:13:16 -04:00
Murphy Berzish a808a8c587 theory_str infer_len_concat_arg 2016-06-21 17:38:49 -04:00
Murphy Berzish 1e46782392 theory_str infer_len_concat 2016-06-21 17:25:28 -04:00
Murphy Berzish ba42478f9b string-integer wip 2016-06-20 20:02:22 -04:00
Murphy Berzish 89a337ba7e quick path with string-integer integration in theory_str::simplify_concat_equality 2016-06-19 18:25:31 -04:00
Murphy Berzish 5b3c868c90 theory_str Replace method 2016-06-15 21:14:54 -04:00
Murphy Berzish fb20951064 theory_str Substr support WIP 2016-06-15 20:26:07 -04:00
Murphy Berzish be5bf7fb80 LastIndexof support 2016-06-15 18:45:01 -04:00
Murphy Berzish 7c8b882ae6 decl and rewriter support for LastIndexof in theory_str (WIP) 2016-06-15 18:04:33 -04:00
Murphy Berzish dc5a334d42 support for Indexof2 in theory_str 2016-06-15 17:37:17 -04:00
Murphy Berzish 881e3056f3 support for IndexOf in theory_str 2016-06-14 21:28:31 -04:00
Murphy Berzish db2a5854e9 decl and rewriter for Indexof (WIP) 2016-06-14 20:10:06 -04:00
Murphy Berzish 7aeeb599ef very very basic Contains support in theory_str 
not included: the 1200 lines of code that make it very fast
 2016-06-14 18:43:51 -04:00
Murphy Berzish a3986d6d0e decl and rewriter support for Contains (WIP) 2016-06-14 18:36:43 -04:00
Murphy Berzish 989d6b577b EndsWith axiomatization in theory_str 2016-06-14 18:05:24 -04:00
Murphy Berzish fd38b4c729 EndsWith decl and rewriter, WIP 2016-06-14 17:55:46 -04:00
Murphy Berzish 4f131ebba7 prevent infinite loop of axiom generation. working StartsWith 2016-06-14 16:42:46 -04:00
Murphy Berzish c5ffb012dd axioms for StartsWith; WIP as I need to fix an infinite recursion bug 2016-06-14 16:16:39 -04:00
Murphy Berzish 7d8e54c50f decl and rewriter for string StartsWith 2016-06-13 22:27:46 -04:00
Murphy Berzish be5cc02a45 working axiomatization for CharAt 2016-06-13 21:57:08 -04:00
Murphy Berzish 389845180c add CharAt to theory_str and basic rewrite rule for constant CharAt exprs 2016-06-13 16:34:24 -04:00
Murphy Berzish 7d09dbb8ec basic infrastructure for string rewriting 2016-06-12 20:46:52 -04:00
Murphy Berzish 18cd47dcd0 add flag for bailing out during a final check infinite loop in theory_str 
also adds more debugging to free variable gen
 2016-06-12 20:14:57 -04:00
Murphy Berzish 08328c5614 add option in theory_str to assert string constant lengths more eagerly 
now passes z3str/concat-025
 2016-06-12 17:16:14 -04:00
Murphy Berzish fd968783a5 fix model generation for theory_str 2016-06-09 20:35:26 -04:00
Murphy Berzish 1520760a04 string-integer integration in free var gen 2016-06-09 20:31:21 -04:00
Murphy Berzish 91d82956b2 string concat-eq type 3 integer integration 2016-06-09 16:25:19 -04:00
Murphy Berzish 6f5ee2c3ce string concat-eq type 2 integer integration 2016-06-09 16:04:13 -04:00
Murphy Berzish ae74b47924 string concat-eq type 1 integer integration 2016-06-09 15:41:31 -04:00
Murphy Berzish 6332372573 more debugging info in theory_str final check; fix variable classification bug 2016-06-08 20:01:56 -04:00
Murphy Berzish bd2b014008 debugging information for dependence analysis 2016-06-08 19:32:25 -04:00
Murphy Berzish 04fe8f66df concat-eq-concat type 1 split 0 2016-06-08 16:22:31 -04:00
Murphy Berzish 513b4922ee tracing code for string-integer integration 2016-06-07 17:40:59 -04:00
Murphy Berzish 62aeff90c5 fix string theory setup so that string-integer integration actually works 2016-06-07 17:38:57 -04:00
Murphy Berzish e0df5bc2ed fixups for string-integer 2016-06-04 16:29:10 -04:00
Murphy Berzish 33205cea71 completely bypass theory_seq; sorry! I'll put it back when I'm done 2016-06-01 17:57:00 -04:00
Murphy Berzish b5fe473c3a fix compilation errors after merge 2016-06-01 17:50:45 -04:00
Murphy Berzish d79837eed0 Merge branch 'develop' into upstream-master 
Conflicts:
	.gitignore
	README
	src/ast/ast_smt2_pp.h
	src/ast/ast_smt_pp.cpp
	src/ast/reg_decl_plugins.cpp
	src/cmd_context/cmd_context.cpp
	src/parsers/smt2/smt2parser.cpp
 2016-06-01 17:40:52 -04:00
Murphy Berzish bc79a73779 lower/upper bound WIP 2016-06-01 17:23:47 -04:00
Murphy Berzish f8f7014a18 use LRA instead of LIA in strings setup, so that the theory_seq integer value code works 2016-06-01 16:34:48 -04:00
Christoph M. Wintersteiger ade2dbe15a Cache cleanup fix for bv_simplifier_plugin. 
Fixes #615
 2016-05-31 16:47:14 +01:00
Christoph M. Wintersteiger 47e75827ee theory_fpa refactoring 2016-05-31 16:22:48 +01:00
Christoph M. Wintersteiger 302c491535 theory_fpa refactoring 2016-05-31 16:22:24 +01:00
Christoph M. Wintersteiger 03f6b465b9 comment typos 2016-05-31 16:14:50 +01:00
Nikolaj Bjorner 39acd3594a test variants for seq_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-30 18:15:10 -07:00
Nikolaj Bjorner f03032bd09 updated seq solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-29 14:01:05 -07:00
Nikolaj Bjorner cddf8091b5 strengthen support for int.to.str and length reasoning. Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 12:36:50 -07:00
Nikolaj Bjorner c3f498a640 strengthen support for int.to.str and length reasoning. Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 12:26:47 -07:00
Nikolaj Bjorner 8c99d3c431 tidy unbound compressor code, add invariant checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 11:05:26 -07:00
Nikolaj Bjorner 3aea63edb1 check for cancellation before internalizing and during to avoid errors. Issue #625 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 17:27:37 -07:00
Nikolaj Bjorner 236f1c2a3e bypass stale rules as part of unbounded compression. Issue #624 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 10:31:28 -07:00
Nikolaj Bjorner 18a9b89e30 bypass stale rules as part of unbounded compression. Issue #624 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 09:38:23 -07:00
Nikolaj Bjorner 50d334e4e9 fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed. reported in issue #619 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 07:51:02 -07:00
Nikolaj Bjorner cfffb0b3c5 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-27 07:49:45 -07:00
Nikolaj Bjorner 84ff6fd62a fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 07:49:38 -07:00
Christoph M. Wintersteiger 18340b0e95 fix for pb2bv_model_converter 2016-05-26 18:42:57 +01:00
Christoph M. Wintersteiger 1fe4a82c76 Added implementation of pb2bv_model_converter::translate 
Fixes #623
 2016-05-26 18:39:51 +01:00
Christoph M. Wintersteiger ec270acd32 Removed hwf.mul/hwf.div test code. 2016-05-26 15:11:21 +01:00
Christoph M. Wintersteiger 9752888704 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-26 15:06:02 +01:00
Christoph M. Wintersteiger e28929c72c Removed hwf.rem test code. 2016-05-26 15:05:55 +01:00
Nikolaj Bjorner cdf3c2571c Merge pull request #622 from dstaple/master 
Export default tactic for use via the SMT-LIB 2 interface.
 2016-05-26 06:47:27 -07:00
Christoph M. Wintersteiger 4b00ea69db refcount fix for theory_fpa 2016-05-26 14:01:06 +01:00
Douglas B. Staple 725b1c56e5 Export default tactic for use via the SMT-LIB 2 interface. 2016-05-26 09:55:08 -03:00
Christoph M. Wintersteiger 15d871cfe0 Bug and style fix for fpa2bv converter. 2016-05-26 13:39:54 +01:00
Nikolaj Bjorner b8716b3339 avoid use-before-def crashes fp-operations.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:32:39 -07:00
Nikolaj Bjorner dfbbea31b7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-25 14:23:17 -07:00
Nikolaj Bjorner a07381ac19 fix regression in evaluator exposed by build failure on fp-array-6.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:23:07 -07:00
Christoph M. Wintersteiger 04a68bbb0a Eliminated a number of potential memory leaks in fpa2bv code. 
Relates to #615
 2016-05-25 18:50:57 +01:00
Christoph M. Wintersteiger f1c915bcf1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-25 18:21:14 +01:00
Christoph M. Wintersteiger ce69072305 Made nra tactic public. 2016-05-25 18:21:04 +01:00
Nikolaj Bjorner cd441c318e add compare utility to compress common cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 09:03:24 -07:00
Nikolaj Bjorner af3cc7e578 tune array evaluation, still disabled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 08:57:59 -07:00
Christoph M. Wintersteiger c4610e0423 renamed variable to avoid clashes 2016-05-24 14:37:43 +01:00
Christoph M. Wintersteiger 9717161bb8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-24 10:58:23 +01:00
Nikolaj Bjorner c20b391cf7 reduce warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-23 14:32:51 -07:00
Christoph M. Wintersteiger 617e941015 fp2bv refactoring 2016-05-23 18:10:17 +01:00
Christoph M. Wintersteiger 8370bb8986 removed unused variable 2016-05-23 16:31:57 +01:00
Christoph M. Wintersteiger bf3a5effbc Fixed and refactored fp.min/fp.max for theory_fpa. 
Fixes #616
 2016-05-23 15:38:25 +01:00
Christoph M. Wintersteiger 184aebab59 variable naming 2016-05-23 15:08:27 +01:00
Nikolaj Bjorner cb6d008da8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-22 17:03:37 -07:00
Nikolaj Bjorner c725fe7698 tune lra optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-22 17:03:29 -07:00
Christoph M. Wintersteiger 218e47f34b Removed unused variable 2016-05-22 18:21:28 +01:00
Christoph M. Wintersteiger d4bc8ebb70 FP to BV translation of UFs refactored. 2016-05-22 18:16:57 +01:00
Christoph M. Wintersteiger 8db17311ae fpa2bv build fixes 2016-05-22 13:13:32 +01:00
Christoph M. Wintersteiger fe3f8466b6 Partial support for fpa2bv translation in complex types. 2016-05-21 18:08:48 +01:00
Christoph M. Wintersteiger b6d90a64da fpa rewriter tidy up 2016-05-21 18:07:37 +01:00
Christoph M. Wintersteiger 8001b1f0c7 typo 2016-05-21 17:43:17 +01:00
Christoph M. Wintersteiger c77941ce54 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-21 12:19:09 +01:00
Christoph M. Wintersteiger 9a10d2dcee bugfix for fpa2bv model converter 2016-05-21 12:19:03 +01:00
Nikolaj Bjorner 927d714d7b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-20 13:46:00 -07:00
Nikolaj Bjorner 339cd6e537 mbo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-20 13:45:50 -07:00
Murphy Berzish ecb069b701 non-fixes to string length code, plus the get_length() code from new Z3 2016-05-20 16:34:11 -04:00
Christoph M. Wintersteiger 2bbca192e3 member init order 2016-05-20 20:16:45 +01:00
Christoph M. Wintersteiger 4ed2b8a0f9 Bugfix for unspecified FP model values. 2016-05-20 20:15:08 +01:00
Christoph M. Wintersteiger cae53c3ec2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-20 19:55:01 +01:00
Christoph M. Wintersteiger 1cc8146aba Bugfixes for FP UFs and arrays. 2016-05-20 19:53:57 +01:00
Christoph M. Wintersteiger 80731ef364 Exposed OP_FPA_MIN/MAX_I to the API 2016-05-20 19:40:45 +01:00
Murphy Berzish 2522e35c5e start work on string-integer integration 2016-05-20 10:22:19 -04:00
Murphy Berzish 2f494a9611 fix null parent bug by making a copy of n_eq_enode->m_parents in simplify_parent 2016-05-19 16:57:01 -04:00
Murphy Berzish c8522c5b78 cleanup before attempting to fix the null enode parent bug 2016-05-19 16:51:43 -04:00
Nikolaj Bjorner d12efb6097 remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:10:43 -07:00
Nikolaj Bjorner 1aa3fdab8a remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:04:20 -07:00