diff --git a/test_max_pb_unit.cpp b/test_max_pb_unit.cpp new file mode 100644 index 000000000..91b245171 --- /dev/null +++ b/test_max_pb_unit.cpp @@ -0,0 +1,65 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + test_pb_max_optimization.cpp + +Abstract: + + Test for max PB constraints optimization feature + +Author: + + GitHub Copilot 2024-12-19 + +--*/ + +#include "opt/opt_context.h" +#include "ast/arith_decl_plugin.h" +#include "util/trace.h" + +void test_max_pb_optimization() { + ast_manager m; + opt::context ctx(m); + arith_util arith(m); + + // Create boolean variables + expr_ref x1(m.mk_const(symbol("x1"), m.mk_bool_sort()), m); + expr_ref x2(m.mk_const(symbol("x2"), m.mk_bool_sort()), m); + expr_ref y1(m.mk_const(symbol("y1"), m.mk_bool_sort()), m); + expr_ref y2(m.mk_const(symbol("y2"), m.mk_bool_sort()), m); + + // Create PB constraints as integer expressions + expr_ref pb1(arith.mk_add( + arith.mk_mul(arith.mk_numeral(rational(2), true), + m.mk_ite(x1, arith.mk_numeral(rational(1), true), arith.mk_numeral(rational(0), true))), + m.mk_ite(x2, arith.mk_numeral(rational(1), true), arith.mk_numeral(rational(0), true))), m); + + expr_ref pb2(arith.mk_add( + m.mk_ite(y1, arith.mk_numeral(rational(1), true), arith.mk_numeral(rational(0), true)), + arith.mk_mul(arith.mk_numeral(rational(2), true), + m.mk_ite(y2, arith.mk_numeral(rational(1), true), arith.mk_numeral(rational(0), true)))), m); + + // Add two maximize objectives + ctx.add_objective(to_app(pb1), true); // maximize + ctx.add_objective(to_app(pb2), true); // maximize + + // Check optimization + expr_ref_vector asms(m); + lbool result = ctx.optimize(asms); + + ENSURE(result == l_true); + + std::cout << "Max PB optimization test passed!" << std::endl; +} + +int main() { + try { + test_max_pb_optimization(); + return 0; + } catch (std::exception& e) { + std::cerr << "Test failed: " << e.what() << std::endl; + return 1; + } +} \ No newline at end of file diff --git a/test_pb_feature.smt2 b/test_pb_feature.smt2 new file mode 100644 index 000000000..b12715fb5 --- /dev/null +++ b/test_pb_feature.smt2 @@ -0,0 +1,29 @@ +;; Test case for max PB constraints optimization feature +;; This demonstrates the transformation from multiple maximize objectives +;; to auxiliary variables with threshold constraints + +(echo "Testing max PB constraints optimization") + +;; Declare boolean variables +(declare-fun x1 () Bool) +(declare-fun x2 () Bool) +(declare-fun y1 () Bool) +(declare-fun y2 () Bool) + +;; Test case: Two PB constraints to maximize +;; PB1: 2*x1 + x2 (max value = 3) +;; PB2: y1 + 2*y2 (max value = 3) + +(maximize (+ (ite x1 2 0) (ite x2 1 0))) +(maximize (+ (ite y1 1 0) (ite y2 2 0))) + +(echo "Before optimization:") +(check-sat) + +;; The implementation should detect these two PB maximize objectives +;; and transform them to auxiliary variables: +;; - For PB1: aux_0_1, aux_0_2, aux_0_3 where PB1 >= k => aux_0_k +;; - For PB2: aux_1_1, aux_1_2, aux_1_3 where PB2 >= k => aux_1_k +;; - Then maximize: aux_0_1 + aux_0_2 + aux_0_3 + aux_1_1 + aux_1_2 + aux_1_3 + +(echo "Max PB optimization feature test completed") \ No newline at end of file