mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Merge branch 'working' of https://z3-1/gw/git/z3 into working

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-10-13 10:13:02 -07:00
parent af469f82ec bccf07be0b
commit 8121386d5e
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
lib/asserted_formulas.cpp
View file

@ -873,11 +873,18 @@ bool asserted_formulas::solve_core() {
}
void asserted_formulas::solve() {
// This method is buggy when unsatisfiable cores are enabled.
// It may eliminate answer literals.
// Since I will remove asserted_formulas.cpp in the future, I just disabled it.
// Note: asserted_formulas.cpp is based on the obsolete preprocessing stack.
// Users should the solve-eqs tactic if they want to eliminate variables.
#if 0
while (solve_core()) {
IF_IVERBOSE(10, verbose_stream() << "reducing...\n";);
flush_cache(); // collect garbage
reduce_asserted_formulas();
}
#endif
}
void asserted_formulas::reduce_asserted_formulas() {

2
lib/install_tactics.cpp
View file

@ -70,6 +70,7 @@ Notes:
#include"qfbv_tactic.h"
#include"subpaving_tactic.h"
#include"unit_subsumption_tactic.h"
#include"qfnra_nlsat_tactic.h"
MK_SIMPLE_TACTIC_FACTORY(simplifier_fct, mk_simplify_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(split_clause_fct, mk_split_clause_tactic(p));
@ -193,6 +194,7 @@ void install_tactics(tactic_manager & ctx) {
ADD_TACTIC_CMD("qflra", "builtin strategy for solving QF_LRA problems.", qflra_fct);
ADD_TACTIC_CMD("qfnia", "builtin strategy for solving QF_NIA problems.", qfnia_fct);
ADD_TACTIC_CMD("qfnra", "builtin strategy for solving QF_NRA problems.", qfnra_fct);
ADD_TACTIC_CMD("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", qfnra_nlsat_fct);
ADD_TACTIC_CMD("qfbv", "builtin strategy for solving QF_BV problems.", qfbv_fct);
#ifndef _EXTERNAL_RELEASE
ADD_TACTIC_CMD("subpaving", "tactic for testing subpaving module.", subpaving_fct);