solver/Solver.h
```00001 /*
00002  * Solver.h
00003  *
00004  *  Created on: Sep 5, 2008
00005  *      Author: tdillig
00006  */
00007
00008 #ifndef SOLVER_H_
00009 #define SOLVER_H_
00010 #include <set>
00011 #include <vector>
00012 #include <map>
00013 using namespace std;
00014 #include "InteractionManager.h"
00015 #include "util.h"
00016
00017
00018 class CNode;
00019 class VarMap;
00020 class NormalForm;
00021 class Clause;
00022 class Term;
00023 class ILPLeaf;
00024 class EqLeaf;
00025 class Leaf;
00026 class FunctionTerm;
00027 class Matrix;
00028 class Equation;
00029 class Connective;
00030
00031 #include "bignum.h"
00032 #include "ClauseSolve.h"
00033 #include "SatSolver.h"
00034 #include "Vec.h"
00035
00036
00037 class Solver {
00038
00039          friend class InteractionManager;
00040          friend class QueryComparator;
00041          friend class ClauseSolve;
00042          friend class VariableEliminator;
00043 protected:
00044
00045         int fresh_var_counter;
00046         int solve_count;
00047         int literal_count;
00048         int clause_cache_hit_count;
00049         int cache_hits;
00050         int solve_time;
00051         int imply_time;
00052         int num_imply;
00053         CNode* res;
00054 public:
00055         Solver(CNode* node, simplification_level level,
00056                         map<Term*, SatValue>* assignments = NULL,
00057                         bool use_dnf = false);
00058
00059         Solver(CNode* node, CNode* assumptions, simplification_level level,
00060                         map<Term*, SatValue>* assignments = NULL);
00061
00062         CNode* solve(CNode* node, CNode* assumptions, simplification_level level,
00063                         map<Term*, SatValue>* assignments);
00064
00065         static bool implies(CNode* node1, CNode* node2);
00066         static bool equivalent(CNode* node1, CNode* node2);
00067
00068         /*
00069          * Slices out parts of the assumptions that are irrelevant for simplifying
00070          * the formula.
00071          */
00072         static CNode* get_relevant_background(CNode* background,
00073                         CNode* formula_to_simplify);
00074
00075
00076         /*
00077          * Node is SAT if and only if the type of the result node is
00078          * not FALSE_NODE.
00079          */
00080         CNode* get_result();
00081         string get_stats();
00082         virtual ~Solver();
00083
00084
00085
00086 protected:
00087         Solver();
00088
00089
00090
00091
00092
00093         /*
00094         * Preprocesses equalities.
00095         */
00096    CNode* propagate_equalities(CNode* node, CNode*& active_constraint);
00097
00098    inline void add_to_replacement_map(Term* to_replace, Term* replacement,
00099                    map<Term*, Term*>& replacement_map);
00100
00101 private:
00102    bool dnf_solve(CNode* node, map<Term*, SatValue>* assignments = NULL,
00103                                 bool verbose = false, bool ilp_only = false);
00104         bool sat_solve(CNode* node);
00105
00106
00107
00108         static CNode* get_relevant_background_internal(CNode* background, set<Term*>&
00109                         relevant_vars);
00110
00111         static bool get_related_vars(CNode* node, set<Term*>& vars);
00112
00113         void collect_constraint(CNode* node, bool sat, const string & path);
00114
00115
00116
00117 };
00118
00119 #endif /* SOLVER_H_ */
```