Constraint.h

/*
 * Constraint.h
 *
 *  Created on: Sep 16, 2008
 *  Author: isil
 */

#ifndef CONSTRAINT_H_
#define CONSTRAINT_H_

#include "ConstraintSolver.h"
#include "Term.h"

#include <set>
#include <iostream>
#include <unordered_map>
#include <unordered_set>
#include <string>
#include <functional>

using namespace std;

class CNode;

class Constraint {
        friend class boost::serialization::access;
private:
        friend struct std::hash<Constraint>;
        friend class ConstraintSolver;
        friend class Term;
        int id;

        template<class Archive>
        void save(Archive & ar, const unsigned int version) const
        {

                CNode* nc = cs.get_nc((int&)id);
                CNode* sc = cs.get_sc((int&)id);
                ar & nc;
                ar & sc;


        }
        template<class Archive>
        void load(Archive & ar, const unsigned int version)
        {
                CNode* nc;
                CNode* sc;
                ar & nc;
                ar & sc;
                nc = CNode::uniquify_cnode(nc);
                sc = CNode::uniquify_cnode(sc);
                pair<CNode*, CNode*> key(nc, sc);
                id = cs.get_id(key);


        }
        BOOST_SERIALIZATION_SPLIT_MEMBER()

        void get_msa_assignment(set<VariableTerm*>&
                        msa_vars, map<Term*, SatValue>& msa);



public:
        static ConstraintSolver cs;
        Constraint();
        Constraint(bool val);
        Constraint(const Constraint& nc, const Constraint& sc);
        Constraint(Term* t1, Term* t2, atom_op_type op);

        Constraint(const Constraint & other);
        Constraint(string s);
        Constraint(const char* s);

        Constraint(CNode* n);

        static void set_geqz_attribute(Term* t);
        static void set_gtz_attribute(Term* t);

        bool sat() const;
        bool unsat() const;
        bool valid() const;
        bool equivalent(Constraint other) const;


        /*
         * These methods do not simplify.
         */
        bool sat_discard() const;
        bool unsat_discard() const;
        bool valid_discard() const;


        Constraint nc() const;
        Constraint sc() const;

        int nc_size() const;
        int sc_size() const;

        /*
         * Checks if the constraint is literally the constant true/false
         */
        bool is_true() const;
        bool is_false() const;

        static void clear();



        Constraint operator&(const Constraint & other) const;
        Constraint operator|(const Constraint & other) const;

        /*
         * Find a constraint C such that b&C=>this and C is consistent with everything
         * in the consistency_constraints set.
         */
        Constraint abduce(Constraint  b,
                        const set<Constraint> & consistency_constraints,
                        map<Term*, int>& costs) const;

        Constraint abduce(Constraint  b,
                        const set<Constraint> & consistency_constraints) const;

        Constraint abduce(Constraint  b) const;

        void operator&=(const Constraint & other);
        void operator|=(const Constraint & other);


        Constraint operator!() const ;

        void operator=(const Constraint &  other);
        bool operator==(const Constraint &  other) const;
        bool operator!=(const Constraint &  other) const;
        bool implies(const Constraint & other) const;
        bool operator<(const Constraint  & other) const;

        /*
         * Returns true if NC==SC, i.e. the current constraint has
         * no imprecision.
         */
        bool is_precise() const;

        /*
         * Functions for eliminating existentially quantified variables
         */
        void eliminate_evar(VariableTerm* var);
        void eliminate_evars(set<VariableTerm*>& vars);

        /*
         * Functions for eliminating universally quantified variables
         */
        void eliminate_uvar(VariableTerm* var);
        void eliminate_uvars(set<VariableTerm*>& vars);

        /*
         * Does this constraint contain a <, <=, >, >=?
         */
        bool contains_inequality();

        void fresh_id();


        /*
         * Functions for eliminating free variables
         */
        void eliminate_free_var(VariableTerm* var);
        void eliminate_free_vars(set<VariableTerm*>& vars);


        /*
         * Yields the set of all terms used in this constraint
         */
        void get_terms(set<Term*>& terms, bool include_nested_terms);

        /*
         * Methods to manage background knowledge, i.e.
         * assumptions on the left side of the turnstile.
         */
        static void add_ground_axiom(Constraint key, Constraint c);
        static void add_quantified_axiom(Constraint key, Constraint c);
        static void set_background_knowledge(Constraint c);

        static void replace_term_in_axioms(Term* old_t, Term* new_t);



        static string background_knowledge_to_string();
        static Constraint get_general_background();


        /*
         * The return value R is a term t' such that (t=t') is
         * implied by this constraint. Returns NULL if no
         * such equality is implied by the constraint.
         */
        Term* find_equality(Term* t) const;

        void find_equalities(Term* t, set<Term*> & eqs) const;


        void replace_term(Term* to_replace, Term* replacement);
        void replace_terms(map<Term*, Term*> & replacements);
        void replace_constraint(Constraint to_replace, Constraint replacement);

        void replace_terms(Term* (*sub_func)(Term* t, void* data), void* my_data)
        {
                c_id old_id = id;
                id = cs.replace_terms(old_id, sub_func, my_data);
        }

        void get_free_variables(set<Term*>& vars);
        bool contains_term(Term* var);
        // Does this constraint contain any of these terms?
        bool contains_term(set<Term*>& terms);



        static void clear_background();

        /*
         * If this method is called, background knowledge is not
         * taken into account when determining satisfiability/validity.
         */
        static void disable_background();

        /*
         * If this constraint contains artificial variables used to enforce,
         * for example, existence and uniqueness, this function
         * eliminates these fake variables and replaces them by
         * what they stand for.
         */
        void propagate_background();

        /*
         * Assume that c holds, i.e. set all leaves from c that occur inside you
         * to true.
         */
        void assume(Constraint c);
        /*
         * Are t1 and t2 related by an equality in this constraint?
         */
        bool has_equality_relation(Term* t1, Term* t2);


        void get_disjunctive_equalities(Term* var,
                        map<Term*, Constraint> & equalities);

        void divide(long int c, Term* t);


        /*
         * Gives a satisfying assignment to all terms in the constraint.
         * e.g. <drf(a), 3>,...
         */
        bool get_assignment(set<pair<string, string> > & assignments);
        bool get_assignment(map<Term*, SatValue> & assignments);


        void replace_terms(Term* (*sub_func)(Term* t));



        string to_string() const;
        string debug_string();

        int msa(map<Term*, SatValue>& msa);
        int  msa(set<VariableTerm*> & msa) const;
        int msa(set<VariableTerm*> & msa, set<Constraint>& bg) const;
        int msa(map<Term*, SatValue> & msa, set<Constraint>& bg);
        int  msa(set<VariableTerm*> & msa,
                        map<VariableTerm*, int>& costs) const;
        int  msa(set<VariableTerm*> & msa, set<Constraint>& bg,
                        map<VariableTerm*, int>& costs) const;
        int  msa(map<Term*, SatValue> & msa, set<Constraint>& bg,
                        map<VariableTerm*, int>& costs);

        pair<CNode*, CNode*> get_cnodes();


        void to_dnf(set<Constraint> & dnf);
        void to_cnf(set<Constraint> & cnf);

};

ostream& operator <<(ostream &os,const Constraint &_obj);

namespace std {
template <>
struct hash<Constraint> {

        size_t operator() (const Constraint & x) const {
                Constraint & c = (Constraint &)x;
                return hash<int>()(c.id);
        }
};


}


#endif /* CONSTRAINT_H_ */