From e9504536858874a1829c5b82514c6c8fb07d4210 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Aug 2019 14:19:16 -0700 Subject: [PATCH] force propagation for smt cubing Signed-off-by: Nikolaj Bjorner --- src/smt/smt_solver.cpp | 3 +++ src/solver/combined_solver.cpp | 3 ++- src/solver/tactic2solver.cpp | 1 + 3 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 8c9510055..ea21bc329 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -281,6 +281,9 @@ namespace smt { ast_manager& m = get_manager(); if (!m_cuber) { m_cuber = alloc(cuber, *this); + // force propagation + push_core(); + pop_core(1); } expr_ref result = m_cuber->cube(); expr_ref_vector lits(m); diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 763e0467c..4339e45aa 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -264,7 +264,8 @@ public: } expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { - return m_solver1->cube(vars, backtrack_level); + switch_inc_mode(); + return m_solver2->cube(vars, backtrack_level); } expr * get_assumption(unsigned idx) const override { diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 0090cc3b0..448adc479 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -80,6 +80,7 @@ public: expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { set_reason_unknown("cubing is not supported on tactics"); + IF_VERBOSE(1, verbose_stream() << "cubing is not supported on tactics\n"); return expr_ref_vector(get_manager()); }