| .NET/Java: API doc update for Context constructor. |
|
More...
|
over 12 years ago
|
| fix UTVPI model generation |
|
More...
|
over 12 years ago
|
| fixing parity bug in model generation for UTVPI |
|
More...
|
over 12 years ago
|
| add experimental Horn clause to AIG (AAG format) converter. Clauses should be over booleans only (or bit-blasted with fixedpoint.bit_blast=true). We will crash if that's not the case. Only linear clauses supported for now |
|
More...
|
over 12 years ago
|
| fix typo in my previous commit |
|
More...
|
over 12 years ago
|
| horn clause bit blasting: propagate output predicates for predicates without rules (most likely an UNSAT prog) |
|
More...
|
over 12 years ago
|
| horn rule bit blaster: fix propagation of output predicates when arity == 0 |
|
More...
|
over 12 years ago
|
| minor code simplification |
|
More...
|
over 12 years ago
|
| remove unimplemented method |
|
More...
|
over 12 years ago
|
| relax pre-processing to untangle non-horn formulas, based on Eldarica/linear benchmarks |
|
More...
|
over 12 years ago
|
| add rewriting option to simplify store equalities |
|
More...
|
over 12 years ago
|
| fix parameters in utvpi and make Karr invariants use backward propagation |
|
More...
|
over 12 years ago
|
| fix for compiler weirdness |
|
More...
|
over 12 years ago
|
| Add new C++ APIs for creating forall/exists expressions. |
|
More...
|
over 12 years ago
|
| fixed bug in label output in duality |
|
More...
|
over 12 years ago
|
| added rule names to duality output |
|
More...
|
over 12 years ago
|
| still adding labels to duality |
|
More...
|
over 12 years ago
|
| FPA: bugfix for QFPA -> QBV conversion. |
|
More...
|
over 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
over 12 years ago
|
| FPA: bugfix for quantified FP -> quantified BV conversion. |
|
More...
|
over 12 years ago
|
| Add expr_vector example |
|
More...
|
over 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
over 12 years ago
|
| postpone rule flushing dependent on engine |
|
More...
|
over 12 years ago
|
| working on duality |
|
More...
|
over 12 years ago
|
| adding labels to duality |
|
More...
|
over 12 years ago
|
| FPA: bugfixes for UF in model converter for fpa2bv. |
|
More...
|
over 12 years ago
|
| FPA: Added support for float-UF to BV-UF translation. |
|
More...
|
over 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
over 12 years ago
|
| FPA: added support for rewriting quantified floats to quantified bit-vectors. |
|
More...
|
over 12 years ago
|
| fix build of unit tests |
|
More...
|
over 12 years ago
|
