mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

disable drat inside of quantifier elaboration

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-30 23:27:37 -07:00
parent 6dfaaa43cd
commit bcf0f671b8
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/q_mbi.cpp
View file

@ -42,6 +42,7 @@ namespace q {
add_plugin(ap); add_plugin(ap);
add_plugin(alloc(mbp::datatype_project_plugin, m)); add_plugin(alloc(mbp::datatype_project_plugin, m));
add_plugin(alloc(mbp::array_project_plugin, m)); add_plugin(alloc(mbp::array_project_plugin, m));
} }
lbool mbqi::operator()() { lbool mbqi::operator()() {
@ -565,7 +566,7 @@ namespace q {
void mbqi::init_solver() { void mbqi::init_solver() {
if (!m_solver) if (!m_solver)
m_solver = mk_smt2_solver(m, ctx.s().params()); m_solver = mk_smt2_solver(m, m_no_drat_params);
} }
void mbqi::init_search() { void mbqi::init_search() {

2
src/sat/smt/q_mbi.h
View file

@ -20,6 +20,7 @@ Author:
#include "qe/mbp/mbp_plugin.h" #include "qe/mbp/mbp_plugin.h"
#include "sat/smt/sat_th.h" #include "sat/smt/sat_th.h"
#include "sat/smt/q_model_fixer.h" #include "sat/smt/q_model_fixer.h"
#include "sat/sat_solver.h"
namespace euf { namespace euf {
class solver; class solver;
@ -60,6 +61,7 @@ namespace q {
stats m_stats; stats m_stats;
model_fixer m_model_fixer; model_fixer m_model_fixer;
model_ref m_model; model_ref m_model;
sat::no_drat_params m_no_drat_params;
ref<::solver> m_solver; ref<::solver> m_solver;
scoped_ptr_vector<obj_hashtable<expr>> m_values; scoped_ptr_vector<obj_hashtable<expr>> m_values;
scoped_ptr_vector<mbp::project_plugin> m_plugins; scoped_ptr_vector<mbp::project_plugin> m_plugins;