From: Andrew Reynolds Date: Wed, 9 May 2018 15:50:55 +0000 (-0500) Subject: Make symmetry-breaker-exp into a preprocessing pass (#1890) X-Git-Tag: cvc5-1.0.0~5073 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df974e62c34f3e1b4f57feb64e439e1e791e87ce;p=cvc5.git Make symmetry-breaker-exp into a preprocessing pass (#1890) --- diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp index 2e8c873cd..c6ad09e91 100644 --- a/src/preprocessing/passes/symmetry_breaker.cpp +++ b/src/preprocessing/passes/symmetry_breaker.cpp @@ -13,6 +13,7 @@ **/ #include "preprocessing/passes/symmetry_breaker.h" +#include "preprocessing/passes/symmetry_detect.h" using namespace std; @@ -47,7 +48,7 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts { for (unsigned int i = 0; i < part.size(); ++i) { - for (unsigned int j = i + 2; j < part.size(); ++i) + for (unsigned int j = i + 2; j < part.size(); ++j) { // Generate consecutive constraints v_i = v_j => v_i = v_{j-1} for all 0 // <= i < j-1 < j < part.size() @@ -100,7 +101,7 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts { return constraints[0]; } - return nm->mkNode(kind::AND, constraints);; + return nm->mkNode(kind::AND, constraints); } Kind SymmetryBreaker::getOrderKind(Node node) @@ -119,6 +120,42 @@ Kind SymmetryBreaker::getOrderKind(Node node) } } +SymBreakerPass::SymBreakerPass(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "sym-break"){}; + +PreprocessingPassResult SymBreakerPass::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl; + // detect symmetries + std::vector> part; + SymmetryDetect symd; + symd.getPartition(part, assertionsToPreprocess->ref()); + if (Trace.isOn("sym-break-pass")) + { + Trace("sym-break-pass") << "Detected symmetry partition:" << std::endl; + for (const std::vector& p : part) + { + Trace("sym-break-pass") << " " << p << std::endl; + } + } + // construct the symmetry breaking constraint + Trace("sym-break-pass") << "Construct symmetry breaking constraint..." + << std::endl; + SymmetryBreaker symb; + Node sbConstraint = symb.generateSymBkConstraints(part); + // add symmetry breaking constraint to the set of assertions + Trace("sym-break-pass") << "...got: " << sbConstraint << std::endl; + // if not true + if (!sbConstraint.isConst()) + { + // add to assertions + assertionsToPreprocess->push_back(sbConstraint); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + } // namespace passes } // namespace preprocessing } // namespace CVC4 diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h index a89f67a61..898b7a122 100644 --- a/src/preprocessing/passes/symmetry_breaker.h +++ b/src/preprocessing/passes/symmetry_breaker.h @@ -20,6 +20,9 @@ #include #include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + namespace CVC4 { namespace preprocessing { namespace passes { @@ -84,6 +87,21 @@ class SymmetryBreaker Kind getOrderKind(Node node); }; +/** + * This class detects symmetries in the input assertions in the form of a + * partition (see symmetry_detect.h), and subsequently adds symmetry breaking + * constraints that correspond to this partition, using the above class. + */ +class SymBreakerPass : public PreprocessingPass +{ + public: + SymBreakerPass(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + } // namespace passes } // namespace preprocessing } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 09a495d1e..c750b8a12 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2600,6 +2600,8 @@ void SmtEnginePrivate::finishInit() { new PseudoBooleanProcessor(d_preprocessingPassContext.get())); std::unique_ptr realToInt( new RealToInt(d_preprocessingPassContext.get())); + std::unique_ptr sbProc( + new SymBreakerPass(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); d_preprocessingPassRegistry.registerPass("bv-abstraction", std::move(bvAbstract)); @@ -2611,6 +2613,7 @@ void SmtEnginePrivate::finishInit() { d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); + d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -4198,11 +4201,8 @@ void SmtEnginePrivate::processAssertions() { if (options::symmetryBreakerExp()) { - SymmetryDetect symd; - SymmetryBreaker symb; - vector> part; - symd.getPartition(part, d_assertions.ref()); - Node sbConstraint = symb.generateSymBkConstraints(part); + // apply symmetry breaking + d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions); } dumpAssertions("pre-static-learning", d_assertions); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b86ee911d..c3de09de2 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1522,6 +1522,7 @@ REG1_TESTS = \ regress1/sym/sym4.smt2 \ regress1/sym/sym5.smt2 \ regress1/sym/sym6.smt2 \ + regress1/sym/sym7-uf.smt2 \ regress1/test12.cvc \ regress1/trim.cvc \ regress1/uf2.smt2 \ diff --git a/test/regress/regress1/sym/sym1.smt2 b/test/regress/regress1/sym/sym1.smt2 index ac1c0215f..c063f8b8f 100644 --- a/test/regress/regress1/sym/sym1.smt2 +++ b/test/regress/regress1/sym/sym1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --symmetry-detect +; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym2.smt2 b/test/regress/regress1/sym/sym2.smt2 index cff424ba9..e2e62cbb6 100644 --- a/test/regress/regress1/sym/sym2.smt2 +++ b/test/regress/regress1/sym/sym2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --symmetry-detect +; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym3.smt2 b/test/regress/regress1/sym/sym3.smt2 index 52f9855c9..c6b87adeb 100644 --- a/test/regress/regress1/sym/sym3.smt2 +++ b/test/regress/regress1/sym/sym3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --symmetry-detect +; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym4.smt2 b/test/regress/regress1/sym/sym4.smt2 index 5582ef7d0..1cbd6f5b2 100644 --- a/test/regress/regress1/sym/sym4.smt2 +++ b/test/regress/regress1/sym/sym4.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --symmetry-detect +; COMMAND-LINE: --symmetry-breaker-exp (set-info :smt-lib-version 2.6) (set-logic QF_LIA) (set-info :category "crafted") @@ -45,4 +45,4 @@ (assert (<= (+ (* 59 x_0) (* 59 x_1) (* 59 x_2) (* 59 x_3) (* 59 x_4) (* 59 x_5) (* 59 x_6) (* 59 x_7) (* 59 x_8) (* 59 x_9) (* 59 x_10) (* 59 x_11) (* 59 x_12) (* 59 x_13) (* 59 x_14) (* 59 x_15) (* (- 382) x_16)) 0)) (assert (>= (+ x_0 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15 x_16) 1)) (check-sat) -(exit) \ No newline at end of file +(exit) diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 index f5ef1d003..6b16d9d35 100644 --- a/test/regress/regress1/sym/sym5.smt2 +++ b/test/regress/regress1/sym/sym5.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --symmetry-detect +; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status unsat) (declare-fun A () (Set Int)) @@ -16,4 +16,4 @@ (assert (subset B A)) (assert (= C (intersection A B))) (assert (member j C)) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2 index 3da6b4cb4..10218ebc9 100644 --- a/test/regress/regress1/sym/sym6.smt2 +++ b/test/regress/regress1/sym/sym6.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --symmetry-detect +; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym7-uf.smt2 b/test/regress/regress1/sym/sym7-uf.smt2 new file mode 100644 index 000000000..ee91240d3 --- /dev/null +++ b/test/regress/regress1/sym/sym7-uf.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status sat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun z () U) +(declare-fun w () U) +(declare-fun u () U) +(declare-fun v () U) +(declare-fun a () U) +(declare-fun P (U) Bool) + +(assert (distinct w u v a)) +(assert (or (= x y) (= x z) (= y z))) +(assert (or (P x) (P y) (P z) (P w))) + +; should get { x, y, z }, { w }, { u, v, a } +(check-sat) +