3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
z3/src/muz/base
Nikolaj Bjorner 2115111dac update display method for datalog to use predicates, throttle use of extensionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-28 20:23:06 -08:00
..
bind_variables.cpp make self-contained bind-variables 2014-09-24 14:30:30 -07:00
bind_variables.h bind variables in queries generated from Horn tactic to enforce that rule formulas don't contain free variables. Issue #328 2015-12-01 14:47:33 -08:00
dl_boogie_proof.cpp move functionality from qe_util to ast_util 2015-06-23 14:33:45 +02:00
dl_boogie_proof.h added missing Copyright forms 2015-06-10 11:54:02 -07:00
dl_context.cpp update display method for datalog to use predicates, throttle use of extensionality 2016-01-28 20:23:06 -08:00
dl_context.h update display method for datalog to use predicates, throttle use of extensionality 2016-01-28 20:23:06 -08:00
dl_costs.cpp re-organization of muz 2013-08-28 22:11:33 -07:00
dl_costs.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
dl_engine_base.h fix query for non-relational engines 2016-01-12 07:57:10 -08:00
dl_rule.cpp Fix Issue #405: Horn normal form ignores implication 2016-01-10 19:16:59 -08:00
dl_rule.h remove unused min-aggregate 2015-12-04 09:23:36 -08:00
dl_rule_set.cpp remove unused min-aggregate 2015-12-04 09:23:36 -08:00
dl_rule_set.h remove unused min-aggregate 2015-12-04 09:23:36 -08:00
dl_rule_subsumption_index.cpp re-organization of muz 2013-08-28 22:11:33 -07:00
dl_rule_subsumption_index.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
dl_rule_transformer.cpp re-organization of muz 2013-08-28 22:11:33 -07:00
dl_rule_transformer.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
dl_util.cpp Refactor count_vars and count_rule_vars 2015-05-14 17:04:38 +01:00
dl_util.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
fixedpoint_params.pyg disable bottom-up COI on rules with negated predicates. Fixes issue #140 2015-06-23 18:57:16 +02:00
hnf.cpp Fix Issue #405: Horn normal form ignores implication 2016-01-10 19:16:59 -08:00
hnf.h cleanup cancelation logic 2015-12-11 12:35:35 -08:00
proof_utils.cpp tabs and indentation 2015-09-17 13:25:22 +01:00
proof_utils.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
rule_properties.cpp strengthen quantifier check for PDR (and other engines) that don't handle quantified predicates 2015-06-12 18:30:33 -07:00
rule_properties.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00