diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 100 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 33 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 144 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 43 | ||||
-rw-r--r-- | src/prop/bvminisat/core/SolverTypes.h | 13 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 15 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 14 | ||||
-rw-r--r-- | src/prop/cryptominisat/MTRand/Makefile.in | 141 | ||||
-rw-r--r-- | src/prop/cryptominisat/Makefile.in | 369 | ||||
-rw-r--r-- | src/prop/cryptominisat/Solver/Makefile.in | 198 | ||||
-rw-r--r-- | src/prop/cryptominisat/man/Makefile.in | 141 | ||||
-rw-r--r-- | src/prop/cryptominisat/mtl/Makefile.in | 141 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 11 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 2 |
16 files changed, 1039 insertions, 332 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index b32483cbe..232502696 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -22,13 +22,19 @@ using namespace CVC4; using namespace prop; -BVMinisatSatSolver::BVMinisatSatSolver() : - d_minisat(new BVMinisat::SimpSolver()) +BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext) +: context::ContextNotifyObj(mainSatContext, false), + d_minisat(new BVMinisat::SimpSolver(mainSatContext)), + d_solveCount(0), + d_assertionsCount(0), + d_assertionsRealCount(mainSatContext, 0), + d_lastPropagation(mainSatContext, 0) { - d_statistics.init(d_minisat); + d_statistics.init(d_minisat); } -BVMinisatSatSolver::~BVMinisatSatSolver() { + +BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) { delete d_minisat; } @@ -42,6 +48,42 @@ void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) { d_minisat->addClause(minisat_clause); } +void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) { + d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit))); +} + +bool BVMinisatSatSolver::getPropagations(std::vector<SatLiteral>& propagations) { + for (; d_lastPropagation < d_minisat->atom_propagations.size(); d_lastPropagation = d_lastPropagation + 1) { + propagations.push_back(toSatLiteral(d_minisat->atom_propagations[d_lastPropagation])); + } + return propagations.size() > 0; +} + +void BVMinisatSatSolver::explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) { + std::vector<BVMinisat::Lit> minisat_explanation; + d_minisat->explainPropagation(toMinisatLit(lit), minisat_explanation); + for (unsigned i = 0; i < minisat_explanation.size(); ++i) { + explanation.push_back(toSatLiteral(minisat_explanation[i])); + } +} + +SatValue BVMinisatSatSolver::assertAssumption(SatLiteral lit, bool propagate) { + d_assertionsCount ++; + d_assertionsRealCount = d_assertionsRealCount + 1; + return toSatLiteralValue(d_minisat->assertAssumption(toMinisatLit(lit), propagate)); +} + +void BVMinisatSatSolver::notify() { + while (d_assertionsCount > d_assertionsRealCount) { + popAssumption(); + d_assertionsCount --; + } +} + +void BVMinisatSatSolver::popAssumption() { + d_minisat->popAssumption(); +} + SatVariable BVMinisatSatSolver::newVar(bool freeze){ return d_minisat->newVar(true, true, freeze); } @@ -74,20 +116,28 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } -SatValue BVMinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){ - Debug("sat::minisat") << "Solve with assumptions "; - context::CDList<SatLiteral>::const_iterator it = assumptions.begin(); - BVMinisat::vec<BVMinisat::Lit> assump; - for(; it!= assumptions.end(); ++it) { - SatLiteral lit = *it; - Debug("sat::minisat") << lit <<" "; - assump.push(toMinisatLit(lit)); - } - Debug("sat::minisat") <<"\n"; - - SatValue result = toSatLiteralValue(d_minisat->solve(assump)); - return result; -} +// SatValue BVMinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions, bool only_bcp){ +// ++d_solveCount; +// ++d_statistics.d_statCallsToSolve; + +// Debug("sat::minisat") << "Solve with assumptions "; +// context::CDList<SatLiteral>::const_iterator it = assumptions.begin(); +// BVMinisat::vec<BVMinisat::Lit> assump; +// for(; it!= assumptions.end(); ++it) { +// SatLiteral lit = *it; +// Debug("sat::minisat") << lit <<" "; +// assump.push(toMinisatLit(lit)); +// } +// Debug("sat::minisat") <<"\n"; + +// clock_t begin, end; +// begin = clock(); +// d_minisat->setOnlyBCP(only_bcp); +// SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); +// end = clock(); +// d_statistics.d_statSolveTime = d_statistics.d_statSolveTime.getData() + (end - begin)/(double)CLOCKS_PER_SEC; +// return result; +// } void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { @@ -98,13 +148,11 @@ void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { } SatValue BVMinisatSatSolver::value(SatLiteral l){ - Unimplemented(); - return SAT_VALUE_UNKNOWN; + return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } SatValue BVMinisatSatSolver::modelValue(SatLiteral l){ - Unimplemented(); - return SAT_VALUE_UNKNOWN; + return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } void BVMinisatSatSolver::unregisterVar(SatLiteral lit) { @@ -191,7 +239,9 @@ BVMinisatSatSolver::Statistics::Statistics() : d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), d_statMaxLiterals("theory::bv::bvminisat::max_literals"), d_statTotLiterals("theory::bv::bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") + d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars"), + d_statCallsToSolve("theory::bv::bvminisat::calls_to_solve", 0), + d_statSolveTime("theory::bv::bvminisat::solve_time", 0) { StatisticsRegistry::registerStat(&d_statStarts); StatisticsRegistry::registerStat(&d_statDecisions); @@ -203,6 +253,8 @@ BVMinisatSatSolver::Statistics::Statistics() : StatisticsRegistry::registerStat(&d_statMaxLiterals); StatisticsRegistry::registerStat(&d_statTotLiterals); StatisticsRegistry::registerStat(&d_statEliminatedVars); + StatisticsRegistry::registerStat(&d_statCallsToSolve); + StatisticsRegistry::registerStat(&d_statSolveTime); } BVMinisatSatSolver::Statistics::~Statistics() { @@ -216,6 +268,8 @@ BVMinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statMaxLiterals); StatisticsRegistry::unregisterStat(&d_statTotLiterals); StatisticsRegistry::unregisterStat(&d_statEliminatedVars); + StatisticsRegistry::unregisterStat(&d_statCallsToSolve); + StatisticsRegistry::unregisterStat(&d_statSolveTime); } void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 4ca1164c0..19b605067 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -21,16 +21,27 @@ #include "prop/sat_solver.h" #include "prop/sat_solver_registry.h" #include "prop/bvminisat/simp/SimpSolver.h" +#include "context/cdo.h" namespace CVC4 { namespace prop { -class BVMinisatSatSolver: public BVSatSolverInterface { +class BVMinisatSatSolver: public BVSatSolverInterface, public context::ContextNotifyObj { BVMinisat::SimpSolver* d_minisat; + unsigned d_solveCount; + unsigned d_assertionsCount; + context::CDO<unsigned> d_assertionsRealCount; + context::CDO<unsigned> d_lastPropagation; public: - BVMinisatSatSolver(); - ~BVMinisatSatSolver(); + BVMinisatSatSolver() : + ContextNotifyObj(NULL, false), + d_assertionsRealCount(NULL, (unsigned)0), + d_lastPropagation(NULL, (unsigned)0) + { Unreachable(); } + BVMinisatSatSolver(context::Context* mainSatContext); + ~BVMinisatSatSolver() throw(AssertionException); + void addClause(SatClause& clause, bool removable); SatVariable newVar(bool theoryAtom = false); @@ -38,10 +49,11 @@ public: void markUnremovable(SatLiteral lit); void interrupt(); - + void notify(); + SatValue solve(); SatValue solve(long unsigned int&); - SatValue solve(const context::CDList<SatLiteral> & assumptions); + SatValue solve(bool quick_solve); void getUnsatCore(SatClause& unsatCore); SatValue value(SatLiteral l); @@ -62,6 +74,15 @@ public: static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); + void addMarkerLiteral(SatLiteral lit); + + bool getPropagations(std::vector<SatLiteral>& propagations); + + void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation); + + SatValue assertAssumption(SatLiteral lit, bool propagate); + + void popAssumption(); class Statistics { public: @@ -71,6 +92,8 @@ public: ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; ReferenceStat<uint64_t> d_statTotLiterals; ReferenceStat<int> d_statEliminatedVars; + IntStat d_statCallsToSolve; + BackedStat<double> d_statSolveTime; Statistics(); ~Statistics(); void init(BVMinisat::SimpSolver* minisat); diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 7ff7b50db..5066d5d8f 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -22,8 +22,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Sort.h" #include "core/Solver.h" +#include <vector> #include <iostream> #include "util/output.h" +#include "util/utility.h" using namespace BVMinisat; @@ -64,7 +66,7 @@ static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction o // Constructor/Destructor: -Solver::Solver() : +Solver::Solver(CVC4::context::Context* c) : // Parameters (user settable): // @@ -112,6 +114,8 @@ Solver::Solver() : , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) + , only_bcp(false) + , d_explanations(c) {} @@ -134,6 +138,7 @@ Var Solver::newVar(bool sign, bool dvar) watches .init(mkLit(v, true )); assigns .push(l_Undef); vardata .push(mkVarData(CRef_Undef, 0)); + marker .push(0); //activity .push(0); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); @@ -226,13 +231,20 @@ void Solver::cancelUntil(int level) { for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; + if (marker[x] == 2) marker[x] = 1; if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) polarity[x] = sign(trail[c]); insertVarOrder(x); } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); - } } + } + + if (level < atom_propagations_lim.size()) { + atom_propagations.shrink(atom_propagations.size() - atom_propagations_lim[level]); + atom_propagations_lim.shrink(atom_propagations_lim.size() - level); + } +} //================================================================================================= @@ -278,7 +290,7 @@ Lit Solver::pickBranchLit() | rest of literals. There may be others from the same level though. | |________________________________________________________________________________________________@*/ -void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) +void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip) { int pathC = 0; Lit p = lit_Undef; @@ -288,6 +300,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt.push(); // (leave room for the asserting literal) int index = trail.size() - 1; + bool done = false; do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; @@ -315,7 +328,18 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) seen[var(p)] = 0; pathC--; - }while (pathC > 0); + switch (uip) { + case UIP_FIRST: + done = pathC == 0; + break; + case UIP_LAST: + done = confl == CRef_Undef || (pathC == 0 && marker[var(p)] == 2); + break; + default: + Unreachable(); + break; + } + } while (!done); out_learnt[0] = ~p; // Simplify conflict clause: @@ -427,8 +451,10 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) Var x = var(trail[i]); if (seen[x]){ if (reason(x) == CRef_Undef){ + if (marker[x] == 2) { assert(level(x) > 0); out_conflict.push(~trail[i]); + } }else{ Clause& c = ca[reason(x)]; for (int j = 1; j < c.size(); j++) @@ -449,8 +475,34 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) assigns[var(p)] = lbool(!sign(p)); vardata[var(p)] = mkVarData(from, decisionLevel()); trail.push_(p); + if (only_bcp && marker[var(p)] == 1 && from != CRef_Undef) { + atom_propagations.push(p); + } +} + +void Solver::popAssumption() { + marker[var(assumptions.last())] = 1; + assumptions.pop(); + conflict.clear(); + cancelUntil(assumptions.size()); } +lbool Solver::assertAssumption(Lit p, bool propagate) { + + assert(marker[var(p)] == 1); + + // add to the assumptions + assumptions.push(p); + conflict.clear(); + + // run the propagation + if (propagate) { + only_bcp = true; + return search(-1, UIP_FIRST); + } else { + return l_True; + } +} /*_________________________________________________________________________________________________ | @@ -628,7 +680,7 @@ bool Solver::simplify() | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. |________________________________________________________________________________________________@*/ -lbool Solver::search(int nof_conflicts) +lbool Solver::search(int nof_conflicts, UIP uip) { assert(ok); int backtrack_level; @@ -644,17 +696,27 @@ lbool Solver::search(int nof_conflicts) if (decisionLevel() == 0) return l_False; learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level); + analyze(confl, learnt_clause, backtrack_level, uip); cancelUntil(backtrack_level); + Lit p = learnt_clause[0]; + bool assumption = marker[var(p)] == 2; + if (learnt_clause.size() == 1){ - uncheckedEnqueue(learnt_clause[0]); + uncheckedEnqueue(p); }else{ CRef cr = ca.alloc(learnt_clause, true); learnts.push(cr); attachClause(cr); claBumpActivity(ca[cr]); - uncheckedEnqueue(learnt_clause[0], cr); + uncheckedEnqueue(p, cr); + } + + // if an assumption, we're done + if (assumption) { + assert(decisionLevel() < assumptions.size()); + analyzeFinal(p, conflict); + return l_False; } varDecayActivity(); @@ -699,12 +761,18 @@ lbool Solver::search(int nof_conflicts) analyzeFinal(~p, conflict); return l_False; }else{ + marker[var(p)] = 2; next = p; break; } } if (next == lit_Undef){ + + if (only_bcp) { + return l_True; + } + // New variable decision: decisions++; next = pickBranchLit(); @@ -767,10 +835,12 @@ static double luby(double y, int x){ // NOTE: assumptions passed in member-variable 'assumptions'. lbool Solver::solve_() { - Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n"; - Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n"; + Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n"; + Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n"; + model.clear(); conflict.clear(); + if (!ok) return l_False; solves++; @@ -799,19 +869,56 @@ lbool Solver::solve_() if (verbosity >= 1) printf("===============================================================================\n"); - if (status == l_True){ // Extend & copy model: - model.growTo(nVars()); - for (int i = 0; i < nVars(); i++) model[i] = value(i); + // model.growTo(nVars()); + // for (int i = 0; i < nVars(); i++) model[i] = value(i); }else if (status == l_False && conflict.size() == 0) ok = false; - cancelUntil(0); return status; } //================================================================================================= +// Bitvector propagations +// + +void Solver::storeExplanation(Lit p) { +} + +void Solver::explainPropagation(Lit p, std::vector<Lit>& explanation) { + vec<Lit> queue; + queue.push(p); + + __gnu_cxx::hash_set<Var> visited; + visited.insert(var(p)); + while(queue.size() > 0) { + Lit l = queue.last(); + assert(value(l) == l_True); + queue.pop(); + if (reason(var(l)) == CRef_Undef) { + if (marker[var(l)] == 2) { + explanation.push_back(l); + visited.insert(var(l)); + } + } else { + Clause& c = ca[reason(var(l))]; + for (int i = 1; i < c.size(); ++i) { + if (var(c[i]) >= vardata.size()) { + std::cerr << "BOOM" << std::endl; + } + if (visited.count(var(c[i])) == 0) { + queue.push(~c[i]); + visited.insert(var(c[i])); + } + } + } + } +} + + + +//================================================================================================= // Writing CNF to DIMACS: // // FIXME: this needs to be rewritten completely. @@ -872,13 +979,13 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) } // Assumptions are added as unit clauses: - cnt += assumptions.size(); + cnt += assumps.size(); fprintf(f, "p cnf %d %d\n", max, cnt); - for (int i = 0; i < assumptions.size(); i++){ - assert(value(assumptions[i]) != l_False); - fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1); + for (int i = 0; i < assumps.size(); i++){ + assert(value(assumps[i]) != l_False); + fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1); } for (int i = 0; i < clauses.size(); i++) @@ -940,4 +1047,3 @@ void Solver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } - diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index f364a2937..33d1900c9 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -27,6 +27,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Alg.h" #include "prop/bvminisat/utils/Options.h" +#include "context/cdhashmap.h" + +#include <ext/hash_set> +#include <vector> namespace BVMinisat { @@ -38,7 +42,7 @@ public: // Constructor/Destructor: // - Solver(); + Solver(CVC4::context::Context* c); virtual ~Solver(); // Problem specification: @@ -63,6 +67,8 @@ public: bool solve (Lit p, Lit q); // Search for a model that respects two assumptions. bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state + lbool assertAssumption(Lit p, bool propagate); // Assert a new assumption, start BCP if propagate = true + void popAssumption(); // Pop an assumption void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec<Lit>& assumps); @@ -138,7 +144,20 @@ public: uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts; uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; - + // Bitvector Propagations + // + + void addMarkerLiteral(Var var) { + marker[var] = 1; + } + + __gnu_cxx::hash_set<Var> assumptions_vars; // all the variables that appear in the current assumptions + vec<Lit> atom_propagations; // the atom literals implied by the last call to solve with assumptions + vec<int> atom_propagations_lim; // for backtracking + + bool only_bcp; // solving mode in which only boolean constraint propagation is done + void setOnlyBCP (bool val) { only_bcp = val;} + void explainPropagation(Lit l, std::vector<Lit>& explanation); protected: // Helper structures: @@ -179,6 +198,7 @@ protected: watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec<lbool> assigns; // The current assignments. vec<char> polarity; // The preferred polarity of each variable. + vec<char> marker; // Is the variable a marker literal vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic. vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. @@ -220,10 +240,19 @@ protected: bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise. CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause. void cancelUntil (int level); // Backtrack until a certain level. - void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) + + enum UIP { + UIP_FIRST, + UIP_LAST + }; + + CVC4::context::CDHashMap<Lit, std::vector<Lit>, LitHashFunction> d_explanations; + + void storeExplanation (Lit p); // make sure that the explanation of p is cached + void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST); // (bt = backtrack) void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - lbool search (int nof_conflicts); // Search for a given number of conflicts. + lbool search (int nof_conflicts, UIP uip = UIP_FIRST); // Search for a given number of conflicts. lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). void reduceDB (); // Reduce the set of learnt clauses. void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses. @@ -275,8 +304,8 @@ protected: //================================================================================================= // Implementation of inline methods: -inline CRef Solver::reason(Var x) const { return vardata[x].reason; } -inline int Solver::level (Var x) const { return vardata[x].level; } +inline CRef Solver::reason(Var x) const { assert(x < vardata.size()); return vardata[x].reason; } +inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; } inline void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } @@ -315,7 +344,7 @@ inline bool Solver::addClause (Lit p) { add_tmp.clear( inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); atom_propagations_lim.push(atom_propagations.size()); } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index 0439a46c4..89ffc8a00 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -53,7 +53,6 @@ struct Lit { bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering. }; - inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } @@ -61,9 +60,15 @@ inline bool sign (Lit p) { return p.x & 1; } inline int var (Lit p) { return p.x >> 1; } // Mapping Literals to and from compact integers suitable for array indexing: -inline int toInt (Var v) { return v; } -inline int toInt (Lit p) { return p.x; } -inline Lit toLit (int i) { Lit p; p.x = i; return p; } +inline int toInt (Var v) { return v; } +inline int toInt (Lit p) { return p.x; } +inline Lit toLit (int i) { Lit p; p.x = i; return p; } + +struct LitHashFunction { + size_t operator () (const Lit& l) const { + return toInt(l); + } +}; //const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants. //const Lit lit_Error = mkLit(var_Undef, true ); // } diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 4af756456..903ffa270 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -43,8 +43,9 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of // Constructor/Destructor: -SimpSolver::SimpSolver() : - grow (opt_grow) +SimpSolver::SimpSolver(CVC4::context::Context* c) : + Solver(c) + , grow (opt_grow) , clause_lim (opt_clause_lim) , subsumption_lim (opt_subsumption_lim) , simp_garbage_frac (opt_simp_garbage_frac) @@ -99,7 +100,13 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) { lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { + vec<Lit> atom_propagations_backup; + atom_propagations.moveTo(atom_propagations_backup); + vec<int> atom_propagations_lim_backup; + atom_propagations_lim.moveTo(atom_propagations_lim_backup); + only_bcp = false; + cancelUntil(0); vec<Var> extra_frozen; lbool result = l_True; @@ -128,8 +135,8 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) else if (verbosity >= 1) printf("===============================================================================\n"); - if (result == l_True) - extendModel(); + atom_propagations_backup.moveTo(atom_propagations); + atom_propagations_lim_backup.moveTo(atom_propagations_lim); if (do_simp) // Unfreeze the assumptions that were frozen: diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index e21a0a9ec..e3ef76212 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Queue.h" #include "prop/bvminisat/core/Solver.h" #include "util/stats.h" +#include "context/context.h" namespace BVMinisat { @@ -34,7 +35,7 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(); + SimpSolver(CVC4::context::Context* c); ~SimpSolver(); // Problem specification: @@ -95,7 +96,8 @@ class SimpSolver : public Solver { int merges; int asymm_lits; int eliminated_vars; - CVC4::TimerStat total_eliminate_time; + CVC4::TimerStat total_eliminate_time; + protected: // Helper structures: @@ -181,12 +183,14 @@ inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } -inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ - budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ + budgetOff(); assumps.copyTo(assumptions); + return solve_(do_simp, turn_off_simp) == l_True; +} inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } diff --git a/src/prop/cryptominisat/MTRand/Makefile.in b/src/prop/cryptominisat/MTRand/Makefile.in index 8cc478cdf..1693a70f2 100644 --- a/src/prop/cryptominisat/MTRand/Makefile.in +++ b/src/prop/cryptominisat/MTRand/Makefile.in @@ -34,17 +34,36 @@ PRE_UNINSTALL = : POST_UNINSTALL = : build_triplet = @build@ host_triplet = @host@ -subdir = MTRand +target_triplet = @target@ +subdir = src/prop/cryptominisat/MTRand DIST_COMMON = $(pkgincludesub_HEADERS) $(srcdir)/Makefile.am \ $(srcdir)/Makefile.in ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/configure.in +am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ + $(top_srcdir)/config/ax_prog_doxygen.m4 \ + $(top_srcdir)/config/ax_tls.m4 \ + $(top_srcdir)/config/bindings.m4 $(top_srcdir)/config/boost.m4 \ + $(top_srcdir)/config/cudd.m4 $(top_srcdir)/config/cvc4.m4 \ + $(top_srcdir)/config/gcc_version.m4 \ + $(top_srcdir)/config/libtool.m4 \ + $(top_srcdir)/config/ltoptions.m4 \ + $(top_srcdir)/config/ltsugar.m4 \ + $(top_srcdir)/config/ltversion.m4 \ + $(top_srcdir)/config/lt~obsolete.m4 \ + $(top_srcdir)/config/pkg.m4 $(top_srcdir)/config/readline.m4 \ + $(top_srcdir)/configure.ac am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ $(ACLOCAL_M4) mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = $(top_builddir)/config.h +CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ SOURCES = DIST_SOURCES = am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; @@ -75,54 +94,128 @@ CTAGS = ctags DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) ACLOCAL = @ACLOCAL@ AMTAR = @AMTAR@ +AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +ANTLR = @ANTLR@ +ANTLR_HOME = @ANTLR_HOME@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ AR = @AR@ +AS = @AS@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BOOST_CPPFLAGS = @BOOST_CPPFLAGS@ +BOOST_LDPATH = @BOOST_LDPATH@ +BOOST_ROOT = @BOOST_ROOT@ +BOOST_THREAD_LDFLAGS = @BOOST_THREAD_LDFLAGS@ +BOOST_THREAD_LDPATH = @BOOST_THREAD_LDPATH@ +BOOST_THREAD_LIBS = @BOOST_THREAD_LIBS@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ +CAMLP4O = @CAMLP4O@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ +CLN_CFLAGS = @CLN_CFLAGS@ +CLN_LIBS = @CLN_LIBS@ CPP = @CPP@ CPPFLAGS = @CPPFLAGS@ +CSHARP_CPPFLAGS = @CSHARP_CPPFLAGS@ +CUDD_CPPFLAGS = @CUDD_CPPFLAGS@ +CUDD_LDFLAGS = @CUDD_LDFLAGS@ +CUDD_LIBS = @CUDD_LIBS@ +CVC4_BINDINGS_LIBRARY_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ +CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ +CVC4_COMPAT_LIBRARY_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ +CVC4_HAS_THREADS = @CVC4_HAS_THREADS@ +CVC4_LANGUAGE_BINDINGS = @CVC4_LANGUAGE_BINDINGS@ +CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ +CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ +CVC4_TLS = @CVC4_TLS@ +CVC4_TLS_SUPPORTED = @CVC4_TLS_SUPPORTED@ +CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@ +CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ +CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ DEPDIR = @DEPDIR@ +DISTCHECK_CONFIGURE_FLAGS = @DISTCHECK_CONFIGURE_FLAGS@ DLLTOOL = @DLLTOOL@ +DOXYGEN_EXTRACT_PRIVATE = @DOXYGEN_EXTRACT_PRIVATE@ +DOXYGEN_EXTRACT_STATIC = @DOXYGEN_EXTRACT_STATIC@ +DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@ DSYMUTIL = @DSYMUTIL@ DUMPBIN = @DUMPBIN@ +DX_CONFIG = @DX_CONFIG@ +DX_DOCDIR = @DX_DOCDIR@ +DX_DOT = @DX_DOT@ +DX_DOXYGEN = @DX_DOXYGEN@ +DX_DVIPS = @DX_DVIPS@ +DX_EGREP = @DX_EGREP@ +DX_ENV = @DX_ENV@ +DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@ +DX_FLAG_chi = @DX_FLAG_chi@ +DX_FLAG_chm = @DX_FLAG_chm@ +DX_FLAG_doc = @DX_FLAG_doc@ +DX_FLAG_dot = @DX_FLAG_dot@ +DX_FLAG_html = @DX_FLAG_html@ +DX_FLAG_man = @DX_FLAG_man@ +DX_FLAG_pdf = @DX_FLAG_pdf@ +DX_FLAG_ps = @DX_FLAG_ps@ +DX_FLAG_rtf = @DX_FLAG_rtf@ +DX_FLAG_xml = @DX_FLAG_xml@ +DX_HHC = @DX_HHC@ +DX_LATEX = @DX_LATEX@ +DX_MAKEINDEX = @DX_MAKEINDEX@ +DX_PDFLATEX = @DX_PDFLATEX@ +DX_PERL = @DX_PERL@ +DX_PROJECT = @DX_PROJECT@ ECHO_C = @ECHO_C@ ECHO_N = @ECHO_N@ ECHO_T = @ECHO_T@ EGREP = @EGREP@ EXEEXT = @EXEEXT@ FGREP = @FGREP@ +FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@ GREP = @GREP@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ INSTALL_PROGRAM = @INSTALL_PROGRAM@ INSTALL_SCRIPT = @INSTALL_SCRIPT@ INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +JAR = @JAR@ +JAVA = @JAVA@ +JAVAC = @JAVAC@ +JAVAH = @JAVAH@ +JAVA_CPPFLAGS = @JAVA_CPPFLAGS@ LD = @LD@ LDFLAGS = @LDFLAGS@ +LFSC = @LFSC@ +LFSCARGS = @LFSCARGS@ LIBOBJS = @LIBOBJS@ LIBS = @LIBS@ LIBTOOL = @LIBTOOL@ LIPO = @LIPO@ LN_S = @LN_S@ LTLIBOBJS = @LTLIBOBJS@ +MAINT = @MAINT@ MAKEINFO = @MAKEINFO@ MANIFEST_TOOL = @MANIFEST_TOOL@ +MAN_DATE = @MAN_DATE@ MKDIR_P = @MKDIR_P@ NM = @NM@ NMEDIT = @NMEDIT@ OBJDUMP = @OBJDUMP@ OBJEXT = @OBJEXT@ -OPENMP_CXXFLAGS = @OPENMP_CXXFLAGS@ +OCAMLC = @OCAMLC@ +OCAMLFIND = @OCAMLFIND@ +OCAMLMKTOP = @OCAMLMKTOP@ OTOOL = @OTOOL@ OTOOL64 = @OTOOL64@ PACKAGE = @PACKAGE@ @@ -133,12 +226,33 @@ PACKAGE_TARNAME = @PACKAGE_TARNAME@ PACKAGE_URL = @PACKAGE_URL@ PACKAGE_VERSION = @PACKAGE_VERSION@ PATH_SEPARATOR = @PATH_SEPARATOR@ +PERL = @PERL@ +PERL_CPPFLAGS = @PERL_CPPFLAGS@ +PHP_CPPFLAGS = @PHP_CPPFLAGS@ +PKG_CONFIG = @PKG_CONFIG@ +PYTHON = @PYTHON@ +PYTHON_CONFIG = @PYTHON_CONFIG@ +PYTHON_CXXFLAGS = @PYTHON_CXXFLAGS@ +PYTHON_EXEC_PREFIX = @PYTHON_EXEC_PREFIX@ +PYTHON_INCLUDE = @PYTHON_INCLUDE@ +PYTHON_PLATFORM = @PYTHON_PLATFORM@ +PYTHON_PREFIX = @PYTHON_PREFIX@ +PYTHON_VERSION = @PYTHON_VERSION@ RANLIB = @RANLIB@ +READLINE_LIBS = @READLINE_LIBS@ +RUBY_CPPFLAGS = @RUBY_CPPFLAGS@ SED = @SED@ SET_MAKE = @SET_MAKE@ SHELL = @SHELL@ +STATIC_BINARY = @STATIC_BINARY@ STRIP = @STRIP@ +SWIG = @SWIG@ +TCL_CPPFLAGS = @TCL_CPPFLAGS@ +TEST_CPPFLAGS = @TEST_CPPFLAGS@ +TEST_CXXFLAGS = @TEST_CXXFLAGS@ +TEST_LDFLAGS = @TEST_LDFLAGS@ VERSION = @VERSION@ +WNO_CONVERSION_NULL = @WNO_CONVERSION_NULL@ abs_builddir = @abs_builddir@ abs_srcdir = @abs_srcdir@ abs_top_builddir = @abs_top_builddir@ @@ -178,17 +292,26 @@ libexecdir = @libexecdir@ localedir = @localedir@ localstatedir = @localstatedir@ mandir = @mandir@ +mk_include = @mk_include@ mkdir_p = @mkdir_p@ oldincludedir = @oldincludedir@ pdfdir = @pdfdir@ +pkgpyexecdir = @pkgpyexecdir@ +pkgpythondir = @pkgpythondir@ prefix = @prefix@ program_transform_name = @program_transform_name@ psdir = @psdir@ +pyexecdir = @pyexecdir@ +pythondir = @pythondir@ sbindir = @sbindir@ sharedstatedir = @sharedstatedir@ srcdir = @srcdir@ sysconfdir = @sysconfdir@ +target = @target@ target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ @@ -197,7 +320,7 @@ pkgincludesub_HEADERS = MersenneTwister.h all: all-am .SUFFIXES: -$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) +$(srcdir)/Makefile.in: @MAINTAINER_MODE_TRUE@ $(srcdir)/Makefile.am $(am__configure_deps) @for dep in $?; do \ case '$(am__configure_deps)' in \ *$$dep*) \ @@ -206,9 +329,9 @@ $(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) exit 1;; \ esac; \ done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu MTRand/Makefile'; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/prop/cryptominisat/MTRand/Makefile'; \ $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --gnu MTRand/Makefile + $(AUTOMAKE) --foreign src/prop/cryptominisat/MTRand/Makefile .PRECIOUS: Makefile Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status @case '$?' in \ @@ -222,9 +345,9 @@ Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status $(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(top_srcdir)/configure: $(am__configure_deps) +$(top_srcdir)/configure: @MAINTAINER_MODE_TRUE@ $(am__configure_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(ACLOCAL_M4): $(am__aclocal_m4_deps) +$(ACLOCAL_M4): @MAINTAINER_MODE_TRUE@ $(am__aclocal_m4_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh $(am__aclocal_m4_deps): diff --git a/src/prop/cryptominisat/Makefile.in b/src/prop/cryptominisat/Makefile.in index 2d9ee8bf8..a6806f0b4 100644 --- a/src/prop/cryptominisat/Makefile.in +++ b/src/prop/cryptominisat/Makefile.in @@ -33,21 +33,37 @@ PRE_UNINSTALL = : POST_UNINSTALL = : build_triplet = @build@ host_triplet = @host@ -subdir = . -DIST_COMMON = README $(am__configure_deps) $(srcdir)/Makefile.am \ - $(srcdir)/Makefile.in $(srcdir)/config.h.in \ - $(top_srcdir)/configure AUTHORS INSTALL NEWS TODO config.guess \ - config.sub depcomp install-sh ltmain.sh missing +target_triplet = @target@ +subdir = src/prop/cryptominisat +DIST_COMMON = README $(srcdir)/Makefile.am $(srcdir)/Makefile.in \ + AUTHORS INSTALL NEWS TODO config.guess config.sub depcomp \ + install-sh ltmain.sh missing ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/configure.in +am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ + $(top_srcdir)/config/ax_prog_doxygen.m4 \ + $(top_srcdir)/config/ax_tls.m4 \ + $(top_srcdir)/config/bindings.m4 $(top_srcdir)/config/boost.m4 \ + $(top_srcdir)/config/cudd.m4 $(top_srcdir)/config/cvc4.m4 \ + $(top_srcdir)/config/gcc_version.m4 \ + $(top_srcdir)/config/libtool.m4 \ + $(top_srcdir)/config/ltoptions.m4 \ + $(top_srcdir)/config/ltsugar.m4 \ + $(top_srcdir)/config/ltversion.m4 \ + $(top_srcdir)/config/lt~obsolete.m4 \ + $(top_srcdir)/config/pkg.m4 $(top_srcdir)/config/readline.m4 \ + $(top_srcdir)/configure.ac am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ $(ACLOCAL_M4) -am__CONFIG_DISTCLEAN_FILES = config.status config.cache config.log \ - configure.lineno config.status.lineno mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = config.h +CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ SOURCES = DIST_SOURCES = RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \ @@ -61,17 +77,11 @@ RECURSIVE_CLEAN_TARGETS = mostlyclean-recursive clean-recursive \ distclean-recursive maintainer-clean-recursive AM_RECURSIVE_TARGETS = $(RECURSIVE_TARGETS:-recursive=) \ $(RECURSIVE_CLEAN_TARGETS:-recursive=) tags TAGS ctags CTAGS \ - distdir dist dist-all distcheck + distdir ETAGS = etags CTAGS = ctags DIST_SUBDIRS = $(SUBDIRS) DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) -distdir = $(PACKAGE)-$(VERSION) -top_distdir = $(distdir) -am__remove_distdir = \ - { test ! -d "$(distdir)" \ - || { find "$(distdir)" -type d ! -perm -200 -exec chmod u+w {} ';' \ - && rm -fr "$(distdir)"; }; } am__relativize = \ dir0=`pwd`; \ sed_first='s,^\([^/]*\)/.*$$,\1,'; \ @@ -97,60 +107,130 @@ am__relativize = \ dir1=`echo "$$dir1" | sed -e "$$sed_rest"`; \ done; \ reldir="$$dir2" -DIST_ARCHIVES = $(distdir).tar.gz -GZIP_ENV = --best -distuninstallcheck_listfiles = find . -type f -print -distcleancheck_listfiles = find . -type f -print ACLOCAL = @ACLOCAL@ AMTAR = @AMTAR@ +AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +ANTLR = @ANTLR@ +ANTLR_HOME = @ANTLR_HOME@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ AR = @AR@ +AS = @AS@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BOOST_CPPFLAGS = @BOOST_CPPFLAGS@ +BOOST_LDPATH = @BOOST_LDPATH@ +BOOST_ROOT = @BOOST_ROOT@ +BOOST_THREAD_LDFLAGS = @BOOST_THREAD_LDFLAGS@ +BOOST_THREAD_LDPATH = @BOOST_THREAD_LDPATH@ +BOOST_THREAD_LIBS = @BOOST_THREAD_LIBS@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ +CAMLP4O = @CAMLP4O@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ +CLN_CFLAGS = @CLN_CFLAGS@ +CLN_LIBS = @CLN_LIBS@ CPP = @CPP@ CPPFLAGS = @CPPFLAGS@ +CSHARP_CPPFLAGS = @CSHARP_CPPFLAGS@ +CUDD_CPPFLAGS = @CUDD_CPPFLAGS@ +CUDD_LDFLAGS = @CUDD_LDFLAGS@ +CUDD_LIBS = @CUDD_LIBS@ +CVC4_BINDINGS_LIBRARY_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ +CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ +CVC4_COMPAT_LIBRARY_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ +CVC4_HAS_THREADS = @CVC4_HAS_THREADS@ +CVC4_LANGUAGE_BINDINGS = @CVC4_LANGUAGE_BINDINGS@ +CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ +CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ +CVC4_TLS = @CVC4_TLS@ +CVC4_TLS_SUPPORTED = @CVC4_TLS_SUPPORTED@ +CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@ +CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ +CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ DEPDIR = @DEPDIR@ +DISTCHECK_CONFIGURE_FLAGS = @DISTCHECK_CONFIGURE_FLAGS@ DLLTOOL = @DLLTOOL@ +DOXYGEN_EXTRACT_PRIVATE = @DOXYGEN_EXTRACT_PRIVATE@ +DOXYGEN_EXTRACT_STATIC = @DOXYGEN_EXTRACT_STATIC@ +DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@ DSYMUTIL = @DSYMUTIL@ DUMPBIN = @DUMPBIN@ +DX_CONFIG = @DX_CONFIG@ +DX_DOCDIR = @DX_DOCDIR@ +DX_DOT = @DX_DOT@ +DX_DOXYGEN = @DX_DOXYGEN@ +DX_DVIPS = @DX_DVIPS@ +DX_EGREP = @DX_EGREP@ +DX_ENV = @DX_ENV@ +DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@ +DX_FLAG_chi = @DX_FLAG_chi@ +DX_FLAG_chm = @DX_FLAG_chm@ +DX_FLAG_doc = @DX_FLAG_doc@ +DX_FLAG_dot = @DX_FLAG_dot@ +DX_FLAG_html = @DX_FLAG_html@ +DX_FLAG_man = @DX_FLAG_man@ +DX_FLAG_pdf = @DX_FLAG_pdf@ +DX_FLAG_ps = @DX_FLAG_ps@ +DX_FLAG_rtf = @DX_FLAG_rtf@ +DX_FLAG_xml = @DX_FLAG_xml@ +DX_HHC = @DX_HHC@ +DX_LATEX = @DX_LATEX@ +DX_MAKEINDEX = @DX_MAKEINDEX@ +DX_PDFLATEX = @DX_PDFLATEX@ +DX_PERL = @DX_PERL@ +DX_PROJECT = @DX_PROJECT@ ECHO_C = @ECHO_C@ ECHO_N = @ECHO_N@ ECHO_T = @ECHO_T@ EGREP = @EGREP@ EXEEXT = @EXEEXT@ FGREP = @FGREP@ +FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@ GREP = @GREP@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ INSTALL_PROGRAM = @INSTALL_PROGRAM@ INSTALL_SCRIPT = @INSTALL_SCRIPT@ INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +JAR = @JAR@ +JAVA = @JAVA@ +JAVAC = @JAVAC@ +JAVAH = @JAVAH@ +JAVA_CPPFLAGS = @JAVA_CPPFLAGS@ LD = @LD@ LDFLAGS = @LDFLAGS@ +LFSC = @LFSC@ +LFSCARGS = @LFSCARGS@ LIBOBJS = @LIBOBJS@ LIBS = @LIBS@ LIBTOOL = @LIBTOOL@ LIPO = @LIPO@ LN_S = @LN_S@ LTLIBOBJS = @LTLIBOBJS@ +MAINT = @MAINT@ MAKEINFO = @MAKEINFO@ MANIFEST_TOOL = @MANIFEST_TOOL@ +MAN_DATE = @MAN_DATE@ MKDIR_P = @MKDIR_P@ NM = @NM@ NMEDIT = @NMEDIT@ OBJDUMP = @OBJDUMP@ OBJEXT = @OBJEXT@ -OPENMP_CXXFLAGS = @OPENMP_CXXFLAGS@ +OCAMLC = @OCAMLC@ +OCAMLFIND = @OCAMLFIND@ +OCAMLMKTOP = @OCAMLMKTOP@ OTOOL = @OTOOL@ OTOOL64 = @OTOOL64@ PACKAGE = @PACKAGE@ @@ -161,12 +241,33 @@ PACKAGE_TARNAME = @PACKAGE_TARNAME@ PACKAGE_URL = @PACKAGE_URL@ PACKAGE_VERSION = @PACKAGE_VERSION@ PATH_SEPARATOR = @PATH_SEPARATOR@ +PERL = @PERL@ +PERL_CPPFLAGS = @PERL_CPPFLAGS@ +PHP_CPPFLAGS = @PHP_CPPFLAGS@ +PKG_CONFIG = @PKG_CONFIG@ +PYTHON = @PYTHON@ +PYTHON_CONFIG = @PYTHON_CONFIG@ +PYTHON_CXXFLAGS = @PYTHON_CXXFLAGS@ +PYTHON_EXEC_PREFIX = @PYTHON_EXEC_PREFIX@ +PYTHON_INCLUDE = @PYTHON_INCLUDE@ +PYTHON_PLATFORM = @PYTHON_PLATFORM@ +PYTHON_PREFIX = @PYTHON_PREFIX@ +PYTHON_VERSION = @PYTHON_VERSION@ RANLIB = @RANLIB@ +READLINE_LIBS = @READLINE_LIBS@ +RUBY_CPPFLAGS = @RUBY_CPPFLAGS@ SED = @SED@ SET_MAKE = @SET_MAKE@ SHELL = @SHELL@ +STATIC_BINARY = @STATIC_BINARY@ STRIP = @STRIP@ +SWIG = @SWIG@ +TCL_CPPFLAGS = @TCL_CPPFLAGS@ +TEST_CPPFLAGS = @TEST_CPPFLAGS@ +TEST_CXXFLAGS = @TEST_CXXFLAGS@ +TEST_LDFLAGS = @TEST_LDFLAGS@ VERSION = @VERSION@ +WNO_CONVERSION_NULL = @WNO_CONVERSION_NULL@ abs_builddir = @abs_builddir@ abs_srcdir = @abs_srcdir@ abs_top_builddir = @abs_top_builddir@ @@ -206,17 +307,26 @@ libexecdir = @libexecdir@ localedir = @localedir@ localstatedir = @localstatedir@ mandir = @mandir@ +mk_include = @mk_include@ mkdir_p = @mkdir_p@ oldincludedir = @oldincludedir@ pdfdir = @pdfdir@ +pkgpyexecdir = @pkgpyexecdir@ +pkgpythondir = @pkgpythondir@ prefix = @prefix@ program_transform_name = @program_transform_name@ psdir = @psdir@ +pyexecdir = @pyexecdir@ +pythondir = @pythondir@ sbindir = @sbindir@ sharedstatedir = @sharedstatedir@ srcdir = @srcdir@ sysconfdir = @sysconfdir@ +target = @target@ target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ @@ -229,71 +339,46 @@ SUBDIRS = Solver mtl MTRand man EXTRA_DIST = HOWTO_VisualCpp HOWTO_MinGW32 \ LICENSE-GPL LICENSE-MIT TODO -all: config.h - $(MAKE) $(AM_MAKEFLAGS) all-recursive +all: all-recursive .SUFFIXES: -am--refresh: - @: -$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) +$(srcdir)/Makefile.in: @MAINTAINER_MODE_TRUE@ $(srcdir)/Makefile.am $(am__configure_deps) @for dep in $?; do \ case '$(am__configure_deps)' in \ *$$dep*) \ - echo ' cd $(srcdir) && $(AUTOMAKE) --foreign'; \ - $(am__cd) $(srcdir) && $(AUTOMAKE) --foreign \ - && exit 0; \ + ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \ + && { if test -f $@; then exit 0; else break; fi; }; \ exit 1;; \ esac; \ done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign Makefile'; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/prop/cryptominisat/Makefile'; \ $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --foreign Makefile + $(AUTOMAKE) --foreign src/prop/cryptominisat/Makefile .PRECIOUS: Makefile Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status @case '$?' in \ *config.status*) \ - echo ' $(SHELL) ./config.status'; \ - $(SHELL) ./config.status;; \ + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \ *) \ - echo ' cd $(top_builddir) && $(SHELL) ./config.status $@ $(am__depfiles_maybe)'; \ - cd $(top_builddir) && $(SHELL) ./config.status $@ $(am__depfiles_maybe);; \ + echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \ + cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \ esac; $(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) - $(SHELL) ./config.status --recheck + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(top_srcdir)/configure: $(am__configure_deps) - $(am__cd) $(srcdir) && $(AUTOCONF) -$(ACLOCAL_M4): $(am__aclocal_m4_deps) - $(am__cd) $(srcdir) && $(ACLOCAL) $(ACLOCAL_AMFLAGS) +$(top_srcdir)/configure: @MAINTAINER_MODE_TRUE@ $(am__configure_deps) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh +$(ACLOCAL_M4): @MAINTAINER_MODE_TRUE@ $(am__aclocal_m4_deps) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh $(am__aclocal_m4_deps): -config.h: stamp-h1 - @if test ! -f $@; then \ - rm -f stamp-h1; \ - $(MAKE) $(AM_MAKEFLAGS) stamp-h1; \ - else :; fi - -stamp-h1: $(srcdir)/config.h.in $(top_builddir)/config.status - @rm -f stamp-h1 - cd $(top_builddir) && $(SHELL) ./config.status config.h -$(srcdir)/config.h.in: $(am__configure_deps) - ($(am__cd) $(top_srcdir) && $(AUTOHEADER)) - rm -f stamp-h1 - touch $@ - -distclean-hdr: - -rm -f config.h stamp-h1 - mostlyclean-libtool: -rm -f *.lo clean-libtool: -rm -rf .libs _libs -distclean-libtool: - -rm -f libtool config.lt - # This directory's subdirectories are mostly independent; you can cd # into them and run `make' without going through this Makefile. # To change the values of `make' variables: instead of editing Makefiles, @@ -374,7 +459,7 @@ ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES) mkid -fID $$unique tags: TAGS -TAGS: tags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \ +TAGS: tags-recursive $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ $(TAGS_FILES) $(LISP) set x; \ here=`pwd`; \ @@ -391,7 +476,7 @@ TAGS: tags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \ set "$$@" "$$include_option=$$here/$$subdir/TAGS"; \ fi; \ done; \ - list='$(SOURCES) $(HEADERS) config.h.in $(LISP) $(TAGS_FILES)'; \ + list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ unique=`for i in $$list; do \ if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ done | \ @@ -409,9 +494,9 @@ TAGS: tags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \ fi; \ fi ctags: CTAGS -CTAGS: ctags-recursive $(HEADERS) $(SOURCES) config.h.in $(TAGS_DEPENDENCIES) \ +CTAGS: ctags-recursive $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ $(TAGS_FILES) $(LISP) - list='$(SOURCES) $(HEADERS) config.h.in $(LISP) $(TAGS_FILES)'; \ + list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ unique=`for i in $$list; do \ if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ done | \ @@ -430,8 +515,6 @@ distclean-tags: -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags distdir: $(DISTFILES) - $(am__remove_distdir) - test -d "$(distdir)" || mkdir "$(distdir)" @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \ list='$(DISTFILES)'; \ @@ -489,124 +572,9 @@ distdir: $(DISTFILES) || exit 1; \ fi; \ done - -test -n "$(am__skip_mode_fix)" \ - || find "$(distdir)" -type d ! -perm -755 \ - -exec chmod u+rwx,go+rx {} \; -o \ - ! -type d ! -perm -444 -links 1 -exec chmod a+r {} \; -o \ - ! -type d ! -perm -400 -exec chmod a+r {} \; -o \ - ! -type d ! -perm -444 -exec $(install_sh) -c -m a+r {} {} \; \ - || chmod -R a+r "$(distdir)" -dist-gzip: distdir - tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz - $(am__remove_distdir) - -dist-bzip2: distdir - tardir=$(distdir) && $(am__tar) | bzip2 -9 -c >$(distdir).tar.bz2 - $(am__remove_distdir) - -dist-lzma: distdir - tardir=$(distdir) && $(am__tar) | lzma -9 -c >$(distdir).tar.lzma - $(am__remove_distdir) - -dist-xz: distdir - tardir=$(distdir) && $(am__tar) | xz -c >$(distdir).tar.xz - $(am__remove_distdir) - -dist-tarZ: distdir - tardir=$(distdir) && $(am__tar) | compress -c >$(distdir).tar.Z - $(am__remove_distdir) - -dist-shar: distdir - shar $(distdir) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).shar.gz - $(am__remove_distdir) - -dist-zip: distdir - -rm -f $(distdir).zip - zip -rq $(distdir).zip $(distdir) - $(am__remove_distdir) - -dist dist-all: distdir - tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz - $(am__remove_distdir) - -# This target untars the dist file and tries a VPATH configuration. Then -# it guarantees that the distribution is self-contained by making another -# tarfile. -distcheck: dist - case '$(DIST_ARCHIVES)' in \ - *.tar.gz*) \ - GZIP=$(GZIP_ENV) gzip -dc $(distdir).tar.gz | $(am__untar) ;;\ - *.tar.bz2*) \ - bzip2 -dc $(distdir).tar.bz2 | $(am__untar) ;;\ - *.tar.lzma*) \ - lzma -dc $(distdir).tar.lzma | $(am__untar) ;;\ - *.tar.xz*) \ - xz -dc $(distdir).tar.xz | $(am__untar) ;;\ - *.tar.Z*) \ - uncompress -c $(distdir).tar.Z | $(am__untar) ;;\ - *.shar.gz*) \ - GZIP=$(GZIP_ENV) gzip -dc $(distdir).shar.gz | unshar ;;\ - *.zip*) \ - unzip $(distdir).zip ;;\ - esac - chmod -R a-w $(distdir); chmod a+w $(distdir) - mkdir $(distdir)/_build - mkdir $(distdir)/_inst - chmod a-w $(distdir) - test -d $(distdir)/_build || exit 0; \ - dc_install_base=`$(am__cd) $(distdir)/_inst && pwd | sed -e 's,^[^:\\/]:[\\/],/,'` \ - && dc_destdir="$${TMPDIR-/tmp}/am-dc-$$$$/" \ - && am__cwd=`pwd` \ - && $(am__cd) $(distdir)/_build \ - && ../configure --srcdir=.. --prefix="$$dc_install_base" \ - $(DISTCHECK_CONFIGURE_FLAGS) \ - && $(MAKE) $(AM_MAKEFLAGS) \ - && $(MAKE) $(AM_MAKEFLAGS) dvi \ - && $(MAKE) $(AM_MAKEFLAGS) check \ - && $(MAKE) $(AM_MAKEFLAGS) install \ - && $(MAKE) $(AM_MAKEFLAGS) installcheck \ - && $(MAKE) $(AM_MAKEFLAGS) uninstall \ - && $(MAKE) $(AM_MAKEFLAGS) distuninstallcheck_dir="$$dc_install_base" \ - distuninstallcheck \ - && chmod -R a-w "$$dc_install_base" \ - && ({ \ - (cd ../.. && umask 077 && mkdir "$$dc_destdir") \ - && $(MAKE) $(AM_MAKEFLAGS) DESTDIR="$$dc_destdir" install \ - && $(MAKE) $(AM_MAKEFLAGS) DESTDIR="$$dc_destdir" uninstall \ - && $(MAKE) $(AM_MAKEFLAGS) DESTDIR="$$dc_destdir" \ - distuninstallcheck_dir="$$dc_destdir" distuninstallcheck; \ - } || { rm -rf "$$dc_destdir"; exit 1; }) \ - && rm -rf "$$dc_destdir" \ - && $(MAKE) $(AM_MAKEFLAGS) dist \ - && rm -rf $(DIST_ARCHIVES) \ - && $(MAKE) $(AM_MAKEFLAGS) distcleancheck \ - && cd "$$am__cwd" \ - || exit 1 - $(am__remove_distdir) - @(echo "$(distdir) archives ready for distribution: "; \ - list='$(DIST_ARCHIVES)'; for i in $$list; do echo $$i; done) | \ - sed -e 1h -e 1s/./=/g -e 1p -e 1x -e '$$p' -e '$$x' -distuninstallcheck: - @$(am__cd) '$(distuninstallcheck_dir)' \ - && test `$(distuninstallcheck_listfiles) | wc -l` -le 1 \ - || { echo "ERROR: files left after uninstall:" ; \ - if test -n "$(DESTDIR)"; then \ - echo " (check DESTDIR support)"; \ - fi ; \ - $(distuninstallcheck_listfiles) ; \ - exit 1; } >&2 -distcleancheck: distclean - @if test '$(srcdir)' = . ; then \ - echo "ERROR: distcleancheck can only run from a VPATH build" ; \ - exit 1 ; \ - fi - @test `$(distcleancheck_listfiles) | wc -l` -eq 0 \ - || { echo "ERROR: files left in build directory after distclean:" ; \ - $(distcleancheck_listfiles) ; \ - exit 1; } >&2 check-am: all-am check: check-recursive -all-am: Makefile config.h all-local +all-am: Makefile all-local installdirs: installdirs-recursive installdirs-am: install: install-recursive @@ -639,10 +607,8 @@ clean: clean-recursive clean-am: clean-generic clean-libtool mostlyclean-am distclean: distclean-recursive - -rm -f $(am__CONFIG_DISTCLEAN_FILES) -rm -f Makefile -distclean-am: clean-am distclean-generic distclean-hdr \ - distclean-libtool distclean-tags +distclean-am: clean-am distclean-generic distclean-tags dvi: dvi-recursive @@ -685,8 +651,6 @@ install-ps-am: installcheck-am: maintainer-clean: maintainer-clean-recursive - -rm -f $(am__CONFIG_DISTCLEAN_FILES) - -rm -rf $(top_srcdir)/autom4te.cache -rm -f Makefile maintainer-clean-am: distclean-am maintainer-clean-generic @@ -704,25 +668,22 @@ ps-am: uninstall-am: -.MAKE: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) all \ - ctags-recursive install-am install-strip tags-recursive +.MAKE: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) ctags-recursive \ + install-am install-strip tags-recursive .PHONY: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) CTAGS GTAGS \ - all all-am all-local am--refresh check check-am clean \ - clean-generic clean-libtool ctags ctags-recursive dist \ - dist-all dist-bzip2 dist-gzip dist-lzma dist-shar dist-tarZ \ - dist-xz dist-zip distcheck distclean distclean-generic \ - distclean-hdr distclean-libtool distclean-tags distcleancheck \ - distdir distuninstallcheck dvi dvi-am html html-am info \ - info-am install install-am install-data install-data-am \ - install-dvi install-dvi-am install-exec install-exec-am \ - install-html install-html-am install-info install-info-am \ - install-man install-pdf install-pdf-am install-ps \ - install-ps-am install-strip installcheck installcheck-am \ - installdirs installdirs-am maintainer-clean \ - maintainer-clean-generic mostlyclean mostlyclean-generic \ - mostlyclean-libtool pdf pdf-am ps ps-am tags tags-recursive \ - uninstall uninstall-am + all all-am all-local check check-am clean clean-generic \ + clean-libtool ctags ctags-recursive distclean \ + distclean-generic distclean-libtool distclean-tags distdir dvi \ + dvi-am html html-am info info-am install install-am \ + install-data install-data-am install-dvi install-dvi-am \ + install-exec install-exec-am install-html install-html-am \ + install-info install-info-am install-man install-pdf \ + install-pdf-am install-ps install-ps-am install-strip \ + installcheck installcheck-am installdirs installdirs-am \ + maintainer-clean maintainer-clean-generic mostlyclean \ + mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \ + tags tags-recursive uninstall uninstall-am all-local: Solver diff --git a/src/prop/cryptominisat/Solver/Makefile.in b/src/prop/cryptominisat/Solver/Makefile.in index dd524fba2..02344edd7 100644 --- a/src/prop/cryptominisat/Solver/Makefile.in +++ b/src/prop/cryptominisat/Solver/Makefile.in @@ -36,16 +36,29 @@ PRE_UNINSTALL = : POST_UNINSTALL = : build_triplet = @build@ host_triplet = @host@ +target_triplet = @target@ bin_PROGRAMS = cryptominisat$(EXEEXT) -subdir = Solver +subdir = src/prop/cryptominisat/Solver DIST_COMMON = $(pkgincludesub_HEADERS) $(srcdir)/Makefile.am \ $(srcdir)/Makefile.in ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/configure.in +am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ + $(top_srcdir)/config/ax_prog_doxygen.m4 \ + $(top_srcdir)/config/ax_tls.m4 \ + $(top_srcdir)/config/bindings.m4 $(top_srcdir)/config/boost.m4 \ + $(top_srcdir)/config/cudd.m4 $(top_srcdir)/config/cvc4.m4 \ + $(top_srcdir)/config/gcc_version.m4 \ + $(top_srcdir)/config/libtool.m4 \ + $(top_srcdir)/config/ltoptions.m4 \ + $(top_srcdir)/config/ltsugar.m4 \ + $(top_srcdir)/config/ltversion.m4 \ + $(top_srcdir)/config/lt~obsolete.m4 \ + $(top_srcdir)/config/pkg.m4 $(top_srcdir)/config/readline.m4 \ + $(top_srcdir)/configure.ac am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ $(ACLOCAL_M4) mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = $(top_builddir)/config.h +CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; @@ -81,29 +94,47 @@ am_libcryptominisat_la_OBJECTS = ClauseCleaner.lo FailedLitSearcher.lo \ ClauseVivifier.lo CompleteDetachReattacher.lo DimacsParser.lo \ OnlyNonLearntBins.lo SolverConf.lo DataSync.lo BothCache.lo libcryptominisat_la_OBJECTS = $(am_libcryptominisat_la_OBJECTS) -libcryptominisat_la_LINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) \ - $(LIBTOOLFLAGS) --mode=link $(CXXLD) $(AM_CXXFLAGS) \ - $(CXXFLAGS) $(libcryptominisat_la_LDFLAGS) $(LDFLAGS) -o $@ +AM_V_lt = $(am__v_lt_$(V)) +am__v_lt_ = $(am__v_lt_$(AM_DEFAULT_VERBOSITY)) +am__v_lt_0 = --silent +libcryptominisat_la_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX \ + $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=link $(CXXLD) \ + $(AM_CXXFLAGS) $(CXXFLAGS) $(libcryptominisat_la_LDFLAGS) \ + $(LDFLAGS) -o $@ PROGRAMS = $(bin_PROGRAMS) am_cryptominisat_OBJECTS = Main.$(OBJEXT) cryptominisat_OBJECTS = $(am_cryptominisat_OBJECTS) cryptominisat_DEPENDENCIES = libcryptominisat.la -cryptominisat_LINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) \ - $(LIBTOOLFLAGS) --mode=link $(CXXLD) $(AM_CXXFLAGS) \ - $(CXXFLAGS) $(cryptominisat_LDFLAGS) $(LDFLAGS) -o $@ +cryptominisat_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX \ + $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=link $(CXXLD) \ + $(AM_CXXFLAGS) $(CXXFLAGS) $(cryptominisat_LDFLAGS) $(LDFLAGS) \ + -o $@ DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) -depcomp = $(SHELL) $(top_srcdir)/depcomp +depcomp = $(SHELL) $(top_srcdir)/config/depcomp am__depfiles_maybe = depfiles am__mv = mv -f CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -LTCXXCOMPILE = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ - --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ - $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) +LTCXXCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \ + $(LIBTOOLFLAGS) --mode=compile $(CXX) $(DEFS) \ + $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) \ + $(AM_CXXFLAGS) $(CXXFLAGS) +AM_V_CXX = $(am__v_CXX_$(V)) +am__v_CXX_ = $(am__v_CXX_$(AM_DEFAULT_VERBOSITY)) +am__v_CXX_0 = @echo " CXX " $@; +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ CXXLD = $(CXX) -CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ - --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \ - $(LDFLAGS) -o $@ +CXXLINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \ + $(LIBTOOLFLAGS) --mode=link $(CXXLD) $(AM_CXXFLAGS) \ + $(CXXFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@ +AM_V_CXXLD = $(am__v_CXXLD_$(V)) +am__v_CXXLD_ = $(am__v_CXXLD_$(AM_DEFAULT_VERBOSITY)) +am__v_CXXLD_0 = @echo " CXXLD " $@; +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; SOURCES = $(libcryptominisat_la_SOURCES) $(cryptominisat_SOURCES) DIST_SOURCES = $(libcryptominisat_la_SOURCES) $(cryptominisat_SOURCES) HEADERS = $(pkgincludesub_HEADERS) @@ -112,54 +143,128 @@ CTAGS = ctags DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) ACLOCAL = @ACLOCAL@ AMTAR = @AMTAR@ +AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +ANTLR = @ANTLR@ +ANTLR_HOME = @ANTLR_HOME@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ AR = @AR@ +AS = @AS@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BOOST_CPPFLAGS = @BOOST_CPPFLAGS@ +BOOST_LDPATH = @BOOST_LDPATH@ +BOOST_ROOT = @BOOST_ROOT@ +BOOST_THREAD_LDFLAGS = @BOOST_THREAD_LDFLAGS@ +BOOST_THREAD_LDPATH = @BOOST_THREAD_LDPATH@ +BOOST_THREAD_LIBS = @BOOST_THREAD_LIBS@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ +CAMLP4O = @CAMLP4O@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ +CLN_CFLAGS = @CLN_CFLAGS@ +CLN_LIBS = @CLN_LIBS@ CPP = @CPP@ CPPFLAGS = @CPPFLAGS@ +CSHARP_CPPFLAGS = @CSHARP_CPPFLAGS@ +CUDD_CPPFLAGS = @CUDD_CPPFLAGS@ +CUDD_LDFLAGS = @CUDD_LDFLAGS@ +CUDD_LIBS = @CUDD_LIBS@ +CVC4_BINDINGS_LIBRARY_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ +CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ +CVC4_COMPAT_LIBRARY_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ +CVC4_HAS_THREADS = @CVC4_HAS_THREADS@ +CVC4_LANGUAGE_BINDINGS = @CVC4_LANGUAGE_BINDINGS@ +CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ +CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ +CVC4_TLS = @CVC4_TLS@ +CVC4_TLS_SUPPORTED = @CVC4_TLS_SUPPORTED@ +CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@ +CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ +CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ DEPDIR = @DEPDIR@ +DISTCHECK_CONFIGURE_FLAGS = @DISTCHECK_CONFIGURE_FLAGS@ DLLTOOL = @DLLTOOL@ +DOXYGEN_EXTRACT_PRIVATE = @DOXYGEN_EXTRACT_PRIVATE@ +DOXYGEN_EXTRACT_STATIC = @DOXYGEN_EXTRACT_STATIC@ +DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@ DSYMUTIL = @DSYMUTIL@ DUMPBIN = @DUMPBIN@ +DX_CONFIG = @DX_CONFIG@ +DX_DOCDIR = @DX_DOCDIR@ +DX_DOT = @DX_DOT@ +DX_DOXYGEN = @DX_DOXYGEN@ +DX_DVIPS = @DX_DVIPS@ +DX_EGREP = @DX_EGREP@ +DX_ENV = @DX_ENV@ +DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@ +DX_FLAG_chi = @DX_FLAG_chi@ +DX_FLAG_chm = @DX_FLAG_chm@ +DX_FLAG_doc = @DX_FLAG_doc@ +DX_FLAG_dot = @DX_FLAG_dot@ +DX_FLAG_html = @DX_FLAG_html@ +DX_FLAG_man = @DX_FLAG_man@ +DX_FLAG_pdf = @DX_FLAG_pdf@ +DX_FLAG_ps = @DX_FLAG_ps@ +DX_FLAG_rtf = @DX_FLAG_rtf@ +DX_FLAG_xml = @DX_FLAG_xml@ +DX_HHC = @DX_HHC@ +DX_LATEX = @DX_LATEX@ +DX_MAKEINDEX = @DX_MAKEINDEX@ +DX_PDFLATEX = @DX_PDFLATEX@ +DX_PERL = @DX_PERL@ +DX_PROJECT = @DX_PROJECT@ ECHO_C = @ECHO_C@ ECHO_N = @ECHO_N@ ECHO_T = @ECHO_T@ EGREP = @EGREP@ EXEEXT = @EXEEXT@ FGREP = @FGREP@ +FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@ GREP = @GREP@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ INSTALL_PROGRAM = @INSTALL_PROGRAM@ INSTALL_SCRIPT = @INSTALL_SCRIPT@ INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +JAR = @JAR@ +JAVA = @JAVA@ +JAVAC = @JAVAC@ +JAVAH = @JAVAH@ +JAVA_CPPFLAGS = @JAVA_CPPFLAGS@ LD = @LD@ LDFLAGS = @LDFLAGS@ +LFSC = @LFSC@ +LFSCARGS = @LFSCARGS@ LIBOBJS = @LIBOBJS@ LIBS = @LIBS@ LIBTOOL = @LIBTOOL@ LIPO = @LIPO@ LN_S = @LN_S@ LTLIBOBJS = @LTLIBOBJS@ +MAINT = @MAINT@ MAKEINFO = @MAKEINFO@ MANIFEST_TOOL = @MANIFEST_TOOL@ +MAN_DATE = @MAN_DATE@ MKDIR_P = @MKDIR_P@ NM = @NM@ NMEDIT = @NMEDIT@ OBJDUMP = @OBJDUMP@ OBJEXT = @OBJEXT@ -OPENMP_CXXFLAGS = @OPENMP_CXXFLAGS@ +OCAMLC = @OCAMLC@ +OCAMLFIND = @OCAMLFIND@ +OCAMLMKTOP = @OCAMLMKTOP@ OTOOL = @OTOOL@ OTOOL64 = @OTOOL64@ PACKAGE = @PACKAGE@ @@ -170,12 +275,33 @@ PACKAGE_TARNAME = @PACKAGE_TARNAME@ PACKAGE_URL = @PACKAGE_URL@ PACKAGE_VERSION = @PACKAGE_VERSION@ PATH_SEPARATOR = @PATH_SEPARATOR@ +PERL = @PERL@ +PERL_CPPFLAGS = @PERL_CPPFLAGS@ +PHP_CPPFLAGS = @PHP_CPPFLAGS@ +PKG_CONFIG = @PKG_CONFIG@ +PYTHON = @PYTHON@ +PYTHON_CONFIG = @PYTHON_CONFIG@ +PYTHON_CXXFLAGS = @PYTHON_CXXFLAGS@ +PYTHON_EXEC_PREFIX = @PYTHON_EXEC_PREFIX@ +PYTHON_INCLUDE = @PYTHON_INCLUDE@ +PYTHON_PLATFORM = @PYTHON_PLATFORM@ +PYTHON_PREFIX = @PYTHON_PREFIX@ +PYTHON_VERSION = @PYTHON_VERSION@ RANLIB = @RANLIB@ +READLINE_LIBS = @READLINE_LIBS@ +RUBY_CPPFLAGS = @RUBY_CPPFLAGS@ SED = @SED@ SET_MAKE = @SET_MAKE@ SHELL = @SHELL@ +STATIC_BINARY = @STATIC_BINARY@ STRIP = @STRIP@ +SWIG = @SWIG@ +TCL_CPPFLAGS = @TCL_CPPFLAGS@ +TEST_CPPFLAGS = @TEST_CPPFLAGS@ +TEST_CXXFLAGS = @TEST_CXXFLAGS@ +TEST_LDFLAGS = @TEST_LDFLAGS@ VERSION = @VERSION@ +WNO_CONVERSION_NULL = @WNO_CONVERSION_NULL@ abs_builddir = @abs_builddir@ abs_srcdir = @abs_srcdir@ abs_top_builddir = @abs_top_builddir@ @@ -215,17 +341,26 @@ libexecdir = @libexecdir@ localedir = @localedir@ localstatedir = @localstatedir@ mandir = @mandir@ +mk_include = @mk_include@ mkdir_p = @mkdir_p@ oldincludedir = @oldincludedir@ pdfdir = @pdfdir@ +pkgpyexecdir = @pkgpyexecdir@ +pkgpythondir = @pkgpythondir@ prefix = @prefix@ program_transform_name = @program_transform_name@ psdir = @psdir@ +pyexecdir = @pyexecdir@ +pythondir = @pythondir@ sbindir = @sbindir@ sharedstatedir = @sharedstatedir@ srcdir = @srcdir@ sysconfdir = @sysconfdir@ +target = @target@ target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ @@ -263,7 +398,7 @@ all: all-am .SUFFIXES: .SUFFIXES: .cpp .lo .o .obj -$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) +$(srcdir)/Makefile.in: @MAINTAINER_MODE_TRUE@ $(srcdir)/Makefile.am $(am__configure_deps) @for dep in $?; do \ case '$(am__configure_deps)' in \ *$$dep*) \ @@ -272,9 +407,9 @@ $(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) exit 1;; \ esac; \ done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu Solver/Makefile'; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/prop/cryptominisat/Solver/Makefile'; \ $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --gnu Solver/Makefile + $(AUTOMAKE) --foreign src/prop/cryptominisat/Solver/Makefile .PRECIOUS: Makefile Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status @case '$?' in \ @@ -288,9 +423,9 @@ Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status $(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(top_srcdir)/configure: $(am__configure_deps) +$(top_srcdir)/configure: @MAINTAINER_MODE_TRUE@ $(am__configure_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(ACLOCAL_M4): $(am__aclocal_m4_deps) +$(ACLOCAL_M4): @MAINTAINER_MODE_TRUE@ $(am__aclocal_m4_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh $(am__aclocal_m4_deps): install-libLTLIBRARIES: $(lib_LTLIBRARIES) @@ -325,7 +460,7 @@ clean-libLTLIBRARIES: rm -f "$${dir}/so_locations"; \ done libcryptominisat.la: $(libcryptominisat_la_OBJECTS) $(libcryptominisat_la_DEPENDENCIES) - $(libcryptominisat_la_LINK) -rpath $(libdir) $(libcryptominisat_la_OBJECTS) $(libcryptominisat_la_LIBADD) $(LIBS) + $(AM_V_CXXLD)$(libcryptominisat_la_LINK) -rpath $(libdir) $(libcryptominisat_la_OBJECTS) $(libcryptominisat_la_LIBADD) $(LIBS) install-binPROGRAMS: $(bin_PROGRAMS) @$(NORMAL_INSTALL) test -z "$(bindir)" || $(MKDIR_P) "$(DESTDIR)$(bindir)" @@ -371,7 +506,7 @@ clean-binPROGRAMS: rm -f $$list cryptominisat$(EXEEXT): $(cryptominisat_OBJECTS) $(cryptominisat_DEPENDENCIES) @rm -f cryptominisat$(EXEEXT) - $(cryptominisat_LINK) $(cryptominisat_OBJECTS) $(cryptominisat_LDADD) $(LIBS) + $(AM_V_CXXLD)$(cryptominisat_LINK) $(cryptominisat_OBJECTS) $(cryptominisat_LDADD) $(LIBS) mostlyclean-compile: -rm -f *.$(OBJEXT) @@ -406,22 +541,25 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/XorSubsumer.Plo@am__quote@ .cpp.o: -@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< -@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +@am__fastdepCXX_FALSE@ $(AM_V_CXX) @AM_BACKSLASH@ @AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@ @AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ @am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ $< .cpp.obj: -@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'` -@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'` +@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po +@am__fastdepCXX_FALSE@ $(AM_V_CXX) @AM_BACKSLASH@ @AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@ @AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ @am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'` .cpp.lo: -@am__fastdepCXX_TRUE@ $(LTCXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< -@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo +@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(LTCXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo +@am__fastdepCXX_FALSE@ $(AM_V_CXX) @AM_BACKSLASH@ @AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@ @AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ @am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) -c -o $@ $< diff --git a/src/prop/cryptominisat/man/Makefile.in b/src/prop/cryptominisat/man/Makefile.in index 5542511eb..7dc705cf1 100644 --- a/src/prop/cryptominisat/man/Makefile.in +++ b/src/prop/cryptominisat/man/Makefile.in @@ -33,16 +33,35 @@ PRE_UNINSTALL = : POST_UNINSTALL = : build_triplet = @build@ host_triplet = @host@ -subdir = man +target_triplet = @target@ +subdir = src/prop/cryptominisat/man DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/configure.in +am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ + $(top_srcdir)/config/ax_prog_doxygen.m4 \ + $(top_srcdir)/config/ax_tls.m4 \ + $(top_srcdir)/config/bindings.m4 $(top_srcdir)/config/boost.m4 \ + $(top_srcdir)/config/cudd.m4 $(top_srcdir)/config/cvc4.m4 \ + $(top_srcdir)/config/gcc_version.m4 \ + $(top_srcdir)/config/libtool.m4 \ + $(top_srcdir)/config/ltoptions.m4 \ + $(top_srcdir)/config/ltsugar.m4 \ + $(top_srcdir)/config/ltversion.m4 \ + $(top_srcdir)/config/lt~obsolete.m4 \ + $(top_srcdir)/config/pkg.m4 $(top_srcdir)/config/readline.m4 \ + $(top_srcdir)/configure.ac am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ $(ACLOCAL_M4) mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = $(top_builddir)/config.h +CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ SOURCES = DIST_SOURCES = am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; @@ -73,54 +92,128 @@ MANS = $(man_MANS) DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) ACLOCAL = @ACLOCAL@ AMTAR = @AMTAR@ +AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +ANTLR = @ANTLR@ +ANTLR_HOME = @ANTLR_HOME@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ AR = @AR@ +AS = @AS@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BOOST_CPPFLAGS = @BOOST_CPPFLAGS@ +BOOST_LDPATH = @BOOST_LDPATH@ +BOOST_ROOT = @BOOST_ROOT@ +BOOST_THREAD_LDFLAGS = @BOOST_THREAD_LDFLAGS@ +BOOST_THREAD_LDPATH = @BOOST_THREAD_LDPATH@ +BOOST_THREAD_LIBS = @BOOST_THREAD_LIBS@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ +CAMLP4O = @CAMLP4O@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ +CLN_CFLAGS = @CLN_CFLAGS@ +CLN_LIBS = @CLN_LIBS@ CPP = @CPP@ CPPFLAGS = @CPPFLAGS@ +CSHARP_CPPFLAGS = @CSHARP_CPPFLAGS@ +CUDD_CPPFLAGS = @CUDD_CPPFLAGS@ +CUDD_LDFLAGS = @CUDD_LDFLAGS@ +CUDD_LIBS = @CUDD_LIBS@ +CVC4_BINDINGS_LIBRARY_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ +CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ +CVC4_COMPAT_LIBRARY_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ +CVC4_HAS_THREADS = @CVC4_HAS_THREADS@ +CVC4_LANGUAGE_BINDINGS = @CVC4_LANGUAGE_BINDINGS@ +CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ +CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ +CVC4_TLS = @CVC4_TLS@ +CVC4_TLS_SUPPORTED = @CVC4_TLS_SUPPORTED@ +CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@ +CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ +CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ DEPDIR = @DEPDIR@ +DISTCHECK_CONFIGURE_FLAGS = @DISTCHECK_CONFIGURE_FLAGS@ DLLTOOL = @DLLTOOL@ +DOXYGEN_EXTRACT_PRIVATE = @DOXYGEN_EXTRACT_PRIVATE@ +DOXYGEN_EXTRACT_STATIC = @DOXYGEN_EXTRACT_STATIC@ +DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@ DSYMUTIL = @DSYMUTIL@ DUMPBIN = @DUMPBIN@ +DX_CONFIG = @DX_CONFIG@ +DX_DOCDIR = @DX_DOCDIR@ +DX_DOT = @DX_DOT@ +DX_DOXYGEN = @DX_DOXYGEN@ +DX_DVIPS = @DX_DVIPS@ +DX_EGREP = @DX_EGREP@ +DX_ENV = @DX_ENV@ +DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@ +DX_FLAG_chi = @DX_FLAG_chi@ +DX_FLAG_chm = @DX_FLAG_chm@ +DX_FLAG_doc = @DX_FLAG_doc@ +DX_FLAG_dot = @DX_FLAG_dot@ +DX_FLAG_html = @DX_FLAG_html@ +DX_FLAG_man = @DX_FLAG_man@ +DX_FLAG_pdf = @DX_FLAG_pdf@ +DX_FLAG_ps = @DX_FLAG_ps@ +DX_FLAG_rtf = @DX_FLAG_rtf@ +DX_FLAG_xml = @DX_FLAG_xml@ +DX_HHC = @DX_HHC@ +DX_LATEX = @DX_LATEX@ +DX_MAKEINDEX = @DX_MAKEINDEX@ +DX_PDFLATEX = @DX_PDFLATEX@ +DX_PERL = @DX_PERL@ +DX_PROJECT = @DX_PROJECT@ ECHO_C = @ECHO_C@ ECHO_N = @ECHO_N@ ECHO_T = @ECHO_T@ EGREP = @EGREP@ EXEEXT = @EXEEXT@ FGREP = @FGREP@ +FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@ GREP = @GREP@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ INSTALL_PROGRAM = @INSTALL_PROGRAM@ INSTALL_SCRIPT = @INSTALL_SCRIPT@ INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +JAR = @JAR@ +JAVA = @JAVA@ +JAVAC = @JAVAC@ +JAVAH = @JAVAH@ +JAVA_CPPFLAGS = @JAVA_CPPFLAGS@ LD = @LD@ LDFLAGS = @LDFLAGS@ +LFSC = @LFSC@ +LFSCARGS = @LFSCARGS@ LIBOBJS = @LIBOBJS@ LIBS = @LIBS@ LIBTOOL = @LIBTOOL@ LIPO = @LIPO@ LN_S = @LN_S@ LTLIBOBJS = @LTLIBOBJS@ +MAINT = @MAINT@ MAKEINFO = @MAKEINFO@ MANIFEST_TOOL = @MANIFEST_TOOL@ +MAN_DATE = @MAN_DATE@ MKDIR_P = @MKDIR_P@ NM = @NM@ NMEDIT = @NMEDIT@ OBJDUMP = @OBJDUMP@ OBJEXT = @OBJEXT@ -OPENMP_CXXFLAGS = @OPENMP_CXXFLAGS@ +OCAMLC = @OCAMLC@ +OCAMLFIND = @OCAMLFIND@ +OCAMLMKTOP = @OCAMLMKTOP@ OTOOL = @OTOOL@ OTOOL64 = @OTOOL64@ PACKAGE = @PACKAGE@ @@ -131,12 +224,33 @@ PACKAGE_TARNAME = @PACKAGE_TARNAME@ PACKAGE_URL = @PACKAGE_URL@ PACKAGE_VERSION = @PACKAGE_VERSION@ PATH_SEPARATOR = @PATH_SEPARATOR@ +PERL = @PERL@ +PERL_CPPFLAGS = @PERL_CPPFLAGS@ +PHP_CPPFLAGS = @PHP_CPPFLAGS@ +PKG_CONFIG = @PKG_CONFIG@ +PYTHON = @PYTHON@ +PYTHON_CONFIG = @PYTHON_CONFIG@ +PYTHON_CXXFLAGS = @PYTHON_CXXFLAGS@ +PYTHON_EXEC_PREFIX = @PYTHON_EXEC_PREFIX@ +PYTHON_INCLUDE = @PYTHON_INCLUDE@ +PYTHON_PLATFORM = @PYTHON_PLATFORM@ +PYTHON_PREFIX = @PYTHON_PREFIX@ +PYTHON_VERSION = @PYTHON_VERSION@ RANLIB = @RANLIB@ +READLINE_LIBS = @READLINE_LIBS@ +RUBY_CPPFLAGS = @RUBY_CPPFLAGS@ SED = @SED@ SET_MAKE = @SET_MAKE@ SHELL = @SHELL@ +STATIC_BINARY = @STATIC_BINARY@ STRIP = @STRIP@ +SWIG = @SWIG@ +TCL_CPPFLAGS = @TCL_CPPFLAGS@ +TEST_CPPFLAGS = @TEST_CPPFLAGS@ +TEST_CXXFLAGS = @TEST_CXXFLAGS@ +TEST_LDFLAGS = @TEST_LDFLAGS@ VERSION = @VERSION@ +WNO_CONVERSION_NULL = @WNO_CONVERSION_NULL@ abs_builddir = @abs_builddir@ abs_srcdir = @abs_srcdir@ abs_top_builddir = @abs_top_builddir@ @@ -176,17 +290,26 @@ libexecdir = @libexecdir@ localedir = @localedir@ localstatedir = @localstatedir@ mandir = @mandir@ +mk_include = @mk_include@ mkdir_p = @mkdir_p@ oldincludedir = @oldincludedir@ pdfdir = @pdfdir@ +pkgpyexecdir = @pkgpyexecdir@ +pkgpythondir = @pkgpythondir@ prefix = @prefix@ program_transform_name = @program_transform_name@ psdir = @psdir@ +pyexecdir = @pyexecdir@ +pythondir = @pythondir@ sbindir = @sbindir@ sharedstatedir = @sharedstatedir@ srcdir = @srcdir@ sysconfdir = @sysconfdir@ +target = @target@ target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ @@ -195,7 +318,7 @@ EXTRA_DIST = $(man_MANS) all: all-am .SUFFIXES: -$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) +$(srcdir)/Makefile.in: @MAINTAINER_MODE_TRUE@ $(srcdir)/Makefile.am $(am__configure_deps) @for dep in $?; do \ case '$(am__configure_deps)' in \ *$$dep*) \ @@ -204,9 +327,9 @@ $(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) exit 1;; \ esac; \ done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu man/Makefile'; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/prop/cryptominisat/man/Makefile'; \ $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --gnu man/Makefile + $(AUTOMAKE) --foreign src/prop/cryptominisat/man/Makefile .PRECIOUS: Makefile Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status @case '$?' in \ @@ -220,9 +343,9 @@ Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status $(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(top_srcdir)/configure: $(am__configure_deps) +$(top_srcdir)/configure: @MAINTAINER_MODE_TRUE@ $(am__configure_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(ACLOCAL_M4): $(am__aclocal_m4_deps) +$(ACLOCAL_M4): @MAINTAINER_MODE_TRUE@ $(am__aclocal_m4_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh $(am__aclocal_m4_deps): diff --git a/src/prop/cryptominisat/mtl/Makefile.in b/src/prop/cryptominisat/mtl/Makefile.in index eb9b73e19..7d8c8ce1b 100644 --- a/src/prop/cryptominisat/mtl/Makefile.in +++ b/src/prop/cryptominisat/mtl/Makefile.in @@ -34,17 +34,36 @@ PRE_UNINSTALL = : POST_UNINSTALL = : build_triplet = @build@ host_triplet = @host@ -subdir = mtl +target_triplet = @target@ +subdir = src/prop/cryptominisat/mtl DIST_COMMON = $(pkgincludesub_HEADERS) $(srcdir)/Makefile.am \ $(srcdir)/Makefile.in ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 -am__aclocal_m4_deps = $(top_srcdir)/configure.in +am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ + $(top_srcdir)/config/ax_prog_doxygen.m4 \ + $(top_srcdir)/config/ax_tls.m4 \ + $(top_srcdir)/config/bindings.m4 $(top_srcdir)/config/boost.m4 \ + $(top_srcdir)/config/cudd.m4 $(top_srcdir)/config/cvc4.m4 \ + $(top_srcdir)/config/gcc_version.m4 \ + $(top_srcdir)/config/libtool.m4 \ + $(top_srcdir)/config/ltoptions.m4 \ + $(top_srcdir)/config/ltsugar.m4 \ + $(top_srcdir)/config/ltversion.m4 \ + $(top_srcdir)/config/lt~obsolete.m4 \ + $(top_srcdir)/config/pkg.m4 $(top_srcdir)/config/readline.m4 \ + $(top_srcdir)/configure.ac am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ $(ACLOCAL_M4) mkinstalldirs = $(install_sh) -d -CONFIG_HEADER = $(top_builddir)/config.h +CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = +AM_V_GEN = $(am__v_GEN_$(V)) +am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY)) +am__v_GEN_0 = @echo " GEN " $@; +AM_V_at = $(am__v_at_$(V)) +am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY)) +am__v_at_0 = @ SOURCES = DIST_SOURCES = am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; @@ -75,54 +94,128 @@ CTAGS = ctags DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) ACLOCAL = @ACLOCAL@ AMTAR = @AMTAR@ +AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@ +ANTLR = @ANTLR@ +ANTLR_HOME = @ANTLR_HOME@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ AR = @AR@ +AS = @AS@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BOOST_CPPFLAGS = @BOOST_CPPFLAGS@ +BOOST_LDPATH = @BOOST_LDPATH@ +BOOST_ROOT = @BOOST_ROOT@ +BOOST_THREAD_LDFLAGS = @BOOST_THREAD_LDFLAGS@ +BOOST_THREAD_LDPATH = @BOOST_THREAD_LDPATH@ +BOOST_THREAD_LIBS = @BOOST_THREAD_LIBS@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ +CAMLP4O = @CAMLP4O@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ +CLN_CFLAGS = @CLN_CFLAGS@ +CLN_LIBS = @CLN_LIBS@ CPP = @CPP@ CPPFLAGS = @CPPFLAGS@ +CSHARP_CPPFLAGS = @CSHARP_CPPFLAGS@ +CUDD_CPPFLAGS = @CUDD_CPPFLAGS@ +CUDD_LDFLAGS = @CUDD_LDFLAGS@ +CUDD_LIBS = @CUDD_LIBS@ +CVC4_BINDINGS_LIBRARY_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ +CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@ +CVC4_COMPAT_LIBRARY_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ +CVC4_HAS_THREADS = @CVC4_HAS_THREADS@ +CVC4_LANGUAGE_BINDINGS = @CVC4_LANGUAGE_BINDINGS@ +CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ +CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ +CVC4_TLS = @CVC4_TLS@ +CVC4_TLS_SUPPORTED = @CVC4_TLS_SUPPORTED@ +CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@ +CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ +CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ DEPDIR = @DEPDIR@ +DISTCHECK_CONFIGURE_FLAGS = @DISTCHECK_CONFIGURE_FLAGS@ DLLTOOL = @DLLTOOL@ +DOXYGEN_EXTRACT_PRIVATE = @DOXYGEN_EXTRACT_PRIVATE@ +DOXYGEN_EXTRACT_STATIC = @DOXYGEN_EXTRACT_STATIC@ +DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@ DSYMUTIL = @DSYMUTIL@ DUMPBIN = @DUMPBIN@ +DX_CONFIG = @DX_CONFIG@ +DX_DOCDIR = @DX_DOCDIR@ +DX_DOT = @DX_DOT@ +DX_DOXYGEN = @DX_DOXYGEN@ +DX_DVIPS = @DX_DVIPS@ +DX_EGREP = @DX_EGREP@ +DX_ENV = @DX_ENV@ +DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@ +DX_FLAG_chi = @DX_FLAG_chi@ +DX_FLAG_chm = @DX_FLAG_chm@ +DX_FLAG_doc = @DX_FLAG_doc@ +DX_FLAG_dot = @DX_FLAG_dot@ +DX_FLAG_html = @DX_FLAG_html@ +DX_FLAG_man = @DX_FLAG_man@ +DX_FLAG_pdf = @DX_FLAG_pdf@ +DX_FLAG_ps = @DX_FLAG_ps@ +DX_FLAG_rtf = @DX_FLAG_rtf@ +DX_FLAG_xml = @DX_FLAG_xml@ +DX_HHC = @DX_HHC@ +DX_LATEX = @DX_LATEX@ +DX_MAKEINDEX = @DX_MAKEINDEX@ +DX_PDFLATEX = @DX_PDFLATEX@ +DX_PERL = @DX_PERL@ +DX_PROJECT = @DX_PROJECT@ ECHO_C = @ECHO_C@ ECHO_N = @ECHO_N@ ECHO_T = @ECHO_T@ EGREP = @EGREP@ EXEEXT = @EXEEXT@ FGREP = @FGREP@ +FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@ GREP = @GREP@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ INSTALL_PROGRAM = @INSTALL_PROGRAM@ INSTALL_SCRIPT = @INSTALL_SCRIPT@ INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +JAR = @JAR@ +JAVA = @JAVA@ +JAVAC = @JAVAC@ +JAVAH = @JAVAH@ +JAVA_CPPFLAGS = @JAVA_CPPFLAGS@ LD = @LD@ LDFLAGS = @LDFLAGS@ +LFSC = @LFSC@ +LFSCARGS = @LFSCARGS@ LIBOBJS = @LIBOBJS@ LIBS = @LIBS@ LIBTOOL = @LIBTOOL@ LIPO = @LIPO@ LN_S = @LN_S@ LTLIBOBJS = @LTLIBOBJS@ +MAINT = @MAINT@ MAKEINFO = @MAKEINFO@ MANIFEST_TOOL = @MANIFEST_TOOL@ +MAN_DATE = @MAN_DATE@ MKDIR_P = @MKDIR_P@ NM = @NM@ NMEDIT = @NMEDIT@ OBJDUMP = @OBJDUMP@ OBJEXT = @OBJEXT@ -OPENMP_CXXFLAGS = @OPENMP_CXXFLAGS@ +OCAMLC = @OCAMLC@ +OCAMLFIND = @OCAMLFIND@ +OCAMLMKTOP = @OCAMLMKTOP@ OTOOL = @OTOOL@ OTOOL64 = @OTOOL64@ PACKAGE = @PACKAGE@ @@ -133,12 +226,33 @@ PACKAGE_TARNAME = @PACKAGE_TARNAME@ PACKAGE_URL = @PACKAGE_URL@ PACKAGE_VERSION = @PACKAGE_VERSION@ PATH_SEPARATOR = @PATH_SEPARATOR@ +PERL = @PERL@ +PERL_CPPFLAGS = @PERL_CPPFLAGS@ +PHP_CPPFLAGS = @PHP_CPPFLAGS@ +PKG_CONFIG = @PKG_CONFIG@ +PYTHON = @PYTHON@ +PYTHON_CONFIG = @PYTHON_CONFIG@ +PYTHON_CXXFLAGS = @PYTHON_CXXFLAGS@ +PYTHON_EXEC_PREFIX = @PYTHON_EXEC_PREFIX@ +PYTHON_INCLUDE = @PYTHON_INCLUDE@ +PYTHON_PLATFORM = @PYTHON_PLATFORM@ +PYTHON_PREFIX = @PYTHON_PREFIX@ +PYTHON_VERSION = @PYTHON_VERSION@ RANLIB = @RANLIB@ +READLINE_LIBS = @READLINE_LIBS@ +RUBY_CPPFLAGS = @RUBY_CPPFLAGS@ SED = @SED@ SET_MAKE = @SET_MAKE@ SHELL = @SHELL@ +STATIC_BINARY = @STATIC_BINARY@ STRIP = @STRIP@ +SWIG = @SWIG@ +TCL_CPPFLAGS = @TCL_CPPFLAGS@ +TEST_CPPFLAGS = @TEST_CPPFLAGS@ +TEST_CXXFLAGS = @TEST_CXXFLAGS@ +TEST_LDFLAGS = @TEST_LDFLAGS@ VERSION = @VERSION@ +WNO_CONVERSION_NULL = @WNO_CONVERSION_NULL@ abs_builddir = @abs_builddir@ abs_srcdir = @abs_srcdir@ abs_top_builddir = @abs_top_builddir@ @@ -178,17 +292,26 @@ libexecdir = @libexecdir@ localedir = @localedir@ localstatedir = @localstatedir@ mandir = @mandir@ +mk_include = @mk_include@ mkdir_p = @mkdir_p@ oldincludedir = @oldincludedir@ pdfdir = @pdfdir@ +pkgpyexecdir = @pkgpyexecdir@ +pkgpythondir = @pkgpythondir@ prefix = @prefix@ program_transform_name = @program_transform_name@ psdir = @psdir@ +pyexecdir = @pyexecdir@ +pythondir = @pythondir@ sbindir = @sbindir@ sharedstatedir = @sharedstatedir@ srcdir = @srcdir@ sysconfdir = @sysconfdir@ +target = @target@ target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ @@ -197,7 +320,7 @@ pkgincludesub_HEADERS = Alg.h Heap.h Vec.h all: all-am .SUFFIXES: -$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) +$(srcdir)/Makefile.in: @MAINTAINER_MODE_TRUE@ $(srcdir)/Makefile.am $(am__configure_deps) @for dep in $?; do \ case '$(am__configure_deps)' in \ *$$dep*) \ @@ -206,9 +329,9 @@ $(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) exit 1;; \ esac; \ done; \ - echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu mtl/Makefile'; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/prop/cryptominisat/mtl/Makefile'; \ $(am__cd) $(top_srcdir) && \ - $(AUTOMAKE) --gnu mtl/Makefile + $(AUTOMAKE) --foreign src/prop/cryptominisat/mtl/Makefile .PRECIOUS: Makefile Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status @case '$?' in \ @@ -222,9 +345,9 @@ Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status $(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(top_srcdir)/configure: $(am__configure_deps) +$(top_srcdir)/configure: @MAINTAINER_MODE_TRUE@ $(am__configure_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh -$(ACLOCAL_M4): $(am__aclocal_m4_deps) +$(ACLOCAL_M4): @MAINTAINER_MODE_TRUE@ $(am__aclocal_m4_deps) cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh $(am__aclocal_m4_deps): diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3a16b0d19..c602d8b9c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -195,6 +195,8 @@ CRef Solver::reason(Var x) { if (varLevel > explLevel) { explLevel = varLevel; } + Assert(value(explanation[i]) != l_Undef); + Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); } // Construct the reason (level 0) diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index f18335048..4fe24fc60 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -72,11 +72,20 @@ public: class BVSatSolverInterface: public SatSolver { public: - virtual SatValue solve(const context::CDList<SatLiteral> & assumptions) = 0; virtual void markUnremovable(SatLiteral lit) = 0; virtual void getUnsatCore(SatClause& unsatCore) = 0; + + virtual void addMarkerLiteral(SatLiteral lit) = 0; + + virtual bool getPropagations(std::vector<SatLiteral>& propagations) = 0; + + virtual void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; + + virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; + + virtual void popAssumption() = 0; }; diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index e6ae5d1e7..3b048af47 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -27,8 +27,8 @@ namespace prop { template class SatSolverConstructor<MinisatSatSolver>; template class SatSolverConstructor<BVMinisatSatSolver>; -BVSatSolverInterface* SatSolverFactory::createMinisat() { - return new BVMinisatSatSolver(); +BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext) { + return new BVMinisatSatSolver(mainSatContext); } DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 367397fdf..379141cc6 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -30,7 +30,7 @@ namespace prop { class SatSolverFactory { public: - static BVSatSolverInterface* createMinisat(); + static BVSatSolverInterface* createMinisat(context::Context* mainSatContext); static DPLLSatSolverInterface* createDPLLMinisat(); static SatSolver* create(const char* id); |