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

add theory case split support to smt_context

Browse source
This commit is contained in:
Murphy Berzish 2017-05-01 10:34:43 -04:00
parent f655e1976e
commit 2f56d128b0
2 changed files with 148 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/smt/smt_context.h
View file

@ -226,6 +226,16 @@ namespace smt {
literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption
expr_ref_vector m_unsat_core;
// -----------------------------------
//
// Theory case split
//
// -----------------------------------
uint_set m_all_th_case_split_literals;
vector<literal_vector> m_th_case_split_sets;
u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in
unsigned m_th_case_split_qhead;
// -----------------------------------
//
// Accessors
@ -820,6 +830,21 @@ namespace smt {
void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = 0);
/*
* Provide a hint to the core solver that the specified literals form a "theory case split".
* The core solver will enforce the condition that exactly one of these literals can be
* assigned 'true' at any time.
* We assume that the theory solver has already asserted the disjunction of these literals
* or some other axiom that means at least one of them must be assigned 'true'.
*/
void mk_th_case_split(unsigned num_lits, literal * lits);
public:
// helper function for trail
void undo_th_case_split(literal l);
bool propagate_th_case_split();
bool_var mk_bool_var(expr * n);