From 6cd1f877b84a9d488d37035bff800e69e02221a7 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 2 May 2017 10:39:32 -0400
Subject: [PATCH] params for theory aware branching
---
src/smt/params/smt_params.cpp | 1 +
src/smt/params/smt_params.h | 3 +++
src/smt/params/smt_params_helper.pyg | 1 +
3 files changed, 5 insertions(+)
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 4b7920596..d4eb0b394 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_restart_factor = p.restart_factor();
m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
m_theory_case_split = p.theory_case_split();
+ m_theory_aware_branching = p.theory_aware_branching();
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index c03eaeaef..eacee95ab 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -110,6 +110,7 @@ struct smt_params : public preprocessor_params,
unsigned m_rel_case_split_order;
bool m_lookahead_diseq;
bool m_theory_case_split;
+ bool m_theory_aware_branching;
// -----------------------------------
//
@@ -240,6 +241,8 @@ struct smt_params : public preprocessor_params,
m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
m_rel_case_split_order(0),
m_lookahead_diseq(false),
+ m_theory_case_split(false),
+ m_theory_aware_branching(false),
m_delay_units(false),
m_delay_units_threshold(32),
m_theory_resolve(false),
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index faa48400d..4c9bbc677 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -62,6 +62,7 @@ def_module_params(module_name='smt',
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
+ ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),