cnode/CNode.h
00001 /*
00002  * CNode.h
00003  *
00004  *  Created on: Sep 1, 2008
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef CNODE_H_
00009 #define CNODE_H_
00010 #include <string>
00011 using namespace std;
00012 #include <map>
00013 #include <iostream>
00014 #include <unordered_map>
00015 #include <unordered_set>
00016 #include <set>
00017 using namespace std;
00018 
00019 #include "SatValue.h"
00020 
00021 #include <boost/serialization/list.hpp>
00022 #include <boost/serialization/string.hpp>
00023 #include <boost/serialization/version.hpp>
00024 #include <boost/serialization/split_member.hpp>
00025 #include <boost/serialization/shared_ptr.hpp>
00026 #include <boost/serialization/base_object.hpp>
00027 #include <boost/serialization/export.hpp>
00028 
00029 
00030 enum cnode_type
00031 {
00032         FALSE_NODE,
00033         TRUE_NODE,
00034         BOOLEAN_VAR,
00035         EQ,
00036         ILP,
00037         MOD,
00038         UNIVERSAL,
00039         NOT,
00040         AND,
00041         OR,
00042         IMPLIES
00043 };
00044 
00045 class VarMap;
00046 class Term;
00047 class Leaf;
00048 
00049 /*
00050  * A CNode is either a connective (and, or, not, implies) or a leaf node
00051  * (EqLeaf, ILPLeaf, ModLeaf, QuantifiedLeaf.)
00052  *
00053  * Among the connective nodes, all implications x->y
00054  * are first converted to !x | y during the preprocessing stage;
00055  * hence we assume all connectives are and, or, or not.
00056  *
00057  * All nodes are shared and created by calling their factory method make.
00058  *
00059  */
00060 
00061 
00062 class CNode;
00063 
00064 namespace std {
00065 template <>
00066 struct hash<CNode*> {
00067         size_t operator() (const CNode* const & x) const;
00068 };
00069 
00070 template <>
00071 struct hash<pair<int, CNode*> > {
00072         size_t operator() (const pair<int, CNode*>  & x) const;
00073 };
00074 
00075 }
00076 
00077 
00078 
00079 /*
00080  * Simplification level for cnodes:
00081  * UNSAT_SIMPLIFY: Only guarantees constraints that are unsat are false,
00082  *                                 nothing else.
00083  * LAZY_SIMPLIFY: Only simplifies part of the constraint necessary to prove
00084  *                                      the constraint SAT.
00085  * FULL_SIMPLIFY: Simplifies all parts of the constraint, not just the part
00086  *                                necessary to prove it SAT.
00087  * SEMANTIC SIMPLIFY: Doesn't just simplify the constraint locally, but does a
00088  *                                      global simplification.
00089  *
00090  */
00091 enum simplification_level {
00092         UNSAT_SIMPLIFY,
00093         BOOLEAN_SIMPLIFY,
00094         HYBRID_SIMPLIFY,
00095         THEORY_SIMPLIFY,
00096         /*-----------*/
00097         _END_SIMPLIFY_
00098 };
00099 
00100 struct node_eq
00101 {
00102   bool operator()(const CNode* l1, const CNode* l2) const;
00103 };
00104 
00105 
00106 
00107 class CNode;
00108 
00109 class CNode {
00110         friend class Term;
00111         friend class boost::serialization::access;
00112 public:
00113         static VarMap vm;
00114         static unordered_set<CNode*, std::hash<CNode*>, node_eq> nodes;
00115         static bool delete_nodes;
00116 
00117         static unordered_map<pair<int,CNode*>, CNode*> simp_map;
00118         size_t hash_c;
00119         cnode_type node_type;
00120 
00121 private:
00122 
00123         template<class Archive>
00124         void save(Archive & ar, const unsigned int version) const
00125         {
00126                 ar & node_type;
00127                 ar & negations_folded;
00128 
00129         }
00130         template<class Archive>
00131         void load(Archive & ar, const unsigned int version)
00132         {
00133                 CNode* cur_folded;
00134                 ar & node_type;
00135                 ar & cur_folded;
00136                 negations_folded = cur_folded;
00137                 negation = NULL;
00138                 factorization = NULL;
00139 
00140         }
00141         BOOST_SERIALIZATION_SPLIT_MEMBER()
00142 
00143         struct refactor_lessthan
00144         {
00145                   inline bool operator()(const pair<CNode*, set<CNode*> >& ref1,
00146                                   const pair<CNode*, set<CNode*> >& ref2) const;
00147         };
00148 
00149 public:
00150         /*
00151          * The canonical node to be used when interpreting the CNode as
00152          * part of a clause. This is may only be different for negations of
00153          * ILP_LEQ leafes.
00154          */
00155         CNode* negations_folded;
00156 
00157         CNode* negation;
00158 
00159         CNode* factorization;
00160 
00161 
00162 protected:
00163         CNode();
00164         virtual ~CNode();
00165         static CNode* get_node(CNode* node);
00166         static set<CNode*> to_delete;
00167         static CNode* uniquify_cnode_rec(CNode* node);
00168 public:
00169         static CNode* uniquify_cnode(CNode* node);
00170         static VarMap& get_varmap();
00171         static CNode* true_node();
00172         static CNode* false_node();
00173         CNode* get_simplification(simplification_level min_level);
00174         void set_simplification(CNode* simplified_node, simplification_level level);
00175 
00176 
00177 
00178         /*
00179          * Refactors this constraint in a locally optimal way.
00180          */
00181         CNode* refactor();
00182 
00183         /*
00184          * Making canonical means reconstructing this CNode with ILP leaves
00185          * having the invariant that their first element always has
00186          * positive coefficient.
00187          */
00188         CNode* make_canonical();
00189         bool check_canonical();
00190 
00191         /*
00192          * Return the conjunction of the constraint
00193          * representing restrictions on terms that appear in
00194          * this formula.
00195          */
00196         CNode* get_attribute_constraints();
00197 
00198 
00199         virtual CNode* substitute(map<Term*, Term*>& subs) = 0;
00200         CNode* substitute(Term* (*sub_func)(Term* t));
00201         CNode* substitute(Term* t1, Term* t2);
00202 
00203         CNode* substitute(Term* (*sub_func)(Term* t, void* data), void* my_data);
00204 
00205 
00206         CNode* substitute(map<CNode*, CNode*> & subs);
00207         inline cnode_type get_type() const
00208         {
00209                 return node_type;
00210         }
00211         virtual bool operator==(const CNode& other) = 0;
00212         virtual string to_string()=0;
00213         string to_prefix_notation();
00214 
00215         /*
00216          * A leaf is either True, False,
00217          * EqLeaf, ILPLeaf, or a universally quantified leaf.
00218          */
00219         bool is_leaf() const;
00220 
00221         /*
00222          * A literal is either a leaf or the negation of a leaf.
00223          */
00224         bool is_literal() const;
00225 
00226         /*
00227          * And, or, not.
00228          */
00229         bool is_connective() const;
00230 
00231         /*
00232          * If a node is a conjunct, it contains no or's.
00233          */
00234         bool is_conjunct() const;
00235 
00236         /*
00237          * If a node is a disjunct, it does not contain and's.
00238          */
00239         bool is_disjunct() const;
00240 
00241         /*
00242          * Does this node contain a (universal) quantifier?
00243          */
00244         bool has_quantifier() const;
00245 
00246         /*
00247          * Does this constraint contain <, <=, >, >=?
00248          */
00249         bool contains_inequality();
00250 
00251         /*
00252          * True or false.
00253          */
00254         bool is_constant() const;
00255         size_t hash_code();
00256         static void clear();
00257         void get_vars(set<string>& vars);
00258         void get_vars(set<int>& vars);
00259         void get_vars(set<Term*>& vars);
00260         bool contains_var(int var_id);
00261         bool contains_term(Term* t);
00262         bool contains_term(set<Term*>& terms);
00263         CNode* rename_variable(int old_var_id, int new_var_id);
00264         CNode* rename_variables(map<int, int>& replacements);
00265 
00266         void get_nested_terms(set<Term*> & terms, bool include_function_subterms,
00267                         bool include_constants = true);
00268 
00269         /*
00270          * Returns another CNode that explicitly includes attributes on the
00271          * terms nested in this CNode. One can specify that only attributes on certain
00272          * terms be added by passing in a valid set of "which_terms".
00273          */
00274         CNode* add_attributes(set<Term*>* which_terms = NULL);
00275 
00276         /*
00277          * If this node entails an equality constraint on the given term t, returns
00278          * another term t' such that t=t'; otherwise NULL.
00279          */
00280         Term* contains_term_equality(Term* t);
00281 
00282         /*
00283          * Set of all equalities involving t.
00284          */
00285         void collect_term_equalities(Term* t, set<Term*>& eqs);
00286 
00287         /*
00288          * If a given leaf contains the term t, this function replaces that leaf
00289          * with the provided replacement node.
00290          */
00291         CNode* replace_leaves_containing_term(Term* t, CNode* replacement);
00292 
00293         CNode* replace(CNode* orig, CNode* replacement);
00294 
00295         /*
00296          * Returns the number of leaves that contain the given term
00297          */
00298         int num_leaves_containing_term(Term* t);
00299 
00300         void get_all_literals(set<CNode*> & literals);
00301         void get_all_leaves(set<CNode*>& leaves);
00302         void get_literals_containing_term(Term* t, set<CNode*>& leaves);
00303 
00304         inline CNode* fold_negated_ilps()
00305         {
00306                 return negations_folded;
00307         }
00308 
00309         int get_size();
00310 
00311         CNode* evaluate_assignment(map<Term*, SatValue>& assignment);
00312         CNode* evaluate_assignment(map<CNode*, bool>& assignments);
00313 
00314 
00315         void get_all_fun_ids(set<int> & ids);
00316 
00317 
00318         void get_all_arguments(int fun_id, int arg_num, set<Term*> & args);
00319 
00320         CNode* replace_first_argument(map<int, Term*>& fun_id_to_replacement);
00321         void get_all_first_arguments(set<int>& fn_ids, map<int, set<Term*> >&
00322                         fn_id_to_first_arg);
00323 
00324         /*
00325          * Fills a set with all terms appearing in ilp leaves
00326          */
00327         void get_all_ilp_terms(set<Term*>& ilp_terms);
00328         /*
00329          * Rewrites a disequality t1 != t2 as t1<t2 or t1>t2
00330          * if at least one terms is an ilp term.
00331          */
00332         CNode* rewrite_ilp_neqs(set<Term*>& ilp_terms);
00333 
00334 
00335         /*
00336          * Integer division on elements in ILP leaf
00337          */
00338         virtual CNode*  divide(long int c, Term* t);
00339 
00340         /*
00341          * Converts this formula to an equivalence-preserving CNF
00342          * (does not introduce new variables!!)
00343          */
00344         CNode* to_cnf();
00345 
00346         /*
00347          * Returns the number of disjuncts in CNode
00348          */
00349         int num_disjuncts();
00350 
00351 
00352 private:
00353         void to_prefix_notation_rec(string& output);
00354         Term* contains_term_equality_internal(Term* t, bool phase);
00355         void collect_term_equalities_internal(Term* t, bool phase, set<Term*> &
00356                         equalities);
00357         void get_attributes(set<CNode*>& attributes);
00358 
00359         template<cnode_type node_type, cnode_type refactor_type>
00360         static CNode* connective_refactor(const set<CNode*>& children);
00361 };
00362 
00363 class CompareCNode:public binary_function<CNode*, CNode*, bool> {
00364 
00365 public:
00366         bool operator()(const CNode* b1, const CNode* b2) const;
00367 };
00368 
00369 
00370 
00371 
00372 
00373 
00374 #endif /* CNODE_H_ */