3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-17 19:09:54 +00:00

Commit graph

  • df35da1acf rule_manager::mk(): default initialization of m_proof to null Nuno Lopes 2013-03-25 10:48:48 -07:00
  • b427958b9e qe_lite> fix crash in is_var_eq() (by me & Nikolaj) Nuno Lopes 2013-03-25 09:53:11 -07:00
  • b1fc6a5cac Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-03-24 18:26:48 -07:00
  • bbe93ef610 fix build warning, make context simplifier traverse subterms Nikolaj Bjorner 2013-03-24 18:26:22 -07:00
  • def69e2521 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2013-03-24 14:59:38 -07:00
  • a71bb549c6 Add option :bv-sort-ac true Leonardo de Moura 2013-03-24 14:59:29 -07:00
  • e61fa50dc3 fix build breaks Nikolaj Bjorner 2013-03-24 11:26:46 -07:00
  • ee5d61bd60 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-03-24 11:26:07 -07:00
  • 6084cbd065 fix build breaks Nikolaj Bjorner 2013-03-24 11:25:43 -07:00
  • 9d0b0df985 Fix gcc compilation errors Leonardo de Moura 2013-03-24 09:07:51 -07:00
  • 5aa84c28a6 Remove trace msg Leonardo de Moura 2013-03-24 09:00:19 -07:00
  • 2633dc56ab Fix non ASCII character Leonardo de Moura 2013-03-24 08:59:43 -07:00
  • 7c3ca302f0 missing hnf Nikolaj Bjorner 2013-03-23 16:56:47 -07:00
  • fb5d2cae17 local changes Nikolaj Bjorner 2013-03-23 16:44:07 -07:00
  • 26f4d3be20 significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations Nikolaj Bjorner 2013-03-23 14:11:54 -07:00
  • e73c06a8b0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-03-23 13:57:12 -07:00
  • 7e0723e42b add unit test for previous commit Nuno Lopes 2013-03-22 11:51:28 -07:00
  • c824178e7e bit_vector: fix operator==() for the case that num_bits is a multiple of 32 Nuno Lopes 2013-03-22 11:50:41 -07:00
  • 54d9fb5c4b Revert "fix crash in qe_lite::is_var_eq" unknown 2013-03-22 01:25:22 +01:00
  • 7b148a73a2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-03-21 17:15:36 -07:00
  • b2d4aa0859 fix crash in qe_lite::is_var_eq unknown 2013-03-22 01:14:08 +01:00
  • 39d7246251 fix overloading of complement from base_table Nuno Lopes 2013-03-20 15:47:56 -07:00
  • ab761c4c32 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nuno Lopes 2013-03-20 10:41:06 -07:00
  • ea2b17d83b remove debug code Nuno Lopes 2013-03-20 10:40:52 -07:00
  • babfc701a6 make model and proof converters a reference Nikolaj Bjorner 2013-03-20 10:36:36 -07:00
  • 5455704af2 move quantifier hoist routines to quant_hoist Nikolaj Bjorner 2013-03-19 15:00:23 -07:00
  • b0787024c7 Move ast_counter to location for common utilities. It depends on get_free_vars, so is in rewriter directory Nikolaj Bjorner 2013-03-19 09:47:52 -07:00
  • b8b73077a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-03-18 21:46:48 -07:00
  • 7e9f4e264d working on separating horn simplificaiton Nikolaj Bjorner 2013-03-18 21:46:42 -07:00
  • d4d3ba104e fix compiler warning for unused variable Nikolaj Bjorner 2013-03-18 21:41:00 -07:00
  • d1ffeb36b0 fix warning messages for unused variables Nikolaj Bjorner 2013-03-18 21:37:44 -07:00
  • b8598225bf fix definition of bit_vector::empty() Nuno Lopes 2013-03-18 09:20:25 -07:00
  • fed2ad2300 Fix nontermination bug Leonardo de Moura 2013-02-05 09:44:41 -08:00
  • 39b9da7118 Fix bug in smt_model_finder, it was producing the incorrect instantiation set. Leonardo de Moura 2013-03-13 19:02:48 -07:00
  • 21f69c2b3a Java API build bugfix. Thanks to Fabian Emmes for reporting this. Christoph M. Wintersteiger 2013-03-12 12:27:08 +00:00
  • 4b973e115f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Christoph M. Wintersteiger 2013-03-11 14:31:33 +00:00
  • ab73c20757 add Karr linear invariants as transformer Nikolaj Bjorner 2013-03-10 17:53:18 -07:00
  • a9c7517275 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Christoph M. Wintersteiger 2013-03-08 13:22:06 +00:00
  • 2b93537366 debugging interpolation Ken McMillan 2013-03-06 18:26:46 -08:00
  • 3810374cdd LRA Nikolaj Bjorner 2013-03-06 15:20:11 -08:00
  • 37a75622a9 LRA tactic Nikolaj Bjorner 2013-03-06 08:32:21 -08:00
  • f9aeeeef36 LRA tactic Nikolaj Bjorner 2013-03-06 08:29:29 -08:00
  • e5307300de FPA: bugfixes in mul() and abs() Christoph M. Wintersteiger 2013-03-06 15:04:58 +00:00
  • ae9276ad9b more work on interpolation Ken McMillan 2013-03-05 21:56:09 -08:00
  • bdc675b1df Fix bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 Leonardo de Moura 2013-03-05 09:04:03 -08:00
  • 9a4331995e FPA: bugfix for bitblaster. Christoph M. Wintersteiger 2013-03-05 14:11:50 +00:00
  • 35906889b6 FPA: compilation bugfixes Christoph M. Wintersteiger 2013-03-05 13:49:42 +00:00
  • d66211c007 working on interpolation API Kenneth McMillan 2013-03-04 23:48:01 -08:00
  • bc6b20d557 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp Kenneth McMillan 2013-03-04 19:53:53 -08:00
  • 12d2d3beef minor fixes for OSX Kenneth McMillan 2013-03-04 19:53:46 -08:00
  • 9792f6dd33 more work on incorporating iz3 Ken McMillan 2013-03-04 18:41:30 -08:00
  • e5f03f999a FPA: Added conversion operator float -> float. Christoph M. Wintersteiger 2013-03-04 20:21:14 +00:00
  • e5f5e008aa fixing file heads to match z3 Kenneth McMillan 2013-03-03 21:22:50 -08:00
  • 68fb01c206 initial commit for interpolation Ken McMillan 2013-03-03 20:45:58 -08:00
  • 197b2e8ddb fix bugs reported by Arie Gurfinkel Nikolaj Bjorner 2013-03-03 13:55:41 -08:00
  • 523dc0fb36 add slicing Nikolaj Bjorner 2013-03-02 21:24:21 -08:00
  • 352912c6b5 add default simplifications as tactic Nikolaj Bjorner 2013-03-02 21:06:13 -08:00
  • ed846a9ff3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-03-02 21:03:15 -08:00
  • 6c3e2e6764 add default simplifications as tactic Nikolaj Bjorner 2013-03-02 21:03:08 -08:00
  • 7822b86b53 FPA: multiple bugfixes for HWF, MPF and a bugfix for FPA2BV (many thanks to Gabriele Paganelli) Christoph M. Wintersteiger 2013-03-01 19:06:01 +00:00
  • 6f3850bfbc FPA bug and leak fixes (thanks to Gabriele Paganelli) Christoph M. Wintersteiger 2013-02-28 18:46:29 +00:00
  • 75eca46d93 added Karr test Nikolaj Bjorner 2013-02-27 17:32:27 -08:00
  • 5d2d89a85c Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-02-26 19:15:04 -08:00
  • 2a75f1d71e update logging for hilbert Nikolaj Bjorner 2013-02-26 19:14:52 -08:00
  • 5598f334d4 optimizations to Hilbert basis Nikolaj Bjorner 2013-02-26 17:01:49 -08:00
  • e8140f5c1f Fix compilation problems when using Visual Studio 32 bit compiler Leonardo de Moura 2013-02-26 12:34:52 -08:00
  • 5fe58c2f2d Java API: renamed assert_(...) to add(...) .NET API: added alias Add(...) for Assert(...) Christoph M. Wintersteiger 2013-02-26 19:13:48 +00:00
  • b2810592e6 Add enumeration_sort method to C++ API. Add as_expr method to goal class in C++ API. Add enum_sort_example to C++ examples/c++/example.cpp Leonardo de Moura 2013-02-26 08:29:01 -08:00
  • 14f582eca5 Java API: added automatic detection of jar Christoph M. Wintersteiger 2013-02-25 16:03:57 +00:00
  • f5cdc14737 Java API: build system bugfixes Christoph M. Wintersteiger 2013-02-25 15:44:54 +00:00
  • ffb1fc37df Java API: New JDK detection routines. Christoph M. Wintersteiger 2013-02-25 15:37:33 +00:00
  • e0c73d9bc1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-02-24 21:52:38 -08:00
  • 562ae7bec5 faster saturation without backwards subsumption and using SOS-style set Nikolaj Bjorner 2013-02-24 21:52:10 -08:00
  • 3d4a42c270 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2013-02-21 11:02:21 -08:00
  • 4922d62311 Fix bug reported at http://z3.codeplex.com/workitem/23 Leonardo de Moura 2013-02-21 11:02:13 -08:00
  • 2c6c09301f Java API: build system bugfixes. Christoph M. Wintersteiger 2013-02-21 16:46:18 +00:00
  • 876c6a361e Java API: build system fix for OSX Christoph M. Wintersteiger 2013-02-21 16:40:10 +00:00
  • 70192b66e9 Remove dead files Leonardo de Moura 2013-02-20 17:03:29 -08:00
  • fa298fc7f6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2013-02-20 13:41:16 -08:00
  • 97bf9418f7 Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream. Leonardo de Moura 2013-02-20 13:41:08 -08:00
  • 6075ae28fc ML/Java: Proper use of Datatype API for List/Enum/Constructor Christoph M. Wintersteiger 2013-02-20 19:40:48 +00:00
  • b4d57e0ab1 Merge branch 'unstable' into contrib Leonardo de Moura 2013-02-19 15:35:05 -08:00
  • 18bae81731 Java Example: build fix Christoph M. Wintersteiger 2013-02-19 22:48:41 +00:00
  • 0f9f01a321 Fix for G++. Christoph M. Wintersteiger 2013-02-19 22:08:44 +00:00
  • 0aa8df98a1 optimizing hilbert basis Nikolaj Bjorner 2013-02-18 18:58:43 -08:00
  • 306855ba55 fix hilbert_basis tests and add heap_trie index Nikolaj Bjorner 2013-02-16 22:45:37 -08:00
  • 47342e5d0c move validation code to unit test Nikolaj Bjorner 2013-02-15 17:46:22 -08:00
  • f46c7f9bd9 Fix the build on g++, Fix g++ warnings Leonardo de Moura 2013-02-15 16:36:57 -08:00
  • 4a97e6daea Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2013-02-15 16:32:30 -08:00
  • 0af4384882 Fix more issues unintepreted sort tests. Leonardo de Moura 2013-02-15 16:31:42 -08:00
  • 943e142bfa Fix bug in ast_smt_pp.cpp. After user_sort_plugin was introduced, it is not that case that if a sort is uninterpreted, then sort->get_family_id() == null_family_id. Leonardo de Moura 2013-02-15 16:27:55 -08:00
  • a242ac46b6 hilbert validation Nikolaj Bjorner 2013-02-15 15:05:39 -08:00
  • aaf0c16e08 working on hilbert basis Nikolaj Bjorner 2013-02-15 09:09:58 -08:00
  • 3a68affb1b cal modifications Nikolaj Bjorner 2013-02-14 15:10:52 -08:00
  • 784307fc30 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2013-02-14 15:06:25 -08:00
  • 6e7d04f94e working on hilbert basis Nikolaj Bjorner 2013-02-14 15:06:17 -08:00
  • 5e72cf0123 Compress windows distribution zip files Leonardo de Moura 2013-02-14 10:55:43 -08:00
  • 9d45d872a7 Compress Z3 distribution zip files Leonardo de Moura 2013-02-14 10:26:15 -08:00
  • 030aef5d5a Fix bug reported by Andrey Kupriyanov Leonardo de Moura 2013-02-14 09:55:42 -08:00
  • 0c0fe40446 Fix Python 2.6 incompatibility at mk_util.py Leonardo de Moura 2013-02-13 19:03:37 -08:00