diff --git a/src/sat/boolean_problem.cc b/src/sat/boolean_problem.cc index 471b85ab73..ee5fb36456 100644 --- a/src/sat/boolean_problem.cc +++ b/src/sat/boolean_problem.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/boolean_problem.h b/src/sat/boolean_problem.h index ebd191c85c..5ec4dc914a 100644 --- a/src/sat/boolean_problem.h +++ b/src/sat/boolean_problem.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/boolean_problem.proto b/src/sat/boolean_problem.proto index a4fba92240..592aa26fdb 100644 --- a/src/sat/boolean_problem.proto +++ b/src/sat/boolean_problem.proto @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/clause.cc b/src/sat/clause.cc index fc3c5edd40..5b5de5cf88 100644 --- a/src/sat/clause.cc +++ b/src/sat/clause.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/clause.h b/src/sat/clause.h index 3871e9feb9..8c237cf896 100644 --- a/src/sat/clause.h +++ b/src/sat/clause.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/encoding.cc b/src/sat/encoding.cc index a43593fab9..3507def31e 100644 --- a/src/sat/encoding.cc +++ b/src/sat/encoding.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/encoding.h b/src/sat/encoding.h index 74e121c85a..090d072cbb 100644 --- a/src/sat/encoding.h +++ b/src/sat/encoding.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/optimization.cc b/src/sat/optimization.cc index 8f953ebac8..d6d06b70ed 100644 --- a/src/sat/optimization.cc +++ b/src/sat/optimization.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/optimization.h b/src/sat/optimization.h index db60436a71..d42a195f8a 100644 --- a/src/sat/optimization.h +++ b/src/sat/optimization.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/pb_constraint.cc b/src/sat/pb_constraint.cc index 26774e785e..845cd16370 100644 --- a/src/sat/pb_constraint.cc +++ b/src/sat/pb_constraint.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/pb_constraint.h b/src/sat/pb_constraint.h index 0cd5c035d1..e4a3a16faa 100644 --- a/src/sat/pb_constraint.h +++ b/src/sat/pb_constraint.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/sat_base.h b/src/sat/sat_base.h index f5c7ec2b73..08838bc4df 100644 --- a/src/sat/sat_base.h +++ b/src/sat/sat_base.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/sat_parameters.proto b/src/sat/sat_parameters.proto index e92144fab3..5664235ed5 100644 --- a/src/sat/sat_parameters.proto +++ b/src/sat/sat_parameters.proto @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/sat_solver.cc b/src/sat/sat_solver.cc index bf71b61793..806a23fcef 100644 --- a/src/sat/sat_solver.cc +++ b/src/sat/sat_solver.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at @@ -908,6 +908,11 @@ SatSolver::Status SatSolver::Solve() { } } +SatSolver::Status SatSolver::SolveWithTimeLimit(double max_time_in_seconds) { + time_limit_.reset(new TimeLimit(max_time_in_seconds)); + return Solve(); +} + std::vector SatSolver::GetLastIncompatibleDecisions() { SCOPED_TIME_STAT(&stats_); std::vector unsat_assumptions; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 9a0be2253b..c606619107 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at @@ -173,6 +173,12 @@ class SatSolver { }; Status Solve(); + // Same as Solve(), but with a given time limit in seconds. Note that this is + // slightly redundant with the max_time_in_seconds() parameter, but because + // SetParameters() resets more than just the time limit, it is useful to have + // this more specific api. + Status SolveWithTimeLimit(double max_time_in_seconds); + // Simple interface to solve a problem under the given assumptions. This // simply ask the solver to solve a problem given a set of variables fixed to // a given value (the assumptions). Compared to simply calling AddUnitClause() diff --git a/src/sat/symmetry.cc b/src/sat/symmetry.cc index 477f4868ae..2c46378c29 100644 --- a/src/sat/symmetry.cc +++ b/src/sat/symmetry.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/symmetry.h b/src/sat/symmetry.h index 8773627c77..33790276a8 100644 --- a/src/sat/symmetry.h +++ b/src/sat/symmetry.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/unsat_proof.cc b/src/sat/unsat_proof.cc index 6d78b81c45..db8cc188aa 100644 --- a/src/sat/unsat_proof.cc +++ b/src/sat/unsat_proof.cc @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at diff --git a/src/sat/unsat_proof.h b/src/sat/unsat_proof.h index edfbfe1d26..d6274392a1 100644 --- a/src/sat/unsat_proof.h +++ b/src/sat/unsat_proof.h @@ -1,4 +1,4 @@ -// Copyright 2010-2013 Google +// Copyright 2010-2014 Google // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at