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

Commit graph

  • 7043386915 enabled extensional arrays in duality and added theory axioms lazily in GreedyReduce Ken McMillan 2013-12-10 14:34:14 -08:00
  • 56b3406ee5 added mbqi.id option, working on quantifiers in duality Ken McMillan 2013-12-10 11:41:25 -08:00
  • 26bf64a0c3 debug pb Nikolaj Bjorner 2013-12-09 19:58:34 -08:00
  • fbf834f4c4 debugging pb Nikolaj Bjorner 2013-12-09 15:48:58 -08:00
  • d1e86f1d42 adding validation code for assignment Nikolaj Bjorner 2013-12-09 15:48:15 -08:00
  • ec84d69206 investigating conflict resolution bug Nikolaj Bjorner 2013-12-08 21:40:53 -08:00
  • 0f0397b05f hunt bugs exposed by so.smt2 Nikolaj Bjorner 2013-12-08 18:58:48 -08:00
  • 97b2fc9ee7 fix bugs exposed by testSolver Nikolaj Bjorner 2013-12-08 18:34:28 -08:00
  • 5566965a5a fix bug exposed from relevancy Nikolaj Bjorner 2013-12-08 18:19:10 -08:00
  • f0ef339623 fix bug exposed by lia2maxsmt4 Nikolaj Bjorner 2013-12-08 12:30:52 -08:00
  • ddb30c51b5 debugging lia2maxsat Nikolaj Bjorner 2013-12-08 12:17:33 -08:00
  • 370a4b66de update lower bounds from feasible solutiosn Nikolaj Bjorner 2013-12-07 22:09:57 -08:00
  • e307c5fdda fix minimize->maxsat Nikolaj Bjorner 2013-12-07 14:47:47 -08:00
  • da348fe1c0 first pass on normalization Nikolaj Bjorner 2013-12-07 14:38:09 -08:00
  • 6300d82224 fix release build break Nikolaj Bjorner 2013-12-07 08:07:02 -08:00
  • a617eac010 enable bounding for various domains Nikolaj Bjorner 2013-12-06 19:36:12 -08:00
  • 437a545c3b fix pretty printer Nikolaj Bjorner 2013-12-06 13:12:35 -08:00
  • 4d6aa1a0f3 add to_string and get_help methods to optimize API Nikolaj Bjorner 2013-12-06 11:34:41 -08:00
  • 7884b2ab31 make lia2card general purpose functions visible Nikolaj Bjorner 2013-12-06 11:00:49 -08:00
  • d38e2b9b78 Expose objective indices to .NET API Anh-Dung Phan 2013-12-05 17:30:40 -08:00
  • 5fc429c501 debugging network simplex Nikolaj Bjorner 2013-12-05 16:31:29 -08:00
  • 192ce11ca6 change model binding time Nikolaj Bjorner 2013-12-05 11:42:04 -08:00
  • a533527004 exception message clarity fix Christoph M. Wintersteiger 2013-12-05 12:45:14 +00:00
  • 56c4fa8f6d expose models, working on network flow Nikolaj Bjorner 2013-12-04 17:39:54 -08:00
  • 686d146cc6 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt Nikolaj Bjorner 2013-12-04 14:38:24 -08:00
  • a1a8aad09b start working on network flow Nikolaj Bjorner 2013-12-04 14:38:03 -08:00
  • ead414c4ee add back skipped consequences, exposed by fu-malik assertion violation Nikolaj Bjorner 2013-12-04 13:11:58 -08:00
  • b980a15177 fix leak by commenting out probe experiment Nikolaj Bjorner 2013-12-04 13:02:49 -08:00
  • d6f0c13f2a bug fixes exposed from regression tests Nikolaj Bjorner 2013-12-04 08:35:46 -08:00
  • 8fa0d6e4f3 bug fixes exposed from regression tests Nikolaj Bjorner 2013-12-04 08:35:27 -08:00
  • 16ebceb9ff Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api Christoph M. Wintersteiger 2013-12-04 13:50:42 +00:00
  • b9d433e3e5 fix bug in conflict resoltion tracking decision variables Nikolaj Bjorner 2013-12-03 21:10:54 -08:00
  • e3fe80fd4d add .NET interface and finish C interface for optimization Nikolaj Bjorner 2013-12-03 20:20:24 -08:00
  • 9e2908c3f5 exposing lower/upper Nikolaj Bjorner 2013-12-03 17:46:52 -08:00
  • 4719aa11bb backfilling API functions Nikolaj Bjorner 2013-12-03 17:00:34 -08:00
  • 222d4a8f01 add sketch of C-based API Nikolaj Bjorner 2013-12-03 14:47:59 -08:00
  • 838a32206c adjust parsing Nikolaj Bjorner 2013-12-03 14:10:07 -08:00
  • 18815e3e53 reorganizing input Nikolaj Bjorner 2013-12-03 13:36:25 -08:00
  • 51704b7b95 tweaking input processing Nikolaj Bjorner 2013-12-03 08:51:46 -08:00
  • 03f5020d0b Nits Nikolaj Bjorner 2013-12-02 22:06:15 -08:00
  • af5d989d6c change verbosity level Nikolaj Bjorner 2013-12-02 21:51:20 -08:00
  • c14c778735 debugging multi-objective interface and pb revisions Nikolaj Bjorner 2013-12-02 14:30:17 -08:00
  • faa59ba7f9 debugging multi-objective interface and pb revisions Nikolaj Bjorner 2013-12-02 14:14:44 -08:00
  • 191efbb72f use expression structure for objectives instead of custom s-expression Nikolaj Bjorner 2013-12-02 13:00:51 -08:00
  • a016caa5d8 add expression conversion Nikolaj Bjorner 2013-12-02 09:47:59 -08:00
  • a3462ba6aa working on duality Ken McMillan 2013-11-27 17:39:49 -08:00
  • 5ed8a48ac2 Add push/pop to box optimization Anh-Dung Phan 2013-11-26 14:16:59 -08:00
  • 4aa9c742ab Revise optimize commands Anh-Dung Phan 2013-11-26 12:54:18 -08:00
  • dbc791d385 Reorganize combination of objectives Anh-Dung Phan 2013-11-26 09:20:11 +01:00
  • 87a2b99091 Clean up Anh-Dung Phan 2013-11-25 12:16:34 -08:00
  • 8fe50ff2d9 Display diff logic optimization and min cost flow in smt2 format Anh-Dung Phan 2013-11-25 02:15:21 +01:00
  • fff3a1aae5 Normalize diff logic's optimal assignments Anh-Dung Phan 2013-11-25 00:30:15 +01:00
  • cc3d65e544 Add facilities to get optimal assignments Anh-Dung Phan 2013-11-24 22:31:52 +01:00
  • 2ff51e9a60 move model_evaluator from pdr to model, call it model_implicant Nikolaj Bjorner 2013-11-23 21:33:35 +01:00
  • b35088f7e5 Update diff logic optimization Anh-Dung Phan 2013-11-22 18:15:34 -08:00
  • 37f5628824 Update basic spanning tree to be on par with threaded one Anh-Dung Phan 2013-11-22 13:44:12 -08:00
  • 7bc7a61a40 Debug undirected dfs and bfs Anh-Dung Phan 2013-11-22 08:58:17 +01:00
  • 3b2dd47cd4 Refactor pivot rules Anh-Dung Phan 2013-11-21 19:05:17 -08:00
  • a93f8b04e5 working on duality and quantified arithmetic in interpolation Ken McMillan 2013-11-21 18:10:21 -08:00
  • 97dfb6d521 moving to rational coefficients Nikolaj Bjorner 2013-11-21 15:55:08 -08:00
  • e44db06bb7 update conflict resolution Nikolaj Bjorner 2013-11-20 16:14:29 -08:00
  • 61385c8489 a.ctx -> self.ctx, thanks gario Nikolaj Bjorner 2013-11-20 09:54:37 -08:00
  • 33895d522b fix and enable learning Nikolaj Bjorner 2013-11-19 20:47:16 -08:00
  • 696db3a6a4 debug conflict Nikolaj Bjorner 2013-11-19 17:25:19 -08:00
  • 96921355cc pb solver Nikolaj Bjorner 2013-11-19 00:54:30 -08:00
  • 1a8ff9cea4 working on pb Nikolaj Bjorner 2013-11-18 22:41:06 -08:00
  • efecb9b6c0 working on pb Nikolaj Bjorner 2013-11-18 21:51:56 -08:00
  • 475072f5da remove theory_card Nikolaj Bjorner 2013-11-18 21:27:36 -08:00
  • 0ff1b63307 remove theory_card Nikolaj Bjorner 2013-11-18 21:26:23 -08:00
  • ee0abfbfe9 rename card->pb Nikolaj Bjorner 2013-11-18 21:25:02 -08:00
  • 2b2d0e155c debugged new pb solver Nikolaj Bjorner 2013-11-18 18:03:49 -08:00
  • 86e22c1186 add validation option Nikolaj Bjorner 2013-11-18 09:44:20 -08:00
  • c42f0d60e6 pb solver Nikolaj Bjorner 2013-11-18 05:10:30 -08:00
  • 9734bab205 pb theory Nikolaj Bjorner 2013-11-17 21:10:15 -08:00
  • 50cc852112 working on pb Nikolaj Bjorner 2013-11-17 20:15:24 -08:00
  • 8cb959127f pb theory Nikolaj Bjorner 2013-11-17 10:41:15 -08:00
  • f3721e5a15 pb theory Nikolaj Bjorner 2013-11-17 10:39:33 -08:00
  • f6c5088cc9 pb theory Nikolaj Bjorner 2013-11-16 21:05:33 -08:00
  • 77cdb2bcde working on pb solver Nikolaj Bjorner 2013-11-16 17:01:43 -08:00
  • 06073db413 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt Nikolaj Bjorner 2013-11-16 10:14:52 -08:00
  • 41efa8a75d Merge branch 'opt' of https://git00.codeplex.com/z3 into opt Nikolaj Bjorner 2013-11-16 10:14:29 -08:00
  • aadfe007c1 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt Anh-Dung Phan 2013-11-15 18:34:12 -08:00
  • 6ddc838628 Add a basic spanning tree Anh-Dung Phan 2013-11-15 18:34:05 -08:00
  • 6da4bae840 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt Nikolaj Bjorner 2013-11-15 17:31:39 -08:00
  • 13c97d12a8 snapshot Nikolaj Bjorner 2013-11-15 17:31:31 -08:00
  • af8da013b5 Fix a few issues related to thread spanning tree Anh-Dung Phan 2013-11-15 17:17:20 -08:00
  • 761c95129b Merge branch 'opt' of https://git01.codeplex.com/z3 into opt Anh-Dung Phan 2013-11-15 16:59:01 -08:00
  • c837f62863 Use quick explain for unsat core in Fu Malik algorithm by default Anh-Dung Phan 2013-11-15 16:58:42 -08:00
  • 314f03c12c started new PB solver Nikolaj Bjorner 2013-11-15 16:44:08 -08:00
  • 074e851d49 Display Fu Malik statistics Anh-Dung Phan 2013-11-15 12:58:11 -08:00
  • 8320144af0 fixed bug in duality logging Ken McMillan 2013-11-15 11:24:02 -08:00
  • 31495bb9d9 bugfix for float rounding to integral values for cases where ebits >= sbits Christoph M. Wintersteiger 2013-11-15 17:19:41 +00:00
  • f9164f4cb1 local updates Nikolaj Bjorner 2013-11-14 20:21:33 -08:00
  • 0acf331ed1 Merge conflicts Anh-Dung Phan 2013-11-14 19:07:23 -08:00
  • 4be11f24e1 Instrument fu_malik to use the new SAT solver (WIP) Anh-Dung Phan 2013-11-14 19:02:15 -08:00
  • e034331f2e working on pb solver Nikolaj Bjorner 2013-11-14 18:04:55 -08:00
  • 06ae0db116 working on pb solver Nikolaj Bjorner 2013-11-14 18:04:05 -08:00
  • d729e89a7b Fix a minor bug on cardinality solver Anh-Dung Phan 2013-11-14 12:36:39 -08:00
  • c96f7b5a51 bugfixes for float to float conversion Christoph M. Wintersteiger 2013-11-14 20:13:37 +00:00
  • b77d408128 bugfix for FPA rounding when ebits is very small. Christoph M. Wintersteiger 2013-11-14 19:11:19 +00:00