1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 nlarith_util.h 7 8 Abstract: 9 10 Utilities for nln-linear arithmetic quantifier elimination and 11 solving. 12 13 Author: 14 15 Nikolaj (nbjorner) 2011-05-13 16 17 Notes: 18 19 --*/ 20 #pragma once 21 22 #include "ast/ast.h" 23 #include "util/lbool.h" 24 25 namespace nlarith { 26 27 /** 28 \brief A summary for branch side conditions and substitutions. 29 30 Each branch in a split comprises of: 31 - preds - a sequence of predicates used for the branching. 32 - branches - a sequence of branch side conditions 33 - subst - a sequence of substitutions that replace 'preds' by formulas 34 not containing the eliminated variable 35 - constraints - a sequence of side constraints to add to the main formula. 36 */ 37 class branch_conditions { 38 expr_ref_vector m_branches; 39 expr_ref_vector m_preds; 40 vector<expr_ref_vector> m_subst; 41 expr_ref_vector m_constraints; 42 expr_ref_vector m_defs; 43 expr_ref_vector m_a; 44 expr_ref_vector m_b; 45 expr_ref_vector m_c; 46 47 public: branch_conditions(ast_manager & m)48 branch_conditions(ast_manager& m) : m_branches(m), m_preds(m), m_constraints(m), m_defs(m), m_a(m), m_b(m), m_c(m) {} add_pred(expr * p)49 void add_pred(expr* p) { m_preds.push_back(p); } add_branch(expr * branch,expr * cond,expr_ref_vector const & subst,expr * def,expr * a,expr * b,expr * c)50 void add_branch(expr* branch, expr* cond, expr_ref_vector const& subst, expr* def, expr* a, expr* b, expr* c) { 51 m_branches.push_back(branch); 52 m_constraints.push_back(cond); 53 m_subst.push_back(subst); 54 m_defs.push_back(def); 55 m_a.push_back(a); 56 m_b.push_back(b); 57 m_c.push_back(c); 58 } preds(unsigned i)59 expr* preds(unsigned i) const { return m_preds[i]; } branches(unsigned i)60 expr* branches(unsigned i) const { return m_branches[i]; } constraints(unsigned i)61 expr* constraints(unsigned i) const { return m_constraints[i]; } def(unsigned i)62 expr* def(unsigned i) const { return m_defs[i]; } a(unsigned i)63 expr* a(unsigned i) const { return m_a[i]; } b(unsigned i)64 expr* b(unsigned i) const { return m_b[i]; } c(unsigned i)65 expr* c(unsigned i) const { return m_c[i]; } subst(unsigned i)66 expr_ref_vector const& subst(unsigned i) const { return m_subst[i]; } branches()67 expr_ref_vector const& branches() const { return m_branches; } preds()68 expr_ref_vector const& preds() const { return m_preds; } subst()69 vector<expr_ref_vector> const& subst() const { return m_subst; } constraints()70 expr_ref_vector const& constraints() const { return m_constraints; } reset()71 void reset() { 72 m_branches.reset(); m_preds.reset(); m_subst.reset(); 73 m_constraints.reset(); m_defs.reset(); 74 m_a.reset(); m_b.reset(); m_c.reset(); 75 } 76 size()77 unsigned size() const { return branches().size(); } num_preds()78 unsigned num_preds() const { return preds().size(); } 79 }; 80 81 class util { 82 class imp; 83 imp* m_imp; 84 public: 85 util(ast_manager& m); 86 ~util(); 87 88 /** 89 \brief Enable handling of linear variables. 90 */ 91 void set_enable_linear(bool enable_linear); 92 93 /** 94 \brief Create branches for non-linear variable x. 95 */ 96 bool create_branches(app* x, unsigned nl, expr* const* lits, branch_conditions& bc); 97 /** 98 \brief Extract non-linear variables from ground formula. 99 */ 100 void extract_non_linear(expr* e, ptr_vector<app>& nl_vars); 101 102 /** 103 \brief literal sets. Opaque state. 104 */ 105 106 class literal_set; 107 108 static void deallocate(literal_set* lits); 109 110 111 112 /** 113 \brief Sign-based branching. v2. 114 */ 115 typedef obj_hashtable<app> atoms; 116 117 class eval { 118 public: ~eval()119 virtual ~eval() {} 120 virtual lbool operator()(app* a) = 0; 121 }; 122 123 enum atom_update { INSERT, REMOVE }; 124 125 class branch { 126 public: ~branch()127 virtual ~branch() {} 128 virtual app* get_constraint() = 0; 129 virtual void get_updates(ptr_vector<app>& atoms, svector<atom_update>& updates) = 0; 130 }; 131 132 /** 133 \brief select literals that contain non-linear variables. 134 */ 135 bool get_sign_literals(atoms const& atoms, eval& eval, literal_set*& lits); 136 137 /** 138 \brief given selected literals, generate branch conditions. 139 */ 140 void get_sign_branches(literal_set& lits, eval& eval, ptr_vector<branch>& branches); 141 142 143 144 }; 145 146 }; 147 148